blob: ca34a5d4e6f4fcd47038f565baf51a137883caf9 (
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
77
78
79
80
81
82
83
84
85
86
|
open import List
open import Num
open import String
open import Show
(** [error] is a type used to represent potentially failing computations. [Success]
* marks a successful completion of a computation, whilst [Fail err] marks a failure,
* with [err] as the reason.
*)
type error 'a
= Success of 'a
| Fail of string
(** [return] is the monadic lifting function for [error], representing a successful
* computation.
*)
val return : forall 'a. 'a -> error 'a
let return r = Success r
(** [fail err] represents a failing computation, with error message [err].
*)
val fail : forall 'a. string -> error 'a
let fail err = Fail err
(** [(>>=)] is the monadic binding function for [error].
*)
val (>>=) : forall 'a 'b. error 'a -> ('a -> error 'b) -> error 'b
let (>>=) x f =
match x with
| Success s -> f s
| Fail err -> Fail err
end
(** [repeatM count action] fails if [action] is a failing computation, or
* successfully produces a list [count] elements long, where each element is
* the value successfully returned by [action].
*)
val repeatM : forall 'a. nat -> error 'a -> error (list 'a)
let rec repeatM count action =
match count with
| 0 -> return []
| m ->
action >>= fun head ->
repeatM (m - 1) action >>= fun tail ->
return (head::tail)
end
(** [repeatM' count seed action] is a variant of [repeatM] that acts like [repeatM]
* apart from any successful result returns a tuple whose second component is [seed]
* and whose first component is the same as would be returned by [repeatM].
*)
val repeatM' : forall 'a 'b. nat -> 'b -> ('b -> error ('a * 'b)) -> error ((list 'a) * 'b)
let rec repeatM' count seed action =
match count with
| 0 -> return ([], seed)
| m ->
action seed >>= fun (head, seed) ->
repeatM' (m - 1) seed action >>= fun (tail, seed) ->
return (head::tail, seed)
end
(** [mapM f xs] maps [f] across [xs], failing if [f] fails on any element of [xs].
*)
val mapM : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b)
let rec mapM f xs =
match xs with
| [] -> return []
| x::xs ->
f x >>= fun hd ->
mapM f xs >>= fun tl ->
return (hd::tl)
end
(** [string_of_error err] produces a string representation of [err].
*)
val string_of_error : forall 'a. Show 'a => error 'a -> string
let string_of_error e =
match e with
| Fail err -> "Fail: " ^ err
| Success s -> show s
end
instance forall 'a. Show 'a => (Show (error 'a))
let show = string_of_error
end
|
