From 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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 0ef7c3d8ba..836b9d6858 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 f87db04cf4..cb062d5c8f 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


From 5806b0476a1ac9b903503641cc3e2997d3e8d960 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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 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
-- 
cgit v1.2.3