| 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 genv ≝ globalenv_noinit ? p in |
|---|
| 23 | let get_pc_lbl ≝ λid,lbl. |
|---|
| 24 | ! bl ← block_of_funct_id … pars genv id ; |
|---|
| 25 | pc_of_label … genv bl lbl in |
|---|
| 26 | mk_joint_global pars |
|---|
| 27 | (prog_var_names ?? p) |
|---|
| 28 | (mk_genv_gen ?? genv ? stack_sizes get_pc_lbl). |
|---|
| 29 | (* (prog_io pars) *). |
|---|
| 30 | #s #H |
|---|
| 31 | elim (find_symbol_exists … p s ?) |
|---|
| 32 | [ #bl #EQ >EQ % #ABS destruct(ABS)|*:] |
|---|
| 33 | @Exists_append_r |
|---|
| 34 | @(Exists_mp … H) // |
|---|
| 35 | qed. |
|---|
| 36 | |
|---|
| 37 | definition joint_exec: sem_params → trans_system io_out io_in ≝ |
|---|
| 38 | λG.mk_trans_system ?? (joint_global G) (λ_. state_pc G) |
|---|
| 39 | (λenv.is_final G (jglobals … env) env exit_pc) |
|---|
| 40 | (λenv.λst.! st' ← eval_state … env st ; |
|---|
| 41 | let charge ≝ match joint_label_of_pc env (pc … st) with |
|---|
| 42 | [ Some c ⇒ Echarge c | None ⇒ E0 ] in |
|---|
| 43 | return 〈charge, st'〉). |
|---|
| 44 | |
|---|
| 45 | definition joint_fullexec : |
|---|
| 46 | sem_params → fullexec io_out io_in ≝ |
|---|
| 47 | λG.mk_fullexec ?? (joint_program G × (ident → option ℕ)) |
|---|
| 48 | (joint_exec G) |
|---|
| 49 | (make_joint_global G) |
|---|
| 50 | (λp_stacks. |
|---|
| 51 | make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))). |
|---|
| 52 | |
|---|
| 53 | definition joint_preclassified_system : sem_params → |
|---|
| 54 | preclassified_system ≝ |
|---|
| 55 | λG.mk_preclassified_system (joint_fullexec G) |
|---|
| 56 | (λenv.λst.¬is_none … (joint_label_of_pc (eval_params_of_global … env) (pc … st))) |
|---|
| 57 | (λenv.joint_classify (eval_params_of_global … env)) |
|---|
| 58 | (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env) s). |
|---|
