source: src/semantics.ma @ 2832

Last change on this file since 2832 was 2828, checked in by sacerdot, 7 years ago
  1. New semantics.ma file that puts together all semantics. It contains a function to observe the semantics of an intermediate program. Note: the type of backend semantics is currently wrong because of the stack cost! If you observe a back-end language now, it will core dump.
  2. Added observations into compiler.ma
File size: 2.5 KB
Line 
1include "compiler.ma".
2include "Clight/Clight_classified_system.ma".
3include "Cminor/Cminor_classified_system.ma".
4include "RTLabs/RTLabs_classified_system.ma".
5include "joint/joint_fullexec.ma".
6include "RTL/RTL_semantics.ma".
7include "ERTL/ERTL_semantics.ma".
8include "ERTLptr/ERTLptr_semantics.ma".
9include "LTL/LTL_semantics.ma".
10include "LIN/LIN_semantics.ma".
11
12record preclassified_system_pass (P:pass) : Type[2] ≝
13 { pcs_pcs:> preclassified_system
14 ; pcs_ok: syntax_of_pass P = program … pcs_pcs
15 }.
16
17definition preclassified_system_of_pass:
18 ∀pass. preclassified_system_pass pass ≝
19 λ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 …
27  | rtl_separate_pass ⇒
28     mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
29  | rtl_uniq_pass ⇒
30     mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
31  | ertl_pass ⇒
32     mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
33  | ertlptr_pass ⇒
34     mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
35  | ltl_pass ⇒
36     mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
37  | lin_pass ⇒
38     mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
39  ].
40try %
41whd in ⊢ (??%%);
42cases daemon (* XXX False! Leads to core dump! *)
43qed.
44
45definition run_and_print:
46 ∀pass'. syntax_of_pass pass' → nat →
47  (pass → unit) → (intensional_event → unit) → (errmsg → unit) → (int → unit) → unit
48
49 λpass,prog,n,print_pass,print_event,print_error,print_exit.
50 let pcs ≝ preclassified_system_of_pass pass in
51  let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
52  let g ≝ make_global … pcs prog in
53  match make_initial_state … pcs prog with
54  [ Error msg ⇒ print_error msg
55  | OK s0 ⇒
56     let i ≝ print_pass pass in
57     let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in
58     match res with
59     [ OK n ⇒ print_exit n
60     | Error msg ⇒ print_error msg ]].
61@pcs_ok
62qed.
Note: See TracBrowser for help on using the repository browser.