Stream: Coq users

Topic: Custom entries and grammar factoring


view this post on Zulip Jason Gross (Jul 30 2023 at 22:26):

Is there a nice way to use custom entries to parse the following grammar? (cc @Hugo Herbelin ?)

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

fancy_slice_list := … | … ',' slice_list | slice_list

slice_list := slice_expr | slice_expr ',' slice_list

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)
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.


(* no tensor *)
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].

view this post on Zulip Jason Gross (Jul 30 2023 at 22:29):

I'm on the verge of giving up on getting something nice, and writing separate printing and parsing notations, where the parsing one fuses the preceeding comma separator into the slice_expr and then uses Ltac to reassociate, and the printing one has levels that don't factor. But hopefully there's a better solution?

view this post on Zulip Jason Gross (Aug 02 2023 at 20:08):

Cross-posted: https://proofassistants.stackexchange.com/questions/2342/factoring-custom-grammar-rules-for-integers-and-lists-in-coq-custom-entries

view this post on Zulip Karl Palmskog (Aug 03 2023 at 10:32):

due to the insanely high search engine ranking StackExchange answers get, I think it's actually a good idea to crosspost questions of general interest like this (assuming the questioner transfers useful answers from the Zulip to SE)

view this post on Zulip Hugo Herbelin (Aug 07 2023 at 11:24):

Does not look simple. Are you suggesting that if negative numerals were not at level 35, that would be easier?

view this post on Zulip Jason Gross (Aug 07 2023 at 17:06):

@Hugo Herbelin My struggle is not yet even with negatives. I'm suggesting that if I could attach number notations to the custom entry directly rather than having to route through constr via "x" := x%uint63, then maybe the parsing would all factor?


Last updated: Jun 23 2024 at 05:02 UTC