Changeset 2821 for src/joint/Traces.ma


Ignore:
Timestamp:
Mar 8, 2013, 11:44:05 AM (7 years ago)
Author:
tranquil
Message:
  • implemented preclassified system for joint (in joint/joint_fullexec.ma)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2796 r2821  
    88(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    99 }.
    10  
    11 
    1210
    1311record prog_params : Type[1] ≝
     
    162160
    163161definition joint_call_ident : ∀p:evaluation_params.
    164   (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
     162  state_pc p → ident ≝
    165163(* this is a definition without a dummy ident :
    166164λp,st.
     
    218216
    219217definition joint_tailcall_ident : ∀p:evaluation_params.
    220   (Σs : state_pc p.joint_classify p s = cl_tailcall) → ident ≝
     218  state_pc p → ident ≝
    221219λp,st.
    222220let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     
    268266  | _ ⇒ None ?
    269267  ].
     268
     269definition joint_label_of_pc ≝
     270  λp : evaluation_params.
     271    (λpc.
     272      match fetch_statement … (ev_genv p) pc with
     273      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
     274      | _ ⇒ None ?
     275      ]).
    270276
    271277definition joint_abstract_status :
     
    281287   (* as_pc_of ≝ *) (pc …)
    282288   (* as_classify ≝ *) (joint_classify p)
    283    (* as_label_of_pc ≝ *)
    284     (λpc.
    285       match fetch_statement … (ev_genv p) pc with
    286       [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
    287       | _ ⇒ None ?
    288       ])
     289   (* as_label_of_pc ≝ *) (joint_label_of_pc p)
    289290   (* as_after_return ≝ *) (joint_after_ret p)
    290291   (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
    291    (* as_call_ident ≝ *) (joint_call_ident p)
    292    (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
     292   (* as_call_ident ≝ *) (λst.joint_call_ident p st)
     293   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
    293294
    294295(* alternative definition with integrated prog_params constructor *)
Note: See TracChangeset for help on using the changeset viewer.