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). |
---|