errorLogMonadScript.sml

1Theory errorLogMonad
2Ancestors
3  errorMonad
4
5Type M = “:('a,'e) error # 'w list”
6  (* e for error, w for log or warning messages *)
7
8Overload emret = “errorMonad$return”
9
10Theorem M_CASES:
11  !M. (?v ms. M = (emret v, ms)) \/ (?e ms. M = (error e, ms))
12Proof
13  metis_tac[TypeBase.nchotomy_of “:('a,'e)error”, pairTheory.pair_CASES]
14QED
15
16Definition return_def:
17  return (v:'a) : ('a,'e,'w)M = (emret v, [])
18End
19
20Definition log_def:
21  log (m : 'l) : (unit,'e,'l)M = (emret (), [m])
22End
23
24Definition error_def:
25  error (e : 'e) : ('a,'e,'l) M = (errorMonad$error e, [])
26End
27
28Definition bind_def:
29  bind (M:('a,'e,'l)M) (f:'a -> ('b,'e,'l)M) =
30  case M of
31  | (emret u, ms1) => (I ## APPEND ms1) (f u)
32  | (error e, ms1) => (error e, ms1)
33End
34
35Theorem bind_IDL[simp]:
36  bind (return (v:'a)) f : ('b,'e,'m) M = f v
37Proof
38  Cases_on ‘f v’ using M_CASES >>
39  simp[bind_def, return_def]
40QED
41
42Theorem bind_IDR[simp]:
43  bind (M:('a,'e,'l)M) return = M
44Proof
45  Cases_on ‘M’ using M_CASES >> simp[bind_def, return_def]
46QED
47
48Theorem bind_EQ_success:
49  bind M f = (emret v, ms) <=> ?u ms0 ms1. M = (emret u, ms0) /\
50                                           f u = (emret v, ms1) /\
51                                           ms = ms0 ++ ms1
52Proof
53  Cases_on ‘M’ using M_CASES >> simp[bind_def, AllCaseEqs()] >>
54  rename [‘(I ## _) (f v)’] >> Cases_on ‘f v’ using M_CASES >>
55  simp[EQ_SYM_EQ]
56QED
57
58Definition silently_def:
59  silently M = (I ## K []) M
60End
61
62Definition choice_def:
63  choice M1 M2 =
64  case M1 of
65  | (emret v, ms1) => (emret v, ms1)
66  | (error e, ms1) => (I ## APPEND ms1) M2
67End
68
69Theorem choice_return[simp]:
70  choice (return v) M = return v
71Proof
72  simp[choice_def, return_def]
73QED
74
75val _ = monadsyntax.declare_monad ("errorLog", {
76  unit = “errorLogMonad$return”,
77  bind = “errorLogMonad$bind”,
78  choice = SOME “errorLogMonad$choice”,
79  guard = NONE,
80  fail = SOME “errorLogMonad$error”,
81  ignorebind = NONE
82  });
83