blob: 201a10106e4573106eeedd89b88c81c72366e2e3 (
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
|
From compcert Require Export Errors.
From vericert Require Import Monad.
From Coq Require Import Lists.List.
Module ErrorMonad <: Monad.
Definition mon := res.
Definition ret {A: Type} (x: A) := OK x.
Definition default {T : Type} (x : T) (u : res T) : T :=
match u with
| OK y => y
| _ => x
end.
Definition map {S : Type} {T : Type} (f : S -> T) (u : mon S) : mon T :=
match u with
| OK y => OK (f y)
| Error m => Error m
end.
Definition liftA2 {T : Type} (f : T -> T -> T) (a : mon T) (b : mon T) : mon T :=
match a with
| OK x => map (f x) b
| Error m => Error m
end.
Definition bind {A B : Type} (g : A -> mon B) (f : mon A) : mon B :=
match f with
| OK a => g a
| Error m => Error m
end.
Definition bind2 {A B C : Type} (g : A -> B -> mon C) (f : mon (A * B)) : mon C :=
match f with
| OK (a, b) => g a b
| Error m => Error m
end.
Definition join {A : Type} (a : mon (mon A)) : mon A :=
match a with
| Error m => Error m
| OK a' => a'
end.
#[global] Instance error_ret : MRet res := @ret.
#[global] Instance error_bind : MBind res := @bind.
#[global] Instance error_join : MJoin res := @join.
#[global] Instance error_map : FMap res := @map.
End ErrorMonad.
Module ErrorMonadExtra := MonadExtra(ErrorMonad).
|