Changeset 2663
- Timestamp:
- Feb 12, 2013, 7:40:11 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTLptr/ERTLtoERTLptrOK.ma
r2662 r2663 1993 1993 @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ] 1994 1994 #LAST_STEP 1995 1995 cases daemon 1996 qed. 1996 1997 1997 1998 lemma eval_seq_no_call_ok : … … 2019 2020 st''. 2020 2021 bool_to_Prop (taaf_non_empty … taf). 2021 #prog #good #stack_size #st #st' #f #fn #stmt #nxt 2022 #prog #good #stack_size #st #st' #f #fn #stmt #nxt #EQfetch #EQeval 2023 cases (foo … translate_step translate_fin_step … EQfetch EQeval) 2024 [2,3: cases daemon (* first one, take out init definition from ERTLtoERTLptr; 2025 second one to be taken from somewhere *) 2026 |4: #x cases daemon (* TO BE DONE, EASY *) 2027 |5: cases daemon (* to be taken in input *) ] 2028 [2: cases daemon 2029 | #st'' * #taaf #_ %{st''} 2030 change with ERTL_uns in match (mk_unserialized_params ???????????????); 2031 change with ERTLptr_uns in match (mk_unserialized_params ???????????????); 2032 change with ERTL_semantics in match (make_sem_graph_params ??); 2033 change with ERTLptr_semantics in match (make_sem_graph_params ??); 2034 2035 2036 #H1 #H2 #H3 * 2037 2038 ∀P1_unser,P2_unser: unserialized_params. 2039 ∀P1_sem_unser,P2_sem_unser. 2040 ∀init,translate_step. 2041 ∀translate_fin_step. 2042 ∀closed_graph_translate. 2043 ∀prog. 2044 ∀stack_size. 2045 ∀sigma_state_pc. 2046 (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) → 2047 ∀st : state_pc P2_sem. 2048 ∀st' : state_pc P1_sem. 2049 ∀f. 2050 ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)). 2051 luniverse_ok … fn → 2052 ∀stmt,nxt. 2053 (∀pre_Instrs',last_Instrs',dst. 2054 ∃st''.∃st'''.∃st''''. 2055 repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size) 2056 f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧ 2057 eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size)) 2058 f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧ 2059 st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size) 2060 st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ 2061 st' = sigma_state_pc st'' ∧ 2062 let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in 2063 let P2_globals ≝ globals P2_prog_params in 2064 All 2065 (joint_seq … P2_globals) 2066 (no_cost_label … P2_globals) 2067 (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) → 2068 2069 2070 2022 2071 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim 2023 2072 [ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
Note: See TracChangeset
for help on using the changeset viewer.