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

Last change on this file since 2645 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
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 init 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 init 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.