When printing a notation with "match", more flexibility in matching equations.

We reason up to order, and accept to match a final catch-all clauses
with any other clause.

This allows for instance to parse and print a notation of the form
"if t is S n then p else q".

5 files changed, 43 insertions, 16 deletions

diff --git a/clib/cList.ml b/clib/cList.ml
index 836b9d6858..627a3e3e00 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -62,7 +62,7 @@ sig
   val fold_right_and_left :
       ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
   val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
-  val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
+  val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
   val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
   val except : 'a eq -> 'a -> 'a list -> 'a list
   val remove : 'a eq -> 'a -> 'a list -> 'a list
@@ -477,14 +477,12 @@ let fold_right_and_left f l hd =
 let rec fold_left2_set e f x l1 l2 =
   match l1 with
   | a1::l1 ->
-     let rec find = function
+     let rec find seen = function
        | [] -> raise e
        | a2::l2 ->
-          try f x a1 a2, l2
-          with e' when e' = e ->
-            let x, l2' = find l2 in x, a2::l2' in
-     let x, l2' = find l2 in
-     fold_left2_set e f x l1 l2'
+          try fold_left2_set e f (f x a1 a2 l1 l2) l1 (List.rev_append seen l2)
+          with e' when e' = e -> find (a2::seen) l2 in
+     find [] l2
   | [] ->
      if l2 = [] then x else raise e
 
diff --git a/clib/cList.mli b/clib/cList.mli
index cb062d5c8f..b3ee28548c 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -127,7 +127,7 @@ sig
       exception otherwise; sets should have the same size; raise the
       given exception if no pairing of the two sets is found;;
       complexity in O(n^2) *)
-  val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
+  val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
 
   val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
   val except : 'a eq -> 'a -> 'a list -> 'a list
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 81cdecf03d..44073c3b5e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -975,14 +975,15 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
-let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 =
+let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 =
   match DAst.get pat1, DAst.get pat2 with
   | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas ->
       bind_binding_env alp sigma id2 [pat1]
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
+  | _, PatVar Anonymous when allow_catchall -> acc
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
-      List.fold_left2 (match_cases_pattern_binders metas)
+      List.fold_left2 (match_cases_pattern_binders false metas)
         (match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
@@ -1129,9 +1130,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
      match_binders u alp metas na1 na2
        (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
   | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
-      when sty1 == sty2
-	 && Int.equal (List.length tml1) (List.length tml2)
-	 && Int.equal (List.length eqnl1) (List.length eqnl2) ->
+      when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) ->
       let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in
       let sigma =
@@ -1141,7 +1140,14 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let sigma = List.fold_left2
       (fun s (tm1,_) (tm2,_) ->
         match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
-      List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2
+      (* Try two different strategies for matching clauses *)
+      (try
+        List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2
+      with
+        No_match ->
+        List.fold_left2_set No_match (match_disjunctive_equations u alp metas) sigma
+           (Detyping.factorize_eqns eqnl1)
+           (List.map (fun (patl,rhs) -> ([patl],rhs)) eqnl2))
   | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
       when Int.equal (List.length nal1) (List.length nal2) ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
@@ -1241,14 +1247,25 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
      let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
      match_in u alp metas sigma b1 b2
 
-and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
+and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 rest2 =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
+  let allow_catchall = (rest2 = [] && ids = []) in
   let (alp,sigma) =
-    List.fold_left2 (match_cases_pattern_binders metas)
+    List.fold_left2 (match_cases_pattern_binders allow_catchall metas)
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
+and match_disjunctive_equations u alp metas sigma (_,(ids,disjpatl1,rhs1)) (disjpatl2,rhs2) _ _ =
+  (* patl1 and patl2 have the same length because they respectively
+     correspond to some tml1 and tml2 that have the same length *)
+  let (alp,sigma) =
+    List.fold_left2_set No_match
+      (fun alp_sigma patl1 patl2 _ _ ->
+        List.fold_left2 (match_cases_pattern_binders false metas) alp_sigma patl1 patl2)
+      (alp,sigma) disjpatl1 disjpatl2 in
+  match_in u alp metas sigma rhs1 rhs2
+
 let match_notation_constr u c (metas,pat) =
   let terms,termlists,binders,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index fa4ff3be64..6d195b5122 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -217,3 +217,7 @@ exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
      : Prop
 ∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
      : Prop
+fun p : nat => if p is S n then n else 0
+     : nat -> nat
+fun p : comparison => if p is Lt then 1 else 0
+     : comparison -> nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9f6302f6f2..b4ad4a7b3c 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -383,3 +383,11 @@ Check fun '(((x,y),true)|((x,y),false)) => x+y.
 Check myexists (((x,y),true)|((x,y),false)), x>y.
 Check exists '(((x,y),true)|((x,y),false)), x>y.
 Check ∀ '(((x,y),true)|((x,y),false)), x>y.
+
+(* Check Georges' printability of a "if is then else" notation *)
+
+Notation "'if' c 'is' p 'then' u 'else' v" :=
+  (match c with p => u | _ => v end)
+  (at level 200, p pattern at level 100).
+Check fun p => if p is S n then n else 0.
+Check fun p => if p is Lt then 1 else 0.