 Timestamp:
 Mar 22, 2013, 7:16:17 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLtoERTLptrOK.ma
r2898 r2940 165 165 definition state_rel ≝ λprog : ertl_program.λf_lbls. 166 166 λf_regs : (block → label → list register). 167 λbl ,st1,st2.∃f,fn.167 λbl.λ_:label.λst1,st2.∃f,fn. 168 168 fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 169 169 let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in … … 236 236 whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind 237 237 normalize nodelta #H @('bind_inversion H) H #st1_no_pc' #EQst1_no_pc' 238 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ) 238 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 239 whd in match (succ_pc ???); normalize nodelta 240 whd in match (set_no_pc ???); normalize nodelta 241 whd in ⊢ (%→?); #EQ destruct(EQ) 239 242 whd in match sigma_state_pc in EQst1_no_pc'; normalize nodelta in EQst1_no_pc'; 240 243 cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) … … 838 841 >EQcall in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); normalize nodelta 839 842 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); 840 >EQfetch' in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); % 843 >EQfetch' in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); normalize nodelta 844 845 [cut (block_of_call 846 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 847 (globals 848 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) 849 (ev_genv 850 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) 851 (inr ident … 〈c_ptr1,c_ptr2〉) 852 (set_regs ERTL_state 853 〈add RegisterTag beval (\fst (regs ERTLptr_semantics st2)) r 854 (\snd (beval_pair_of_pc 855 (pc_of_point ERTLptr_semantics 856 (pc_block (pc ERTLptr_semantics st2)) mid1))), 857 \snd (regs ERTLptr_semantics st2)〉 858 st_no_pc_pre_call) = 859 block_of_call (mk_prog_params ERTL_semantics prog stack_size) 860 (globals (mk_prog_params ERTL_semantics prog stack_size)) 861 (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) 862 (inr ident … 〈c_ptr1,c_ptr2〉) 863 (sigma_state_pc prog f_lbls f_regs st2)) 864 [ 865 866 generalize in match (block_of_call ?????); 867 868 % 841 869 *: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 842 870 @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
Note: See TracChangeset
for help on using the changeset viewer.