2
$\begingroup$

Is there a nice way to use custom entries to parse the following grammar? ("nice" meaning ~ "without massive duplication" and ~ "without needing to resort to separate printing and parsing notations and Ltac)

slicing              := constr '.[' slice_list ']'

slice_list           := '…' | slice_expr | slice_list ',' slice_expr

slice_expr           := single_slice_expr | slice_expr_with_step | slice_expr_no_step
slice_expr_no_step   := ':' | INT ':' | ':' INT | INT ':' INT
slice_expr_with_step := slice_expr_no_step ':' INT
single_slice_expr    := 'None' | INT

(where INT is parsed according to Number Notation, which for now I'm using constr%uint63 for)

(Note that my lists are left-associative, by design; they will be parsed to snoc-lists.)

I cannot seem to find a way to get the INT from single_slice_expr to factor with the leading INTs from the other alternatives of slice_expr (and to make it trickier the 'None' literal needs to be at level 0 to avoiding making None a keyword).

So far I have

(* -*- coding: utf-8 -*- *)
From Coq Require Import Sint63 Uint63.
Set Implicit Arguments.
Set Boolean Equality Schemes.
Set Decidable Equality Schemes.

#[local] Coercion is_true : bool >-> Sortclass.
Record Slice I := { start : option I ; stop : option I ; step : option I }.

Fixpoint radd (n m : nat) {struct m} : nat
  := match m with
     | 0 => n
     | S p => S (radd n p)
     end.
Fixpoint rsub (n m : nat) {struct m} : nat
  := match m, n with
     | 0, n => n
     | S p, S k => rsub k p
     | S p, 0 => 0
     end.

Reserved Infix "+'" (at level 48, left associativity).
Reserved Infix "-'" (at level 50, left associativity).
Module Export Notations.
  Infix "+'" := radd : nat_scope.
  Infix "-'" := rsub : nat_scope.
End Notations.

Definition Rank := nat.
Definition IndexType := int.
Inductive SliceIndexType : Rank -> Rank -> Type :=
| slice_index (s : Slice IndexType) : SliceIndexType 1 1
| broadcast_one_index : SliceIndexType 0 1
| single_index (i : IndexType) : SliceIndexType 1 0
.

#[export] Set Warnings Append "-uniform-inheritance,-ambiguous-paths".
#[global] Set Warnings Append "-uniform-inheritance,-ambiguous-paths".
#[global] Coercion slice_index : Slice >-> SliceIndexType.
#[export] Set Warnings Append "uniform-inheritance,ambiguous-paths".
#[global] Set Warnings Append "uniform-inheritance,ambiguous-paths".
#[global] Coercion single_index : IndexType >-> SliceIndexType.
#[global] Coercion inject_int (x : int) : IndexType := x.

Inductive SliceIndex : Rank (* input *) -> Rank (* output *) -> Type :=
| nil : SliceIndex 0 0
| elipsis {r} : SliceIndex r r
| snoc {ris ros ri ro} : SliceIndex ris ros -> SliceIndexType ri ro -> SliceIndex (ris +' ri) (ros +' ro).


Declare Custom Entry fancy_slice.
Declare Custom Entry less_fancy_slice.
Notation ":" := (slice_index (@Build_Slice _ None None None)) (in custom fancy_slice at level 1).
(* N.B. 35 is the minimum level for negative integers to parse *)
Notation "start : stop : step" := (slice_index (@Build_Slice _ (Some start%sint63) (Some stop%sint63) (Some step%sint63))) (in custom fancy_slice at level 2, start constr at level 35, stop constr at level 35, step constr at level 35, format "start : stop : step").
Notation "start :: step" := (slice_index (@Build_Slice _ (Some start%sint63) None (Some step%sint63))) (in custom fancy_slice at level 2, start constr at level 35, step constr at level 35, format "start :: step").
Notation "start : : step" := (slice_index (@Build_Slice _ (Some start%sint63) None (Some step%sint63))) (in custom fancy_slice at level 2, start constr at level 35, step constr at level 35, format "start : : step").
Notation "start :: step" := (slice_index (@Build_Slice _ (Some start%sint63) None (Some step%sint63))) (in custom fancy_slice at level 2, start constr at level 35, step constr at level 35, format "start :: step").
Notation ": stop : step" := (slice_index (@Build_Slice _ None (Some stop%sint63) (Some step%sint63))) (in custom fancy_slice at level 1, stop constr at level 35, step constr at level 35, format ": stop : step").
Notation ": : step" := (slice_index (@Build_Slice _ None None (Some step%sint63))) (in custom fancy_slice at level 1, step constr at level 35, format ": : step").
Notation ":: step" := (slice_index (@Build_Slice _ None None (Some step%sint63))) (in custom fancy_slice at level 1, step constr at level 35, format ":: step").
Notation "start : stop" := (slice_index (@Build_Slice _ (Some start%sint63) (Some stop%sint63) None)) (in custom fancy_slice at level 2, start constr at level 35, stop constr at level 35, format "start : stop").
Notation "start :" := (slice_index (@Build_Slice _ (Some start%sint63) None None)) (in custom fancy_slice at level 2, start constr at level 35, format "start :").
Notation ": stop" := (slice_index (@Build_Slice _ None (Some stop%sint63) None)) (in custom fancy_slice at level 1, stop constr at level 35, format ": stop").
Notation "'None'" := broadcast_one_index (in custom less_fancy_slice at level 0). (* need to avoid breaking Datatypes.None *)
Notation "x" := x%sint63 (in custom less_fancy_slice at level 0, x constr at level 55).
Notation "x" := x (in custom fancy_slice at level 1, x custom less_fancy_slice at level 0).
Notation "'None'" := broadcast_one_index (in custom fancy_slice at level 0). (* need to avoid breaking Datatypes.None *)

Declare Scope tensor_scope.
Delimit Scope tensor_scope with tensor.

Notation "t .[ x , .. , y ]"
  := (t%tensor (snoc .. (snoc nil x) .. y))
       (at level 2, x custom fancy_slice at level 60, y custom fancy_slice at level 60, left associativity, format "t .[ x ,  .. ,  y ]")
    : tensor_scope.
Notation "t .[ … , x , .. , y ]"
  := (t%tensor (snoc .. (snoc elipsis x) .. y))
       (at level 2, x custom fancy_slice at level 60, y custom fancy_slice at level 60, left associativity, format "t .[ … ,  x ,  .. ,  y ]")
    : tensor_scope.

Open Scope tensor_scope.
Eval cbn in  _.[0:1:1].
Eval cbn in  _.[1:-1:1].
Eval cbn in  _.[1:-1:1,1:-1:1].
Eval cbn in  _.[1:-1].
Eval cbn in  _.[:-1].
Eval cbn in  _.[1:].
Eval cbn in  _.[1::1].
Eval cbn in  _.[1::1,:1].
Eval cbn in  _.[1::1,1:].
Eval cbn in  _.[:].
Eval cbn in  _.[::1].
Eval cbn in  _.[:1].
Eval cbn in  _.[:1].
Eval cbn in  _.[1]. (* Error: Syntax error: '::' or ':' expected after [term level 35] (in [custom:fancy_slice]). *)
Eval cbn in  _.[None].
Eval cbn in  _.[1::1,1].
Eval cbn in  _.[1:-1:1, None, 0].
Eval cbn in  _.[:, None, 0].
Eval cbn in  _.[:1, None, 0].
Eval cbn in  _.[:-1:1, None, 0].

(Cross-posted from Zulip)

$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.