blob: 3ac5b6ca0fe1a626b6fb57f93eeb7d6977bf1780 (
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
136
|
(** 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]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
ref_incr_fwd_back (x : i32) : i32 result =
i32_add x (int_to_i32 1)
’
val test_incr_fwd_def = Define ‘
(** [paper::test_incr]: forward function *)
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]: forward function *)
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]: backward function 0 *)
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]: forward function *)
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]: forward function *)
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]: backward function 0 *)
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]: forward function *)
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]: forward function *)
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]: forward function *)
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 ()
|
