diff options
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/egramcoq.ml | 68 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 72 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 14 | ||||
-rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 51 | ||||
-rw-r--r-- | parsing/pcoq.ml | 12 | ||||
-rw-r--r-- | parsing/pcoq.mli | 25 |
7 files changed, 134 insertions, 110 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ea6266dd4..cad837d08 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -226,14 +226,14 @@ type _ target = type prod_info = production_level * production_position type (_, _) entry = -| TTName : ('self, Name.t Loc.located) entry +| TTName : ('self, Misctypes.lname) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry -| TTBinder : ('self, local_binder_expr list) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry -| TTBinderListT : ('self, local_binder_expr list) entry -| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry +| TTPattern : int -> ('self, cases_pattern_expr) entry +| TTOpenBinderList : ('self, local_binder_expr list) entry +| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry @@ -289,40 +289,34 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as Alist1 (symbol_of_target typ' assoc from forpat) | TTConstrList (typ', tkl, forpat) -> Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) -| TTBinderListF [] -> Alist1 (Aentry Constr.binder) -| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) +| TTPattern p -> Aentryl (Constr.pattern, p) +| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) +| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) | TTName -> Aentry Prim.name -| TTBinder -> Aentry Constr.binder -| TTBinderListT -> Aentry Constr.open_binders +| TTOpenBinderList -> Aentry Constr.open_binders | TTBigint -> Aentry Prim.bigint | TTReference -> Aentry Constr.global let interp_entry forpat e = match e with -| ETName -> TTAny TTName -| ETReference -> TTAny TTReference -| ETBigint -> TTAny TTBigint -| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList.") -| ETBinder false -> TTAny TTBinder -| ETConstr p -> TTAny (TTConstr (p, forpat)) -| ETPattern -> assert false (** not used *) -| ETOther _ -> assert false (** not used *) -| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) -| ETBinderList (true, []) -> TTAny TTBinderListT -| ETBinderList (true, _) -> assert false -| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl) - -let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with - | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None) - | Name id -> CRef (Ident (Loc.tag ?loc id), None) - -let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with +| ETProdName -> TTAny TTName +| ETProdReference -> TTAny TTReference +| ETProdBigint -> TTAny TTBigint +| ETProdConstr p -> TTAny (TTConstr (p, forpat)) +| ETProdPattern p -> TTAny (TTPattern p) +| ETProdOther _ -> assert false (** not used *) +| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList +| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) + +let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None | Name id -> CPatAtom (Some (Ident (Loc.tag ?loc id))) type 'r env = { constrs : 'r list; constrlists : 'r list list; - binders : (local_binder_expr list * bool) list; + binders : cases_pattern_expr list; + binderlists : local_binder_expr list list; } let push_constr subst v = { subst with constrs = v :: subst.constrs } @@ -332,12 +326,16 @@ match e with | TTConstr _ -> push_constr subst v | TTName -> begin match forpat with - | ForConstr -> push_constr subst (constr_expr_of_name v) + | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders } | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) end -| TTBinder -> { subst with binders = (v, true) :: subst.binders } -| TTBinderListT -> { subst with binders = (v, true) :: subst.binders } -| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } +| TTPattern _ -> + begin match forpat with + | ForConstr -> { subst with binders = v :: subst.binders } + | ForPattern -> push_constr subst v + end +| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists } +| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (v,true))) @@ -437,11 +435,9 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> - let env = (env.constrs, env.constrlists, List.map fst env.binders) in - CAst.make ~loc @@ CNotation (notation , env) + let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in + CAst.make ~loc @@ CNotation (notation, env) | ForPattern -> fun notation loc env -> - let invalid = List.exists (fun (_, b) -> not b) env.binders in - let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in let env = (env.constrs, env.constrlists) in CAst.make ~loc @@ CPatNotation (notation, env, []) @@ -457,7 +453,7 @@ let extend_constr state forpat ng = let needed_levels, state = register_empty_levels state isforpat pure_sublevels in let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in - let empty = { constrs = []; constrlists = []; binders = [] } in + let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = (name, p4assoc, [Rule (symbs, act)]) in let r = ExtendRule (entry, reinit, (pos, [rule])) in diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index db68a75e0..8a1e6d121 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -36,21 +36,21 @@ let mk_cast = function let loc = Loc.merge_opt (constr_loc c) (constr_loc ty) in CAst.make ?loc @@ CCast(c, CastConv ty) -let binder_of_name expl (loc,na) = - CLocalAssum ([loc, na], Default expl, +let binder_of_name expl { CAst.loc = loc; v = na } = + CLocalAssum ([CAst.make ?loc na], Default expl, CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) let binders_of_names l = List.map (binder_of_name Explicit) l -let mk_fixb (id,bl,ann,body,(loc,tyc)) = +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)) = - let _ = Option.map (fun (aloc,_) -> +let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = + let _ = Option.map (fun { CAst.loc = aloc } -> CErrors.user_err ?loc:aloc ~hdr:"Constr:mk_cofixb" (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in @@ -61,10 +61,10 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let mk_fix(loc,kw,id,dcls) = if kw then - let fb = List.map mk_fixb dcls in + let fb : fix_expr list = List.map mk_fixb dcls in CAst.make ~loc @@ CFix(id,fb) else - let fb = List.map mk_cofixb dcls in + let fb : cofix_expr list = List.map mk_cofixb dcls in CAst.make ~loc @@ CCoFix(id,fb) let mk_single_fix (loc,kw,dcl) = @@ -120,7 +120,7 @@ let name_colon = | _ -> err ()) | _ -> err ()) -let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None +let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family @@ -131,7 +131,7 @@ GEXTEND Gram [ [ id = Prim.ident -> id ] ] ; Prim.name: - [ [ "_" -> Loc.tag ~loc:!@loc Anonymous ] ] + [ [ "_" -> CAst.make ~loc:!@loc Anonymous ] ] ; global: [ [ r = Prim.reference -> r ] ] @@ -196,8 +196,9 @@ GEXTEND Gram | "10" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args) | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) - | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> - let args = List.map (fun x -> CAst.make @@ CRef (Ident x,None), None) args in + | "@"; lid = pattern_identref; args=LIST1 identref -> + let { CAst.loc = locid; v = id } = lid in + let args = List.map (fun x -> CAst.make @@ CRef (Ident Loc.(tag ?loc:x.CAst.loc x.CAst.v), None), None) args in CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> @@ -216,9 +217,11 @@ GEXTEND Gram | "("; c = operconstr LEVEL "200"; ")" -> (match c.CAst.v with | CPrim (Numeral (n,true)) -> - CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) + CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c + | "{"; c = binder_constr ; "}" -> + CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[])) | "`{"; c = operconstr LEVEL "200"; "}" -> CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> @@ -254,11 +257,11 @@ GEXTEND Gram Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in - let (li,id) = match fixp.CAst.v with + let { CAst.loc = li; v = id } = match fixp.CAst.v with CFix(id,_) -> id | CCoFix(id,_) -> id | _ -> assert false in - CAst.make ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c) + CAst.make ~loc:!@loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; @@ -267,17 +270,17 @@ GEXTEND Gram | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) + CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc:!@loc ([[p]], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -286,7 +289,7 @@ GEXTEND Gram ; appl_arg: [ [ id = lpar_id_coloneq; c=lconstr; ")" -> - (c,Some (Loc.tag ~loc:!@loc @@ ExplByName id)) + (c,Some (CAst.make ~loc:!@loc @@ ExplByName id)) | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: @@ -366,7 +369,7 @@ GEXTEND Gram ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; - "=>"; rhs = lconstr -> (Loc.tag ~loc:!@loc (pll,rhs)) ] ] + "=>"; rhs = lconstr -> (CAst.make ~loc:!@loc (pll,rhs)) ] ] ; record_pattern: [ [ id = global; ":="; pat = pattern -> (id, pat) ] ] @@ -385,19 +388,9 @@ GEXTEND Gram | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ p = pattern; "as"; id = ident -> - CAst.make ~loc:!@loc @@ CPatAlias (p, id) - | p = pattern; lp = LIST1 NEXT -> - (let open CAst in match p with - | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp) - | { v = CPatCstr (r, None, l2); loc } -> - CErrors.user_err ?loc ~hdr:"compound_pattern" - (Pp.str "Nested applications not supported.") - | { v = CPatCstr (r, l1, l2) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp) - | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp) - | _ -> CErrors.user_err - ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern" - (Pp.str "Such pattern cannot have arguments.")) + [ p = pattern; "as"; na = name -> + CAst.make ~loc:!@loc @@ CPatAlias (p, na) + | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp | "@"; r = Prim.reference; lp = LIST0 NEXT -> CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] | "1" LEFTA @@ -428,7 +421,8 @@ GEXTEND Gram (fun na -> CLocalAssum (na::nal,Default Implicit,c)) | nal=LIST1 name; "}" -> (fun na -> CLocalAssum (na::nal,Default Implicit, - CAst.make ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) + 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)) ] ] @@ -441,7 +435,7 @@ GEXTEND Gram ] ] ; impl_name_head: - [ [ id = impl_ident_head -> (Loc.tag ~loc:!@loc @@ Name id) ] ] + [ [ id = impl_ident_head -> (CAst.make ~loc:!@loc @@ Name id) ] ] ; binders_fixannot: [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> @@ -461,7 +455,7 @@ GEXTEND Gram | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2], + [CLocalAssum ([id1;(CAst.make ~loc:!@loc (Name ldots_var));id2], Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | bl = closed_binder; bl' = binders -> bl@bl' @@ -503,17 +497,17 @@ GEXTEND Gram | CPatCast (p, ty) -> (p, Some ty) | _ -> (p, None) in - [CLocalPattern (Loc.tag ~loc:!@loc (p, ty))] + [CLocalPattern (CAst.make ~loc:!@loc (p, ty))] ] ] ; typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> (Loc.tag ~loc:!@loc Anonymous), true, c + [ [ "!" ; c = operconstr LEVEL "200" -> (CAst.make ~loc:!@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" -> - (Loc.tag ~loc:!@loc iid), expl, c + (CAst.make ~loc:!@loc iid), expl, c | c = operconstr LEVEL "200" -> - (Loc.tag ~loc:!@loc Anonymous), false, c + (CAst.make ~loc:!@loc Anonymous), false, c ] ] ; diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 891c232ee..0b7efe739 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -43,13 +43,13 @@ GEXTEND Gram [ [ LEFTQMARK; id = ident -> id ] ] ; pattern_identref: - [ [ id = pattern_ident -> Loc.tag ~loc:!@loc id ] ] + [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ] ; var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> Loc.tag ~loc:!@loc id ] ] + [ [ id = ident -> CAst.make ~loc:!@loc id ] ] ; identref: - [ [ id = ident -> Loc.tag ~loc:!@loc id ] ] + [ [ id = ident -> CAst.make ~loc:!@loc id ] ] ; field: [ [ s = FIELD -> Id.of_string s ] ] @@ -70,8 +70,8 @@ GEXTEND Gram ] ] ; name: - [ [ IDENT "_" -> Loc.tag ~loc:!@loc Anonymous - | id = ident -> Loc.tag ~loc:!@loc @@ Name id ] ] + [ [ IDENT "_" -> CAst.make ~loc:!@loc Anonymous + | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ] ; reference: [ [ id = ident; (l,id') = fields -> @@ -95,7 +95,7 @@ GEXTEND Gram ] ] ; ne_lstring: - [ [ s = ne_string -> Loc.tag ~loc:!@loc s ] ] + [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ] ; dirpath: [ [ id = ident; l = LIST0 field -> @@ -105,7 +105,7 @@ GEXTEND Gram [ [ s = STRING -> s ] ] ; lstring: - [ [ s = string -> (Loc.tag ~loc:!@loc s) ] ] + [ [ s = string -> (CAst.make ~loc:!@loc s) ] ] ; integer: [ [ i = INT -> my_int_of_string (!@loc) i diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1c3ba7837..482373150 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -29,7 +29,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> - VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((Loc.tag ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) + VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; c = lconstr -> VernacExactProof c diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d42b5f622..93e534e0b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -115,7 +115,7 @@ GEXTEND Gram ; located_vernac: - [ [ v = vernac_control -> Loc.tag ~loc:!@loc v ] ] + [ [ v = vernac_control -> CAst.make ~loc:!@loc v ] ] ; END @@ -134,7 +134,7 @@ let test_plural_form_types loc kwd = function | _ -> () let lname_of_lident : lident -> lname = - Loc.map (fun s -> Name s) + CAst.map (fun s -> Name s) let name_of_ident_decl : ident_decl -> name_decl = on_fst lname_of_lident @@ -629,12 +629,12 @@ GEXTEND Gram VernacCanonical (ByNotation ntn) | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag (Name s)),None),d) + VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,Coercion),((Loc.tag (Name s)),None),d) + VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (f, s, t) @@ -745,7 +745,7 @@ GEXTEND Gram ; argument_spec: [ [ b = OPT "!"; id = name ; s = OPT scope -> - snd id, not (Option.is_empty b), Option.map (fun x -> Loc.tag ~loc:!@loc x) s + id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc:!@loc x) s ] ]; (* List of arguments implicit status, scope, modifiers *) @@ -758,7 +758,7 @@ GEXTEND Gram | "/" -> [`Slash] | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; @@ -766,7 +766,7 @@ GEXTEND Gram implicit_status = NotImplicit}) items | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; @@ -774,7 +774,7 @@ GEXTEND Gram implicit_status = Implicit}) items | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; @@ -784,11 +784,11 @@ GEXTEND Gram ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> [(snd name, Vernacexpr.NotImplicit)] + [ name = name -> [(name.CAst.v, Vernacexpr.NotImplicit)] | "["; items = LIST1 name; "]" -> - List.map (fun name -> (snd name, Vernacexpr.Implicit)) items + List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items | "{"; items = LIST1 name; "}" -> - List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items + List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items ] ]; strategy_level: @@ -800,9 +800,9 @@ GEXTEND Gram ; instance_name: [ [ name = ident_decl; sup = OPT binders -> - (let ((loc,id),l) = name in ((loc, Name id),l)), + (CAst.map (fun id -> Name id) (fst name), snd name), (Option.default [] sup) - | -> ((Loc.tag ~loc:!@loc Anonymous), None), [] ] ] + | -> ((CAst.make ~loc:!@loc Anonymous), None), [] ] ] ; hint_info: [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> @@ -1134,8 +1134,8 @@ GEXTEND Gram | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> - let (loc,s) = s in - VernacSyntaxExtension (true,((loc,"x '"^s^"' y"),l)) + let s = CAst.map (fun s -> "x '"^s^"' y") s in + VernacSyntaxExtension (true,(s,l)) | IDENT "Reserved"; IDENT "Notation"; s = ne_lstring; @@ -1166,14 +1166,16 @@ GEXTEND Gram | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> SetCompatVersion (parse_compat_version s) - | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s]; - s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] -> + | IDENT "format"; s1 = [s = STRING -> CAst.make ~loc:!@loc s]; + s2 = OPT [s = STRING -> CAst.make ~loc:!@loc s] -> begin match s1, s2 with - | (_,k), Some s -> SetFormat(k,s) + | { CAst.v = k }, Some s -> SetFormat(k,s) | s, None -> SetFormat ("text",s) end | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) + | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev) + | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None) | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) ] ] ; @@ -1181,7 +1183,20 @@ GEXTEND Gram [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference | IDENT "bigint" -> ETBigint | IDENT "binder" -> ETBinder true + | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n) + | IDENT "pattern" -> ETPattern (false,None) + | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n) + | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None) + | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n) | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; + at_level: + [ [ "at"; n = level -> n ] ] + ; + constr_as_binder_kind: + [ [ "as"; IDENT "ident" -> AsIdent + | "as"; IDENT "pattern" -> AsIdentOrPattern + | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ] + ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 73e103995..7a51908d9 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -638,3 +638,15 @@ let () = Grammar.register0 wit_constr (Constr.constr); Grammar.register0 wit_red_expr (Vernac_.red_expr); () + +(** Registering extra grammar *) + +type any_entry = AnyEntry : 'a Gram.entry -> any_entry + +let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty + +let register_grammars_by_name name grams = + grammar_names := String.Map.add name grams !grammar_names + +let find_grammars_by_name name = + String.Map.find name !grammar_names diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 75378d2c6..f36250176 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -192,17 +192,17 @@ module Prim : open Libnames val preident : string Gram.entry val ident : Id.t Gram.entry - val name : Name.t located Gram.entry - val identref : Id.t located Gram.entry + val name : lname Gram.entry + val identref : lident Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry - val pattern_identref : Id.t located Gram.entry + val pattern_identref : lident Gram.entry val base_ident : Id.t Gram.entry val natural : int Gram.entry val bigint : Constrexpr.raw_natural_number Gram.entry val integer : int Gram.entry val string : string Gram.entry - val lstring : string located Gram.entry + val lstring : lstring Gram.entry val qualid : qualid located Gram.entry val fullyqualid : Id.t list located Gram.entry val reference : reference Gram.entry @@ -210,8 +210,8 @@ module Prim : val smart_global : reference or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry - val ne_lstring : string located Gram.entry - val var : Id.t located Gram.entry + val ne_lstring : lstring Gram.entry + val var : lident Gram.entry end module Constr : @@ -233,10 +233,10 @@ module Constr : val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) val binders : local_binder_expr list Gram.entry (* list of binder *) val open_binders : local_binder_expr list Gram.entry - val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry - val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry + val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry + val typeclass_constraint : (lname * bool * constr_expr) Gram.entry val record_declaration : constr_expr Gram.entry - val appl_arg : (constr_expr * explicitation located option) Gram.entry + val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry end module Module : @@ -315,3 +315,10 @@ val (!@) : Ploc.t -> Loc.t type frozen_t val parser_summary_tag : frozen_t Summary.Dyn.tag + +(** Registering grammars by name *) + +type any_entry = AnyEntry : 'a Gram.entry -> any_entry + +val register_grammars_by_name : string -> any_entry list -> unit +val find_grammars_by_name : string -> any_entry list |