Changeset 2553 for src/joint/Traces.ma


Ignore:
Timestamp:
Dec 12, 2012, 2:43:03 PM (8 years ago)
Author:
tranquil
Message:

as_classify changed to a partial function
added a status for tailcalls

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2538 r2553  
    124124
    125125definition joint_classify_final :
    126   ∀p : evaluation_params.joint_fin_step p → status_class ≝
    127   λp,stmt.
     126  ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
     127  λp,st,stmt.
    128128  match stmt with
    129129  [ GOTO _ ⇒ cl_other
    130130  | RETURN ⇒ cl_return
    131   | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
     131  | TAILCALL _ f args ⇒
     132    match (! bl ← block_of_call … (ev_genv p) f st ;
     133            fetch_function … (ev_genv p) bl) with
     134    [ OK id_fn ⇒
     135      match \snd id_fn with
     136      [ Internal _ ⇒ cl_tailcall
     137      | External _ ⇒ cl_return
     138      ]
     139    | Error _ ⇒ cl_other
     140    ]
    132141  ].
    133142
    134143definition joint_classify :
    135   ∀p : evaluation_params.state_pc p → status_class ≝
     144  ∀p : evaluation_params.state_pc p → option status_class ≝
    136145  λp,st.
    137   match fetch_statement … (ev_genv p) (pc … st) with
    138   [ OK i_f_s ⇒
    139     match \snd i_f_s with
    140     [ sequential s _ ⇒ joint_classify_step p st s
    141     | final s ⇒ joint_classify_final p s
    142     | FCOND _ _ _ _ ⇒ cl_jump
    143     ]
    144   | Error _ ⇒ cl_other
     146  ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
     147  match s with
     148  [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
     149  | final s ⇒ Some ? (joint_classify_final p st s)
     150  | FCOND _ _ _ _ ⇒ Some ? cl_jump
    145151  ].
    146152
     
    179185
    180186lemma joint_classify_call : ∀p : evaluation_params.∀st.
    181   joint_classify p st = cl_call →
     187  joint_classify p st = Some ? cl_call →
    182188  ∃i_f,f',args,dest,next,bl,i',fd'.
    183189  fetch_statement … (ev_genv p) (pc … st) =
     
    187193#p #st
    188194whd in match joint_classify; normalize nodelta
    189 inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta
    190 [2: #e #_ #ABS destruct(ABS) ]
     195inversion (fetch_statement … (ev_genv p) (pc … st))
     196[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
    191197* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
    192   normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    193 @cond_call_other
    194 [ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
    195 |3: #s #no_call #nxt #_ whd in match joint_classify_step;
    196   normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS)
    197 ]
    198 #f' #args #dest #nxt #fetch
     198>m_return_bind normalize nodelta
     199  [3: whd in match joint_classify_final; normalize nodelta
     200    generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
     201    normalize nodelta ]
     202  #ABS destruct(ABS) ]
     203@cond_call_other [ #a #lbl | #f' #args #dest | #s #s_no_call ] #nxt #fetch >m_return_bind
     204normalize nodelta
     205[ normalize in ⊢ (%→?); #ABS destruct(ABS)
     206|3: whd in match joint_classify_step;
     207  normalize nodelta >(no_call_other … s_no_call) #ABS destruct(ABS)
     208]
    199209whd in match joint_classify_step; whd in match joint_classify_seq;
    200210normalize nodelta
     
    215225
    216226definition joint_after_ret : ∀p:evaluation_params.
    217   (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
     227  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
    218228λp,s1,s2.
    219229match fetch_statement … (ev_genv p) (pc … s1) with
     
    228238
    229239definition joint_call_ident : ∀p:evaluation_params.
    230   (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
     240  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
    231241(* this is a definition without a dummy ident :
    232242λp,st.
     
    283293].
    284294
     295definition joint_tailcall_ident : ∀p:evaluation_params.
     296  (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
     297λp,st.
     298let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     299match fetch_statement … (ev_genv p) (pc … st) with
     300[ OK x ⇒
     301  match \snd x with
     302  [ final s ⇒
     303    match s with
     304    [ TAILCALL _ f' args ⇒
     305      match
     306        (! bl ← block_of_call … (ev_genv p) f' st;
     307         fetch_internal_function … (ev_genv p) bl) with
     308      [ OK i_f ⇒ \fst i_f
     309      | _ ⇒ dummy
     310      ]
     311    | _ ⇒ dummy
     312    ]
     313  | _ ⇒ dummy
     314  ]
     315| _ ⇒ dummy
     316].
     317
    285318definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
    286319*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
     
    342375   (* as_after_return ≝ *) (joint_after_ret p)
    343376   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
    344    (* as_call_ident ≝ *) (joint_call_ident p).
     377   (* as_call_ident ≝ *) (joint_call_ident p)
     378   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracChangeset for help on using the changeset viewer.