source: src/Clight/test/insertsort.test.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 2.1 KB
Line 
1(* Note that the c.ma file needs tweaked to have an Init_null at the end of the
2   list because acc doesn't use them *)
3
4include "Clight/test/insertsort.c.ma".
5
6(* The id for the function which outputs the sorted list. *)
7definition f_id ≝ 18.
8
9example exec:
10  (do s ← exec_up_to clight_fullexec myprog 1000
11     [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)];
12   match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? [ ] ]) = OK ?
13[EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0));
14 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0));
15 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0));
16 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0));
17 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0));
18 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0));
19 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))]
20.
21normalize  (* you can examine the result here *)
22@refl
23qed.
24
25include "Clight/label.ma".
26
27example labelled_exec:
28  (let p ≝ clight_label myprog in
29   do s ← exec_up_to clight_fullexec p 1000
30     [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)];
31   match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? [ ] ]) = OK ?
32[EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0));
33 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0));
34 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0));
35 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0));
36 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0));
37 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0));
38 EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))]
39.
40normalize  (* you can examine the result here *)
41@refl
42qed.
Note: See TracBrowser for help on using the repository browser.