Merge pull request #49 from AeneasVerif/son_merge_back

Allow the extraction of structures as tuples

2 files changed, 36 insertions, 10 deletions

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 0c7dff8e..8ee8ad9e 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -35,7 +35,7 @@ inductive Enum :=
 
 /- [no_nested_borrows::EmptyStruct]
    Source: 'src/no_nested_borrows.rs', lines 39:0-39:22 -/
-structure EmptyStruct where
+@[reducible] def EmptyStruct := Unit
 
 /- [no_nested_borrows::Sum]
    Source: 'src/no_nested_borrows.rs', lines 41:0-41:20 -/
@@ -643,4 +643,33 @@ def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
 def test_shared_borrow_enum2 : Result U32 :=
   Result.ret 0#u32
 
+/- [no_nested_borrows::Tuple]
+   Source: 'src/no_nested_borrows.rs', lines 530:0-530:24 -/
+def Tuple (T1 T2 : Type) := T1 × T2
+
+/- [no_nested_borrows::use_tuple_struct]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ())
+   Source: 'src/no_nested_borrows.rs', lines 532:0-532:48 -/
+def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
+  Result.ret (1#u32, x.1)
+
+/- [no_nested_borrows::create_tuple_struct]: forward function
+   Source: 'src/no_nested_borrows.rs', lines 536:0-536:61 -/
+def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
+  Result.ret (x, y)
+
+/- [no_nested_borrows::IdType]
+   Source: 'src/no_nested_borrows.rs', lines 541:0-541:20 -/
+@[reducible] def IdType (T : Type) := T
+
+/- [no_nested_borrows::use_id_type]: forward function
+   Source: 'src/no_nested_borrows.rs', lines 543:0-543:40 -/
+def use_id_type (T : Type) (x : IdType T) : Result T :=
+  Result.ret x
+
+/- [no_nested_borrows::create_id_type]: forward function
+   Source: 'src/no_nested_borrows.rs', lines 547:0-547:43 -/
+def create_id_type (T : Type) (x : T) : Result (IdType T) :=
+  Result.ret x
+
 end no_nested_borrows
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 653384d6..17118203 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -190,13 +190,11 @@ def h4
 
 /- [traits::TestType]
    Source: 'src/traits.rs', lines 122:0-122:22 -/
-structure TestType (T : Type) where
-  _0 : T
+@[reducible] def TestType (T : Type) := T
 
 /- [traits::{traits::TestType<T>#6}::test::TestType1]
    Source: 'src/traits.rs', lines 127:8-127:24 -/
-structure TestType.test.TestType1 where
-  _0 : U64
+@[reducible] def TestType.test.TestType1 := U64
 
 /- Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
    Source: 'src/traits.rs', lines 128:8-128:23 -/
@@ -207,7 +205,7 @@ structure TestType.test.TestTrait (Self : Type) where
    Source: 'src/traits.rs', lines 139:12-139:34 -/
 def TestType.test.TestType1.test
   (self : TestType.test.TestType1) : Result Bool :=
-  Result.ret (self._0 > 1#u64)
+  Result.ret (self > 1#u64)
 
 /- Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
    Source: 'src/traits.rs', lines 138:8-138:36 -/
@@ -225,13 +223,12 @@ def TestType.test
   do
     let x0 ← ToU64TInst.to_u64 x
     if x0 > 0#u64
-    then TestType.test.TestType1.test { _0 := 0#u64 }
+    then TestType.test.TestType1.test 0#u64
     else Result.ret false
 
 /- [traits::BoolWrapper]
    Source: 'src/traits.rs', lines 150:0-150:22 -/
-structure BoolWrapper where
-  _0 : Bool
+@[reducible] def BoolWrapper := Bool
 
 /- [traits::{traits::BoolWrapper#7}::to_type]: forward function
    Source: 'src/traits.rs', lines 156:4-156:25 -/
@@ -239,7 +236,7 @@ def BoolWrapper.to_type
   (T : Type) (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) :
   Result T
   :=
-  ToTypeBoolTInst.to_type self._0
+  ToTypeBoolTInst.to_type self
 
 /- Trait implementation: [traits::{traits::BoolWrapper#7}]
    Source: 'src/traits.rs', lines 152:0-152:33 -/