blob: e0b493feec38c0870afca4ab4956ce352e344f5e (
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
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`
|
