Changeset 2855 for src/joint

Timestamp:

Mar 12, 2013, 6:51:15 PM (8 years ago)

Author:

piccolo

Message:

little bug fixed in TranslateUtils?.

Location:

src/joint

Files:

• StatusSimulationHelper.ma (modified) (4 diffs)
• TranslateUtils.ma (modified) (1 diff)

src/joint/StatusSimulationHelper.ma

@@ -34 +34 @@
 qed.
 
-let rec bind_new_arity (B : Type[0]) (b : B) (E : Type[0]) (x : bind_new B E) on x : ℕ ≝ 
-match x with
-[bret y ⇒ 0
-|bnew f ⇒ 1 + bind_new_arity … b … (f b)
-].
 
-lemma bcompile_ok : ∀U,R,E,fresh,b.
+lemma bind_new_bind_new_instantiates : 
+∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P.
+bind_new_instantiates B X x m l → bind_new_P' ?? P m → 
+P l x.
+#B #X #m elim m normalize nodelta
+[#x #y * normalize // #B #l' #P *
+| #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H)
+ @Hr
+]
+qed. 
 
 
-lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
+lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
 ∀prog : joint_program P_in.
 ∀stack_sizes.
@@ -56 +60 @@
 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
 R st1 st2 → 
+let step ≝ (COND P_in ? a ltrue) in
+bind_new_P' ??
+ (λregs1.λdata.∀lbl.bind_new_P' ?? 
+  (λregs2.λblp.
+   (∀mid1.∃st2'.
+     repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? (\fst (\fst blp)) mid1) (st_no_pc … st2) 
+     = return (st_no_pc … st2') ∧
+     pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
+     last_pop … st2' = last_pop … st2)
+   ) (f_step ??? data lbl step)   
+  ) (init ? fn) → 
  fetch_statement P_in …
   (globalenv_noinit ? prog) (pc … st1) =
-    return 〈f, fn,  sequential … (COND P_in … a ltrue) lfalse〉 → 
+    return 〈f, fn,  sequential … step lfalse〉 → 
  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 
             st1 = return st1' → 
 as_costed (joint_abstract_status prog_pars_in) st1' →
-(*(∀mid1.∃st2'.
-   repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2) 
-           = return (st_no_pc … st2') ∧
-           pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
-           last_pop … st2' = last_pop … st2)) → *)
 ∃ st2'. R st1' st2' ∧ 
 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
 bool_to_Prop (taaf_non_empty … taf).
 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2 
-#f #fn #a #ltrue #lfalse #R #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta 
+#f #fn #a #ltrue #lfalse #R #Rst1st2 #Hb_graph #EQfetch whd in match eval_state; normalize nodelta 
 >EQfetch >m_return_bind
 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
@@ -99 +109 @@
            pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
            last_pop … st2' = last_pop … st2)
-   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
+   [2,4: assumption ]
 #st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
 >(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
@@ -129 +139 @@
 |*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
 ]
-qed.
+qed.*)

src/joint/TranslateUtils.ma

@@ -378 +378 @@
 [ bret x ⇒ P [ ] x
 | bnew f ⇒
-  ∀r.bind_new_P' R X (λl.P (l @ [r])) (f r)
+  ∀r.bind_new_P' R X (λl.P (r::l)) (f r)
 ].