Changeset 2889

Timestamp:

Mar 15, 2013, 7:36:04 PM (4 years ago)

Author:

sacerdot

Message:

It works very nice!

File:

• src/ERTLptr/ERTLptrToLTLProof.ma (modified) (3 diffs)

src/ERTLptr/ERTLptrToLTLProof.ma

@@ -274 +274 @@
 ∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) → 
 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 
-eliminable ? (after l) stmt = None ? → 
+eliminable ? (after l) stmt = false → 
 lives (inl ? ? r)  (livebefore  … fn l after).
 #fix_comp #prog #fn #l *
@@ -429 +429 @@
   letin p_out ≝ (mk_prog_params LTL_semantics ??) 
   letin trans_prog ≝ (b_graph_transform_program ????)
-  #st1 #st1' #st2 #f #fn * 
+  #st1 #st1' #st2 #f #fn *
   [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?); 
       normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
@@ -444 +444 @@
       change with p_in in match p_in;
       change with trans_prog in match trans_prog;
-      #mid #mid1 #EQmid % [%]
-      [ cases (andb ??) whd in match (preserve_carry_bit ???);
-        whd in match ensure_step_block; normalize nodelta
-        XXX
-      
-      
-      whd normalize nodelta
-      change with p_out in match p_out;
-      change with p_in in match p_in;
-      change with trans_prog in match trans_prog;
-      letin coloured_dst ≝ (colouring ???)
-      letin coloured_src ≝ (colouring ???)
-      whd in match translate_op1; normalize nodelta
-
-
-
-      whd in match (translate_op1 ?????);
-      change with (bind_new_P' ? (? × ?) ?
-       (f_step ERTLptr_semantics ?????));
-      whd in match (translate_data ????);
-      change with (bind_new_P' ??? (f_step ??????));
-      whd in match (f_step ??????); 
-      @(λH.H)
-      
-      whd in match (  #mid whd #
- 
-
+      % [2: % [ % | ] | skip]
 qed.