source: src/joint/Traces.ma @ 2317

include "joint/semantics.ma".

record evaluation_params : Type[1] ≝
 { globals: list ident
 ; sparams:> sem_params
 ; exit: cpointer
 ; ev_genv: genv sparams globals
 ; io_env : state sparams → ∀o:io_out.res (io_in o)
 } .

(*record classifier_params : Type[1] ≝
  { cl_pars :> evaluation_parameters
  ; cl_ext_step : ext_step cl_pars → status_class
  ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class
  }.*)


definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
*#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
[ #EQ destruct % #H %
| * #NEQ % #ABS destruct elim (NEQ ?) %
]
qed.

let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
  match c with
  [ Value x ⇒ OK … x
  | Interact o f ⇒
    ! i ← env o ;
    io_evaluate O I X env (f i)
  | Wrong e ⇒ Error … e
  ].

definition cost_label_of_stmt :
  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
  λp,s.match s with
  [ sequential s _ ⇒
    match s with
    [ step_seq s ⇒
      match s with
      [ COST_LABEL lbl ⇒ Some ? lbl
      | _ ⇒ None ?
      ]
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

definition joint_abstract_status :
 ∀p : evaluation_params.
 abstract_status ≝
 λp.
 mk_abstract_status
   (* as_status ≝ *) (state_pc p)
   (* as_execute ≝ *)
    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
   (* as_pc ≝ *) cpointerDeq
   (* as_pc_of ≝ *) (pc …)
   (* as_classifier ≝ *)
    (λs,cl.∃fn,stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
     stmt_classifier … stmt = cl)
   (* as_label_of_pc ≝ *)
    (λpc.
      match fetch_statement ? p … (ev_genv p) pc with
      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
      | _ ⇒ None ?
      ])
   (* as_after_return ≝ *)
    (λs1,s2.
      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
      succ_pc p p (pc … s1) nxt = return pc … s2)
   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).