diff options
author | Son Ho | 2023-12-07 14:43:28 +0100 |
---|---|---|
committer | Son Ho | 2023-12-07 14:43:28 +0100 |
commit | 6c0a23ec75c7365f4b8cabe88652e1403008bd3c (patch) | |
tree | 272bf5c1666a1583ee3f889e5499a2f220444914 /tests/fstar | |
parent | 2fc876ab40bed10e36f6ee6581f516cdda3b9bc4 (diff) |
Regenerate the tests
Diffstat (limited to 'tests/fstar')
-rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 29 | ||||
-rw-r--r-- | tests/fstar/traits/Traits.fst | 12 |
2 files changed, 35 insertions, 6 deletions
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 *) |