include "compiler.ma". include "Clight/Clight_classified_system.ma". include "Cminor/Cminor_classified_system.ma". include "RTLabs/RTLabs_classified_system.ma". include "joint/joint_fullexec.ma". include "RTL/RTL_semantics.ma". include "ERTL/ERTL_semantics.ma". include "LTL/LTL_semantics.ma". include "LIN/LIN_semantics.ma". include "ASM/Interpret2.ma". record preclassified_system_pass (P:pass) : Type[2] ≝ { pcs_pcs:> preclassified_system ; pcs_ok: syntax_of_pass P = program … pcs_pcs }. definition preclassified_system_of_pass: ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝ λpass. match pass return λpass.syntax_of_pass pass → preclassified_system_pass pass with [ clight_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … | clight_switch_removed_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … | clight_label_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … | clight_simplified_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … | cminor_pass ⇒ λ_.mk_preclassified_system_pass … Cminor_pcs … | rtlabs_pass ⇒ λ_.mk_preclassified_system_pass … RTLabs_pcs … | rtl_separate_pass ⇒ λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) … | rtl_uniq_pass ⇒ λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) … | ertl_pass ⇒ λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) … | ltl_pass ⇒ λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) … | lin_pass ⇒ λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ? | assembly_pass ⇒ λprog. let 〈code,sigma,policy〉 ≝ prog in mk_preclassified_system_pass … (ASM_preclassified_system code sigma policy) … | object_code_pass ⇒ λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) … ]. % qed. definition run_and_print: ∀pass'. syntax_of_pass pass' → nat → (pass → unit) → (intensional_event → unit) → (errmsg → unit) → (int → unit) → unit ≝ λpass,prog,n,print_pass,print_event,print_error,print_exit. let pcs ≝ preclassified_system_of_pass pass prog in let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in let g ≝ make_global … pcs prog in match make_initial_state … pcs prog with [ Error msg ⇒ print_error msg | OK s0 ⇒ let i ≝ print_pass pass in let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in match res with [ OK n ⇒ print_exit n | Error msg ⇒ print_error msg ]]. @pcs_ok qed.