diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml | 14 | ||||
| -rw-r--r-- | parsing/dune | 10 | ||||
| -rw-r--r-- | parsing/extend.ml | 18 | ||||
| -rw-r--r-- | parsing/g_constr.mlg | 391 | ||||
| -rw-r--r-- | parsing/g_prim.mlg | 35 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 100 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 20 |
7 files changed, 267 insertions, 321 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index a27d6450b7..4611d64665 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -195,14 +195,14 @@ let lookup_utf8_tail loc c cs = match Stream.npeek 3 cs with | [_;c2;c3] -> check_utf8_trailing_byte loc cs c2; - check_utf8_trailing_byte loc cs c3; + check_utf8_trailing_byte loc cs c3; 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + (Char.code c3 land 0x3F) | _ -> error_utf8 loc cs else match Stream.npeek 4 cs with | [_;c2;c3;c4] -> check_utf8_trailing_byte loc cs c2; - check_utf8_trailing_byte loc cs c3; + check_utf8_trailing_byte loc cs c3; check_utf8_trailing_byte loc cs c4; 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 + (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) @@ -436,7 +436,7 @@ let comment_stop ep = let bp = match !comment_begin with Some bp -> bp | None -> - Feedback.msg_notice + Feedback.msg_debug (str "No begin location for comment '" ++ str current_s ++str"' ending at " ++ int ep); @@ -785,12 +785,14 @@ let next_token ~diff_mode loc s = (* Location table system for creating tables associating a token count to its location in a char stream (the source) *) -let locerr () = invalid_arg "Lexer: location function" +let locerr i = + let m = "Lexer: location function called on token "^string_of_int i in + invalid_arg m let loct_create () = Hashtbl.create 207 let loct_func loct i = - try Hashtbl.find loct i with Not_found -> locerr () + try Hashtbl.find loct i with Not_found -> locerr i let loct_add loct i loc = Hashtbl.add loct i loc @@ -831,7 +833,7 @@ let func next_token ?loc cs = Stream.from (fun i -> let (tok, loc) = next_token !cur_loc cs in - cur_loc := after loc; + cur_loc := after loc; loct_add loct i loc; Some tok) in (ts, loct_func loct) diff --git a/parsing/dune b/parsing/dune index 2bb8611e09..8a31434101 100644 --- a/parsing/dune +++ b/parsing/dune @@ -4,12 +4,4 @@ (wrapped false) (libraries coq.gramlib interp)) -(rule - (targets g_prim.ml) - (deps (:mlg-file g_prim.mlg)) - (action (run coqpp %{mlg-file}))) - -(rule - (targets g_constr.ml) - (deps (:mlg-file g_constr.mlg)) - (action (run coqpp %{mlg-file}))) +(coq.pp (modules g_prim g_constr)) diff --git a/parsing/extend.ml b/parsing/extend.ml index 63e121c0d1..ed6ebe5aed 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -79,8 +79,10 @@ type ('a,'b,'c) ty_user_symbol = (** {5 Type-safe grammar extension} *) -type norec = NoRec (* just two *) -type mayrec = MayRec (* incompatible types *) +(* Should be merged with gramlib's implementation *) + +type norec = Gramlib.Grammar.ty_norec +type mayrec = Gramlib.Grammar.ty_mayrec type ('self, 'trec, 'a) symbol = | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol @@ -107,15 +109,3 @@ and 'a rules = type 'a production_rule = | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - -type 'a single_extend_statement = - string option * - (* Level *) - Gramlib.Gramext.g_assoc option * - (* Associativity *) - 'a production_rule list - (* Symbol list with the interpretation function *) - -type 'a extend_statement = - Gramlib.Gramext.position option * - 'a single_extend_statement list diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 8fdec7d1a8..af1e973261 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -19,7 +19,6 @@ open Constrexpr_ops open Util open Tok open Namegen -open Decl_kinds open Pcoq open Pcoq.Prim @@ -51,76 +50,46 @@ let binder_of_name expl { CAst.loc = loc; v = na } = let binders_of_names l = List.map (binder_of_name Explicit) l -let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = - let ty = match tyc with - Some ty -> ty - | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in - (id,ann,bl,ty,body) - -let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = - Option.iter (fun { CAst.loc = aloc } -> - CErrors.user_err ?loc:aloc - ~hdr:"Constr:mk_cofixb" - (Pp.str"Annotation forbidden in cofix expression.")) ann; - let ty = match tyc with - Some ty -> ty - | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in - (id,bl,ty,body) - -let mk_fix(loc,kw,id,dcls) = - if kw then - let fb : fix_expr list = List.map mk_fixb dcls in - CAst.make ~loc @@ CFix(id,fb) - else - let fb : cofix_expr list = List.map mk_cofixb dcls in - CAst.make ~loc @@ CCoFix(id,fb) - -let mk_single_fix (loc,kw,dcl) = - let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) - let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let lpar_id_coloneq = Pcoq.Entry.of_parser "test_lpar_id_coloneq" - (fun strm -> + (fun _ strm -> match stream_nth 0 strm with | KEYWORD "(" -> (match stream_nth 1 strm with - | IDENT s -> + | IDENT s -> (match stream_nth 2 strm with | KEYWORD ":=" -> stream_njunk 3 strm; Names.Id.of_string s - | _ -> err ()) + | _ -> err ()) | _ -> err ()) | _ -> err ()) -let impl_ident_head = - Pcoq.Entry.of_parser "impl_ident_head" - (fun strm -> +let ensure_fixannot = + Pcoq.Entry.of_parser "check_fixannot" + (fun _ strm -> match stream_nth 0 strm with - | KEYWORD "{" -> - (match stream_nth 1 strm with - | IDENT ("wf"|"struct"|"measure") -> err () - | IDENT s -> - stream_njunk 2 strm; - Names.Id.of_string s - | _ -> err ()) - | _ -> err ()) + | KEYWORD "{" -> + (match stream_nth 1 strm with + | IDENT ("wf"|"struct"|"measure") -> () + | _ -> err ()) + | _ -> err ()) let name_colon = Pcoq.Entry.of_parser "name_colon" - (fun strm -> + (fun _ strm -> match stream_nth 0 strm with - | IDENT s -> + | IDENT s -> (match stream_nth 1 strm with | KEYWORD ":" -> stream_njunk 2 strm; Name (Names.Id.of_string s) | _ -> err ()) - | KEYWORD "_" -> + | KEYWORD "_" -> (match stream_nth 1 strm with | KEYWORD ":" -> stream_njunk 2 strm; @@ -137,7 +106,7 @@ GRAMMAR EXTEND Gram universe_level universe_name sort sort_family global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot - record_declaration typeclass_constraint pattern appl_arg; + record_declaration typeclass_constraint pattern appl_arg type_cstr; Constr.ident: [ [ id = Prim.ident -> { id } ] ] ; @@ -159,15 +128,13 @@ GRAMMAR EXTEND Gram | "SProp" -> { UNamed [GSProp,0] } | "Type" -> { UAnonymous {rigid=true} } | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} } - | "Type"; "@{"; u = universe; "}" -> { UNamed u } - ] ] + | "Type"; "@{"; u = universe; "}" -> { UNamed u } ] ] ; sort_family: [ [ "Set" -> { Sorts.InSet } | "Prop" -> { Sorts.InProp } | "SProp" -> { Sorts.InSProp } - | "Type" -> { Sorts.InType } - ] ] + | "Type" -> { Sorts.InType } ] ] ; universe_increment: [ [ "+"; n = natural -> { n } @@ -183,57 +150,50 @@ GRAMMAR EXTEND Gram ; universe: [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids } - | u = universe_expr -> { [u] } - ] ] + | u = universe_expr -> { [u] } ] ] ; lconstr: [ [ c = operconstr LEVEL "200" -> { c } ] ] ; constr: [ [ c = operconstr LEVEL "8" -> { c } - | "@"; f=global; i = instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ] + | "@"; f=global; i = univ_instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ] ; operconstr: [ "200" RIGHTA [ c = binder_constr -> { c } ] | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<:"; c2 = SELF -> + [ c1 = operconstr; "<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<<:"; c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; "<<:"; c2 = SELF -> + | c1 = operconstr; "<<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; ":";c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastConv c2) } - | c1 = operconstr; ":"; c2 = SELF -> + | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastConv c2) } | c1 = operconstr; ":>" -> { 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 = instance; args=LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } - | "@"; lid = pattern_identref; args=LIST1 identref -> + [ 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) } + | "@"; lid = pattern_identref; 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"; ".." -> - { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ] + [ ".."; c = operconstr 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; ")" -> - { 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 = operconstr; ".("; 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"); ")" -> { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) } - | c=operconstr; "%"; key=IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ] + | c = operconstr; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ] | "0" - [ c=atomic_constr -> { c } - | c=match_constr -> { c } + [ c = atomic_constr -> { c } + | c = match_constr -> { c } | "("; c = operconstr LEVEL "200"; ")" -> { (* Preserve parentheses around numerals so that constrintern does not collapse -(3) into the numeral -3. *) @@ -243,86 +203,81 @@ GRAMMAR EXTEND Gram | _ -> c) } | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> - { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } + { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> - { CAst.make ~loc @@ CGeneralization (Implicit, None, c) } + { CAst.make ~loc @@ CGeneralization (Implicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> - { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } - ] ] + { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ] ; record_declaration: - [ [ fs = record_fields -> { CAst.make ~loc @@ CRecord fs } ] ] + [ [ fs = fields_def -> { CAst.make ~loc @@ CRecord fs } ] ] ; - - record_fields: - [ [ f = record_field_declaration; ";"; fs = record_fields -> { f :: fs } - | f = record_field_declaration -> { [f] } - | -> { [] } - ] ] + fields_def: + [ [ f = field_def; ";"; fs = fields_def -> { f :: fs } + | f = field_def -> { [f] } + | -> { [] } ] ] ; - - record_field_declaration: + field_def: [ [ id = global; bl = binders; ":="; c = lconstr -> - { (id, mkLambdaCN ~loc bl c) } ] ] + { (id, mkLambdaCN ~loc bl c) } ] ] ; binder_constr: [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> - { mkProdCN ~loc bl c } + { mkProdCN ~loc bl c } | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> - { mkLambdaCN ~loc bl c } - | "let"; id=name; bl = binders; ty = type_cstr; ":="; + { mkLambdaCN ~loc bl c } + | "let"; id=name; bl = binders; ty = let_type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr 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"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> - { let fixp = mk_single_fix fx in - let { CAst.loc = li; v = id } = match fixp.CAst.v with - CFix(id,_) -> id - | CCoFix(id,_) -> id - | _ -> assert false in - CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c) } + | "let"; "fix"; fx = fix_decl; "in"; c = operconstr 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 {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" -> - { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) } + po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; + c2 = operconstr LEVEL "200" -> + { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) } | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; - "in"; c2 = operconstr LEVEL "200" -> - { CAst.make ~loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) } + "in"; c2 = operconstr 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" -> - { CAst.make ~loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) } - + rt = case_type; "in"; c2 = operconstr 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" -> - { 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" -> - { CAst.make ~loc @@ CIf (c, po, b1, b2) } - | c=fix_constr -> { c } ] ] + ":="; c1 = operconstr LEVEL "200"; rt = case_type; + "in"; c2 = operconstr 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" -> + { 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: - [ [ id = lpar_id_coloneq; c=lconstr; ")" -> - { (c,Some (CAst.make ~loc @@ ExplByName id)) } + [ [ id = lpar_id_coloneq; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) } | c=operconstr LEVEL "9" -> { (c,None) } ] ] ; atomic_constr: - [ [ g=global; i=instance -> { CAst.make ~loc @@ CRef (g,i) } - | s=sort -> { CAst.make ~loc @@ CSort s } - | n=NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (SPlus,n)) } - | s=string -> { CAst.make ~loc @@ CPrim (String s) } + [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) } + | s = sort -> { CAst.make ~loc @@ CSort s } + | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (SPlus,n)) } + | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } - | "?"; "["; id=ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } - | "?"; "["; id=pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) } - | id=pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] + | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } + | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) } + | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] ; inst: [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ] @@ -331,7 +286,7 @@ GRAMMAR EXTEND Gram [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l } | -> { [] } ] ] ; - instance: + univ_instance: [ [ "@{"; l = LIST0 universe_level; "}" -> { Some l } | -> { None } ] ] ; @@ -341,52 +296,50 @@ GRAMMAR EXTEND Gram | "Prop" -> { UNamed GProp } | "Type" -> { UAnonymous {rigid=true} } | "_" -> { UAnonymous {rigid=false} } - | id = global -> { UNamed (GType id) } - ] ] - ; - fix_constr: - [ [ fx1=single_fix -> { mk_single_fix fx1 } - | f=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; - "for"; id=identref -> - { let (_,kw,dcl1) = f in - mk_fix(loc,kw,id,dcl1::dcls) } - ] ] + | id = global -> { UNamed (GType id) } ] ] ; - single_fix: - [ [ kw=fix_kw; dcl=fix_decl -> { (loc,kw,dcl) } ] ] + 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 -> + { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ] ; - fix_kw: - [ [ "fix" -> { true } - | "cofix" -> { false } ] ] + 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 -> + { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ] ; fix_decl: - [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":="; - c=operconstr LEVEL "200" -> - { (id,fst bl,snd bl,c,ty) } ] ] + [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":="; + c = operconstr 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" -> + { CAst.make ~loc (id,bl,ty,c) } ] ] ; match_constr: - [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; - br=branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ] + [ [ "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"; - ona = OPT ["as"; id=name -> { id } ]; + [ [ c = operconstr LEVEL "100"; + ona = OPT ["as"; id = name -> { id } ]; ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] -> - { (c,ona,ty) } ] ] + { (c,ona,ty) } ] ] ; case_type: [ [ "return"; ty = operconstr LEVEL "100" -> { ty } ] ] ; return_type: - [ [ a = OPT [ na = OPT["as"; na=name -> { na } ]; + [ [ a = OPT [ na = OPT["as"; na = name -> { na } ]; ty = case_type -> { (na,ty) } ] -> { match a with | None -> None, None - | Some (na,t) -> (na, Some t) } - ] ] + | Some (na,t) -> (na, Some t) } ] ] ; branches: - [ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ] + [ [ OPT"|"; br = LIST0 eqn SEP "|" -> { br } ] ] ; mult_pattern: [ [ pl = LIST1 pattern LEVEL "200" SEP "," -> { pl } ] ] @@ -400,18 +353,14 @@ GRAMMAR EXTEND Gram ; record_patterns: [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps } - | p = record_pattern; ";" -> { [p] } | p = record_pattern-> { [p] } - | -> { [] } - ] ] + | -> { [] } ] ] ; pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; ":"; ty = binder_constr -> - {CAst.make ~loc @@ CPatCast (p, ty) } - | p = pattern; ":"; ty = operconstr LEVEL "100" -> - {CAst.make ~loc @@ CPatCast (p, ty) } ] + [ p = pattern; ":"; ty = operconstr LEVEL "200" -> + { CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA @@ -421,68 +370,47 @@ GRAMMAR EXTEND Gram | "@"; r = Prim.reference; lp = LIST0 NEXT -> { CAst.make ~loc @@ CPatCstr (r, Some lp, []) } ] | "1" LEFTA - [ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ] + [ c = pattern; "%"; key = IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ] | "0" [ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) } | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat } | "_" -> { CAst.make ~loc @@ CPatAtom None } | "("; p = pattern LEVEL "200"; ")" -> - { (* Preserve parentheses around numerals so that constrintern does not - collapse -(3) into the numeral -3. *) - (match p.CAst.v with - | CPatPrim (Numeral (SPlus,n)) -> - CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) - | _ -> p) } + { (* Preserve parentheses around numerals so that constrintern does not + collapse -(3) into the numeral -3. *) + match p.CAst.v with + | CPatPrim (Numeral (SPlus,n)) -> + CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) + | _ -> p } | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> { CAst.make ~loc @@ CPatOr (p::pl) } | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ] ; - impl_ident_tail: - [ [ "}" -> { binder_of_name Implicit } - | nal=LIST1 name; ":"; c=lconstr; "}" -> - { (fun na -> CLocalAssum (na::nal,Default Implicit,c)) } - | nal=LIST1 name; "}" -> - { (fun na -> CLocalAssum (na::nal,Default Implicit, - CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some loc)) @@ - CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))) } - | ":"; c=lconstr; "}" -> - { (fun na -> CLocalAssum ([na],Default Implicit,c)) } - ] ] - ; fixannot: - [ [ "{"; IDENT "struct"; id=identref; "}" -> { CAst.make ~loc @@ CStructRec id } - | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CAst.make ~loc @@ CWfRec(id,rel) } - | "{"; IDENT "measure"; m=constr; id=OPT identref; - rel=OPT constr; "}" -> { CAst.make ~loc @@ CMeasureRec (id,m,rel) } - ] ] - ; - impl_name_head: - [ [ id = impl_ident_head -> { CAst.make ~loc @@ Name id } ] ] + [ [ "{"; IDENT "struct"; id = identref; "}" -> { CAst.make ~loc @@ CStructRec id } + | "{"; IDENT "wf"; rel = constr; id = identref; "}" -> { CAst.make ~loc @@ CWfRec(id,rel) } + | "{"; IDENT "measure"; m = constr; id = OPT identref; rel = OPT constr; "}" -> + { CAst.make ~loc @@ CMeasureRec (id,m,rel) } ] ] ; binders_fixannot: - [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> - { (assum na :: fst bl), snd bl } - | f = fixannot -> { [], Some f } + [ [ ensure_fixannot; f = fixannot -> { [], Some f } | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl } - | -> { [], None } - ] ] + | -> { [], None } ] ] ; open_binders: (* Same as binders but parentheses around a closed binder are optional if the latter is unique *) - [ [ - id = name; idl = LIST0 name; ":"; c = lconstr -> - { [CLocalAssum (id::idl,Default Explicit,c)] - (* binders factorized with open binder *) } + [ [ id = name; idl = LIST0 name; ":"; c = lconstr -> + { [CLocalAssum (id::idl,Default Explicit,c)] } + (* binders factorized with open binder *) | id = name; idl = LIST0 name; bl = binders -> - { binders_of_names (id::idl) @ bl } + { binders_of_names (id::idl) @ bl } | id1 = name; ".."; id2 = name -> - { [CLocalAssum ([id1;(CAst.make ~loc (Name ldots_var));id2], - Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + { [CLocalAssum ([id1;(CAst.make ~loc (Name ldots_var));id2], + Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } | bl = closed_binder; bl' = binders -> - { bl@bl' } - ] ] + { bl@bl' } ] ] ; binders: [ [ l = LIST0 binder -> { List.flatten l } ] ] @@ -492,49 +420,50 @@ GRAMMAR EXTEND Gram | bl = closed_binder -> { bl } ] ] ; closed_binder: - [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> - { [CLocalAssum (id::idl,Default Explicit,c)] } - | "("; id=name; ":"; c=lconstr; ")" -> - { [CLocalAssum ([id],Default Explicit,c)] } - | "("; id=name; ":="; c=lconstr; ")" -> - { (match c.CAst.v with + [ [ "("; id = name; idl = LIST1 name; ":"; c = lconstr; ")" -> + { [CLocalAssum (id::idl,Default Explicit,c)] } + | "("; id = name; ":"; c = lconstr; ")" -> + { [CLocalAssum ([id],Default Explicit,c)] } + | "("; id = name; ":="; c = lconstr; ")" -> + { match c.CAst.v with | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)] - | _ -> [CLocalDef (id,c,None)]) } - | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - { [CLocalDef (id,c,Some t)] } - | "{"; id=name; "}" -> - { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } - | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> - { [CLocalAssum (id::idl,Default Implicit,c)] } - | "{"; id=name; ":"; c=lconstr; "}" -> - { [CLocalAssum ([id],Default Implicit,c)] } - | "{"; id=name; idl=LIST1 name; "}" -> - { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + | _ -> [CLocalDef (id,c,None)] } + | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" -> + { [CLocalDef (id,c,Some t)] } + | "{"; id = name; "}" -> + { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" -> + { [CLocalAssum (id::idl,Default Implicit,c)] } + | "{"; id = name; ":"; c = lconstr; "}" -> + { [CLocalAssum ([id],Default Implicit,c)] } + | "{"; id = name; idl = LIST1 name; "}" -> + { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } | "'"; p = pattern LEVEL "0" -> - { let (p, ty) = + { let (p, ty) = match p.CAst.v with | CPatCast (p, ty) -> (p, Some ty) | _ -> (p, None) in - [CLocalPattern (CAst.make ~loc (p, ty))] } - ] ] + [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" -> - { id, expl, c } - | iid=name_colon ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> + { id, expl, c } + | iid = name_colon ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> { (CAst.make ~loc iid), expl, c } | c = operconstr LEVEL "200" -> - { (CAst.make ~loc Anonymous), false, c } - ] ] + { (CAst.make ~loc Anonymous), false, c } ] ] ; - type_cstr: - [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ] + [ [ ":"; c = lconstr -> { c } + | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ] + ; + let_type_cstr: + [ [ c = OPT [":"; c = lconstr -> { c } ] -> { Loc.tag ~loc c } ] ] ; END diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index c1f52c5b39..020501aedf 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -31,10 +31,35 @@ let my_int_of_string loc s = with Failure _ -> CErrors.user_err ~loc (Pp.str "This number is too large.") -let check_nospace loc expected = - let (bp, ep) = Loc.unloc loc in - if ep = bp + String.length expected then () else - Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected")) +let rec contiguous tok n m = + n == m + || + let (_, ep) = Loc.unloc (tok n) in + let (bp, _) = Loc.unloc (tok (n + 1)) in + Int.equal ep bp && contiguous tok (succ n) m + +let rec lookahead_kwds strm n = function + | [] -> () + | x :: xs -> + let toks = Stream.npeek (n+1) strm in + match List.nth toks n with + | Tok.KEYWORD y -> + if String.equal x y then lookahead_kwds strm (succ n) xs + else raise Stream.Failure + | _ -> raise Stream.Failure + | exception (Failure _) -> raise Stream.Failure + +(* [test_nospace m] fails if the next m tokens are not contiguous keywords *) +let test_nospace m = assert(m <> []); Pcoq.Entry.of_parser "test_nospace" + (fun tok strm -> + let n = Stream.count strm in + lookahead_kwds strm 0 m; + if contiguous tok n (n + List.length m - 1) then () + else raise Stream.Failure) + +let test_nospace_pipe_closedcurly = + test_nospace ["|"; "}"] + } @@ -130,6 +155,6 @@ GRAMMAR EXTEND Gram [ [ i = NUMERAL -> { check_int loc i } ] ] ; bar_cbrace: - [ [ "|"; "}" -> { check_nospace loc "|}" } ] ] + [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ] ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 3aaba27579..734dd8ee8a 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -131,73 +131,57 @@ end (** Binding general entry keys to symbol *) -type ('s, 'trec, 'a, 'r) casted_rule = -| CastedRNo : ('s, G.ty_norec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, norec, 'a, 'r) casted_rule -| CastedRMay : ('s, G.ty_mayrec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, mayrec, 'a, 'r) casted_rule - -type ('s, 'trec, 'a) casted_symbol = -| CastedSNo : ('s, G.ty_norec, 'a) G.ty_symbol -> ('s, norec, 'a) casted_symbol -| CastedSMay : ('s, G.ty_mayrec, 'a) G.ty_symbol -> ('s, mayrec, 'a) casted_symbol - -let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) casted_symbol = +let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.ty_symbol = function -| Atoken t -> CastedSNo (G.s_token t) +| Atoken t -> G.s_token t | Alist1 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1 s) - | CastedSMay s -> CastedSMay (G.s_list1 s) end + let s = symbol_of_prod_entry_key s in + G.s_list1 s | Alist1sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list1sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list1sep s sep false | Alist0 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0 s) - | CastedSMay s -> CastedSMay (G.s_list0 s) end + let s = symbol_of_prod_entry_key s in + G.s_list0 s | Alist0sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list0sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list0sep s sep false | Aopt s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_opt s) - | CastedSMay s -> CastedSMay (G.s_opt s) end -| Aself -> CastedSMay G.s_self -| Anext -> CastedSMay G.s_next -| Aentry e -> CastedSNo (G.s_nterm e) -| Aentryl (e, n) -> CastedSNo (G.s_nterml e n) + let s = symbol_of_prod_entry_key s in + G.s_opt s +| Aself -> G.s_self +| Anext -> G.s_next +| Aentry e -> G.s_nterm e +| Aentryl (e, n) -> G.s_nterml e n | Arules rs -> let warning msg = Feedback.msg_warning Pp.(str msg) in - CastedSNo (G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)) + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) -and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) casted_rule = function -| Stop -> CastedRNo (G.r_stop, fun act loc -> act loc) +and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.ty_rule = function +| Stop -> + G.r_stop | Next (r, s) -> - begin match symbol_of_rule r, symbol_of_prod_entry_key s with - | CastedRNo (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRNo (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) end + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next r s | NextNoRec (r, s) -> - let CastedRNo (r, cast) = symbol_of_rule r in - let CastedSNo s = symbol_of_prod_entry_key s in - CastedRNo (G.r_next_norec r s, (fun act x -> cast (act x))) + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next_norec r s and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function | Rules (r, act) -> - let CastedRNo (symb, cast) = symbol_of_rule r in - G.rules (symb, cast act) + let symb = symbol_of_rule r in + G.rules (symb,act) (** FIXME: This is a hack around a deficient camlp5 API *) type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function | Rule (toks, act) -> - match symbol_of_rule toks with - | CastedRNo (symb, cast) -> AnyProduction (symb, cast act) - | CastedRMay (symb, cast) -> AnyProduction (symb, cast act) + AnyProduction (symbol_of_rule toks, act) let of_coq_single_extend_statement (lvl, assoc, rule) = (lvl, assoc, List.map of_coq_production_rule rule) @@ -215,6 +199,18 @@ let fix_extend_statement (pos, st) = (** Type of reinitialization data *) type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + type extend_rule = | ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule @@ -455,6 +451,7 @@ module Constr = let typeclass_constraint = Entry.create "constr:typeclass_constraint" let record_declaration = Entry.create "constr:record_declaration" let appl_arg = Entry.create "constr:appl_arg" + let type_cstr = Entry.create "constr:type_cstr" end module Module = @@ -462,11 +459,10 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end + let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) = - let r = - match symbol_of_prod_entry_key e with - | CastedSNo s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) - | CastedSMay s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in + let s = symbol_of_prod_entry_key e in + let r = G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in let warning msg = Feedback.msg_warning Pp.(str msg) in @@ -602,7 +598,7 @@ let unfreeze (grams, lex) = (** No need to provide an init function : the grammar state is statically available, and already empty initially, while the lexer state should not be reset, since it contains - keywords declared in g_*.ml4 *) + keywords declared in g_*.mlg *) let parser_summary_tag = Summary.declare_summary_tag "GRAMMAR_LEXER" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index cde867d2ef..404fbdb4fd 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -29,7 +29,7 @@ module Entry : sig val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit - val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t + val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a val name : 'a t -> string end @@ -108,7 +108,7 @@ end - "f" constr(x) (developer gives an EXTEND rule) | - | macro-generation in tacextend.ml4/vernacextend.ml4/argextend.ml4 + | macro-generation in tacextend.mlg/vernacextend.mlg/argextend.mlg V [GramTerminal "f"; GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")] @@ -197,6 +197,7 @@ module Constr : val typeclass_constraint : (lname * bool * constr_expr) Entry.t val record_declaration : constr_expr Entry.t val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t + val type_cstr : constr_expr Entry.t end module Module : @@ -212,8 +213,19 @@ val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self optio type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) -val grammar_extend : 'a Entry.t -> gram_reinit option -> - 'a Extend.extend_statement -> unit +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + +val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) |