From 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 09:26:25 +0100 Subject: [ast] Improve precision of Ast location recognition in serialization. We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way. --- parsing/egramcoq.ml | 4 ++-- parsing/g_constr.ml4 | 50 ++++++++++++++++++++++++++------------------------ parsing/g_prim.ml4 | 14 +++++++------- parsing/g_proofs.ml4 | 2 +- parsing/g_vernac.ml4 | 36 ++++++++++++++++++------------------ parsing/pcoq.mli | 18 +++++++++--------- 6 files changed, 63 insertions(+), 61 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index a3d257154..cad837d08 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -226,7 +226,7 @@ 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 | TTConstr : prod_info * 'r target -> ('r, 'r) entry @@ -308,7 +308,7 @@ let interp_entry forpat e = match e with | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) -let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with +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))) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9f12db649..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) = @@ -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"; ".." -> @@ -256,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"; @@ -269,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" -> @@ -288,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: @@ -368,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) ] ] @@ -420,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)) ] ] @@ -433,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 -> @@ -453,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' @@ -495,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 d90fd3eb7..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,10 +1166,10 @@ 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) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index accb51366..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 : -- cgit v1.2.3