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

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

Remove init from a testcase.

File size: 2.9 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/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/RTLabs_semantics.ma".
27include "Clight/label.ma".
28
29example e2: finishes_with (repr I32 74) ? (
30let 〈p0,init〉 ≝ clight_label myprog in
31bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
32(λp1. let p2 ≝ cminor_to_rtlabs p1 in
33  exec_up_to RTLabs_fullexec p2 1000 [ ])).
34normalize
35%
36qed.
37
38include "RTLabs/CostCheck.ma".
39
40definition readable_body ≝
41λfn. insert_sort ?
42       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
43       (elements ?? (f_graph fn)).
44(*
45example c2: result ? (
46  let 〈p0,init〉 ≝ clight_label myprog in
47  ! p1 ← clight_to_cminor (simplify_program p0);
48  let p2 ≝ cminor_to_rtlabs init p1 in
49  match prog_funct … p2 with
50  [ nil ⇒ Error ? (msg MISSING)
51  | cons h _ ⇒
52    match \snd h with
53    [ External _ ⇒ Error ? (msg EXTERNAL)
54    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
55    ]
56  ]).
57normalize
58*)
59example c2: (
60  let 〈p0,init〉 ≝ clight_label myprog in
61  ! p1 ← clight_to_cminor (simplify_program p0);
62  let p2 ≝ cminor_to_rtlabs p1 in
63  return (check_cost_program p2)) = OK bool true.
64normalize
65%
66qed.
67
68
69
70(*
71include "RTLabs/RTLabsToRTL.ma".
72include alias "basics/lists/list.ma".
73
74definition take_out: ∀A. res A → A ≝
75 λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
76cases daemon
77qed.
78
79example CSC: True.
80letin xxx ≝
81 (let p ≝ take_out … (clight_to_cminor myprog) in
82  let p ≝ take_out … (cminor_to_rtlabs p) in
83(*   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *)
84  let p ≝ rtlabs_to_rtl p in
85   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p))
86 )
87[2: cases daemon]
88normalize in xxx;
89
90
91[2:
92  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)))
93(*  OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)))
94*)
95[2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
96normalize in xxx
97*)
Note: See TracBrowser for help on using the repository browser.