summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon HO2023-12-07 15:02:44 +0100
committerGitHub2023-12-07 15:02:44 +0100
commitd4ebd6c1f0ba150e5e52d812d361189c89e43695 (patch)
tree4b3fa3d48c86ba379c78d01fca88d2084c2678c2 /tests/lean
parent9eb117dc9e94d1b04d24c87d278d014f456b2d89 (diff)
parent613496f6c76b3f8c7211ef5bc98e3cc170e45ed1 (diff)
Merge pull request #49 from AeneasVerif/son_merge_back
Allow the extraction of structures as tuples
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/NoNestedBorrows.lean31
-rw-r--r--tests/lean/Traits.lean15
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 -/