From c1cab3ba606f7034f2785f06c0d3892bca3976cf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Aug 2017 11:36:05 +0200
Subject: Removing cumbersome location in multiple patterns.

This is to have a better symmetry between CCases and GCases.
---
 interp/constrexpr_ops.ml | 8 +++-----
 interp/constrextern.ml   | 2 +-
 interp/constrintern.ml   | 8 ++++++--
 3 files changed, 10 insertions(+), 8 deletions(-)

(limited to 'interp')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8b78a91b5b..7cc8de85d2 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 bc8debd02d..6704ed4b7b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -967,7 +967,7 @@ and extern_local_binder scopes vars = function
       (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],
+  Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
 
 and extern_notation (tmp_scope,scopes as allscopes) vars t = function
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 977146b2fe..74ae321202 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
 
-- 
cgit v1.2.3


From 5c9d569cee804c099c44286777ab084e0370399f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 14:51:08 +0200
Subject: In printing, factorizing "match" clauses with same right-hand side.

Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.

Adding options

  Unset Printing Allow Default Clause.

to deactivate the second behavior, and

  Unset Printing Factorizable Match Patterns.

to deactivate the first behavior (deactivating the first one
deactivates also the second one).

E.g. printing

  match x with Eq => 1 | _ => 0 end

gives

  match x with
  | Eq => 1
  | _ => 0
  end

or (with default clause deactivates):

  match x with
  | Eq => 1
  | Lt | Gt => 0
  end

More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
---
 interp/constrextern.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6704ed4b7b..1330b3741e 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 ([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
-- 
cgit v1.2.3