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