diff options
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 34 | ||||
| -rw-r--r-- | tests/coq/traits/Traits.v | 21 | ||||
| -rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 29 | ||||
| -rw-r--r-- | tests/fstar/traits/Traits.fst | 12 | ||||
| -rw-r--r-- | tests/lean/NoNestedBorrows.lean | 31 | ||||
| -rw-r--r-- | tests/lean/Traits.lean | 15 |
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 -/ |