Changeset 2875 for src/semantics.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/semantics.ma

    r2841 r2875  
    99include "LTL/LTL_semantics.ma".
    1010include "LIN/LIN_semantics.ma".
     11include "ASM/Interpret2.ma".
    1112
    1213record preclassified_system_pass (P:pass) : Type[2] ≝
     
    1617
    1718definition preclassified_system_of_pass:
    18  ∀pass. preclassified_system_pass pass ≝
     19 ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝
    1920 λpass.
    20   match pass with
    21   [ 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 …
    2728  | 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) …
    2930  | 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) …
    3132  | ertl_pass ⇒
    32      mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
     33     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
    3334  | ertlptr_pass ⇒
    34      mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
     35     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
    3536  | ltl_pass ⇒
    36      mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
     37     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
    3738  | 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) …
    3944  ].
    40 %
     45try % cases daemon
    4146qed.
    4247
     
    4651
    4752 λpass,prog,n,print_pass,print_event,print_error,print_exit.
    48  let pcs ≝ preclassified_system_of_pass pass in
     53 let pcs ≝ preclassified_system_of_pass pass prog in
    4954  let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
    5055  let g ≝ make_global … pcs prog in
Note: See TracChangeset for help on using the changeset viewer.