Merge PR #13219: Rename mlg grammar nonterminals to make documented and mlg grammars more consistent

Reviewed-by: Zimmi48
Reviewed-by: herbelin
Ack-by: SkySkimmer

3 files changed, 70 insertions, 61 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 644493a010..349e14bba3 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -80,11 +80,11 @@ let test_array_closing =
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: binder_constr lconstr constr operconstr
+  GLOBAL: binder_constr lconstr constr term
   universe_level universe_name sort sort_family
-  global constr_pattern lconstr_pattern Constr.ident
+  global constr_pattern cpattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
-  record_declaration typeclass_constraint pattern appl_arg type_cstr;
+  record_declaration typeclass_constraint pattern arg type_cstr;
   Constr.ident:
     [ [ id = Prim.ident -> { id } ] ]
   ;
@@ -97,7 +97,7 @@ GRAMMAR EXTEND Gram
   constr_pattern:
     [ [ c = constr -> { c } ] ]
   ;
-  lconstr_pattern:
+  cpattern:
     [ [ c = lconstr -> { c } ] ]
   ;
   sort:
@@ -131,48 +131,48 @@ GRAMMAR EXTEND Gram
       | u = universe_expr -> { [u] } ] ]
   ;
   lconstr:
-    [ [ c = operconstr LEVEL "200" -> { c } ] ]
+    [ [ c = term LEVEL "200" -> { c } ] ]
   ;
   constr:
