include "joint/Traces.ma".
include "common/Measurable.ma".

definition joint_exec: sem_params → trans_system io_out io_in ≝
  λG.mk_trans_system ?? (evaluation_params G)  (λ_. state_pc G)
   (λenv.joint_final … env)
   (λenv.λst.! st' ← eval_state … env st ;
    let charge ≝ match joint_label_of_pc … env (pc … st) with
      [ Some c ⇒ Echarge c | None ⇒ E0 ] in
     return 〈charge, st'〉).

definition joint_fullexec :
  sem_params → fullexec io_out io_in ≝
  λG.mk_fullexec ?? (joint_program G × (ident → option ℕ))
    (joint_exec G)
    (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr)))
    (λp_stacks.
      make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).

definition joint_preclassified_system : sem_params →
  preclassified_system ≝
  λG.mk_preclassified_system (joint_fullexec G)
    (λenv.λst.¬is_none … (joint_label_of_pc  … env (pc … st)))
    (λenv.joint_classify … env)
    (λenv.λs.λ_.joint_call_ident … env s).