include "joint/Traces.ma". include "common/Measurable.ma". (* fullexec and co. *) record joint_global (p : sem_params) : Type[0] ≝ { jglobals : list ident ; jgenv :> genv p jglobals }. definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝ λp,gl.mk_evaluation_params (jglobals … gl) p gl. coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝ eval_params_of_global on _gl : joint_global ? to evaluation_params. definition make_joint_global : ∀p : sem_params. (joint_program p × (ident → option ℕ)) → joint_global p ≝ λpars, p_stack. let p ≝ \fst p_stack in let stack_sizes ≝ \snd p_stack in let genv ≝ globalenv_noinit ? p in let get_pc_lbl ≝ λid,lbl. ! bl ← block_of_funct_id … pars genv id ; pc_of_label … genv bl lbl in mk_joint_global pars (prog_var_names ?? p) (mk_genv_gen ?? genv ? stack_sizes get_pc_lbl). (* (prog_io pars) *). #s #H elim (find_symbol_exists … p s ?) [ #bl #EQ >EQ % #ABS destruct(ABS)|*:] @Exists_append_r @(Exists_mp … H) // qed. definition joint_exec: sem_params → trans_system io_out io_in ≝ λG.mk_trans_system ?? (joint_global G) (λ_. state_pc G) (λenv.is_final G (jglobals … env) env exit_pc) (λ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) (make_joint_global G) (λ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 (eval_params_of_global … env) (pc … st))) (λenv.joint_classify (eval_params_of_global … env)) (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env) s).