1(* A general theory of functional-big-step equivalence with small-step for 2 * deterministic languages *) 3 4open HolKernel boolLib bossLib lcsymtacs Parse; 5open integerTheory stringTheory alistTheory listTheory pred_setTheory relationTheory; 6open pairTheory optionTheory finite_mapTheory arithmeticTheory; 7open simple_traceTheory; 8 9val _ = set_trace "Goalstack.print_goal_at_top" 0; 10val _ = ParseExtras.temp_tight_equality(); 11 12val _ = new_theory "determSem"; 13 14(* ----------- Generic small-step --------- *) 15 16val _ = Datatype ` 17 result = 18 Terminate 'a 19 | Diverge 20 | Crash`; 21 22(* A deterministic small-step semantics has 23 * - a type of states, 'st, 24 * - a step function (to an option for representing stuckness), 25 * - a predicate on states to distinguish stuck ones from good results 26 * - load and unload functions that convert from programs to states, and from 27 * states to results 28 * *) 29 30val _ = Datatype ` 31 small = <| step : 'st -> 'st option; 32 is_value : 'st -> bool; 33 load : 'prog -> 'st; 34 unload : 'st -> 'res |>`; 35 36(* Given a small-step semantics and program, get the result *) 37val small_sem_def = Define ` 38 small_sem sem prog = 39 let step_rel = (\s1 s2. sem.step s1 = SOME s2)^* in 40 let init_state = sem.load prog in 41 case some s'. step_rel init_state s' ��� sem.step s' = NONE of 42 NONE => Diverge 43 | SOME s' => 44 if sem.is_value s' then 45 Terminate (sem.unload s') 46 else 47 Crash`; 48 49(* ----------- Generic functional big-step --------- *) 50 51val _ = Datatype ` 52 fbs_res = 53 Timeout 54 | Error 55 | Val 'a`; 56 57(* A functional big-step semantics has 58 * - a type of states, 'st, and environments 'env, and inital values for them 59 * - a evaluation function 60 * - an unload mapping from the evaluator's result to the actual result 61 * - functions to get and set the clock from the state 62 *) 63val _ = Datatype ` 64 fbs = <| eval : 'st -> 'env -> 'prog -> 'st # 'v fbs_res; 65 init_st : 'st; 66 init_env : 'env; 67 set_clock : num -> 'st -> 'st; 68 get_clock : 'st -> num; 69 unload : 'v -> 'a |>`; 70 71val eval_with_clock_def = Define ` 72 eval_with_clock sem c p = 73 sem.eval (sem.set_clock c sem.init_st) sem.init_env p`; 74 75val fbs_sem_def = Define ` 76 fbs_sem sem prog = 77 case some c. SND (eval_with_clock sem c prog) ��� Timeout of 78 NONE => Diverge 79 | SOME c => 80 case SND (eval_with_clock sem c prog) of 81 Val r => Terminate (sem.unload r) 82 | Error => Crash`; 83 84(* 2 theorems showing when a small-step and functional big-step are equivalent *) 85 86val check_result_def = Define ` 87 (check_result unload_f (Val x) r ��� unload_f x = r) ��� 88 (check_result unload_f _ r ��� T)`; 89 90local val rw = srw_tac[] val fs = fsrw_tac[] in 91val small_fbs_equiv = Q.store_thm ("small_fbs_equiv", 92`!sem_f sem_s. 93 (?f. 94 unbounded f ��� 95 !c p. 96 SND (eval_with_clock sem_f c p) = Timeout ��� 97 ?tr. f c ��� LENGTH tr ��� tr ��� [] ��� HD tr = sem_s.load p ��� check_trace sem_s.step tr) ��� 98 (!c p r. 99 SND (eval_with_clock sem_f c p) = r ��� r ��� Timeout ��� 100 ?r'. (��s1 s2. sem_s.step s1 = SOME s2)^* (sem_s.load p) r' ��� 101 sem_s.step r' = NONE ��� 102 (r = Error ��� ~sem_s.is_value r') ��� 103 check_result sem_f.unload r (sem_s.unload r')) 104 ��� 105 !prog. 106 fbs_sem sem_f prog = small_sem sem_s prog`, 107 rw [small_sem_def, fbs_sem_def] >> 108 `!s s'. 109 (step_rel init_state s ��� sem_s.step s = NONE) ��� 110 (step_rel init_state s' ��� sem_s.step s' = NONE) 111 ��� 112 s = s'` 113 by metis_tac [step_rel_determ] >> 114 every_case_tac >> 115 fs [some_no_choice] >> 116 rfs [some_exists_determ] 117 >- ( (* big diverge, small value *) 118 unabbrev_all_tac >> 119 fs [check_trace_thm] >> 120 rw [] >> 121 `?c'. LENGTH tr < f c'` by metis_tac [unbounded_def] >> 122 last_x_assum (qspecl_then [`c'`, `prog`] mp_tac) >> 123 rw [] >> 124 CCONTR_TAC >> 125 fs [] >> 126 `LENGTH tr < LENGTH tr'` by decide_tac >> 127 metis_tac [trace_extends, NOT_SOME_NONE]) 128 >- ( (* big_diverge, small crash *) 129 unabbrev_all_tac >> 130 fs [check_trace_thm] >> 131 rw [] >> 132 `?c'. LENGTH tr < f c'` by metis_tac [unbounded_def] >> 133 last_x_assum (qspecl_then [`c'`, `prog`] mp_tac) >> 134 rw [] >> 135 CCONTR_TAC >> 136 fs [] >> 137 `LENGTH tr < LENGTH tr'` by decide_tac >> 138 metis_tac [trace_extends, NOT_SOME_NONE]) 139 >- ( 140 fs [some_def] >> 141 metis_tac []) 142 >- ( 143 fs [some_def] >> 144 metis_tac []) 145 >- ( 146 fs [some_def] >> 147 metis_tac []) 148 >- ( 149 fs [some_def] >> 150 metis_tac []) 151 >- ( 152 fs [some_def] >> 153 metis_tac []) 154 >- ( 155 fs [some_def] >> 156 metis_tac []) 157 >- ( (* big term, small diverge *) 158 first_x_assum (qspecl_then [`x`, `prog`] mp_tac) >> 159 rw [check_result_def] >> 160 CCONTR_TAC >> 161 fs [] >> 162 metis_tac []) 163 >- ( (* big term, small value *) 164 first_x_assum (qspecl_then [`x`, `prog`] mp_tac) >> 165 rw [check_result_def] >> 166 metis_tac [])); 167end 168 169val same_result_def = Define ` 170 (same_result sem_f sem_s (Val a) s ��� 171 sem_f.unload a = sem_s.unload s ��� 172 sem_s.is_value s ��� 173 sem_s.step s = NONE) ��� 174 (same_result sem_f sem_s Error s ��� 175 ��sem_s.is_value s ��� 176 sem_s.step s = NONE) ��� 177 (same_result sem_f sem_s Timeout s ��� 178 ?s'. sem_s.step s = SOME s')`; 179 180val small_fbs_equiv2 = Q.store_thm ("small_fbs_equiv2", 181`!sem_f sem_s. 182 (!c p. 183 SND (eval_with_clock sem_f c p) = Timeout ��� 184 sem_f.get_clock (FST (eval_with_clock sem_f c p)) = 0) ��� 185 (?f. 186 unbounded f ��� 187 !c p st r. 188 eval_with_clock sem_f c p = r ��� 189 ?tr. f (c - sem_f.get_clock (FST r)) ��� LENGTH tr ��� tr ��� [] ��� HD tr = sem_s.load p ��� check_trace sem_s.step tr ��� 190 same_result sem_f sem_s (SND r) (LAST tr)) 191 ��� 192 !prog. 193 fbs_sem sem_f prog = small_sem sem_s prog`, 194 rpt gen_tac >> 195 DISCH_TAC >> 196 match_mp_tac small_fbs_equiv >> 197 rw [] 198 >- ( 199 qexists_tac `f` >> 200 rw [] >> 201 first_x_assum (qspecl_then [`c`, `p`] mp_tac) >> 202 rw [] >> 203 metis_tac []) 204 >- ( 205 rw [check_trace_thm] >> 206 first_x_assum (qspecl_then [`c`, `p`] mp_tac) >> 207 rw [] >> 208 qexists_tac `LAST tr` >> 209 rw [] 210 >- metis_tac [] >> 211 Cases_on `SND (eval_with_clock sem_f c p)` >> 212 fs [same_result_def, check_result_def])); 213 214val _ = export_theory (); 215