diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-15 14:55:44 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:05 +0100 |
commit | 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 (patch) | |
tree | 7dc6f685aa30f0b5bb3da704f1d96c7060eb19e5 /clib | |
parent | 00bfd6fa443232bc908cfa13553e2fa1cf783ffa (diff) |
In printing notations with "match", reasoning up to the order of clauses.
Diffstat (limited to 'clib')
-rw-r--r-- | clib/cList.ml | 16 | ||||
-rw-r--r-- | clib/cList.mli | 8 |
2 files changed, 24 insertions, 0 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 |