diff options
Diffstat (limited to 'src/elf_model/missing_pervasives.lem')
| -rw-r--r-- | src/elf_model/missing_pervasives.lem | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/elf_model/missing_pervasives.lem b/src/elf_model/missing_pervasives.lem index 308c43c3..e0b493fe 100644 --- a/src/elf_model/missing_pervasives.lem +++ b/src/elf_model/missing_pervasives.lem @@ -14,6 +14,27 @@ let rec intercalate sep xs = | x::xs -> x::sep::intercalate sep xs end +(** [mapMaybei f xs] maps a function expecting an index (the position in the list + * [xs] that it is currently viewing) and producing a [maybe] type across a list. + * Elements that produce [Nothing] under [f] are discarded in the output, whilst + * those producing [Just e] for some [e] are kept. + *) +val mapMaybei' : forall 'a 'b. (nat -> 'a -> maybe 'b) -> nat -> list 'a -> list 'b +let rec mapMaybei' f idx xs = + match xs with + | [] -> [] + | x::xs -> + match f idx x with + | Nothing -> mapMaybei' f (1 + idx) xs + | Just e -> e :: mapMaybei' f (1 + idx) xs + end + end + +val mapMaybei : forall 'a 'b. (nat -> 'a -> maybe 'b) -> list 'a -> list 'b + +let mapMaybei f xs = + mapMaybei' f 0 xs + (** [unlines xs] concatenates a list of strings [xs], placing each entry * on a new line. *) @@ -52,4 +73,4 @@ declare ocaml target_rep function string_of_nat = `string_of_int` * Fails if the index is negative, or beyond the end of the string. *) val string_suffix : nat -> string -> maybe string -declare ocaml target_rep function string_suffix = `Ml_bindings.string_suffix`
\ No newline at end of file +declare ocaml target_rep function string_suffix = `Ml_bindings.string_suffix` |