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