blob: a2ae256391a37b5f12485ff77c74395f4e6668ce (
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
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [loops]: function definitions *)
module Loops.Funs
open Primitives
include Loops.Types
include Loops.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [loops::sum] *)
let rec sum_loop0_fwd
(max : u32) (i : u32) (s : u32) :
Tot (result u32) (decreases (sum_decreases max i s))
=
if i < max
then
begin match u32_add s i with
| Fail e -> Fail e
| Return s0 ->
begin match u32_add i 1 with
| Fail e -> Fail e
| Return i0 -> sum_loop0_fwd max i0 s0
end
end
else u32_mul s 2
(** [loops::sum] *)
let sum_fwd (max : u32) : result u32 = sum_loop0_fwd max 0 0
(** [loops::list_nth_mut_loop] *)
let rec list_nth_mut_loop_loop0_fwd
(t : Type0) (ls : list_t t) (i : u32) :
Tot (result t) (decreases (list_nth_mut_loop_decreases t ls i))
=
begin match ls with
| ListCons x tl ->
if i = 0
then Return x
else
begin match u32_sub i 1 with
| Fail e -> Fail e
| Return i0 -> list_nth_mut_loop_loop0_fwd t tl i0
end
| ListNil -> Fail Failure
end
(** [loops::list_nth_mut_loop] *)
let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
list_nth_mut_loop_loop0_fwd t ls i
(** [loops::list_nth_mut_loop] *)
let rec list_nth_mut_loop_loop0_back
(t : Type0) (ls : list_t t) (i : u32) (ret : t) :
Tot (result (list_t t)) (decreases (list_nth_mut_loop_decreases t ls i))
=
begin match ls 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_loop_loop0_back t tl i0 ret with
| Fail e -> Fail e
| Return l -> Return (ListCons x l)
end
end
| ListNil -> Fail Failure
end
(** [loops::list_nth_mut_loop] *)
let list_nth_mut_loop_back
(t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
list_nth_mut_loop_loop0_back t ls i ret
|
