Changeset 2875 for src/semantics.ma

Timestamp:

Mar 15, 2013, 1:32:50 AM (8 years ago)

Author:

sacerdot

Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File:

• src/semantics.ma (modified) (3 diffs)

src/semantics.ma

@@ -9 +9 @@
 include "LTL/LTL_semantics.ma".
 include "LIN/LIN_semantics.ma".
+include "ASM/Interpret2.ma".
 
 record preclassified_system_pass (P:pass) : Type[2] ≝
@@ -16 +17 @@
 
 definition preclassified_system_of_pass:
- ∀pass. preclassified_system_pass pass ≝
+ ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝
  λpass.
-  match 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 …
+  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) …
+     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
   | rtl_uniq_pass ⇒
-     mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
+     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
   | ertl_pass ⇒
-     mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
+     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
   | ertlptr_pass ⇒
-     mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
+     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
   | ltl_pass ⇒
-     mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
+     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
   | lin_pass ⇒
-     mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
+     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
+  | assembly_pass ⇒
+     ?
+  | object_code_pass ⇒
+     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
   ].
-%
+try % cases daemon
 qed.
 
@@ -46 +51 @@
 ≝
  λpass,prog,n,print_pass,print_event,print_error,print_exit.
- let pcs ≝ preclassified_system_of_pass pass in
+ let pcs ≝ preclassified_system_of_pass pass prog in
   let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
   let g ≝ make_global … pcs prog in