blob: 308c43c317f46332af2b4d03e6e7af56498fc1be (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
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`
|
