-
Notifications
You must be signed in to change notification settings - Fork 25
/
tests.v
87 lines (61 loc) · 2.5 KB
/
tests.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
From CertiCoq.Plugin Require Import CertiCoq.
Require Import Arith PArith List String Ascii.
Require Import ExtLib.Data.String.
Import ListNotations.
(* Example 1: printing axioms *)
Axiom (print_nat : nat -> unit).
Axiom (print_str : string -> unit).
Axiom (new_line : unit -> unit).
Definition print_list (l : list nat) : unit :=
let aux :=
fix aux l :=
match l with
| [] => tt
| [x] => print_nat x
| x :: l =>
let _ := print_nat x in
let _ := print_str ";" in
aux l
end in
let _ := print_str "[" in
let _ := aux l in
let _ := print_str "]" in new_line tt.
Definition print_lst := print_list [1;2;3;4;5].
CertiCoq Compile print_lst
Extract Constants [ print_nat => "print_gallina_nat", print_str => "print_gallina_string", new_line => "print_new_line" ]
Include [ "print.h" ].
(* Example 2: int 63 *)
Axiom (int63 : Type).
Axiom (add_int63 : int63 -> int63 -> int63).
Axiom (minus : int63 -> int63 -> int63).
Axiom (mul : int63 -> int63 -> int63).
Axiom (print_int63 : int63 -> unit).
Axiom (zero_int63 : int63).
Axiom (one_int63 : int63).
Fixpoint fib_aux (n : nat) (prev0 prev1 : int63) :=
match n with
| 0 => prev0
| 1 => prev1
| S n => fib_aux n prev1 (add_int63 prev0 prev1)
end.
Definition fib (n : nat) := fib_aux n zero_int63 one_int63.
Definition fibn : unit :=
let _ := print_int63 (fib 11) in
new_line tt.
CertiCoq Compile fibn
Extract Constants [ add_int63 => "add_int63", zero_int63 => "zero_int63", one_int63 => "one_int63", print_int63 => "print_int63", new_line => "print_new_line" ]
Include [ "int63.h" ].
(* Example 3: list_sum with int63 -- add_int63 is first class *)
Definition list_sum_int63 :=
let n := List.fold_left add_int63 (List.repeat one_int63 100) zero_int63 in
let _ := print_int63 n in new_line tt.
CertiCoq Compile list_sum_int63
Extract Constants [ add_int63 => "add_int63", zero_int63 => "zero_int63", one_int63 => "one_int63", print_int63 => "print_int63", new_line => "print_new_line" ]
Include [ "int63.h" ].
(* "Dummy" example with tinfo (tifno is not used by the C function) *)
Definition list_sum_int63_tinfo :=
let n := List.fold_left add_int63 (List.repeat one_int63 100) zero_int63 in
let _ := print_int63 n in new_line tt.
CertiCoq Compile list_sum_int63_tinfo
Extract Constants [ add_int63 => "add_int63" with tinfo, zero_int63 => "zero_int63", one_int63 => "one_int63", print_int63 => "print_int63" with tinfo, new_line => "print_new_line" ]
Include [ "int63_tinfo.h" ].