summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/NoNestedBorrows.v34
-rw-r--r--tests/coq/traits/Traits.v21
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst29
-rw-r--r--tests/fstar/traits/Traits.fst12
-rw-r--r--tests/lean/NoNestedBorrows.lean31
-rw-r--r--tests/lean/Traits.lean15
6 files changed, 110 insertions, 32 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 1a0014c0..e8230fad 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -42,7 +42,7 @@ Inductive Enum_t := | Enum_Variant1 : Enum_t | Enum_Variant2 : Enum_t.
(** [no_nested_borrows::EmptyStruct]
Source: 'src/no_nested_borrows.rs', lines 39:0-39:22 *)
-Record EmptyStruct_t := mkEmptyStruct_t { }.
+Definition EmptyStruct_t : Type := unit.
(** [no_nested_borrows::Sum]
Source: 'src/no_nested_borrows.rs', lines 41:0-41:20 *)
@@ -644,4 +644,36 @@ Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
Definition test_shared_borrow_enum2 : result u32 :=
Return 0%u32.
+(** [no_nested_borrows::Tuple]
+ Source: 'src/no_nested_borrows.rs', lines 530:0-530:24 *)
+Definition Tuple_t (T1 T2 : Type) : 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 *)
+Definition use_tuple_struct (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) :=
+ let (_, i) := x in Return (1%u32, i)
+.
+
+(** [no_nested_borrows::create_tuple_struct]: forward function
+ Source: 'src/no_nested_borrows.rs', lines 536:0-536:61 *)
+Definition create_tuple_struct
+ (x : u32) (y : u64) : result (Tuple_t u32 u64) :=
+ Return (x, y)
+.
+
+(** [no_nested_borrows::IdType]
+ Source: 'src/no_nested_borrows.rs', lines 541:0-541:20 *)
+Definition IdType_t (T : Type) : Type := T.
+
+(** [no_nested_borrows::use_id_type]: forward function
+ Source: 'src/no_nested_borrows.rs', lines 543:0-543:40 *)
+Definition use_id_type (T : Type) (x : IdType_t T) : result T :=
+ Return x.
+
+(** [no_nested_borrows::create_id_type]: forward function
+ Source: 'src/no_nested_borrows.rs', lines 547:0-547:43 *)
+Definition create_id_type (T : Type) (x : T) : result (IdType_t T) :=
+ Return x.
+
End NoNestedBorrows.
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 549a7116..2448e8f3 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -223,18 +223,11 @@ Definition h4
(** [traits::TestType]
Source: 'src/traits.rs', lines 122:0-122:22 *)
-Record TestType_t (T : Type) := mkTestType_t { testType_0 : T; }.
-
-Arguments mkTestType_t { _ }.
-Arguments testType_0 { _ }.
+Definition TestType_t (T : Type) : Type := T.
(** [traits::{traits::TestType<T>#6}::test::TestType1]
Source: 'src/traits.rs', lines 127:8-127:24 *)
-Record TestType_test_TestType1_t :=
-mkTestType_test_TestType1_t {
- testType_test_TestType1_0 : u64;
-}
-.
+Definition TestType_test_TestType1_t : Type := u64.
(** Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
Source: 'src/traits.rs', lines 128:8-128:23 *)
@@ -249,7 +242,7 @@ Arguments TestType_test_TestTrait_t_test { _ }.
Source: 'src/traits.rs', lines 139:12-139:34 *)
Definition testType_test_TestType1_test
(self : TestType_test_TestType1_t) : result bool :=
- Return (self.(testType_test_TestType1_0) s> 1%u64)
+ Return (self s> 1%u64)
.
(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
@@ -266,14 +259,12 @@ Definition testType_test
result bool
:=
x0 <- toU64TInst.(ToU64_t_to_u64) x;
- if x0 s> 0%u64
- then testType_test_TestType1_test {| testType_test_TestType1_0 := 0%u64 |}
- else Return false
+ if x0 s> 0%u64 then testType_test_TestType1_test 0%u64 else Return false
.
(** [traits::BoolWrapper]
Source: 'src/traits.rs', lines 150:0-150:22 *)
-Record BoolWrapper_t := mkBoolWrapper_t { boolWrapper_0 : bool; }.
+Definition BoolWrapper_t : Type := bool.
(** [traits::{traits::BoolWrapper#7}::to_type]: forward function
Source: 'src/traits.rs', lines 156:4-156:25 *)
@@ -281,7 +272,7 @@ Definition boolWrapper_to_type
(T : Type) (toTypeBoolTInst : ToType_t bool T) (self : BoolWrapper_t) :
result T
:=
- toTypeBoolTInst.(ToType_t_to_type) self.(boolWrapper_0)
+ toTypeBoolTInst.(ToType_t_to_type) self
.
(** Trait implementation: [traits::{traits::BoolWrapper#7}]
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 130b02f2..0c66d3ac 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -560,3 +560,32 @@ let test_shared_borrow_enum1 (l : list_t u32) : result u32 =
let test_shared_borrow_enum2 : result u32 =
Return 0
+(** [no_nested_borrows::Tuple]
+ Source: 'src/no_nested_borrows.rs', lines 530:0-530:24 *)
+type tuple_t (t1 t2 : Type0) = 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 *)
+let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) =
+ let (_, i) = x in Return (1, i)
+
+(** [no_nested_borrows::create_tuple_struct]: forward function
+ Source: 'src/no_nested_borrows.rs', lines 536:0-536:61 *)
+let create_tuple_struct (x : u32) (y : u64) : result (tuple_t u32 u64) =
+ Return (x, y)
+
+(** [no_nested_borrows::IdType]
+ Source: 'src/no_nested_borrows.rs', lines 541:0-541:20 *)
+type idType_t (t : Type0) = t
+
+(** [no_nested_borrows::use_id_type]: forward function
+ Source: 'src/no_nested_borrows.rs', lines 543:0-543:40 *)
+let use_id_type (t : Type0) (x : idType_t t) : result t =
+ Return x
+
+(** [no_nested_borrows::create_id_type]: forward function
+ Source: 'src/no_nested_borrows.rs', lines 547:0-547:43 *)
+let create_id_type (t : Type0) (x : t) : result (idType_t t) =
+ Return x
+
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 8252aad4..7d504cb5 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -177,11 +177,11 @@ let h4
(** [traits::TestType]
Source: 'src/traits.rs', lines 122:0-122:22 *)
-type testType_t (t : Type0) = { _0 : t; }
+type testType_t (t : Type0) = t
(** [traits::{traits::TestType<T>#6}::test::TestType1]
Source: 'src/traits.rs', lines 127:8-127:24 *)
-type testType_test_TestType1_t = { _0 : u64; }
+type testType_test_TestType1_t = u64
(** Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
Source: 'src/traits.rs', lines 128:8-128:23 *)
@@ -193,7 +193,7 @@ noeq type testType_test_TestTrait_t (self : Type0) = {
Source: 'src/traits.rs', lines 139:12-139:34 *)
let testType_test_TestType1_test
(self : testType_test_TestType1_t) : result bool =
- Return (self._0 > 1)
+ Return (self > 1)
(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
Source: 'src/traits.rs', lines 138:8-138:36 *)
@@ -209,11 +209,11 @@ let testType_test
result bool
=
let* x0 = toU64TInst.to_u64 x in
- if x0 > 0 then testType_test_TestType1_test { _0 = 0 } else Return false
+ if x0 > 0 then testType_test_TestType1_test 0 else Return false
(** [traits::BoolWrapper]
Source: 'src/traits.rs', lines 150:0-150:22 *)
-type boolWrapper_t = { _0 : bool; }
+type boolWrapper_t = bool
(** [traits::{traits::BoolWrapper#7}::to_type]: forward function
Source: 'src/traits.rs', lines 156:4-156:25 *)
@@ -221,7 +221,7 @@ let boolWrapper_to_type
(t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) :
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 *)
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 -/