Skip to content

Commit 3b1a307

Browse files
SkySkimmerSkySkimmer
committed
Inline binder_constr
cf #21670 However this is not backwards compatible AFAICT so not sure how to work from here.
1 parent c4fa328 commit 3b1a307

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+227
-239
lines changed

‎doc/tools/docgram/common.edit_mlg‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,7 @@ term_forall_or_fun: [
259259
| "forall" open_binders "," type
260260
]
261261

262-
binder_constr: [
262+
term10: [
263263
| DELETE "forall" open_binders "," term200
264264
| MOVETO term_forall_or_fun "fun" open_binders "=>" term200
265265
| MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200
@@ -2320,7 +2320,6 @@ SPLICE: [
23202320
| ext_module_expr
23212321
| ext_module_type
23222322
| test
2323-
| binder_constr
23242323
| atomic_constr
23252324
| let_type_cstr
23262325
| name_colon

‎doc/tools/docgram/fullGrammar‎

Lines changed: 10 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,16 @@ term10: [
101101
| term10 LIST1 arg
102102
| "@" global univ_annot LIST0 term9
103103
| "@" pattern_ident LIST1 identref
104-
| binder_constr
104+
| "forall" open_binders "," term200
105+
| "fun" open_binders "=>" term200
106+
| "let" name binders let_type_cstr ":=" term200 "in" term200
107+
| "let" "fix" fix_decl "in" term200
108+
| "let" "cofix" cofix_body "in" term200
109+
| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
110+
| "let" "'" pattern200 OPT [ "in" pattern200 ] ":=" term200 OPT case_type "in" term200
111+
| "if" term200 as_return_type "then" term200 "else" term200
112+
| "fix" fix_decls
113+
| "cofix" cofix_decls
105114
| term9
106115
]
107116

@@ -154,19 +163,6 @@ field_def: [
154163
| global binders ":=" lconstr
155164
]
156165

157-
binder_constr: [
158-
| "forall" open_binders "," term200
159-
| "fun" open_binders "=>" term200
160-
| "let" name binders let_type_cstr ":=" term200 "in" term200
161-
| "let" "fix" fix_decl "in" term200
162-
| "let" "cofix" cofix_body "in" term200
163-
| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
164-
| "let" "'" pattern200 OPT [ "in" pattern200 ] ":=" term200 OPT case_type "in" term200
165-
| "if" term200 as_return_type "then" term200 "else" term200
166-
| "fix" fix_decls
167-
| "cofix" cofix_decls
168-
]
169-
170166
arg: [
171167
| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
172168
| test_lpar_nat_coloneq "(" natural ":=" lconstr ")"

‎parsing/g_constr.mlg‎

Lines changed: 35 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ let sigref loc = Libnames.qualid_of_string ~loc "Corelib.Init.Specif.sig"
122122
}
123123

124124
GRAMMAR EXTEND Gram
125-
GLOBAL: binder_constr lconstr constr term
125+
GLOBAL: lconstr constr term
126126
universe_name sort sort_quality_or_set sort_quality_var
127127
global constr_pattern cpattern Constr.ident
128128
closed_binder open_binders binder binders binders_fixannot
@@ -215,7 +215,40 @@ GRAMMAR EXTEND Gram
215215
{ let { CAst.loc = locid; v = id } = lid in
216216
let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
217217
CAst.make ~loc @@ CApp(CAst.make ?loc:locid @@ CPatVar id,args) }
218-
| c = binder_constr -> { c } ]
218+
| "forall"; bl = open_binders; ","; c = term LEVEL "200" ->
219+
{ mkProdCN ~loc bl c }
220+
| "fun"; bl = open_binders; "=>"; c = term LEVEL "200" ->
221+
{ mkLambdaCN ~loc bl c }
222+
| "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
223+
c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" ->
224+
{ let ty,c1 = match ty, c1 with
225+
| (_,None), { CAst.v = CCast(c, Some DEFAULTcast, t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
226+
| _, _ -> ty, c1 in
227+
CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
228+
Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
229+
| "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" ->
230+
{ let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_,_ as dcl)} = fx in
231+
let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in
232+
CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) }
233+
| "let"; "cofix"; fx = cofix_body; "in"; c = term LEVEL "200" ->
234+
{ let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
235+
let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in
236+
CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) }
237+
| "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
238+
po = as_return_type; ":="; c1 = term LEVEL "200"; "in";
239+
c2 = term LEVEL "200" ->
240+
{ CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
241+
| "let"; "'"; p = pattern LEVEL "200"; t = OPT [ "in"; t = pattern LEVEL "200" -> { t } ];
242+
":="; c1 = term LEVEL "200"; rt = OPT case_type;
243+
"in"; c2 = term LEVEL "200" ->
244+
{ CAst.make ~loc @@
245+
CCases (LetPatternStyle, rt, [c1, aliasvar p, t], [CAst.make ~loc ([[p]], c2)]) }
246+
| "if"; c = term LEVEL "200"; po = as_return_type;
247+
"then"; b1 = term LEVEL "200";
248+
"else"; b2 = term LEVEL "200" ->
249+
{ CAst.make ~loc @@ CIf (c, po, b1, b2) }
250+
| "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) }
251+
| "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ]
219252
| "9"
220253
[ ".."; c = term LEVEL "0"; ".." ->
221254
{ CAst.make ~loc @@ CAppExpl ((qualid_of_ident ~loc ldots_var, None),[c]) } ]
@@ -270,42 +303,6 @@ GRAMMAR EXTEND Gram
270303
[ [ id = global; bl = binders; ":="; c = lconstr ->
271304
{ (id, mkLambdaCN ~loc bl c) } ] ]
272305
;
273-
binder_constr:
274-
[ [ "forall"; bl = open_binders; ","; c = term LEVEL "200" ->
275-
{ mkProdCN ~loc bl c }
276-
| "fun"; bl = open_binders; "=>"; c = term LEVEL "200" ->
277-
{ mkLambdaCN ~loc bl c }
278-
| "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
279-
c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" ->
280-
{ let ty,c1 = match ty, c1 with
281-
| (_,None), { CAst.v = CCast(c, Some DEFAULTcast, t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
282-
| _, _ -> ty, c1 in
283-
CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
284-
Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
285-
| "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" ->
286-
{ let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_,_ as dcl)} = fx in
287-
let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in
288-
CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) }
289-
| "let"; "cofix"; fx = cofix_body; "in"; c = term LEVEL "200" ->
290-
{ let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
291-
let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in
292-
CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) }
293-
| "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
294-
po = as_return_type; ":="; c1 = term LEVEL "200"; "in";
295-
c2 = term LEVEL "200" ->
296-
{ CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
297-
| "let"; "'"; p = pattern LEVEL "200"; t = OPT [ "in"; t = pattern LEVEL "200" -> { t } ];
298-
":="; c1 = term LEVEL "200"; rt = OPT case_type;
299-
"in"; c2 = term LEVEL "200" ->
300-
{ CAst.make ~loc @@
301-
CCases (LetPatternStyle, rt, [c1, aliasvar p, t], [CAst.make ~loc ([[p]], c2)]) }
302-
| "if"; c = term LEVEL "200"; po = as_return_type;
303-
"then"; b1 = term LEVEL "200";
304-
"else"; b2 = term LEVEL "200" ->
305-
{ CAst.make ~loc @@ CIf (c, po, b1, b2) }
306-
| "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) }
307-
| "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
308-
;
309306
arg:
310307
[ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
311308
| test_lpar_nat_coloneq; "("; n = natural; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByPos n)) }

‎parsing/procq.ml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -345,7 +345,6 @@ module Constr =
345345
let term = Entry.make "term"
346346
let constr_eoi = eoi_entry constr
347347
let lconstr = Entry.make "lconstr"
348-
let binder_constr = Entry.make "binder_constr"
349348
let ident = Entry.make "ident"
350349
let global = Entry.make "global"
351350
let universe_name = Entry.make "universe_name"

‎parsing/procq.mli‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,6 @@ module Constr :
173173
val constr : constr_expr Entry.t
174174
val constr_eoi : constr_expr Entry.t
175175
val lconstr : constr_expr Entry.t
176-
val binder_constr : constr_expr Entry.t
177176
val term : constr_expr Entry.t
178177
val ident : Id.t Entry.t
179178
val global : qualid Entry.t

‎plugins/ssr/ssrvernac.mlg‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ let mk_pat c (na, t) = (c, na, t)
8484
}
8585

8686
GRAMMAR EXTEND Gram
87-
GLOBAL: binder_constr;
87+
GLOBAL: term;
8888
ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
8989
ssr_mpat: [[ p = pattern -> { [[p]] } ]];
9090
ssr_dpat: [
@@ -95,7 +95,7 @@ GRAMMAR EXTEND Gram
9595
ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]];
9696
ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
9797
ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
98-
binder_constr: TOP [
98+
term: LEVEL "10" [
9999
[ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
100100
{ let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
101101
| "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->

‎test-suite/_CoqProject‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
-Q prerequisite TestSuite
1+
-R prerequisite TestSuite

‎test-suite/bugs/bug_12467.v‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
44
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
55
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
66
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
7-
(at level 200, x1 at level 0, x2t2 closed binder, P at level 100, Q at level 100, only parsing).
7+
(at level 10, x1 at level 0, x2t2 closed binder, P at level 100, Q at level 100, only parsing).
88
Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
99

1010
End ClosedBinder.
@@ -26,7 +26,7 @@ Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
2626
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
2727
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
2828
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
29-
(at level 200, x1 at level 0, x2t2, P at level 100, Q at level 100, only parsing).
29+
(at level 10, x1 at level 0, x2t2, P at level 100, Q at level 100, only parsing).
3030
(* Fail because, constr used for binder defaults to name *)
3131
Fail Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
3232

@@ -38,7 +38,7 @@ Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
3838
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
3939
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
4040
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
41-
(at level 200, x1 at level 0, x2t2 constr as pattern, P at level 100, Q at level 100, only parsing).
41+
(at level 10, x1 at level 0, x2t2 constr as pattern, P at level 100, Q at level 100, only parsing).
4242
Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
4343

4444
End ConstrAsPattern.
@@ -49,15 +49,15 @@ Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
4949
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
5050
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
5151
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
52-
(at level 200, x1 at level 0, x2t2 pattern, P at level 100, Q at level 100, only parsing).
52+
(at level 10, x1 at level 0, x2t2 pattern, P at level 100, Q at level 100, only parsing).
5353
Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
5454

5555
End Pattern.
5656

5757
Module OnlyRecursiveBinderPartOfIssue17904.
5858

5959
Notation "∀ x .. y , P" := (forall x , .. (forall y , P) .. )
60-
(at level 200, x constr at level 8 as pattern, right associativity,
60+
(at level 10, x constr at level 8 as pattern, P at level 200,
6161
format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope.
6262
Check ∀ a b, a + b = 0.
6363

‎test-suite/bugs/bug_14221.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Require Setoid.
1010
Require Export Corelib.Classes.CMorphisms.
1111

1212
Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
13-
(at level 200, x binder, y binder, right associativity).
13+
(at level 10, x binder, y binder, P at level 200).
1414

1515
Class Setoid A := {
1616
equiv : crelation A;

‎test-suite/bugs/bug_16975.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11

22
Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..)
3-
(at level 200, x binder, y binder, right associativity) : type_scope.
3+
(at level 10, x binder, y binder, P at level 200) : type_scope.
44

55
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
6-
(at level 200, x binder, y binder, right associativity).
6+
(at level 10, x binder, y binder, t at level 200).
77

88
Reserved Notation "X ≃ Y" (at level 80, no associativity).
99

@@ -20,7 +20,7 @@ Arguments pr1 {_ _} _.
2020
Arguments pr2 {_ _} _.
2121

2222
Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
23-
(at level 200, x binder, y binder, right associativity) : type_scope.
23+
(at level 10, x binder, y binder, P at level 200) : type_scope.
2424

2525

2626

0 commit comments

Comments
 (0)