-    [ [ c = operconstr LEVEL "8" -> { c }
-      | "@"; f=global; i = univ_instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
+    [ [ c = term LEVEL "8" -> { c }
+      | "@"; f=global; i = univ_annot -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
   ;
-  operconstr:
+  term:
     [ "200" RIGHTA
       [ c = binder_constr -> { c } ]
     | "100" RIGHTA
-      [ c1 = operconstr; "<:"; c2 = operconstr LEVEL "200" ->
+      [ c1 = term; "<:"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, CastVM c2) }
-      | c1 = operconstr; "<<:"; c2 = operconstr LEVEL "200" ->
+      | c1 = term; "<<:"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, CastNative c2) }
-      | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" ->
+      | c1 = term; ":"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, CastConv c2) }
-      | c1 = operconstr; ":>" ->
+      | c1 = term; ":>" ->
                  { CAst.make ~loc @@ CCast(c1, CastCoerce) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
-      | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
+      [ f = term; args = LIST1 arg -> { CAst.make ~loc @@ CApp((None,f),args) }
+      | "@"; f = global; i = univ_annot; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
       | "@"; lid = pattern_ident; args = LIST1 identref ->
         { let { CAst.loc = locid; v = id } = lid in
           let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
           CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ]
     | "9"
-      [ ".."; c = operconstr LEVEL "0"; ".." ->
+      [ ".."; c = term LEVEL "0"; ".." ->
         { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ]
     | "8" [ ]
     | "1" LEFTA
-      [ c = operconstr; ".("; f = global; args = LIST0 appl_arg; ")" ->
+      [ c = term; ".("; f = global; args = LIST0 arg; ")" ->
         { CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) }
-      | c = operconstr; ".("; "@"; f = global;
-        args = LIST0 (operconstr LEVEL "9"); ")" ->
+      | c = term; ".("; "@"; f = global;
+        args = LIST0 (term LEVEL "9"); ")" ->
         { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) }
-      | c = operconstr; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
+      | c = term; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
     | "0"
       [ c = atomic_constr -> { c }
-      | c = match_constr -> { c }
-      | "("; c = operconstr LEVEL "200"; ")" ->
+      | c = term_match -> { c }
+      | "("; c = term LEVEL "200"; ")" ->
         { (* Preserve parentheses around numerals so that constrintern does not
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
@@ -182,14 +182,14 @@ GRAMMAR EXTEND Gram
       | "{|"; c = record_declaration; bar_cbrace -> { c }
       | "{"; c = binder_constr ; "}" ->
         { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) }
-      | "`{"; c = operconstr LEVEL "200"; "}" ->
+      | "`{"; c = term LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
-      | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_instance ->
+      | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_annot ->
         { let t = Array.make (List.length ls) def in
           List.iteri (fun i e -> t.(i) <- e) ls;
           CAst.make ~loc @@ CArray(u, t, def, ty)
         }
-      | "`("; c = operconstr LEVEL "200"; ")" ->
+      | "`("; c = term LEVEL "200"; ")" ->
         { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ]
   ;
   array_elems:
@@ -208,55 +208,55 @@ GRAMMAR EXTEND Gram
         { (id, mkLambdaCN ~loc bl c) } ] ]
   ;
   binder_constr:
-    [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
+    [ [ "forall"; bl = open_binders; ","; c = term LEVEL "200" ->
         { mkProdCN ~loc bl c }
-      | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
+      | "fun"; bl = open_binders; "=>"; c = term LEVEL "200" ->
         { mkLambdaCN ~loc bl c }
       | "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
-        c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
+        c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" ->
         { let ty,c1 = match ty, c1 with
           | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
           CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
                  Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
-      | "let"; "fix"; fx = fix_decl; "in"; c = operconstr LEVEL "200" ->
+      | "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" ->
         { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
           let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) }
-      | "let"; "cofix"; fx = cofix_decl; "in"; c = operconstr LEVEL "200" ->
+      | "let"; "cofix"; fx = cofix_body; "in"; c = term LEVEL "200" ->
         { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_ as dcl)} = fx in
           let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) }
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
-        po = return_type; ":="; c1 = operconstr LEVEL "200"; "in";
-        c2 = operconstr LEVEL "200" ->
+        po = as_return_type; ":="; c1 = term LEVEL "200"; "in";
+        c2 = term LEVEL "200" ->
         { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
-      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
-        "in"; c2 = operconstr LEVEL "200" ->
+      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200";
+        "in"; c2 = term LEVEL "200" ->
         { CAst.make ~loc @@
           CCases (LetPatternStyle, None,    [c1, None, None],       [CAst.make ~loc ([[p]], c2)]) }
-      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
-        rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
+      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200";
+        rt = case_type; "in"; c2 = term LEVEL "200" ->
         { CAst.make ~loc @@
           CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) }
       | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200";
-        ":="; c1 = operconstr LEVEL "200"; rt = case_type;
-        "in"; c2 = operconstr LEVEL "200" ->
+        ":="; c1 = term LEVEL "200"; rt = case_type;
+        "in"; c2 = term LEVEL "200" ->
         { CAst.make ~loc @@
           CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) }
-      | "if"; c = operconstr LEVEL "200"; po = return_type;
-        "then"; b1 = operconstr LEVEL "200";
-        "else"; b2 = operconstr LEVEL "200" ->
+      | "if"; c = term LEVEL "200"; po = as_return_type;
+        "then"; b1 = term LEVEL "200";
+        "else"; b2 = term LEVEL "200" ->
         { CAst.make ~loc @@ CIf (c, po, b1, b2) }
       | "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) }
       | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
   ;
-  appl_arg:
+  arg:
     [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
-      | c=operconstr LEVEL "9" -> { (c,None) } ] ]
+      | c=term LEVEL "9" -> { (c,None) } ] ]
   ;
   atomic_constr:
-    [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) }
+    [ [ g = global; i = univ_annot -> { CAst.make ~loc @@ CRef (g,i) }
       | s = sort   -> { CAst.make ~loc @@  CSort s }
       | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
@@ -272,7 +272,7 @@ GRAMMAR EXTEND Gram
     [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l }
       | -> { [] } ] ]
   ;
-  univ_instance:
+  univ_annot:
     [ [ "@{"; l = LIST0 universe_level; "}" -> { Some l }
       | -> { None } ] ]
   ;
@@ -290,34 +290,34 @@ GRAMMAR EXTEND Gram
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
   cofix_decls:
