1 files changed, 55 insertions, 0 deletions
diff --git a/src/elf_model/missing_pervasives.lem b/src/elf_model/missing_pervasives.lem
new file mode 100644
index 00000000..308c43c3
--- /dev/null
+++ b/src/elf_model/missing_pervasives.lem
@@ -0,0 +1,55 @@
+open import Basic_classes
+open import Bool
+open import List
+open import Maybe
+open import Num
+open import String
+
+(** [intercalate sep xs] places [sep] between all elements of [xs]. *)
+val intercalate : forall 'a. 'a -> list 'a -> list 'a
+let rec intercalate sep xs =
+	match xs with
+		| []    -> []
+		| [x]   -> [x]
+		| x::xs -> x::sep::intercalate sep xs
+	end
+
+(** [unlines xs] concatenates a list of strings [xs], placing each entry
+  * on a new line.
+  *)
+val unlines : list string -> string
+let unlines xs =
+  foldr (^) "" (intercalate "\n" xs)
+
+(** [bracket xs] concatenates a list of strings [xs], separating each entry with a
+  * space, and bracketing the resulting string.
+  *)
+val bracket : list string -> string
+let bracket xs =
+  "(" ^ foldr (^) "" (intercalate " " xs) ^ ")"
+
+(** [null_char] is the null character. *)
+val null_char : char
+
+declare ocaml target_rep function null_char = `'\000'`
+
+(** [split_string_on_char s c] splits a string [s] into a list of substrings
+  * on character [c], otherwise returning the singleton list containing [s]
+  * if [c] is not found in [s].
+  *)
+val split_string_on_char : string -> char -> list string
+declare ocaml target_rep function split_string_on_char = `Ml_bindings.split_string_on_char`
+
+(** [print s] prints [s] to stdout. *)
+val print : string -> unit
+declare ocaml target_rep function print = `print_endline`
+
+(** [string_of_nat m] produces a string representation of natural number [m]. *)
+val string_of_nat : nat -> string
+declare ocaml target_rep function string_of_nat = `string_of_int`
+
+(** [string_suffix i s] chops [i] characters off [s], returning a new string.
+  * 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