- Timestamp:
- Mar 12, 2013, 6:51:15 PM (8 years ago)
- Location:
- src/joint
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/StatusSimulationHelper.ma
r2851 r2855 34 34 qed. 35 35 36 let rec bind_new_arity (B : Type[0]) (b : B) (E : Type[0]) (x : bind_new B E) on x : ℕ ≝37 match x with38 [bret y ⇒ 039 |bnew f ⇒ 1 + bind_new_arity … b … (f b)40 ].41 36 42 lemma bcompile_ok : ∀U,R,E,fresh,b. 37 lemma bind_new_bind_new_instantiates : 38 ∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P. 39 bind_new_instantiates B X x m l → bind_new_P' ?? P m → 40 P l x. 41 #B #X #m elim m normalize nodelta 42 [#x #y * normalize // #B #l' #P * 43 | #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H) 44 @Hr 45 ] 46 qed. 43 47 44 48 45 lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params.49 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. 46 50 ∀prog : joint_program P_in. 47 51 ∀stack_sizes. … … 56 60 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop. 57 61 R st1 st2 → 62 let step ≝ (COND P_in ? a ltrue) in 63 bind_new_P' ?? 64 (λregs1.λdata.∀lbl.bind_new_P' ?? 65 (λregs2.λblp. 66 (∀mid1.∃st2'. 67 repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? (\fst (\fst blp)) mid1) (st_no_pc … st2) 68 = return (st_no_pc … st2') ∧ 69 pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧ 70 last_pop … st2' = last_pop … st2) 71 ) (f_step ??? data lbl step) 72 ) (init ? fn) → 58 73 fetch_statement P_in … 59 74 (globalenv_noinit ? prog) (pc … st1) = 60 return 〈f, fn, sequential … (COND P_in … a ltrue)lfalse〉 →75 return 〈f, fn, sequential … step lfalse〉 → 61 76 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 62 77 st1 = return st1' → 63 78 as_costed (joint_abstract_status prog_pars_in) st1' → 64 (*(∀mid1.∃st2'.65 repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2)66 = return (st_no_pc … st2') ∧67 pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧68 last_pop … st2' = last_pop … st2)) → *)69 79 ∃ st2'. R st1' st2' ∧ 70 80 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 71 81 bool_to_Prop (taaf_non_empty … taf). 72 82 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2 73 #f #fn #a #ltrue #lfalse #R #Rst1st2 # EQfetch whd in match eval_state; normalize nodelta83 #f #fn #a #ltrue #lfalse #R #Rst1st2 #Hb_graph #EQfetch whd in match eval_state; normalize nodelta 74 84 >EQfetch >m_return_bind 75 85 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind … … 99 109 pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧ 100 110 last_pop … st2' = last_pop … st2) 101 [2,4: cases daemon (* THE EXTENSIONAL PROOF *)]111 [2,4: assumption ] 102 112 #st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid 103 113 >(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1 … … 129 139 |*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption 130 140 ] 131 qed. 141 qed.*) -
src/joint/TranslateUtils.ma
r2843 r2855 378 378 [ bret x ⇒ P [ ] x 379 379 | bnew f ⇒ 380 ∀r.bind_new_P' R X (λl.P ( l @ [r])) (f r)380 ∀r.bind_new_P' R X (λl.P (r::l)) (f r) 381 381 ]. 382 382
Note: See TracChangeset
for help on using the changeset viewer.