From b402adc12c00ba72046423d3a1737ccad517f70e Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 11 Oct 2020 18:39:16 -0700 Subject: Rename operconstr -> term --- parsing/g_constr.mlg | 88 ++++++++++++++++++++++++++-------------------------- parsing/pcoq.ml | 3 +- parsing/pcoq.mli | 2 ++ 3 files changed, 48 insertions(+), 45 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 644493a010..bfd1fed6f0 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -80,7 +80,7 @@ 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 closed_binder open_binders binder binders binders_fixannot @@ -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 } + [ [ c = term LEVEL "8" -> { c } | "@"; f=global; i = univ_instance -> { 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 = term; 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) } | "@"; 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 appl_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 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 -> { 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,52 +208,52 @@ 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_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 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 = 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 = 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: [ [ 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) } @@ -294,14 +294,14 @@ GRAMMAR EXTEND Gram | dcl = cofix_decl; "with"; dcls = LIST1 cofix_decl SEP "with"; "for"; id = identref -> { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ] ; - fix_decl: + fix_decl:~loc @@ ExplByName id)) [ [ 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: [ [ id = identref; bl = binders; ty = type_cstr; ":="; - c = operconstr LEVEL "200" -> + c = term LEVEL "200" -> { CAst.make ~loc (id,bl,ty,c) } ] ] ; match_constr: @@ -309,13 +309,13 @@ GRAMMAR EXTEND Gram 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: [ [ a = OPT [ na = OPT["as"; na = name -> { na } ]; @@ -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..ce73cee3be 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" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8e60bbf504..ccdf8abeda 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 -- cgit v1.2.3 From 41b07808c84a86ea4b77e0c7855b22bfd3906669 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 12 Oct 2020 21:55:00 -0700 Subject: Rename misc nonterminals --- parsing/g_constr.mlg | 48 ++++++++++++++++++++++++------------------------ parsing/pcoq.ml | 6 ++++-- parsing/pcoq.mli | 4 ++++ 3 files changed, 32 insertions(+), 26 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index bfd1fed6f0..a4660bfe8b 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -82,9 +82,9 @@ let test_array_closing = GRAMMAR EXTEND Gram 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: @@ -135,7 +135,7 @@ GRAMMAR EXTEND Gram ; constr: [ [ c = term LEVEL "8" -> { c } - | "@"; f=global; i = univ_instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ] + | "@"; f=global; i = univ_annot -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ] ; term: [ "200" RIGHTA @@ -152,8 +152,8 @@ GRAMMAR EXTEND Gram | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ f = term; 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 @@ -163,7 +163,7 @@ GRAMMAR EXTEND Gram { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ] | "8" [ ] | "1" LEFTA - [ c = term; ".("; 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 = term; ".("; "@"; f = global; args = LIST0 (term LEVEL "9"); ")" -> @@ -171,7 +171,7 @@ GRAMMAR EXTEND Gram | c = term; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ] | "0" [ c = atomic_constr -> { c } - | c = match_constr -> { c } + | c = term_match -> { c } | "("; c = term LEVEL "200"; ")" -> { (* Preserve parentheses around numerals so that constrintern does not collapse -(3) into the numeral -3. *) @@ -184,7 +184,7 @@ GRAMMAR EXTEND Gram { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) } | "`{"; 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) @@ -219,16 +219,16 @@ GRAMMAR EXTEND Gram | _, _ -> 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 = term LEVEL "200" -> + | "let"; "fix"; fx = fix_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 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 = term 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 = term LEVEL "200"; "in"; + 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 = term LEVEL "200"; @@ -244,19 +244,19 @@ GRAMMAR EXTEND Gram "in"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) } - | "if"; c = term LEVEL "200"; po = return_type; + | "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=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 } ] ] ; @@ -285,26 +285,26 @@ GRAMMAR EXTEND Gram | id = global -> { UNamed (GType id) } ] ] ; fix_decls: - [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } - | dcl = fix_decl; "with"; dcls = LIST1 fix_decl SEP "with"; "for"; id = identref -> + [ [ dcl = fix_body -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } + | dcl = fix_body; "with"; dcls = LIST1 fix_body SEP "with"; "for"; id = identref -> { (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:~loc @@ ExplByName id)) + fix_body: [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":="; 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 = 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) } ] ] ; @@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram case_type: [ [ "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 diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index ce73cee3be..22b5e70311 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -321,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" @@ -329,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 ccdf8abeda..ce4c91d51f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -196,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 *) @@ -204,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 -- cgit v1.2.3 From 480d34fc22c195d4b19f639345fa993652838894 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Thu, 22 Oct 2020 21:32:48 -0700 Subject: Change a few nonterminal names in mlgs and update doc to match --- parsing/g_constr.mlg | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index a4660bfe8b..349e14bba3 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -219,7 +219,7 @@ GRAMMAR EXTEND Gram | _, _ -> 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_body; "in"; c = term 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) } @@ -285,8 +285,8 @@ GRAMMAR EXTEND Gram | id = global -> { UNamed (GType id) } ] ] ; fix_decls: - [ [ dcl = fix_body -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } - | dcl = fix_body; "with"; dcls = LIST1 fix_body SEP "with"; "for"; id = identref -> + [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } + | dcl = fix_decl; "with"; dcls = LIST1 fix_decl SEP "with"; "for"; id = identref -> { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ] ; cofix_decls: @@ -294,7 +294,7 @@ GRAMMAR EXTEND Gram | dcl = cofix_body; "with"; dcls = LIST1 cofix_body SEP "with"; "for"; id = identref -> { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ] ; - fix_body: + fix_decl: [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":="; c = term LEVEL "200" -> { CAst.make ~loc (id,snd bl,fst bl,ty,c) } ] ] -- cgit v1.2.3