1open HolKernel Parse boolLib bossLib lcsymtacs;
2open forTheory state_transformerTheory
3
4val _ = new_theory "for_monadic";
5val _ = temp_tight_equality ();
6
7(*
8This file casts the semantics for the FOR language from forTheory using a monad
9instead of explicit case expressions.
10*)
11
12(* the r-state monad *)
13
14val mbind_def = Define`
15  mbind f g s =
16    case f s of
17    | (Rval x,s) => g x s
18    | r => r`;
19
20val mibind_def = Define`
21  mibind f g = mbind f (��x. g)`;
22
23val mfail_def = Define`
24  mfail = return Rfail`;
25
26val _ =
27    monadsyntax.declare_monad ("for_state", {
28      bind = ���mbind���, ignorebind = SOME ���mibind���,
29      unit = ���state_transformer$UNIT���,
30      guard = NONE, fail = NONE, choice = NONE
31    })
32val _ = monadsyntax.enable_monad "for_state"
33
34val mbreak_def = Define`
35  mbreak = return Rbreak`;
36
37val mtimeout_def = Define`
38  mtimeout = return Rtimeout`;
39
40val mreturn_def = Define`
41  mreturn = return o Rval`;
42
43val mtry_def = Define`
44  mtry m h k s =
45  case m s of
46  | (Rbreak, s) => h s
47  | _ => mibind m k s`;
48
49val lookup_store_def = Define`
50  lookup_store x s =
51    case FLOOKUP s.store x of
52    | NONE => mfail s
53    | SOME n => mreturn n s`;
54
55val get_clock_def = Define`
56  get_clock s = (s.clock,s)`;
57
58val update_state_def = Define`
59  update_state f s = ((),f s)`;
60
61(* Expression evaluation *)
62
63val _ = overload_on("mon_sem_e",``combin$C sem_e``);
64
65val mon_sem_e_var = Q.prove(
66  `���x. mon_sem_e (Var x) = lookup_store x`,
67  rw[FUN_EQ_THM] >> EVAL_TAC >>
68  BasicProvers.EVERY_CASE_TAC);
69
70val mon_sem_e_num = Q.prove(
71  `���num. mon_sem_e (Num num) = mreturn num`,
72  EVAL_TAC >> rw[]);
73
74val mon_sem_e_add = Q.prove(
75  `���e1 e2.
76   mon_sem_e (Add e1 e2) =
77   do
78     n1 <- mon_sem_e e1;
79     n2 <- mon_sem_e e2;
80     mreturn (n1+n2)
81   od`,
82  rw[FUN_EQ_THM] >>
83  EVAL_TAC >>
84  BasicProvers.EVERY_CASE_TAC);
85
86val mon_sem_e_assign = Q.prove(
87  `���x e.
88   mon_sem_e (Assign x e) =
89   do
90     n <- mon_sem_e e;
91     update_state (store_var x n);
92     mreturn n
93   od`,
94  rw[FUN_EQ_THM] >>
95  EVAL_TAC >>
96  BasicProvers.EVERY_CASE_TAC);
97
98val monadic_sem_e = save_thm("monadic_sem_e",
99  LIST_CONJ[mon_sem_e_var,mon_sem_e_num,mon_sem_e_add,mon_sem_e_assign]);
100
101(* Statement evaluation *)
102
103val _ = overload_on("mon_sem_t",``combin$C sem_t``);
104
105val mon_sem_t_exp = Q.prove(
106  `���e. mon_sem_t (Exp e) = mon_sem_e e`,
107  rw[FUN_EQ_THM] >> EVAL_TAC);
108
109val mon_sem_t_dec = Q.prove(
110  `���x t. mon_sem_t (Dec x t) =
111   do update_state (store_var x 0);
112     mon_sem_t t
113   od`,
114  rw[FUN_EQ_THM] >> EVAL_TAC);
115
116val mon_sem_t_break = Q.prove(
117  `mon_sem_t Break = mbreak`,
118  rw[FUN_EQ_THM] >> EVAL_TAC);
119
120val mon_sem_t_seq = Q.prove(
121  `���t1 t2. mon_sem_t (Seq t1 t2) =
122   do mon_sem_t t1; mon_sem_t t2 od`,
123  rw[FUN_EQ_THM] >> EVAL_TAC >>
124  BasicProvers.EVERY_CASE_TAC);
125
126val mon_sem_t_if = Q.prove(
127  `���e t1 t2. mon_sem_t (If e t1 t2) =
128   do
129     n1 <- mon_sem_e e;
130     mon_sem_t (if n1 = 0 then t2 else t1)
131   od`,
132  rw[FUN_EQ_THM] >> EVAL_TAC >>
133  BasicProvers.EVERY_CASE_TAC);
134
135val dec_clock_then_def = Define`
136  dec_clock_then f =
137  do
138    k <- get_clock;
139    if k = 0 then mtimeout
140    else do update_state dec_clock; f od
141  od`;
142
143val mon_sem_t_for = Q.prove(
144  `���e1 e2 t. mon_sem_t (For e1 e2 t) =
145   do
146     n1 <- mon_sem_e e1;
147     if n1 = 0 then mreturn 0 else
148     mtry (mon_sem_t t) (mreturn 0)
149     do
150       mon_sem_e e2;
151       dec_clock_then (mon_sem_t (For e1 e2 t))
152     od
153   od`,
154  rw[FUN_EQ_THM] >>
155  rw[Once sem_t_def,dec_clock_then_def,mbind_def,mibind_def,mreturn_def,UNIT_DEF] >>
156  BasicProvers.EVERY_CASE_TAC >>
157  fs[mtry_def,mibind_def,mbind_def,BIND_DEF,IGNORE_BIND_DEF,get_clock_def,update_state_def,mtimeout_def,UNIT_DEF]);
158
159val monadic_sem_t = save_thm("monadic_sem_t",
160  LIST_CONJ[mon_sem_t_exp,mon_sem_t_dec,mon_sem_t_seq,mon_sem_t_seq,mon_sem_t_if,mon_sem_t_for]);
161
162val _ = export_theory ();
163