| 1 | include "joint/Traces.ma". |
|---|
| 2 | include "common/Measurable.ma". |
|---|
| 3 | |
|---|
| 4 | (* fullexec and co. *) |
|---|
| 5 | record joint_global (p : sem_params) : Type[0] ≝ |
|---|
| 6 | { jglobals : list ident |
|---|
| 7 | ; jgenv :> genv p jglobals |
|---|
| 8 | }. |
|---|
| 9 | |
|---|
| 10 | definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝ |
|---|
| 11 | λp,gl.mk_evaluation_params (jglobals … gl) p gl. |
|---|
| 12 | |
|---|
| 13 | coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝ |
|---|
| 14 | eval_params_of_global on _gl : joint_global ? to evaluation_params. |
|---|
| 15 | |
|---|
| 16 | definition make_joint_global : ∀p : sem_params. |
|---|
| 17 | (joint_program p × (ident → option ℕ)) → |
|---|
| 18 | joint_global p ≝ |
|---|
| 19 | λpars, p_stack. |
|---|
| 20 | let p ≝ \fst p_stack in |
|---|
| 21 | let stack_sizes ≝ \snd p_stack in |
|---|
| 22 | let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in |
|---|
| 23 | mk_joint_global pars |
|---|
| 24 | (globals … ev_pars) |
|---|
| 25 | (ev_genv … ev_pars). |
|---|
| 26 | |
|---|
| 27 | definition joint_exec: sem_params → trans_system io_out io_in ≝ |
|---|
| 28 | λG.mk_trans_system ?? (joint_global G) (λ_. state_pc G) |
|---|
| 29 | (λenv.joint_final G (jglobals … env) env) |
|---|
| 30 | (λenv.λst.! st' ← eval_state … env st ; |
|---|
| 31 | let charge ≝ match joint_label_of_pc env (pc … st) with |
|---|
| 32 | [ Some c ⇒ Echarge c | None ⇒ E0 ] in |
|---|
| 33 | return 〈charge, st'〉). |
|---|
| 34 | |
|---|
| 35 | definition joint_fullexec : |
|---|
| 36 | sem_params → fullexec io_out io_in ≝ |
|---|
| 37 | λG.mk_fullexec ?? (joint_program G × (ident → option ℕ)) |
|---|
| 38 | (joint_exec G) |
|---|
| 39 | (make_joint_global G) |
|---|
| 40 | (λp_stacks. |
|---|
| 41 | return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))). |
|---|
| 42 | |
|---|
| 43 | definition joint_preclassified_system : sem_params → |
|---|
| 44 | preclassified_system ≝ |
|---|
| 45 | λG.mk_preclassified_system (joint_fullexec G) |
|---|
| 46 | (λenv.λst.¬is_none … (joint_label_of_pc (eval_params_of_global … env) (pc … st))) |
|---|
| 47 | (λenv.joint_classify (eval_params_of_global … env)) |
|---|
| 48 | (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env) s). |
|---|
