source: src/semantics.ma

Last change on this file was 3035, checked in by mckinna, 7 years ago

Tweak: tidied up ?/\ldots
Conceptual: better monadic threading of Error before final handling by print_exit/print_error: res should be implemented by ML-level raise/try_with.

File size: 2.6 KB
RevLine 
[2828]1include "compiler.ma".
2include "Clight/Clight_classified_system.ma".
3include "Cminor/Cminor_classified_system.ma".
4include "RTLabs/RTLabs_classified_system.ma".
5include "joint/joint_fullexec.ma".
6include "RTL/RTL_semantics.ma".
7include "ERTL/ERTL_semantics.ma".
8include "LTL/LTL_semantics.ma".
9include "LIN/LIN_semantics.ma".
[2875]10include "ASM/Interpret2.ma".
[2828]11
12record preclassified_system_pass (P:pass) : Type[2] ≝
13 { pcs_pcs:> preclassified_system
14 ; pcs_ok: syntax_of_pass P = program … pcs_pcs
15 }.
16
17definition preclassified_system_of_pass:
[2875]18 ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝
[2828]19 λpass.
[2875]20  match pass return λpass.syntax_of_pass pass → preclassified_system_pass pass with
21  [ clight_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
22  | clight_switch_removed_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
23  | clight_label_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
24  | clight_simplified_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
25  | cminor_pass ⇒ λ_.mk_preclassified_system_pass … Cminor_pcs …
26  | rtlabs_pass ⇒ λ_.mk_preclassified_system_pass … RTLabs_pcs …
[2828]27  | rtl_separate_pass ⇒
[2875]28     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
[2828]29  | rtl_uniq_pass ⇒
[2875]30     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
[2828]31  | ertl_pass ⇒
[2875]32     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
[2828]33  | ltl_pass ⇒
[2875]34     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
[2828]35  | lin_pass ⇒
[3035]36     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) …
[2875]37  | assembly_pass ⇒
[2899]38     λprog. let 〈code,sigma,policy〉 ≝ prog in
[2905]39      mk_preclassified_system_pass … (ASM_preclassified_system code sigma policy) …
[2875]40  | object_code_pass ⇒
[3035]41     λprog. mk_preclassified_system_pass … (OC_preclassified_system prog) …
[2828]42  ].
[2899]43%
[2828]44qed.
45
46definition run_and_print:
47 ∀pass'. syntax_of_pass pass' → nat →
48  (pass → unit) → (intensional_event → unit) → (errmsg → unit) → (int → unit) → unit
49
50 λpass,prog,n,print_pass,print_event,print_error,print_exit.
[3035]51 let res ≝
52  let pcs ≝ preclassified_system_of_pass pass prog in
[2828]53  let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
54  let g ≝ make_global … pcs prog in
[3035]55  ! s0 ← make_initial_state … pcs prog ;
56  let i ≝ print_pass pass in
57  let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in
58    res
59 in
60    match res with
[2828]61     [ OK n ⇒ print_exit n
[3035]62     | Error msg ⇒ print_error msg ]
63.
[2828]64@pcs_ok
[2899]65qed.
Note: See TracBrowser for help on using the repository browser.