Changeset 2561 for src/joint/Traces.ma


Ignore:
Timestamp:
Dec 18, 2012, 5:03:29 PM (8 years ago)
Author:
tranquil
Message:
  • moved CALL as different case than joint_seq: lots of broken code now
  • changed save_frame flag from bool to more descriprive variant type call_kind
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2556 r2561  
    7979  (* use exit_pc as ra and call_dest_for_main as dest *)
    8080  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    81   ! st0_no_pc ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
     81  ! st0_no_pc ← save_frame ?? sem_globals call_id (call_dest_for_main … pars) st0' ;
    8282  let st0'' ≝ set_no_pc … st0_no_pc st0' in
    8383  ! bl ← block_of_call … ge (inl … main) st0'';
     
    9191  ].
    9292
    93 definition joint_classify_seq :
    94   ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
     93definition joint_classify_step :
     94  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
    9595  λp,st,stmt.
    9696  match stmt with
    97   [ CALL f args dest ⇒
     97  [ step_seq _ ⇒ cl_other
     98  | CALL f args dest ⇒
    9899    match (! bl ← block_of_call … (ev_genv p) f st ;
    99100            fetch_function … (ev_genv p) bl) with
     
    105106    | Error _ ⇒ cl_other
    106107    ]
    107   | _ ⇒ cl_other
    108   ].
    109 
    110 definition joint_classify_step :
    111   ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
    112   λp,st,stmt.
    113   match stmt with
    114   [ step_seq s ⇒ joint_classify_seq p st s
    115108  | COND _ _ ⇒ cl_jump
    116109  ].
     
    144137  ].
    145138
    146 definition no_call : ∀p,g.joint_seq p g → Prop ≝
    147   λp,g,s.match s with
    148   [ CALL _ _ _ ⇒ False
    149   | _ ⇒ True
    150   ].
    151 
    152139definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
    153140  λp,g,s.match s with
     
    155142  | _ ⇒ True
    156143  ].
    157 
    158 lemma no_call_advance : ∀p : evaluation_params.
    159 ∀s,nxt.∀st : state_pc p.
    160 no_call p (globals p) s →
    161 eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st.
    162 #p * // #f #args #dest #nxt #st *
    163 qed.
    164 
    165 lemma no_call_other : ∀p : evaluation_params.∀st,s.
    166 no_call p (globals p) s →
    167 joint_classify_seq … st s = cl_other.
    168 #p #st * // #f #args #dest *
    169 qed.
    170 
    171 lemma cond_call_other :
    172   ∀p,globals.∀P : joint_step p globals → Prop.
    173   (∀a,lbltrue.P (COND … a lbltrue)) →
    174   (∀f,args,dest.P (CALL … f args dest)) →
    175   (∀s.no_call ?? s → P s) →
    176   ∀s.P s.
    177 #p #globals #P #H1 #H2 #H3 * // * /2 by / qed.
    178144
    179145lemma joint_classify_call : ∀p : evaluation_params.∀st.
     
    194160    normalize nodelta ]
    195161  #ABS destruct(ABS) ]
    196 @cond_call_other [ #a #lbl | #f' #args #dest | #s #s_no_call ] #nxt #fetch >m_return_bind
     162* [ #s | #f' #args #dest | #a #lbl ] #nxt #fetch >m_return_bind
    197163normalize nodelta
    198 [ normalize in ⊢ (%→?); #ABS destruct(ABS)
    199 |3: whd in match joint_classify_step;
    200   normalize nodelta >(no_call_other … s_no_call) #ABS destruct(ABS)
    201 ]
    202 whd in match joint_classify_step; whd in match joint_classify_seq;
     164[1,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     165whd in match joint_classify_step;
    203166normalize nodelta
    204167inversion (block_of_call ?????)
Note: See TracChangeset for help on using the changeset viewer.