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

1 files changed, 14 insertions, 27 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a592b4cff..3ba5d985f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -59,31 +59,31 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
 
 let eq_located f (_, x) (_, y) = f x y
 
-let rec cases_pattern_expr_eq p1 p2 =
+let rec cases_pattern_expr_eq (l1, p1) (l2, p2) =
   if p1 == p2 then true
   else match p1, p2 with
-  | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) ->
+  | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
       Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
-  | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
+  | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
       eq_reference c1 c2 &&
       Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
       List.equal cases_pattern_expr_eq b1 b2
-  | CPatAtom(_,r1), CPatAtom(_,r2) ->
+  | CPatAtom(r1), CPatAtom(r2) ->
       Option.equal eq_reference r1 r2
-  | CPatOr (_, a1), CPatOr (_, a2) ->
+  | CPatOr a1, CPatOr a2 ->
       List.equal cases_pattern_expr_eq a1 a2
-  | CPatNotation (_, n1, s1, l1), CPatNotation (_, n2, s2, l2) ->
+  | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
     String.equal n1 n2 &&
     cases_pattern_notation_substitution_eq s1 s2 &&
     List.equal cases_pattern_expr_eq l1 l2
-  | CPatPrim(_,i1), CPatPrim(_,i2) ->
+  | CPatPrim i1, CPatPrim i2 ->
       prim_token_eq i1 i2
-  | CPatRecord (_, l1), CPatRecord (_, l2) ->
+  | CPatRecord l1, CPatRecord l2 ->
       let equal (r1, e1) (r2, e2) =
         eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
       in
       List.equal equal l1 l2
-  | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) ->
+  | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) ->
       String.equal s1 s2 && cases_pattern_expr_eq e1 e2
   | _ -> false
 
@@ -183,7 +183,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   Option.equal (eq_located Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
 
-and branch_expr_eq (_, p1, e1) (_, p2, e2) =
+and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
   List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 &&
   constr_expr_eq e1 e2
 
@@ -252,22 +252,9 @@ let constr_loc = function
   | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
 
-let cases_pattern_expr_loc = function
-  | CPatAlias (loc,_,_) -> loc
-  | CPatCstr (loc,_,_,_) -> loc
-  | CPatAtom (loc,_) -> loc
-  | CPatOr (loc,_) -> loc
-  | CPatNotation (loc,_,_,_) -> loc
-  | CPatRecord (loc, _) -> loc
-  | CPatPrim (loc,_) -> loc
-  | CPatDelimiters (loc,_,_) -> loc
-  | CPatCast(loc,_,_) -> loc
-
-let raw_cases_pattern_expr_loc = function
-  | RCPatAlias (loc,_,_) -> loc
-  | RCPatCstr (loc,_,_,_) -> loc
-  | RCPatAtom (loc,_) -> loc
-  | RCPatOr (loc,_) -> loc
+let cases_pattern_expr_loc (l,_) = l
+
+let raw_cases_pattern_expr_loc (l, _) = l
 
 let local_binder_loc = function
   | CLocalAssum ((loc,_)::_,_,t)
@@ -330,7 +317,7 @@ let expand_binders mkC loc bl c =
             let c =
               CCases
                 (loc, LetPatternStyle, None, [(e,None,None)],
-                 [(loc1, [(loc1,[p])], c)])
+                 [(loc1, ([(loc1,[p])], c))])
             in
             (ni :: env, mkC loc ([id],Default Explicit,ty) c)
   in