Merge PR #978: In printing, experimenting factorizing "match" clauses with same right-hand side.

3 files changed, 13 insertions, 11 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8b78a91b5..7cc8de85d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -188,7 +188,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   Option.equal cases_pattern_expr_eq p1 p2
 
 and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
-  List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 &&
+  List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
   constr_expr_eq e1 e2
 
 and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
@@ -260,7 +260,6 @@ let local_binders_loc bll = match bll with
 
 (* Legacy functions *)
 let down_located f (_l, x) = f x
-let located_fold_left f x (_l, y) = f x y
 
 let is_constructor id =
   try Globnames.isConstructRef
@@ -292,8 +291,7 @@ let ids_of_pattern =
 
 let ids_of_pattern_list =
   List.fold_left
-    (located_fold_left
-       (List.fold_left (cases_pattern_fold_names Id.Set.add)))
+    (List.fold_left (cases_pattern_fold_names Id.Set.add))
     Id.Set.empty
 
 let ids_of_cases_indtype p =
@@ -571,7 +569,7 @@ let expand_binders ?loc mkC bl c =
         let c = CAst.make ?loc @@
           CCases
             (LetPatternStyle, None, [(e,None,None)],
-             [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))])
+             [(Loc.tag ?loc:loc1 ([[p]], c))])
         in
         (ni :: env, mkC ?loc ([id],Default Explicit,ty) c)
   in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bc8debd02..1330b3741 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -852,7 +852,7 @@ let rec extern inctx scopes vars r =
                              ) x))
                 tml
     in
-    let eqns = List.map (extern_eqn inctx scopes vars) eqns in
+    let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in
     CCases (sty,rtntypopt',tml,eqns)
 
   | GLetTuple (nal,(na,typopt),tm,b) ->
@@ -966,9 +966,9 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) = extern_local_binder scopes vars l in
       (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
 
-and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
-  Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
-   extern inctx scopes vars c)
+and extern_eqn inctx scopes vars (loc,(ids,pll,c)) =
+  let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
+  Loc.tag ?loc (pll,extern inctx scopes vars c)
 
 and extern_notation (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 977146b2f..74ae32120 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -958,8 +958,11 @@ let rec has_duplicate = function
   | [] -> None
   | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l
 
+let loc_of_multiple_pattern pl =
+ Loc.merge_opt (cases_pattern_expr_loc (List.hd pl)) (cases_pattern_expr_loc (List.last pl))
+
 let loc_of_lhs lhs =
- Loc.merge_opt (fst (List.hd lhs)) (fst (List.last lhs))
+ Loc.merge_opt (loc_of_multiple_pattern (List.hd lhs)) (loc_of_multiple_pattern (List.last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -1873,8 +1876,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     intern_local_binder_aux intern ntnvars env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
-  and intern_multiple_pattern env n (loc,pl) =
+  and intern_multiple_pattern env n pl =
     let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in
+    let loc = loc_of_multiple_pattern pl in
     check_number_of_pattern loc n pl;
     product_of_cases_patterns empty_alias idsl_pll