source: src/Clight/test/sum.test.ma @ 2253

Last change on this file since 2253 was 2253, checked in by campbell, 7 years ago

Cminor to RTLabs is now a total function.

File size: 2.0 KB
Line 
1include "Clight/test/sum.c.ma".
2
3example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
4normalize  (* you can examine the result here *)
5%
6qed.
7
8include "Clight/SimplifyCasts.ma".
9
10example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
11normalize  (* you can examine the result here *)
12%
13qed.
14
15include "Clight/toCminor.ma".
16include "Cminor/semantics.ma".
17
18example e1: finishes_with (repr I32 74) ?
19  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
20   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
21normalize
22%
23qed.
24
25include "Cminor/toRTLabs.ma".
26include "RTLabs/semantics.ma".
27
28example e2: finishes_with (repr I32 74) ? (
29bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
30(λp1. let p2 ≝ cminor_to_rtlabs p1 in
31  exec_up_to RTLabs_fullexec p2 1000 [ ])).
32normalize
33%
34qed.
35(*
36include "RTLabs/RTLabsToRTL.ma".
37include alias "basics/lists/list.ma".
38
39definition take_out: ∀A. res A → A ≝
40 λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
41cases daemon
42qed.
43
44example CSC: True.
45letin xxx ≝
46 (let p ≝ take_out … (clight_to_cminor myprog) in
47  let p ≝ take_out … (cminor_to_rtlabs p) in
48(*   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *)
49  let p ≝ rtlabs_to_rtl p in
50   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p))
51 )
52[2: cases daemon]
53normalize in xxx;
54
55
56[2:
57  OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ? | Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p)))
58(*  OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)))
59*)
60[2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
61normalize in xxx
62*)
Note: See TracBrowser for help on using the repository browser.