Changeset 2886


Ignore:
Timestamp:
Mar 15, 2013, 7:19:56 PM (4 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/StatusSimulationHelper.ma

    r2885 r2886  
    6363]
    6464qed.
    65  
     65
     66check ensure_step_block
    6667
    6768record good_state_relation (P_in : sem_graph_params)
     
    138139     (λregs1.λdata.bind_new_P' ??
    139140     (λregs2.λblp.
    140        ∃l: LISTA FRU FRU. blp = l ∧
    141        
     141       ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes)
     142                            (globals (mk_prog_params P_out trans_prog stack_sizes))).
     143                            blp = (ensure_step_block ?? l) ∧ True
     144       (*
    142145       TUTTO IL RESTO PARLA DI R
    143146       
     
    159162                         (pc_of_point P_out (pc_block(pc … st2)) nxt)
    160163                         (last_pop … st2) in
    161            R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
     164           R st1' st2_fin *) ) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
    162165      ) (init ? fn)         
    163166}.
    164 @hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    165 qed.
     167(*@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     168qed.*)
    166169
    167170lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    268271(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
    269272 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
     273cases daemon qed.
     274 
     275(*
    270276#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
    271277#st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
     
    290296    #seq_mid cases daemon (*TODO*)
    291297    qed.
    292    
    293 (*   
     298       
    294299    cases(blm mid1) in
    295300#stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC;  destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ)
Note: See TracChangeset for help on using the changeset viewer.