source: src/joint/joint_fullexec.ma @ 2939

Last change on this file since 2939 was 2821, checked in by tranquil, 7 years ago
  • implemented preclassified system for joint (in joint/joint_fullexec.ma)
File size: 2.0 KB
Line 
1include "joint/Traces.ma".
2include "common/Measurable.ma".
3
4(* fullexec and co. *)
5record joint_global (p : sem_params) : Type[0] ≝
6{ jglobals : list ident
7; jgenv :> genv p jglobals
8}.
9
10definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝
11λp,gl.mk_evaluation_params (jglobals … gl) p gl.
12
13coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝
14eval_params_of_global on _gl : joint_global ? to evaluation_params.
15
16definition make_joint_global : ∀p : sem_params.
17  (joint_program p × (ident → option ℕ)) →
18  joint_global p ≝
19λpars, p_stack.
20let p ≝ \fst p_stack in
21let stack_sizes ≝ \snd p_stack in
22let genv ≝ globalenv_noinit ? p in
23let get_pc_lbl ≝ λid,lbl.
24  ! bl ← block_of_funct_id … pars genv id ;
25  pc_of_label … genv bl lbl in
26mk_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
31elim (find_symbol_exists … p s ?)
32[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
33@Exists_append_r
34@(Exists_mp … H) //
35qed.
36
37definition 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
45definition 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
53definition 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).
Note: See TracBrowser for help on using the repository browser.