Changeset 2663


Ignore:
Timestamp:
Feb 12, 2013, 7:40:11 PM (6 years ago)
Author:
piccolo
Message:

some minor modifications to ERTLtoERTLptr

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2662 r2663  
    19931993  @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ]
    19941994#LAST_STEP
    1995 
     1995cases daemon
     1996qed.
    19961997
    19971998lemma eval_seq_no_call_ok :
     
    20192020  st''.
    20202021 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
     2023cases (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 
    20222071whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
    20232072[ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
Note: See TracChangeset for help on using the changeset viewer.