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