Changeset 2663

Timestamp:

Feb 12, 2013, 7:40:11 PM (8 years ago)

Author:

piccolo

Message:

some minor modifications to ERTLtoERTLptr

File:

• src/ERTLptr/ERTLtoERTLptrOK.ma (modified) (2 diffs)

src/ERTLptr/ERTLtoERTLptrOK.ma

@@ -1993 +1993 @@
   @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ]
 #LAST_STEP
-
+cases daemon
+qed.
 
 lemma eval_seq_no_call_ok :
@@ -2019 +2020 @@
   st''.
  bool_to_Prop (taaf_non_empty … taf).
-#prog #good #stack_size #st #st' #f #fn #stmt #nxt 
+#prog #good #stack_size #st #st' #f #fn #stmt #nxt #EQfetch #EQeval
+cases (foo … translate_step translate_fin_step … EQfetch EQeval)
+[2,3: cases daemon (* first one, take out init definition from ERTLtoERTLptr;
+                      second one to be taken from somewhere *)
+|4: #x cases daemon (* TO BE DONE, EASY *)
+|5: cases daemon (* to be taken in input *) ]
+[2: cases daemon
+| #st'' * #taaf #_ %{st''}
+  change with ERTL_uns in match (mk_unserialized_params ???????????????);
+  change with ERTLptr_uns in match (mk_unserialized_params ???????????????);
+  change with ERTL_semantics in match (make_sem_graph_params ??);
+  change with ERTLptr_semantics in match (make_sem_graph_params ??);
+
+
+#H1 #H2 #H3 *
+
+ ∀P1_unser,P2_unser: unserialized_params.
+ ∀P1_sem_unser,P2_sem_unser.
+ ∀init,translate_step.
+ ∀translate_fin_step.
+ ∀closed_graph_translate.
+ ∀prog.
+ ∀stack_size.
+ ∀sigma_state_pc.
+ (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) →
+ ∀st : state_pc P2_sem. 
+ ∀st' : state_pc P1_sem. 
+ ∀f.
+ ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)).
+ luniverse_ok … fn → 
+ ∀stmt,nxt.
+ (∀pre_Instrs',last_Instrs',dst.
+   ∃st''.∃st'''.∃st''''.
+    repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size)
+     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
+    eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size))
+                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
+    st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
+     st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ 
+    st' = sigma_state_pc st'' ∧
+    let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
+    let P2_globals ≝ globals P2_prog_params in 
+     All
+      (joint_seq … P2_globals)
+      (no_cost_label … P2_globals)
+      (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) →
+
+
+ 
 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
 [ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]