From 5806b0476a1ac9b903503641cc3e2997d3e8d960 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 24 Aug 2017 15:18:23 +0200
Subject: 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".
---
 clib/cList.ml  | 12 +++++-------
 clib/cList.mli |  2 +-
 2 files changed, 6 insertions(+), 8 deletions(-)

(limited to 'clib')

diff --git a/clib/cList.ml b/clib/cList.ml
index 836b9d685..627a3e3e0 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 cb062d5c8..b3ee28548 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
-- 
cgit v1.2.3