In printing notations with "match", reasoning up to the order of clauses.

5 files changed, 34 insertions, 1 deletions

diff --git a/clib/cList.ml b/clib/cList.ml
index 0ef7c3d8b..836b9d685 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -62,6 +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 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
@@ -472,6 +473,21 @@ let fold_right_and_left f l hd =
     | a::l -> let hd = aux (a::tl) l in f hd a tl
    in aux [] l
 
+(* Match sets as lists according to a matching function, also folding a side effect *)
+let rec fold_left2_set e f x l1 l2 =
+  match l1 with
+  | a1::l1 ->
+     let rec find = 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'
+  | [] ->
+     if l2 = [] then x else raise e
+
 let iteri f l = fold_left_i (fun i _ x -> f i x) 0 () l
 
 let for_all_i p =
diff --git a/clib/cList.mli b/clib/cList.mli
index f87db04cf..cb062d5c8 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -121,6 +121,14 @@ 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
+
+  (** Fold sets, i.e. lists up to order; the folding function tells
+      when elements match by returning a value and raising the given
+      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 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
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 602271bf6..e68e8dd97 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1163,7 +1163,7 @@ 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 (match_equations u alp metas) sigma eqnl1 eqnl2
+      List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 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
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 58dabe51e..9c711ff26 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -191,3 +191,5 @@ pair
      : prod
          (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat))
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
+fun x : nat => if x is n .+ 1 then n else 1
+     : nat -> nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index fd5846e71..d81cc702a 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -326,3 +326,10 @@ Check {{RLRR 1 , 2}}.
 Unset Printing Notations.
 Check {{RLRR 1 , 2}}.
 Set Printing Notations.
+
+(* Check insensitivity of "match" clauses to order *)
+
+Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
+  (match t with S n => p | 0 => q end)
+  (at level 200).
+Check fun x => if x is n.+1 then n else 1.