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

(** [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.
  *)
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`