Changeset 2595 for src/joint/semantics_blocks.ma
- Timestamp:
- Jan 30, 2013, 7:25:39 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semantics_blocks.ma
r2529 r2595 2 2 include "joint/Traces.ma". 3 3 include "joint/semanticsUtils.ma". 4 5 include "common/StatusSimulation.ma". (* for trace_any_any_free *) 4 6 5 7 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ … … 13 15 m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn). 14 16 15 definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ]. 17 definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3. 18 as_execute S s1 s2 → 19 as_classifier … s1 cl_other → 20 ∀taaf : trace_any_any_free S s2 s3. 21 (if taaf_non_empty … taaf then ¬as_costed … s2 else True) → 22 trace_any_any_free S s1 s3 ≝ 23 λS,s1,s2,s3,H,I,tl. 24 match tl return λs2,s3,tl. 25 as_execute … s1 s2 → 26 if taaf_non_empty … tl then ¬as_costed … s2 else True → 27 trace_any_any_free S s1 s3 28 with 29 [ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I 30 | taaf_step s2 s3 s4 taa H' I' ⇒ 31 λH,J.taaf_step … (taa_step … H I J taa) H' I' 32 | taaf_step_jump s2 s3 s4 taa H' I' K' ⇒ 33 λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K' 34 ] H. 16 35 17 let rec produce_trace_any_any 36 lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J. 37 bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)). 38 #S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl 39 [ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ] 40 qed. 41 42 let rec produce_trace_any_any_free_aux 18 43 (p : evaluation_params) 19 44 (st : state_pc p) … … 26 51 return 〈curr_id, curr_fn〉 → 27 52 let src ≝ point_of_pc p (pc … st) in 28 if list_not_empty ? b then 29 ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ? 30 else 31 True → 53 (* disambiguation: select 3rd (step list in code) *) 32 54 src ~❨b, l❩~> dst in joint_if_code … curr_fn → 33 All ? ( λx.And (no_call … x) (no_cost_label … x)) b →55 All ? (no_cost_label …) b → 34 56 repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' → 35 trace_any_any (joint_abstract_status p) st 36 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝ match b 37 return λb.∀l,dst.?→?→?→?→?→?→? 57 Σtaaf : trace_any_any_free (joint_abstract_status p) st 58 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). 59 (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝ 60 match b 61 return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf)) 38 62 with 39 63 [ nil ⇒ 40 λl,dst,st',fd_prf, dst_prf,in_code,all_other,EQ1.41 (taa_base (joint_abstract_status p) st)42 ⌈trace_any_any ??? ↦ ?⌉64 λl,dst,st',fd_prf,in_code,all_other,EQ1. 65 «taaf_base (joint_abstract_status p) st 66 ⌈trace_any_any_free ??? ↦ ?⌉,?» 43 67 | cons hd tl ⇒ 44 68 λl. 45 match l return λx.∀dst,st'.?→?→?→?→ ?→?with46 [ nil ⇒ λdst,st',fd_prf, dst_prf,in_code.⊥69 match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with 70 [ nil ⇒ λdst,st',fd_prf,in_code.⊥ 47 71 | cons mid rest ⇒ 48 λdst,st',fd_prf, dst_prf,in_code,all_other,EQ1.72 λdst,st',fd_prf,in_code,all_other,EQ1. 49 73 let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in 50 74 match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st 51 75 return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x → 52 trace_any_any (joint_abstract_status p) st 53 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with 54 [ Value st_mid ⇒ λEQ2. 55 let tr_tl ≝ produce_trace_any_any ? 56 (mk_state_pc ? st_mid mid_pc) 57 curr_id curr_fn tl rest dst ?????? in 58 taa_step … tr_tl 76 Σtaaf : trace_any_any_free (joint_abstract_status p) st 77 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). 78 (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with 79 [ OK st_mid ⇒ λEQ2. 80 let tr_tl ≝ produce_trace_any_any_free_aux ? 81 (mk_state_pc ? st_mid mid_pc (last_pop … st)) 82 curr_id curr_fn tl rest dst ????? in 83 «taaf_cons … tr_tl ?,?» 59 84 | _ ⇒ λEQ2.⊥ 60 85 ] (refl …) 61 86 ] 62 ]. 63 [ whd in EQ1 : (??%%); 64 cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct 65 >pc_of_point_of_pc cases st // 87 ]. @hide_prf 88 [1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ] 89 whd in EQ1 : (??%%); 90 cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct 91 >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta * 66 92 | @in_code 67 |3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1) 93 |12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1) 94 |4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other; 95 [ #_ #_ * #_ cases (taaf_non_empty ????) 96 [ #ABS cases (ABS I) | #_ % ] 97 | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' * 98 * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other' 99 #_ * #H #_ >(H I) % whd in ⊢ (%→?); 100 whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??); 101 >fetch_statement_eq [2: whd in match point_of_pc; 102 normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:] 103 normalize nodelta 104 >(no_label_uncosted … hd_other') * #ABS @ABS % 105 ] 106 |7: % [2: #_ %] * @taaf_cons_non_empty 68 107 ] 69 108 change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1; 70 109 >EQ2 in EQ1; >m_return_bind 71 110 cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code 72 cases all_other -all_other * #hd_no_call#hd_no_cost #tl_other111 cases all_other -all_other #hd_no_cost #tl_other 73 112 #EQ1 74 113 try assumption 75 [ whd whd in match eval_state; normalize nodelta114 [2: whd whd in match eval_state; normalize nodelta 76 115 >(fetch_statement_eq … fd_prf EQ_stmt_at) 77 116 >m_return_bind … … 79 118 >EQ2 >m_return_bind 80 119 whd in match eval_statement_advance; normalize nodelta 81 >(no_call_advance … hd_no_call)82 120 whd in match next; normalize nodelta 83 121 whd in match succ_pc; normalize nodelta 84 122 >EQ_mid % 85 | whd whd in ⊢ (??%?); 86 >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta 87 @(no_call_other … hd_no_call) 88 | whd in ⊢ (?%); 89 whd in match as_label; normalize nodelta 90 %* #H @H -H whd in ⊢ (??%?); 91 whd in match (as_pc_of ??); 92 inversion (fetch_statement ????) normalize nodelta 93 [2: // ] 94 ** #i' #f' #stmt' #EQ 95 elim (fetch_statement_inv … EQ) 96 >fd_prf 97 whd in ⊢ (??%?→?); #EQ destruct(EQ) 98 whd in ⊢ (%→?); 99 whd in match (point_of_pc ??); >point_of_offset_of_point 100 #EQ' 101 cases tl in tl_other rest_in_code; 102 [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ) 103 >EQ' in dst_prf; >m_return_bind #H @H 104 | #hd' #tl' ** #_ #hd_no_cost' #_ 105 cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_ 106 >EQ_stmt_at' in EQ'; #EQ' destruct(EQ') 107 @(no_label_uncosted … hd_no_cost') 108 ] 109 | >dst_prf cases (list_not_empty ??) % 110 | normalize nodelta >point_of_pc_of_point assumption 123 |1: whd whd in ⊢ (??%?); 124 >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta % 125 |3: normalize nodelta >point_of_pc_of_point assumption 111 126 ] 112 127 qed. 128 129 definition produce_trace_any_any_free : 130 ∀p : evaluation_params. 131 ∀st : state_pc p. 132 ∀curr_id,curr_fn. 133 ∀b : list (joint_seq p (globals p)). 134 ∀l : list (code_point p). 135 ∀dst : code_point p. 136 ∀st' : state p. 137 fetch_internal_function … (ev_genv p) (pc_block (pc … st)) = 138 return 〈curr_id, curr_fn〉 → 139 let src ≝ point_of_pc p (pc … st) in 140 (* disambiguation: select 3rd (step list in code) *) 141 src ~❨b, l❩~> dst in joint_if_code … curr_fn → 142 All ? (no_cost_label …) b → 143 repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' → 144 trace_any_any_free (joint_abstract_status p) st 145 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝ 146 λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4. 147 produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
Note: See TracChangeset
for help on using the changeset viewer.