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

Last change on this file since 1545 was 1515, checked in by campbell, 9 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.