diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 14 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
2 files changed, 14 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml index 04086e20f3..a9d9655eda 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -363,7 +363,19 @@ let list_prefix_of prefl l = | ([], _) -> true | (_, _) -> false in - prefrec (prefl,l) + prefrec (prefl,l) + +let list_drop_prefix p l = +(* if l=p++t then return t else l *) + let rec list_drop_prefix_rec = function + | ([], tl) -> Some tl + | (_, []) -> None + | (h1::tp, h2::tl) -> + if h1 = h2 then list_drop_prefix_rec (tp,tl) else None + in + match list_drop_prefix_rec (p,l) with + | Some r -> r + | None -> l let list_map_append f l = List.flatten (List.map f l) diff --git a/lib/util.mli b/lib/util.mli index ababb2ff9a..e93094f898 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -123,6 +123,7 @@ val list_last : 'a list -> 'a val list_lastn : int -> 'a list -> 'a list val list_skipn : int -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool +val list_drop_prefix : 'a list -> 'a list -> 'a list (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) val list_map_append : ('a -> 'b list) -> 'a list -> 'b list (* raises [Invalid_argument] if the two lists don't have the same length *) |