blob: 0f8604d10581022a14c6596e1a48fe2951e83016 (
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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [paper] *)
module Paper
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [paper::ref_incr] *)
let ref_incr_fwd_back (x : i32) : result i32 =
begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end
(** [paper::test_incr] *)
let test_incr_fwd : result unit =
begin match ref_incr_fwd_back 0 with
| Fail e -> Fail e
| Return x -> if not (x = 1) then Fail Failure else Return ()
end
(** Unit test for [paper::test_incr] *)
let _ = assert_norm (test_incr_fwd = Return ())
(** [paper::choose] *)
let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
if b then Return x else Return y
(** [paper::choose] *)
let choose_back
(t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
if b then Return (ret, y) else Return (x, ret)
(** [paper::test_choose] *)
let test_choose_fwd : result unit =
begin match choose_fwd i32 true 0 0 with
| Fail e -> Fail e
| Return z ->
begin match i32_add z 1 with
| Fail e -> Fail e
| Return z0 ->
if not (z0 = 1)
then Fail Failure
else
begin match choose_back i32 true 0 0 z0 with
| Fail e -> Fail e
| Return (x, y) ->
if not (x = 1)
then Fail Failure
else if not (y = 0) then Fail Failure else Return ()
end
end
end
(** Unit test for [paper::test_choose] *)
let _ = assert_norm (test_choose_fwd = Return ())
(** [paper::List] *)
type list_t (t : Type0) =
| ListCons : t -> list_t t -> list_t t
| ListNil : list_t t
(** [paper::list_nth_mut] *)
let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
begin match l with
| ListCons x tl ->
if i = 0
then Return x
else
begin match u32_sub i 1 with
| Fail e -> Fail e
| Return i0 ->
begin match list_nth_mut_fwd t tl i0 with
| Fail e -> Fail e
| Return x0 -> Return x0
end
end
| ListNil -> Fail Failure
end
(** [paper::list_nth_mut] *)
let rec list_nth_mut_back
(t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
begin match l with
| ListCons x tl ->
if i = 0
then Return (ListCons ret tl)
else
begin match u32_sub i 1 with
| Fail e -> Fail e
| Return i0 ->
begin match list_nth_mut_back t tl i0 ret with
| Fail e -> Fail e
| Return tl0 -> Return (ListCons x tl0)
end
end
| ListNil -> Fail Failure
end
(** [paper::sum] *)
let rec sum_fwd (l : list_t i32) : result i32 =
begin match l with
| ListCons x tl ->
begin match sum_fwd tl with
| Fail e -> Fail e
| Return i ->
begin match i32_add x i with
| Fail e -> Fail e
| Return i0 -> Return i0
end
end
| ListNil -> Return 0
end
(** [paper::test_nth] *)
let test_nth_fwd : result unit =
let l = ListNil in
let l0 = ListCons 3 l in
let l1 = ListCons 2 l0 in
begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
| Fail e -> Fail e
| Return x ->
begin match i32_add x 1 with
| Fail e -> Fail e
| Return x0 ->
begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
| Fail e -> Fail e
| Return l2 ->
begin match sum_fwd l2 with
| Fail e -> Fail e
| Return i -> if not (i = 7) then Fail Failure else Return ()
end
end
end
end
(** Unit test for [paper::test_nth] *)
let _ = assert_norm (test_nth_fwd = Return ())
(** [paper::call_choose] *)
let call_choose_fwd (p : (u32 & u32)) : result u32 =
let (px, py) = p in
begin match choose_fwd u32 true px py with
| Fail e -> Fail e
| Return pz ->
begin match u32_add pz 1 with
| Fail e -> Fail e
| Return pz0 ->
begin match choose_back u32 true px py pz0 with
| Fail e -> Fail e
| Return (px0, _) -> Return px0
end
end
end
|
