Changeset 2889


Ignore:
Timestamp:
Mar 15, 2013, 7:36:04 PM (4 years ago)
Author:
sacerdot
Message:

It works very nice!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2883 r2889  
    274274∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
    275275let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
    276 eliminable ? (after l) stmt = None ?
     276eliminable ? (after l) stmt = false
    277277lives (inl ? ? r)  (livebefore  … fn l after).
    278278#fix_comp #prog #fn #l *
     
    429429  letin p_out ≝ (mk_prog_params LTL_semantics ??)
    430430  letin trans_prog ≝ (b_graph_transform_program ????)
    431   #st1 #st1' #st2 #f #fn * 
     431  #st1 #st1' #st2 #f #fn *
    432432  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
    433433      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
     
    444444      change with p_in in match p_in;
    445445      change with trans_prog in match trans_prog;
    446       #mid #mid1 #EQmid % [%]
    447       [ cases (andb ??) whd in match (preserve_carry_bit ???);
    448         whd in match ensure_step_block; normalize nodelta
    449         XXX
    450      
    451      
    452       whd normalize nodelta
    453       change with p_out in match p_out;
    454       change with p_in in match p_in;
    455       change with trans_prog in match trans_prog;
    456       letin coloured_dst ≝ (colouring ???)
    457       letin coloured_src ≝ (colouring ???)
    458       whd in match translate_op1; normalize nodelta
    459 
    460 
    461 
    462       whd in match (translate_op1 ?????);
    463       change with (bind_new_P' ? (? × ?) ?
    464        (f_step ERTLptr_semantics ?????));
    465       whd in match (translate_data ????);
    466       change with (bind_new_P' ??? (f_step ??????));
    467       whd in match (f_step ??????);
    468       @(λH.H)
    469      
    470       whd in match (  #mid whd #
    471  
    472 
     446      % [2: % [ % | ] | skip]
    473447qed.
    474448
Note: See TracChangeset for help on using the changeset viewer.