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.