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

1 files changed, 31 insertions, 29 deletions

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 211cad3f5..0d8044f19 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -130,7 +130,7 @@ let pr_ssrhyp _ _ _ = pr_hyp
 let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
-  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in
+  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in
   if not_section_id id then hyp else
   hyp_err ?loc "Can't clear section hypothesis " id
 
@@ -316,7 +316,7 @@ END
 
 
 let pr_index = function
-  | Misctypes.ArgVar (_, id) -> pr_id id
+  | Misctypes.ArgVar {CAst.v=id} -> pr_id id
   | Misctypes.ArgArg n when n > 0 -> int n
   | _ -> mt ()
 let pr_ssrindex _ _ _ = pr_index
@@ -330,13 +330,13 @@ let mk_index ?loc = function
   | iv -> iv
 
 let interp_index ist gl idx =
-  Tacmach.project gl, 
+  Tacmach.project gl,
   match idx with
   | Misctypes.ArgArg _ -> idx
-  | Misctypes.ArgVar (loc, id) ->
+  | Misctypes.ArgVar id ->
     let i =
       try
-        let v = Id.Map.find id ist.Tacinterp.lfun in
+        let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
         begin match Tacinterp.Value.to_int v with
         | Some i -> i
         | None ->
@@ -350,8 +350,8 @@ let interp_index ist gl idx =
           end
         | None -> raise Not_found
         end end
-    with _ -> CErrors.user_err ?loc (str"Index not a number") in
-    Misctypes.ArgArg (check_index ?loc i)
+    with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
+    Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
 
 open Pltac
 
@@ -1014,22 +1014,22 @@ let rec mkBstruct i = function
   | [] -> []
 
 let rec format_local_binders h0 bl0 = match h0, bl0 with
-  | BFvar :: h, CLocalAssum ([_, x], _,  _) :: bl ->
+  | BFvar :: h, CLocalAssum ([{CAst.v=x}], _,  _) :: bl ->
     Bvar x :: format_local_binders h bl
   | BFdecl _ :: h, CLocalAssum (lxs, _, t) :: bl ->
-    Bdecl (List.map snd lxs, t) :: format_local_binders h bl
-  | BFdef :: h, CLocalDef ((_, x), v, oty) :: bl ->
+    Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl
+  | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl ->
     Bdef (x, oty, v) :: format_local_binders h bl
   | _ -> []
   
 let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
-  | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } ->
+  | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } ->
     let bs, c' = format_constr_expr h c in
     Bvar x :: bs, c'
   | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } ->
     let bs, c' = format_constr_expr h c in
-    Bdecl (List.map snd lxs, t) :: bs, c'
-  | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } ->
+    Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c'
+  | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
     let bs, c' = format_constr_expr h c in
     Bdef (x, oty, v) :: bs, c'
   | [BFcast], { v = CCast (c, CastConv t) } ->
@@ -1037,7 +1037,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | BFrec (has_str, has_cast) :: h, 
     { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
     let bs = format_local_binders h bl in
-    let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in
+    let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
     bs @ bstr @ (if has_cast then [Bcast t] else []), c 
   | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } ->
     format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
@@ -1156,18 +1156,18 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
 END
 
 let bvar_lname = let open CAst in function
-  | { v = CRef (Ident (loc, id), _) } -> Loc.tag ?loc @@ Name id
-  | { loc = loc } -> Loc.tag ?loc Anonymous
+  | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id
+  | { loc = loc } -> CAst.make ?loc Anonymous
 
 let pr_ssrbinder prc _ _ (_, c) = prc c
 
 ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder
  | [ ssrbvar(bv) ] ->
-   [ let xloc, _ as x = bvar_lname bv in
+   [ let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
      CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
  | [ "(" ssrbvar(bv) ")" ] ->
-   [ let xloc, _ as x = bvar_lname bv in
+   [ let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
      CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
  | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
@@ -1191,7 +1191,7 @@ GEXTEND Gram
   [  ["of" | "&"]; c = operconstr LEVEL "99" ->
      let loc = !@loc in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ]
   ];
 END
 
@@ -1250,13 +1250,13 @@ END
 let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
 
 let bvar_locid = function
-  | { CAst.v = CRef (Ident (loc, id), _) } -> loc, id
+  | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id
   | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")
 
 
 ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
   | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] ->
-    [ let (_, id) as lid = bvar_locid bv in
+    [ let { CAst.v=id } as lid = bvar_locid bv in
       let (fk, h), (ck, (rc, oc)) = fwd in
       let c = Option.get oc in
       let has_cast, t', c' = match format_constr_expr h c with
@@ -1265,8 +1265,10 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
       let lb = fix_binders bs in
       let has_struct, i =
         let rec loop = function
-          (l', Name id') :: _ when Option.equal Id.equal sid (Some id') -> true, (l', id')
-          | [l', Name id'] when sid = None -> false, (l', id')
+          | {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') ->
+            true, CAst.make ?loc:l' id'
+          | [{CAst.loc=l';v=Name id'}] when sid = None ->
+            false, CAst.make ?loc:l' id'
           | _ :: bn -> loop bn
           | [] -> CErrors.user_err (Pp.str "Bad structural argument") in
         loop (names_of_local_assums lb) in
@@ -1282,7 +1284,7 @@ let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd
 
 ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd
   | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] ->
-    [ let _, id as lid = bvar_locid bv in
+    [ let { CAst.v=id } as lid = bvar_locid bv in
       let (fk, h), (ck, (rc, oc)) = fwd in
       let c = Option.get oc in
       let has_cast, t', c' = match format_constr_expr h c with
@@ -1323,7 +1325,7 @@ END
 
 let intro_id_to_binder = List.map (function 
   | IPatId id ->
-      let xloc, _ as x = bvar_lname (mkCVar id) in
+      let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
         CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
           mkCHole None)
@@ -1332,9 +1334,9 @@ let intro_id_to_binder = List.map (function
 let binder_to_intro_id = CAst.(List.map (function
   | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) }
   | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } ->
-      List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids
-  | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id]
-  | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One]
+      List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon One) ids
+  | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
+  | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon One]
   | _ -> anomaly "ssrbinder is not a binder"))
 
 let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) =
@@ -1405,7 +1407,7 @@ let ssrorelse = Gram.entry_create "ssrorelse"
 GEXTEND Gram
   GLOBAL: ssrorelse ssrseqarg;
   ssrseqidx: [
-    [ test_ssrseqvar; id = Prim.ident -> ArgVar (Loc.tag ~loc:!@loc id)
+    [ test_ssrseqvar; id = Prim.ident -> ArgVar (CAst.make ~loc:!@loc id)
     | n = Prim.natural -> ArgArg (check_index ~loc:!@loc n)
     ] ];
   ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]];