[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.

6 files changed, 63 insertions, 61 deletions

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 :