diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-24 15:18:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:06 +0100 |
| commit | 5806b0476a1ac9b903503641cc3e2997d3e8d960 (patch) | |
| tree | fc77bdb02dec76f18af12c045620eca52f8b03e6 /clib | |
| parent | e4d93d1cef27d3a8c1e36139fc1e118730406f67 (diff) | |
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".
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cList.ml | 12 | ||||
| -rw-r--r-- | clib/cList.mli | 2 |
2 files changed, 6 insertions, 8 deletions
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 |