source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2849

Last change on this file since 2849 was 2849, checked in by piccolo, 7 years ago

partial commit

File size: 19.7 KB
Line 
1include "ERTLptr/ERTLptrToLTL.ma".
2include "ERTLptr/ERTLptr_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6include "common/AssocList.ma".
7
8
9
10(* Inefficient, replace with Trie lookup *)
11definition lookup_stack_cost ≝
12 λp.λid : ident.
13  assoc_list_lookup ? ℕ id (eq_identifier …) p.
14
15(*TO BE MOVED*)
16definition ERTLptr_status ≝
17λprog : ertlptr_program.λstack_sizes.
18joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
19
20definition LTL_status ≝
21λprog : ltl_program.λstack_sizes.
22joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
23
24axiom sigma_stored_pc : ertlptr_program → (block → label → list label) → 
25program_counter → program_counter.
26
27axiom sigma_fb_state: ertlptr_program → (block → label → list label) →
28 (block → label → list register) → list register →
29  state ERTLptr_semantics → state ERTLptr_semantics.
30
31axiom sigma_sb_state: ertlptr_program → (block → label → list label) →
32 (block → label → list register) → list register →
33  state LTL_semantics → state ERTLptr_semantics.
34
35definition dummy_state : state ERTLptr_semantics ≝
36mk_state ERTL_semantics
37   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
38
39definition dummy_state_pc : state_pc ERTLptr_semantics ≝
40mk_state_pc ? dummy_state (null_pc one) (null_pc one).
41
42
43definition sigma_fb_state_pc : ertlptr_program → (block → label → list label) →
44 (block → label → list register) →
45 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
46λprog,f_lbls,f_regs,st.
47let ge ≝ globalenv_noinit … prog in
48let globals ≝ prog_var_names … prog in
49match fetch_internal_function … ge (pc_block (pc … st)) with
50  [ OK y ⇒ ?
51  | Error e ⇒ dummy_state_pc
52  ].
53cases daemon qed.
54
55definition sigma_sb_state_pc : ertlptr_program → (block → label → list label) →
56 (block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
57λprog,f_lbls,f_regs,st.
58let ge ≝ globalenv_noinit … prog in
59let globals ≝ prog_var_names … prog in
60match fetch_internal_function … ge (pc_block (pc … st)) with
61  [ OK y ⇒ ?
62  | Error e ⇒ dummy_state_pc
63  ].
64cases daemon qed.
65
66
67definition ERTLptr_to_LTL_StatusSimulation :
68∀fix_comp : fixpoint_computer.
69∀colour : coloured_graph_computer.
70∀ prog : ertlptr_program.
71∀ f_lbls. ∀ f_regs. ∀f_bl_r.
72b_graph_transform_program_props ERTLptr_semantics LTL_semantics
73     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
74let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
75let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
76let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
77let stacksizes ≝ lookup_stack_cost … m in 
78status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
79λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood.
80    mk_status_rel ??
81    (* sem_rel ≝ *)
82         (λs1:ERTLptr_status ? ?
83          .λs2:LTL_status ? ?
84           .sigma_fb_state_pc prog f_lbls f_regs s1
85            =sigma_sb_state_pc prog f_lbls f_regs s2)
86    (* call_rel ≝ *) 
87       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
88          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
89           .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2))
90    (* sim_final ≝ *) ?.
91cases daemon
92qed.
93
94axiom as_label_ok :
95∀fix_comp,colour.
96∀prog.∀f_lbls,f_regs. ∀f_bl_r.
97∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
98     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
99∀st1,st2,fn,id,stmt.
100let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
101R st1 st2 → 
102fetch_statement ERTLptr_semantics (prog_var_names … prog)
103      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
104as_label ? st2 = as_label ? st1.
105
106
107
108
109(*
110(* Copy the proof too from previous pass *)
111axiom fetch_stmt_ok_sigma_state_ok :
112∀prog : ertlptr_program.
113∀ f_lbls,f_regs,id,fn,stmt,st.
114fetch_statement ERTLptr_semantics (prog_var_names … prog)
115    (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
116               return 〈id,fn,stmt〉 →
117let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
118                                               (f_regs (pc_block (pc … st)))) in
119st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
120sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
121*)
122
123lemma set_no_pc_eta:
124 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
125#P * //
126qed.
127
128lemma pc_of_label_eq :
129  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
130  ∀globals,ge,bl,i_fn,lbl.
131  fetch_internal_function ? ge bl = return i_fn →
132  pc_of_label pars globals ge bl lbl =
133    OK ? (pc_of_point ERTL_semantics bl lbl).
134#p #p' #globals #ge #bl #i_fn #lbl #EQf
135whd in match pc_of_label;
136normalize nodelta >EQf >m_return_bind %
137qed.
138
139lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
140 #T #x #y #EQ destruct %
141qed.
142
143
144axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
145∀prog.∀ f_lbls,f_regs.∀f_bl_r.
146∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
147     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
148∀st1,st2.
149let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
150R st1 st2 →
151pc_block (pc … st1) = pc_block (pc … st2).
152
153axiom pc_eq_sigma_commute : ∀fix_comp,colour.
154∀prog.∀ f_lbls,f_regs.∀f_bl_r.
155∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
156     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
157∀st1,st2.
158let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
159R st1 st2 →
160(pc … st1) = (pc … st2).
161
162
163axiom change_pc_sigma_commute : ∀fix_comp,colour.
164∀prog.∀ f_lbls,f_regs.∀f_bl_r.
165∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
166     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
167∀st1,st2.
168let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
169R st1 st2 →
170∀pc1,pc2.pc1 = pc2 →
171R (set_pc … pc1 st1) (set_pc … pc2 st2).
172(*
173axiom globals_commute : ∀fix_comp,colour.
174∀prog.
175∀p_out,m,n.
176∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
177prog_var_names … prog = prog_var_names … p_out.*)
178
179lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
180〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
181#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
182qed.
183
184include "joint/semantics_blocks.ma".
185include "ASM/Util.ma".
186
187lemma eval_cond_ok :
188∀fix_comp,colour.
189∀prog.
190∀ f_lbls,f_regs.∀f_bl_r.
191∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
192     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
193∀st1,st2,st1',f,fn,a,ltrue,lfalse.
194let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
195R st1 st2 →
196 fetch_statement ERTLptr_semantics …
197  (globalenv_noinit ? prog) (pc … st1) =
198    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
199let stacksizes ≝ lookup_stack_cost …
200                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 
201 eval_state ERTLptr_semantics
202   (prog_var_names … ℕ prog)
203   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
204   st1 = return st1' →
205as_costed (ERTLptr_status prog stacksizes) st1' →
206∃ st2'. R st1' st2' ∧
207∃taf : trace_any_any_free (LTL_status ? ?)
208st2 st2'.
209bool_to_Prop (taaf_non_empty … taf).
210#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
211#ltrue #lfalse #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta
212>EQfetch >m_return_bind
213whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
214whd in match eval_statement_advance; normalize nodelta
215change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
216#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
217#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
218lapply(fetch_statement_inv … EQfetch) * #EQfn #_
219[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
220| whd in match next; normalize nodelta
221]
222whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) -EQ -st1' #n_cost
223cases(b_graph_transform_program_fetch_statement … good … EQfetch)
224#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
225[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
226[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
227whd in match translate_step; normalize nodelta *** #blp #blm #bls *
228whd in ⊢ (% → ?); #EQbl
229whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
230#seq_pre_l
231letin stacksizes ≝ (lookup_stack_cost …
232                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
233letin p≝ (mk_prog_params LTL_semantics
234                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
235                         stacksizes)
236cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
237           pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧
238           last_pop … st2' = last_pop … st2)
239   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
240#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
241>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
242>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
243whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
244>EQ in EQmid ⊢ %; -nxt1 #EQmid
245lapply(taaf_to_taa ???
246           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
247                                       seq_pre_l res_st2_pre_mid) ?)
248[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
249      whd in match (as_label ??); whd in match (as_pc_of ??);
250      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
251      >m_return_bind whd in match point_of_pc; normalize nodelta
252      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
253      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
254#taa_pre_mid whd in ⊢ (% → ?);
255cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
256                     return st2_cond )
257[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
258#st2_mid #EQst2_mid
259cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_mid = cl_jump)
260[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
261* #EQ1 #EQ2 destruct(EQ1 EQ2)
262#seq_post_l   
263lapply(taaf_to_taa ???
264           (produce_trace_any_any_free p st2_cond f t_fn1 ??? st2_pre_mid EQt_fn1
265                                       seq_pre_l res_st2_pre_mid) ?)
266                 
267
268cases(appoggio ????????? EQbl) * #_ #_ #EQ1 >EQ1 -EQ1
269whd in ⊢ (% →  ?); * #EQ2 #EQ3 >EQ3 in seq_pre_l EQcond; -mid2 #se_pre_l #EQcond 
270>EQ2 in EQmid1; #EQmid1 -l2
271%{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2_pre_cond)}
272[ @ltrue |3: @lfalse]
273% [1,3: @(change_pc_sigma_commute … good … Rst1st2) % ]
274%{(taaf_step_jump ? ??? taa_pre_cond ???) I}
275[2,5:  whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
276       >EQt_fn1  >m_return_bind >point_of_pc_of_point >EQcond >m_return_bind
277       cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDENT * #_ #EQ #_ >EQ -EQ % *)
278|3,6: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
279       >EQt_fn1  >m_return_bind >point_of_pc_of_point >EQcond >m_return_bind
280       cases(appoggio ????????? EQbl) * #_ #EQ #_ >EQ -EQ
281       whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
282       whd in match eval_statement_advance; normalize nodelta
283       change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
284       cases
285 -bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2
286*** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
287#nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
288whd in EQmid1 : (??%%); destruct(EQmid1)
289%{(taaf_step_jump … (taa_base …) …) I}
290[2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 
291      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
292      >EQcond %
293|3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc;
294      normalize nodelta whd in match fetch_statement; normalize nodelta
295      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
296      >EQcond >m_return_bind normalize nodelta >m_return_bind
297      whd in match eval_statement_advance; normalize nodelta
298      change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
299      cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1
300      >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool)
301      #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta
302      >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto;
303      normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1
304      >(pc_of_label_eq … EQt_fn1) >m_return_bind %
305|*: lapply n_cost whd in match as_costed; normalize nodelta
306    [ cut((mk_state_pc ERTL_semantics
307   (sigma_state prog f_lbls f_regs
308    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
309     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
310   (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
311   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
312   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
313    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
314    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
315    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %]
316    #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
317    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
318    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *)
319    | cut((mk_state_pc ERTL_semantics
320   (sigma_state prog f_lbls f_regs
321    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
322     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
323   (succ_pc ERTL_semantics (pc ERTLptr_semantics st2)
324    (point_of_succ ERTLptr_semantics
325     (point_of_pc ERTLptr_semantics
326      (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
327   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
328   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
329    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
330     (point_of_succ ERTLptr_semantics
331      (point_of_pc ERTLptr_semantics
332       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
333    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
334    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ
335    >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
336    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
337     (point_of_succ ERTLptr_semantics
338      (point_of_pc ERTLptr_semantics
339       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
340    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *)
341]
342qed.*)
343
344
345theorem ERTLptrToLTL_ok :
346∀fix_comp : fixpoint_computer.
347∀colour : coloured_graph_computer.
348∀p_in : ertlptr_program.
349let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
350let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
351let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
352(* what should we do with n? *)
353let stacksizes ≝ lookup_stack_cost m in
354∃[1] R.
355  status_simulation
356    (joint_status ERTLptr_semantics p_in stacksizes)
357    (joint_status LTL_semantics p_out stacksizes)
358    R.
359#fix_comp #colour #p_in
360cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
361          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
362#fregs * #f_lbls * #f_bl_r #good
363%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
364whd in match status_simulation; normalize nodelta
365whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
366whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
367change with
368  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
369#EQeval @('bind_inversion EQeval)
370** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
371#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
372cases stmt in EQfetch; -stmt
373[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
374#EQfetch
375change with (joint_classify ??) in
376                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
377[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
378  (* XXX
379  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
380  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
381  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
382  *) cases daemon
383| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
384          normalize nodelta #is_call_st1
385          (* XXX
386          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
387          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
388          #call_rel * #taa * #st2' * #sem_rel #eval_rel
389          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
390          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
391          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
392          *) cases daemon
393| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
394          normalize nodelta #n_costed
395          cases(eval_cond_ok  … good … EQst2 … EQfetch EQeval … n_costed)
396          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
397          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
398| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
399          normalize nodelta
400          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
401          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
402          % [% //] whd >(as_label_ok … good … st3) [%]
403          cases daemon (*needs lemma about preservation of fetch_statement *)
404|  cases fin_step in EQfetch;
405  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
406     >EQfetch normalize nodelta
407    cases (eval_goto_ok … good  … EQfetch EQeval)
408    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
409    % [% //] whd >(as_label_ok … good … st3) [%]
410    cases daemon (*needs lemma about preservation of fetch_statement *)
411  | (*RETURN*) #EQfetch
412     whd in match joint_classify; normalize nodelta
413    >EQfetch  normalize nodelta
414    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
415    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
416    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
417    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
418    % [2: assumption] % [2: %] % [2: assumption] % assumption
419  | (*TAILCALL*) *
420  ]
421]
422
Note: See TracBrowser for help on using the repository browser.