[constrexpr] Make patterns use Loc.located for location information

This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.

Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.

Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.

`git grep 'Loc.t \*'` gives an overview of the remaining work to do.

We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.

3 files changed, 39 insertions, 38 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 496b200020..a973a539a6 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -318,8 +318,8 @@ let constr_expr_of_name (loc,na) = match na with
   | Name id -> CRef (Ident (loc,id), None)
 
 let cases_pattern_expr_of_name (loc,na) = match na with
-  | Anonymous -> CPatAtom (loc,None)
-  | Name id -> CPatAtom (loc,Some (Ident (loc,id)))
+  | Anonymous -> Loc.tag ~loc @@ CPatAtom None
+  | Name id   -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
 
 type 'r env = {
   constrs : 'r list;
@@ -342,13 +342,13 @@ match e with
 | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
   begin match forpat with
-  | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v))
-  | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v))
+  | ForConstr ->  push_constr subst (CPrim (Loc.ghost, Numeral v))
+  | ForPattern -> push_constr subst (Loc.tag @@ CPatPrim (Numeral v))
   end
 | TTReference ->
   begin match forpat with
-  | ForConstr -> push_constr subst (CRef (v, None))
-  | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v))
+  | ForConstr  -> push_constr subst (CRef (v, None))
+  | ForPattern -> push_constr subst (Loc.tag @@ CPatAtom (Some v))
   end
 | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
 
@@ -436,7 +436,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   let invalid = List.exists (fun (_, b) -> not b) env.binders in
   let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in
   let env = (env.constrs, env.constrlists) in
-  CPatNotation (loc, notation, env, [])
+  Loc.tag ~loc @@ CPatNotation (notation, env, [])
 
 let extend_constr state forpat ng =
   let n = ng.notgram_level in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0f2ed88fea..6ca8134c06 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -120,7 +120,7 @@ let name_colon =
               | _ -> err ())
         | _ -> err ())
 
-let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
+let aliasvar = function loc, CPatAlias (_, id) -> Some (loc,Name id) | _ -> None
 
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr universe_level sort global
@@ -254,14 +254,14 @@ GEXTEND Gram
           CLetTuple (!@loc,lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)])
+	    CCases (!@loc, LetPatternStyle, None,    [c1, None, None],       [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -349,7 +349,7 @@ GEXTEND Gram
   ;
   eqn:
     [ [ pll = LIST1 mult_pattern SEP "|";
-        "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
+        "=>"; rhs = lconstr -> (Loc.tag ~loc:!@loc (pll,rhs)) ] ]
   ;
   record_pattern:
     [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
@@ -364,46 +364,46 @@ GEXTEND Gram
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ]
+      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> !@loc, CPatOr (p::pl) ]
     | "99" RIGHTA [ ]
     | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
-	  CPatAlias (!@loc, p, id) ]
+        Loc.tag ~loc:!@loc @@ CPatAlias (p, id) ]
     | "10" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
-	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
-	  | CPatCstr (_, r, None, l2) -> CErrors.user_err
-              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
-              (Pp.str "Nested applications not supported.")
-	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
-	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
+	  | _,   CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp)
+	  | loc, CPatCstr (r, None, l2) ->
+                 CErrors.user_err ~loc ~hdr:"compound_pattern"
+                 (Pp.str "Nested applications not supported.")
+	  | _,   CPatCstr (r, l1, l2)   -> Loc.tag ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
+	  | _,   CPatNotation (n, s, l) -> Loc.tag ~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."))
       |"@"; r = Prim.reference; lp = LIST0 NEXT ->
-        CPatCstr (!@loc, r, Some lp, []) ]
+        !@loc, CPatCstr (r, Some lp, []) ]
     | "1" LEFTA
-      [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
+      [ c = pattern; "%"; key=IDENT -> !@loc, CPatDelimiters (key,c) ]
     | "0"
-      [ r = Prim.reference -> CPatAtom (!@loc,Some r)
-      | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
-      | "_" -> CPatAtom (!@loc,None)
+      [ r = Prim.reference                -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r)
+      | "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat
+      | "_" -> !@loc, CPatAtom None
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
-              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CPatNotation(!@loc,"( _ )",([p],[]),[])
+            | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+                 Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p)
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           let p =
             match p with
-              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CPatNotation(!@loc,"( _ )",([p],[]),[])
+            | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+                 Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p
           in
-	  CPatCast (!@loc, p, ty)
-      | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n))
-      | s = string -> CPatPrim (!@loc, String s) ] ]
+	  !@loc, CPatCast (p, ty)
+      | n = INT    -> Loc.tag ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
+      | s = string -> Loc.tag ~loc:!@loc @@ CPatPrim (String s) ] ]
   ;
   impl_ident_tail:
     [ [ "}" -> binder_of_name Implicit
@@ -482,7 +482,7 @@ GEXTEND Gram
       | "'"; p = pattern LEVEL "0" ->
           let (p, ty) =
             match p with
-            | CPatCast (_, p, ty) -> (p, Some ty)
+            | _, CPatCast (p, ty) -> (p, Some ty)
             | _ -> (p, None)
           in
           [CLocalPattern (!@loc, p, ty)]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 011565d86a..a43f1127a9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -511,11 +511,11 @@ GEXTEND Gram
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> me
-      | me1 = module_expr; me2 = module_expr_atom -> CMapply (!@loc,me1,me2)
+      | me1 = module_expr; me2 = module_expr_atom -> Loc.tag ~loc:!@loc @@ CMapply (me1,me2)
       ] ]
   ;
   module_expr_atom:
-    [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ]
+    [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
@@ -525,11 +525,12 @@ GEXTEND Gram
       ] ]
   ;
   module_type:
-    [ [ qid = qualid -> CMident qid
+    [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid)
       | "("; mt = module_type; ")" -> mt
-      | mty = module_type; me = module_expr_atom -> CMapply (!@loc,mty,me)
+      | mty = module_type; me = module_expr_atom ->
+          Loc.tag ~loc:!@loc @@ CMapply (mty,me)
       | mty = module_type; "with"; decl = with_declaration ->
-          CMwith (!@loc,mty,decl)
+          Loc.tag ~loc:!@loc @@ CMwith (mty,decl)
       ] ]
   ;
   (* Proof using *)