From aa8e74197687ecc6d8f925babc8ba3cd6c739990 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 18 Jun 2024 22:47:35 +0200
Subject: Support for renaming using the rename attribute in charon (#239)

* support for renaming using the rename attribute in charon

* support for global decl

* add support for renaming field

* applied suggested changes and began adding support for variant

* finished support for renaming variant

* applied suggested changes

* add tests

* fixed variant and field renaming

* update charon-pin

* update flake.lock

* Update the charon pin

* Fix an issue with renaming trait method implementations

* Fix an issue with the renaming of trait implementations

* Fix an issue when renaming enumerations

* Update the Charon pin

* Fix the F* tests

* Fix an issue with the spans for the loops

* Fix the tests

* Update a comment

* Use fuel in the coq tests

* Generate the template decreases clauses by default

---------

Co-authored-by: Escherichia <escherichia@charlotte>
Co-authored-by: Son Ho <hosonmarc@gmail.com>---
 tests/coq/rename_attribute/RenameAttribute.v | 103 +++++++++++++++++++++++++++
 1 file changed, 103 insertions(+)
 create mode 100644 tests/coq/rename_attribute/RenameAttribute.v

(limited to 'tests/coq/rename_attribute/RenameAttribute.v')

diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v
new file mode 100644
index 00000000..3ce7ba5c
--- /dev/null
+++ b/tests/coq/rename_attribute/RenameAttribute.v
@@ -0,0 +1,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.
-- 
cgit v1.2.3