blob: f5339339ee94f5ef43aa0f3fcefc4e4978dac850 (
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
|
(** 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::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 ->
begin match list_nth_mut_loop_loop0_fwd t tl i0 with
| Fail e -> Fail e
| Return x0 -> Return x0
end
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 =
begin match list_nth_mut_loop_loop0_fwd t ls i with
| Fail e -> Fail e
| Return x -> Return x
end
(** [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) =
begin match list_nth_mut_loop_loop0_back t ls i ret with
| Fail e -> Fail e
| Return l -> Return l
end
|
