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
153
154
155
156
157
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [demo] *)
module Demo
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [demo::choose]:
Source: 'src/demo.rs', lines 5:0-5:70 *)
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
then let back = fun ret -> Ok (ret, y) in Ok (x, back)
else let back = fun ret -> Ok (x, ret) in Ok (y, back)
(** [demo::mul2_add1]:
Source: 'src/demo.rs', lines 13:0-13:31 *)
let mul2_add1 (x : u32) : result u32 =
let* i = u32_add x x in u32_add i 1
(** [demo::use_mul2_add1]:
Source: 'src/demo.rs', lines 17:0-17:43 *)
let use_mul2_add1 (x : u32) (y : u32) : result u32 =
let* i = mul2_add1 x in u32_add i y
(** [demo::incr]:
Source: 'src/demo.rs', lines 21:0-21:31 *)
let incr (x : u32) : result u32 =
u32_add x 1
(** [demo::use_incr]:
Source: 'src/demo.rs', lines 25:0-25:17 *)
let use_incr : result unit =
let* x = incr 0 in let* x1 = incr x in let* _ = incr x1 in Ok ()
(** [demo::CList]
Source: 'src/demo.rs', lines 34:0-34:17 *)
type cList_t (t : Type0) =
| CList_CCons : t -> cList_t t -> cList_t t
| CList_CNil : cList_t t
(** [demo::list_nth]:
Source: 'src/demo.rs', lines 39:0-39:56 *)
let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0 then Ok x else let* i1 = u32_sub i 1 in list_nth t n1 tl i1
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut]:
Source: 'src/demo.rs', lines 54:0-54:68 *)
let rec list_nth_mut
(t : Type0) (n : nat) (l : cList_t t) (i : u32) :
result (t & (t -> result (cList_t t)))
=
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0
then let back = fun ret -> Ok (CList_CCons ret tl) in Ok (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t n1 tl i1 in
let back =
fun ret -> let* tl1 = list_nth_mut_back ret in Ok (CList_CCons x tl1)
in
Ok (x1, back)
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut1]: loop 0:
Source: 'src/demo.rs', lines 69:0-78:1 *)
let rec list_nth_mut1_loop
(t : Type0) (n : nat) (l : cList_t t) (i : u32) :
result (t & (t -> result (cList_t t)))
=
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0
then let back = fun ret -> Ok (CList_CCons ret tl) in Ok (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, back) = list_nth_mut1_loop t n1 tl i1 in
let back1 = fun ret -> let* tl1 = back ret in Ok (CList_CCons x tl1) in
Ok (x1, back1)
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut1]:
Source: 'src/demo.rs', lines 69:0-69:77 *)
let list_nth_mut1
(t : Type0) (n : nat) (l : cList_t t) (i : u32) :
result (t & (t -> result (cList_t t)))
=
list_nth_mut1_loop t n l i
(** [demo::i32_id]:
Source: 'src/demo.rs', lines 80:0-80:28 *)
let rec i32_id (n : nat) (i : i32) : result i32 =
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
if i = 0
then Ok 0
else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1
(** [demo::list_tail]:
Source: 'src/demo.rs', lines 88:0-88:64 *)
let rec list_tail
(t : Type0) (n : nat) (l : cList_t t) :
result ((cList_t t) & (cList_t t -> result (cList_t t)))
=
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
let* (c, list_tail_back) = list_tail t n1 tl in
let back =
fun ret -> let* tl1 = list_tail_back ret in Ok (CList_CCons x tl1) in
Ok (c, back)
| CList_CNil -> Ok (CList_CNil, Ok)
end
(** Trait declaration: [demo::Counter]
Source: 'src/demo.rs', lines 97:0-97:17 *)
noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); }
(** [demo::{(demo::Counter for usize)}::incr]:
Source: 'src/demo.rs', lines 102:4-102:31 *)
let counterUsize_incr (self : usize) : result (usize & usize) =
let* self1 = usize_add self 1 in Ok (self, self1)
(** Trait implementation: [demo::{(demo::Counter for usize)}]
Source: 'src/demo.rs', lines 101:0-101:22 *)
let counterUsize : counter_t usize = { incr = counterUsize_incr; }
(** [demo::use_counter]:
Source: 'src/demo.rs', lines 109:0-109:59 *)
let use_counter
(t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) =
counterInst.incr cnt
|
