source: src/joint/joint_fullexec.ma

Last change on this file was 2968, checked in by sacerdot, 7 years ago

The initial status memory was not really initialized. Now it is.

File size: 1.0 KB
Line 
1include "joint/Traces.ma".
2include "common/Measurable.ma".
3
4definition joint_exec: sem_params → trans_system io_out io_in ≝
5  λG.mk_trans_system ?? (evaluation_params G)  (λ_. state_pc G)
6   (λenv.joint_final … env)
7   (λenv.λst.! st' ← eval_state … env st ;
8    let charge ≝ match joint_label_of_pc … env (pc … st) with
9      [ Some c ⇒ Echarge c | None ⇒ E0 ] in
10     return 〈charge, st'〉).
11
12definition joint_fullexec :
13  sem_params → fullexec io_out io_in ≝
14  λG.mk_fullexec ?? (joint_program G × (ident → option ℕ))
15    (joint_exec G)
16    (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr)))
17    (λp_stacks.
18      make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
19
20definition joint_preclassified_system : sem_params →
21  preclassified_system ≝
22  λG.mk_preclassified_system (joint_fullexec G)
23    (λenv.λst.¬is_none … (joint_label_of_pc  … env (pc … st)))
24    (λenv.joint_classify … env)
25    (λenv.λs.λ_.joint_call_ident … env s).
Note: See TracBrowser for help on using the repository browser.