-    [ [ dcl = cofix_decl -> { let (id,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
-      | dcl = cofix_decl; "with"; dcls = LIST1 cofix_decl SEP "with"; "for"; id = identref ->
+    [ [ dcl = cofix_body -> { let (id,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
+      | dcl = cofix_body; "with"; dcls = LIST1 cofix_body SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
   fix_decl:
     [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":=";
-        c = operconstr LEVEL "200" ->
+        c = term LEVEL "200" ->
         { CAst.make ~loc (id,snd bl,fst bl,ty,c) } ] ]
   ;
-  cofix_decl:
+  cofix_body:
     [ [ id = identref; bl = binders; ty = type_cstr; ":=";
-        c = operconstr LEVEL "200" ->
+        c = term LEVEL "200" ->
         { CAst.make ~loc (id,bl,ty,c) } ] ]
   ;
-  match_constr:
+  term_match:
     [ [ "match"; ci = LIST1 case_item SEP ","; ty = OPT case_type; "with";
         br = branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ]
   ;
   case_item:
-    [ [ c = operconstr LEVEL "100";
+    [ [ c = term LEVEL "100";
         ona = OPT ["as"; id = name -> { id } ];
         ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] ->
         { (c,ona,ty) } ] ]
   ;
   case_type:
-    [ [ "return"; ty = operconstr LEVEL "100" -> { ty } ] ]
+    [ [ "return"; ty = term LEVEL "100" -> { ty } ] ]
   ;
-  return_type:
+  as_return_type:
     [ [ a = OPT [ na = OPT["as"; na = name -> { na } ];
                   ty = case_type -> { (na,ty) } ] ->
         { match a with
@@ -345,7 +345,7 @@ GRAMMAR EXTEND Gram
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; ":"; ty = operconstr LEVEL "200" ->
+      [ p = pattern; ":"; ty = term LEVEL "200" ->
         { CAst.make ~loc @@ CPatCast (p, ty) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
@@ -447,12 +447,12 @@ GRAMMAR EXTEND Gram
           [CLocalPattern (CAst.make ~loc (p, ty))] } ] ]
   ;
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
-      | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+    [ [ "!" ; c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
+      | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" ->
           { id, expl, c }
-      | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+      | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" ->
           { iid, expl, c }
-      | c = operconstr LEVEL "200" ->
+      | c = term LEVEL "200" ->
           { (CAst.make ~loc Anonymous), false, c } ] ]
   ;
   type_cstr:
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 996aa0925c..22b5e70311 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -308,7 +308,8 @@ module Constr =
 
     (* Entries that can be referred via the string -> Entry.t table *)
     let constr = Entry.create "constr"
-    let operconstr = Entry.create "operconstr"
+    let term = Entry.create "term"
+    let operconstr = term
     let constr_eoi = eoi_entry constr
     let lconstr = Entry.create "lconstr"
     let binder_constr = Entry.create "binder_constr"
@@ -320,7 +321,8 @@ module Constr =
     let sort_family = Entry.create "sort_family"
     let pattern = Entry.create "pattern"
     let constr_pattern = Entry.create "constr_pattern"
-    let lconstr_pattern = Entry.create "lconstr_pattern"
+    let cpattern = Entry.create "cpattern"
+    let lconstr_pattern = cpattern
     let closed_binder = Entry.create "closed_binder"
     let binder = Entry.create "binder"
     let binders = Entry.create "binders"
@@ -328,7 +330,8 @@ module Constr =
     let binders_fixannot = Entry.create "binders_fixannot"
     let typeclass_constraint = Entry.create "typeclass_constraint"
     let record_declaration = Entry.create "record_declaration"
-    let appl_arg = Entry.create "appl_arg"
+    let arg = Entry.create "arg"
+    let appl_arg = arg
     let type_cstr = Entry.create "type_cstr"
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8e60bbf504..ce4c91d51f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -185,7 +185,9 @@ module Constr :
     val constr_eoi : constr_expr Entry.t
     val lconstr : constr_expr Entry.t
     val binder_constr : constr_expr Entry.t
+    val term : constr_expr Entry.t
     val operconstr : constr_expr Entry.t
+      [@@deprecated "Deprecated in 8.13; use 'term' instead"]
     val ident : Id.t Entry.t
     val global : qualid Entry.t
     val universe_name : Glob_term.glob_sort_name Entry.t
@@ -194,7 +196,9 @@ module Constr :
     val sort_family : Sorts.family Entry.t
     val pattern : cases_pattern_expr Entry.t
     val constr_pattern : constr_expr Entry.t
+    val cpattern : constr_expr Entry.t
     val lconstr_pattern : constr_expr Entry.t
+      [@@deprecated "Deprecated in 8.13; use 'cpattern' instead"]
     val closed_binder : local_binder_expr list Entry.t
     val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
     val binders : local_binder_expr list Entry.t (* list of binder *)
@@ -202,7 +206,9 @@ module Constr :
     val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
+    val arg : (constr_expr * explicitation CAst.t option) Entry.t
     val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
+      [@@deprecated "Deprecated in 8.13; use 'arg' instead"]
     val type_cstr : constr_expr Entry.t
   end