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
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [rename_attribute] *)
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
Require Import List.
Import ListNotations.
Local Open Scope Primitives_scope.
Module RenameAttribute.
(** Trait declaration: [rename_attribute::BoolTrait]
Source: 'tests/src/rename_attribute.rs', lines 8:0-8:19 *)
Record BoolTest_t (Self : Type) := mkBoolTest_t {
BoolTest_t_getTest : Self -> result bool;
}.
Arguments mkBoolTest_t { _ }.
Arguments BoolTest_t_getTest { _ }.
(** [rename_attribute::{(rename_attribute::BoolTrait for bool)}::get_bool]:
Source: 'tests/src/rename_attribute.rs', lines 22:4-22:30 *)
Definition boolTraitBool_getTest (self : bool) : result bool :=
Ok self.
(** Trait implementation: [rename_attribute::{(rename_attribute::BoolTrait for bool)}]
Source: 'tests/src/rename_attribute.rs', lines 21:0-21:23 *)
Definition BoolImpl : BoolTest_t bool := {|
BoolTest_t_getTest := boolTraitBool_getTest;
|}.
(** [rename_attribute::BoolTrait::ret_true]:
Source: 'tests/src/rename_attribute.rs', lines 15:4-15:30 *)
Definition boolTrait_retTest
{Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool :=
Ok true
.
(** [rename_attribute::test_bool_trait]:
Source: 'tests/src/rename_attribute.rs', lines 28:0-28:42 *)
Definition boolFn (T : Type) (x : bool) : result bool :=
b <- boolTraitBool_getTest x;
if b then boolTrait_retTest BoolImpl x else Ok false
.
(** [rename_attribute::SimpleEnum]
Source: 'tests/src/rename_attribute.rs', lines 36:0-36:15 *)
Inductive VariantsTest_t :=
| VariantsTest_Variant1 : VariantsTest_t
| VariantsTest_SecondVariant : VariantsTest_t
| VariantsTest_ThirdVariant : VariantsTest_t
.
(** [rename_attribute::Foo]
Source: 'tests/src/rename_attribute.rs', lines 44:0-44:10 *)
Record StructTest_t := mkStructTest_t { structTest_FieldTest : u32; }.
(** [rename_attribute::C]
Source: 'tests/src/rename_attribute.rs', lines 50:0-50:12 *)
Definition const_test_body : result u32 :=
i <- u32_add 100%u32 10%u32; u32_add i 1%u32
.
Definition const_test : u32 := const_test_body%global.
(** [rename_attribute::CA]
Source: 'tests/src/rename_attribute.rs', lines 53:0-53:13 *)
Definition const_aeneas11_body : result u32 := u32_add 10%u32 1%u32.
Definition const_aeneas11 : u32 := const_aeneas11_body%global.
(** [rename_attribute::factorial]:
Source: 'tests/src/rename_attribute.rs', lines 56:0-56:27 *)
Fixpoint factfn (n : nat) (n1 : u64) : result u64 :=
match n with
| O => Fail_ OutOfFuel
| S n2 =>
if n1 s<= 1%u64
then Ok 1%u64
else (i <- u64_sub n1 1%u64; i1 <- factfn n2 i; u64_mul n1 i1)
end
.
(** [rename_attribute::sum]: loop 0:
Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 *)
Fixpoint no_borrows_sum_loop
(n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
match n with
| O => Fail_ OutOfFuel
| S n1 =>
if i s< max
then (
s1 <- u32_add s i;
i1 <- u32_add i 1%u32;
no_borrows_sum_loop n1 max i1 s1)
else u32_mul s 2%u32
end
.
(** [rename_attribute::sum]:
Source: 'tests/src/rename_attribute.rs', lines 65:0-65:27 *)
Definition no_borrows_sum (n : nat) (max : u32) : result u32 :=
no_borrows_sum_loop n max 0%u32 0%u32
.
End RenameAttribute.
|
