From 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 15 Aug 2017 14:55:44 +0200
Subject: In printing notations with "match", reasoning up to the order of
 clauses.

---
 clib/cList.ml  | 16 ++++++++++++++++
 clib/cList.mli |  8 ++++++++
 2 files changed, 24 insertions(+)

(limited to 'clib')

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
-- 
cgit v1.2.3