Changeset 2757 for src/joint


Ignore:
Timestamp:
Mar 1, 2013, 7:13:49 PM (7 years ago)
Author:
tranquil
Message:

many things are still broken, but there is a partial backtrack on Structured traces's execute

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2688 r2757  
    117117
    118118definition joint_classify :
    119   ∀p : evaluation_params.state_pc p → option status_class ≝
     119  ∀p : evaluation_params.state_pc p → status_class ≝
    120120  λp,st.
    121   ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
    122   match s with
    123   [ sequential s _ ⇒ Some ? (joint_classify_step p s)
    124   | final s ⇒ Some ? (joint_classify_final p s)
    125   | FCOND _ _ _ _ ⇒ Some ? cl_jump
     121  match fetch_statement … (ev_genv p) (pc … st) with
     122  [ OK i_fn_s ⇒
     123    match \snd i_fn_s with
     124    [ sequential s _ ⇒ joint_classify_step p s
     125    | final s ⇒ joint_classify_final p s
     126    | FCOND _ _ _ _ ⇒ cl_jump
     127    ]
     128  | _ ⇒ cl_other
    126129  ].
    127130
    128131lemma joint_classify_call : ∀p : evaluation_params.∀st.
    129   joint_classify p st = Some ? cl_call →
     132  joint_classify p st = cl_call →
    130133  ∃i_f,f',args,dest,next.
    131134  fetch_statement … (ev_genv p) (pc … st) =
     
    137140* #i_f *
    138141[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
    139   >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct
    140 ]
    141 * [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
     142  normalize nodelta normalize in ⊢ (%→?); #ABS destruct
     143]
     144* [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch normalize nodelta
    142145normalize in ⊢ (%→?); #EQ destruct
    143146%[|%[|%[|%[|%[| %]]]]]
     
    145148
    146149definition joint_after_ret : ∀p:evaluation_params.
    147   (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
     150  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
    148151λp,s1,s2.
    149152match fetch_statement … (ev_genv p) (pc … s1) with
     
    159162
    160163definition joint_call_ident : ∀p:evaluation_params.
    161   (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
     164  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
    162165(* this is a definition without a dummy ident :
    163166λp,st.
     
    215218
    216219definition joint_tailcall_ident : ∀p:evaluation_params.
    217   (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
     220  (Σs : state_pc p.joint_classify p s = cl_tailcall) → ident ≝
    218221λp,st.
    219222let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     
    267270
    268271definition joint_abstract_status :
    269  ∀p : evaluation_params.
     272 ∀p : prog_params.
    270273 abstract_status ≝
    271274 λp.
     
    273276   (* as_status ≝ *) (state_pc p)
    274277   (* as_execute ≝ *)
    275     (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
     278    (λs1,s2.eval_state … (ev_genv p) s1 = return s2)
     279   (* (* as_init ≝ *) (make_initial_state p) *)
    276280   (* as_pc ≝ *) pcDeq
    277281   (* as_pc_of ≝ *) (pc …)
     
    284288      ])
    285289   (* as_after_return ≝ *) (joint_after_ret p)
    286    (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
     290   (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
    287291   (* as_call_ident ≝ *) (joint_call_ident p)
    288    (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). 
     292   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracChangeset for help on using the changeset viewer.