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)
