Changeset 2875 for src/semantics.ma
- Timestamp:
- Mar 15, 2013, 1:32:50 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/semantics.ma
r2841 r2875 9 9 include "LTL/LTL_semantics.ma". 10 10 include "LIN/LIN_semantics.ma". 11 include "ASM/Interpret2.ma". 11 12 12 13 record preclassified_system_pass (P:pass) : Type[2] ≝ … … 16 17 17 18 definition preclassified_system_of_pass: 18 ∀pass. preclassified_system_pass pass ≝19 ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝ 19 20 λpass. 20 match pass with21 [ 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 …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 … 27 28 | rtl_separate_pass ⇒ 28 mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …29 λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) … 29 30 | rtl_uniq_pass ⇒ 30 mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …31 λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) … 31 32 | ertl_pass ⇒ 32 mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …33 λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) … 33 34 | ertlptr_pass ⇒ 34 mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …35 λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) … 35 36 | ltl_pass ⇒ 36 mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …37 λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) … 37 38 | lin_pass ⇒ 38 mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ? 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) … 39 44 ]. 40 % 45 try % cases daemon 41 46 qed. 42 47 … … 46 51 ≝ 47 52 λpass,prog,n,print_pass,print_event,print_error,print_exit. 48 let pcs ≝ preclassified_system_of_pass pass in53 let pcs ≝ preclassified_system_of_pass pass prog in 49 54 let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in 50 55 let g ≝ make_global … pcs prog in
Note: See TracChangeset
for help on using the changeset viewer.