From b1d749e59444f86e40f897c41739168bb1b1b9b3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 25 Feb 2018 22:43:42 +0100 Subject: [located] Push inner locations in `reference` to a CAst.t node. The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now. --- parsing/egramcoq.ml | 2 +- parsing/g_constr.ml4 | 4 ++-- parsing/g_prim.ml4 | 10 +++++----- parsing/g_vernac.ml4 | 8 ++++---- parsing/pcoq.mli | 2 +- 5 files changed, 13 insertions(+), 13 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index c0ead3a0a..5f63d21c4 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -312,7 +312,7 @@ let interp_entry forpat e = match e 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))) + | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id)) type 'r env = { constrs : 'r list; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index b4f09ee6a..9c2806bea 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -200,11 +200,11 @@ GEXTEND Gram | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@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 (Ident Loc.(tag ?loc:x.CAst.loc x.CAst.v), None), None) args in + let args = List.map (fun x -> CAst.make @@ CRef (CAst.make ?loc:x.CAst.loc @@ Ident 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"; ".." -> - CAst.make ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ] + CAst.make ~loc:!@loc @@ CAppExpl ((None, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 69dc391c4..b25ea766a 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -77,16 +77,16 @@ GEXTEND Gram ; reference: [ [ id = ident; (l,id') = fields -> - Qualid (Loc.tag ~loc:!@loc @@ local_make_qualid (l@[id]) id') - | id = ident -> Ident (Loc.tag ~loc:!@loc id) + CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id') + | id = ident -> CAst.make ~loc:!@loc @@ Ident id ] ] ; by_notation: - [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> CAst.make ~loc:!@loc (s, sc) ] ] + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ] ; smart_global: - [ [ c = reference -> Misctypes.AN c - | ntn = by_notation -> Misctypes.ByNotation ntn ] ] + [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c + | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ] ; qualid: [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 99eec9742..72c3cc14a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -624,9 +624,9 @@ GEXTEND Gram VernacSetStrategy l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> - VernacCanonical (AN qid) + VernacCanonical CAst.(make ~loc:!@loc @@ AN qid) | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> - VernacCanonical (ByNotation ntn) + VernacCanonical CAst.(make ~loc:!@loc @@ ByNotation ntn) | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) @@ -640,10 +640,10 @@ GEXTEND Gram VernacIdentityCoercion (f, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (AN qid, s, t) + VernacCoercion (CAst.make ~loc:!@loc @@ AN qid, s, t) | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (ByNotation ntn, s, t) + VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) | IDENT "Context"; c = binders -> VernacContext c diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0f8aad110..9f186224b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -210,7 +210,7 @@ module Prim : val qualid : qualid CAst.t Gram.entry val fullyqualid : Id.t list CAst.t Gram.entry val reference : reference Gram.entry - val by_notation : (string * string option) CAst.t Gram.entry + val by_notation : (string * string option) Gram.entry val smart_global : reference or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry -- cgit v1.2.3