diff options
author | 2017-07-24 20:04:46 +0200 | |
---|---|---|
committer | 2017-08-29 05:18:49 +0200 | |
commit | f442efebd8354b233827e4991a80d27082c772e1 (patch) | |
tree | dfdc1a38defaa4f2e7ca413aaca883f5c2b728fa /test-suite/bugs | |
parent | 7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (diff) |
A little reorganization of notations + a fix to #5608.
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/5608.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v new file mode 100644 index 000000000..f02eae69c --- /dev/null +++ b/test-suite/bugs/closed/5608.v @@ -0,0 +1,33 @@ +Reserved Notation "'slet' x .. y := A 'in' b" + (at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b"). +Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "T x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). + +Delimit Scope ctype_scope with ctype. +Local Open Scope ctype_scope. +Delimit Scope expr_scope with expr. +Inductive base_type := TZ | TWord (logsz : nat). +Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type). +Context {var : base_type -> Type}. +Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t : +flat_type) := + match t with + | Tbase t => interp_base_type t + | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type +interp_base_type y) + end. +Inductive exprf : flat_type -> Type := +| Var {t} (v : var t) : exprf (Tbase t) +| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) : +exprf tC +| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty). +Global Arguments Var {_} _. +Global Arguments LetIn {_} _ {_} _. +Global Arguments Pair {_} _ {_} _. +Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A +(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope. +Definition foo := + (fun x3 => + (LetIn (Var x3) (fun x18 : var TZ + => (Pair (Var x18) (Var x18))))). +Print foo. |