blob: 4d6e99ba54ceb42ffa442d30ecaf32d8134aa215 (
plain)
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [paper] *)
open primitivesLib divDefLib
val _ = new_theory "paper"
val ref_incr_fwd_back_def = Define ‘
(** [paper::ref_incr] *)
ref_incr_fwd_back (x : i32) : i32 result =
i32_add x (int_to_i32 1)
’
val test_incr_fwd_def = Define ‘
(** [paper::test_incr] *)
test_incr_fwd : unit result =
do
x <- ref_incr_fwd_back (int_to_i32 0);
if ~ (x = int_to_i32 1) then Fail Failure else Return ()
od
’
(** Unit test for [paper::test_incr] *)
val _ = assert_return (“test_incr_fwd”)
val choose_fwd_def = Define ‘
(** [paper::choose] *)
choose_fwd (b : bool) (x : 't) (y : 't) : 't result =
if b then Return x else Return y
’
val choose_back_def = Define ‘
(** [paper::choose] *)
choose_back (b : bool) (x : 't) (y : 't) (ret : 't) : ('t # 't) result =
if b then Return (ret, y) else Return (x, ret)
’
val test_choose_fwd_def = Define ‘
(** [paper::test_choose] *)
test_choose_fwd : unit result =
do
z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
z0 <- i32_add z (int_to_i32 1);
if ~ (z0 = int_to_i32 1)
then Fail Failure
else (
do
(x, y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
if ~ (x = int_to_i32 1)
then Fail Failure
else if ~ (y = int_to_i32 0) then Fail Failure else Return ()
od)
od
’
(** Unit test for [paper::test_choose] *)
val _ = assert_return (“test_choose_fwd”)
Datatype:
(** [paper::List] *)
list_t = | ListCons 't list_t | ListNil
End
val [list_nth_mut_fwd_def] = DefineDiv ‘
(** [paper::list_nth_mut] *)
list_nth_mut_fwd (l : 't list_t) (i : u32) : 't result =
(case l of
| ListCons x tl =>
if i = int_to_u32 0
then Return x
else (do
i0 <- u32_sub i (int_to_u32 1);
list_nth_mut_fwd tl i0
od)
| ListNil => Fail Failure)
’
val [list_nth_mut_back_def] = DefineDiv ‘
(** [paper::list_nth_mut] *)
list_nth_mut_back (l : 't list_t) (i : u32) (ret : 't) : 't list_t result =
(case l of
| ListCons x tl =>
if i = int_to_u32 0
then Return (ListCons ret tl)
else (
do
i0 <- u32_sub i (int_to_u32 1);
tl0 <- list_nth_mut_back tl i0 ret;
Return (ListCons x tl0)
od)
| ListNil => Fail Failure)
’
val [sum_fwd_def] = DefineDiv ‘
(** [paper::sum] *)
sum_fwd (l : i32 list_t) : i32 result =
(case l of
| ListCons x tl => do
i <- sum_fwd tl;
i32_add x i
od
| ListNil => Return (int_to_i32 0))
’
val test_nth_fwd_def = Define ‘
(** [paper::test_nth] *)
test_nth_fwd : unit result =
let l = ListNil in
let l0 = ListCons (int_to_i32 3) l in
let l1 = ListCons (int_to_i32 2) l0 in
do
x <- list_nth_mut_fwd (ListCons (int_to_i32 1) l1) (int_to_u32 2);
x0 <- i32_add x (int_to_i32 1);
l2 <- list_nth_mut_back (ListCons (int_to_i32 1) l1) (int_to_u32 2) x0;
i <- sum_fwd l2;
if ~ (i = int_to_i32 7) then Fail Failure else Return ()
od
’
(** Unit test for [paper::test_nth] *)
val _ = assert_return (“test_nth_fwd”)
val call_choose_fwd_def = Define ‘
(** [paper::call_choose] *)
call_choose_fwd (p : (u32 # u32)) : u32 result =
let (px, py) = p in
do
pz <- choose_fwd T px py;
pz0 <- u32_add pz (int_to_u32 1);
(px0, _) <- choose_back T px py pz0;
Return px0
od
’
val _ = export_theory ()
|
