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
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [paper] *)
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
Require Import List.
Import ListNotations.
Local Open Scope Primitives_scope.
Module Paper.
(** [paper::ref_incr]: merged forward/backward function
(there is a single backward function, and the forward function returns ())
Source: 'src/paper.rs', lines 4:0-4:28 *)
Definition ref_incr (x : i32) : result i32 :=
i32_add x 1%i32.
(** [paper::test_incr]: forward function
Source: 'src/paper.rs', lines 8:0-8:18 *)
Definition test_incr : result unit :=
x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_incr] *)
Check (test_incr )%return.
(** [paper::choose]: forward function
Source: 'src/paper.rs', lines 15:0-15:70 *)
Definition choose (T : Type) (b : bool) (x : T) (y : T) : result T :=
if b then Return x else Return y
.
(** [paper::choose]: backward function 0
Source: 'src/paper.rs', lines 15:0-15:70 *)
Definition choose_back
(T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) :=
if b then Return (ret, y) else Return (x, ret)
.
(** [paper::test_choose]: forward function
Source: 'src/paper.rs', lines 23:0-23:20 *)
Definition test_choose : result unit :=
z <- choose i32 true 0%i32 0%i32;
z0 <- i32_add z 1%i32;
if negb (z0 s= 1%i32)
then Fail_ Failure
else (
p <- choose_back i32 true 0%i32 0%i32 z0;
let (x, y) := p in
if negb (x s= 1%i32)
then Fail_ Failure
else if negb (y s= 0%i32) then Fail_ Failure else Return tt)
.
(** Unit test for [paper::test_choose] *)
Check (test_choose )%return.
(** [paper::List]
Source: 'src/paper.rs', lines 35:0-35:16 *)
Inductive List_t (T : Type) :=
| List_Cons : T -> List_t T -> List_t T
| List_Nil : List_t T
.
Arguments List_Cons { _ }.
Arguments List_Nil { _ }.
(** [paper::list_nth_mut]: forward function
Source: 'src/paper.rs', lines 42:0-42:67 *)
Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result T :=
match l with
| List_Cons x tl =>
if i s= 0%u32
then Return x
else (i0 <- u32_sub i 1%u32; list_nth_mut T tl i0)
| List_Nil => Fail_ Failure
end
.
(** [paper::list_nth_mut]: backward function 0
Source: 'src/paper.rs', lines 42:0-42:67 *)
Fixpoint list_nth_mut_back
(T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
match l with
| List_Cons x tl =>
if i s= 0%u32
then Return (List_Cons ret tl)
else (
i0 <- u32_sub i 1%u32;
tl0 <- list_nth_mut_back T tl i0 ret;
Return (List_Cons x tl0))
| List_Nil => Fail_ Failure
end
.
(** [paper::sum]: forward function
Source: 'src/paper.rs', lines 57:0-57:32 *)
Fixpoint sum (l : List_t i32) : result i32 :=
match l with
| List_Cons x tl => i <- sum tl; i32_add x i
| List_Nil => Return 0%i32
end
.
(** [paper::test_nth]: forward function
Source: 'src/paper.rs', lines 68:0-68:17 *)
Definition test_nth : result unit :=
let l := List_Nil in
let l0 := List_Cons 3%i32 l in
let l1 := List_Cons 2%i32 l0 in
x <- list_nth_mut i32 (List_Cons 1%i32 l1) 2%u32;
x0 <- i32_add x 1%i32;
l2 <- list_nth_mut_back i32 (List_Cons 1%i32 l1) 2%u32 x0;
i <- sum l2;
if negb (i s= 7%i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_nth] *)
Check (test_nth )%return.
(** [paper::call_choose]: forward function
Source: 'src/paper.rs', lines 76:0-76:44 *)
Definition call_choose (p : (u32 * u32)) : result u32 :=
let (px, py) := p in
pz <- choose u32 true px py;
pz0 <- u32_add pz 1%u32;
p0 <- choose_back u32 true px py pz0;
let (px0, _) := p0 in
Return px0
.
End Paper.
|
