diff options
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 33 | ||||
-rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 29 | ||||
-rw-r--r-- | tests/lean/NoNestedBorrows.lean | 31 | ||||
-rw-r--r-- | tests/src/no_nested_borrows.rs | 14 |
4 files changed, 85 insertions, 22 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 46b08184..923609c5 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -531,30 +531,49 @@ Definition read_then_incr (x : u32) : result (u32 * u32) := Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 *) Definition Tuple_t (T1 T2 : Type) : Type := T1 * T2. -(** [no_nested_borrows::use_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 *) -Definition use_tuple_struct (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) := +(** [no_nested_borrows::read_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:40 *) +Definition read_tuple (x : (u32 * u32)) : result u32 := + let (i, _) := x in Ok i +. + +(** [no_nested_borrows::update_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 *) +Definition update_tuple (x : (u32 * u32)) : result (u32 * u32) := + let (_, i) := x in Ok (1%u32, i) +. + +(** [no_nested_borrows::read_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 *) +Definition read_tuple_struct (x : Tuple_t u32 u32) : result u32 := + let (i, _) := x in Ok i +. + +(** [no_nested_borrows::update_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 *) +Definition update_tuple_struct + (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) := let (_, i) := x in Ok (1%u32, i) . (** [no_nested_borrows::create_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 *) + Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 *) Definition create_tuple_struct (x : u32) (y : u64) : result (Tuple_t u32 u64) := Ok (x, y) . (** [no_nested_borrows::IdType] - Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 *) + Source: 'tests/src/no_nested_borrows.rs', lines 503:0-503:20 *) Definition IdType_t (T : Type) : Type := T. (** [no_nested_borrows::use_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 505:0-505:40 *) Definition use_id_type (T : Type) (x : IdType_t T) : result T := Ok x. (** [no_nested_borrows::create_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 *) + Source: 'tests/src/no_nested_borrows.rs', lines 509:0-509:43 *) Definition create_id_type (T : Type) (x : T) : result (IdType_t T) := Ok x. diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index a5ba31bc..f45d7f23 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -446,27 +446,42 @@ let read_then_incr (x : u32) : result (u32 & u32) = Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 *) type tuple_t (t1 t2 : Type0) = t1 * t2 -(** [no_nested_borrows::use_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 *) -let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) = +(** [no_nested_borrows::read_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:40 *) +let read_tuple (x : (u32 & u32)) : result u32 = + let (i, _) = x in Ok i + +(** [no_nested_borrows::update_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 *) +let update_tuple (x : (u32 & u32)) : result (u32 & u32) = + let (_, i) = x in Ok (1, i) + +(** [no_nested_borrows::read_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 *) +let read_tuple_struct (x : tuple_t u32 u32) : result u32 = + let (i, _) = x in Ok i + +(** [no_nested_borrows::update_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 *) +let update_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) = let (_, i) = x in Ok (1, i) (** [no_nested_borrows::create_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 *) + Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 *) let create_tuple_struct (x : u32) (y : u64) : result (tuple_t u32 u64) = Ok (x, y) (** [no_nested_borrows::IdType] - Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 *) + Source: 'tests/src/no_nested_borrows.rs', lines 503:0-503:20 *) type idType_t (t : Type0) = t (** [no_nested_borrows::use_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 505:0-505:40 *) let use_id_type (t : Type0) (x : idType_t t) : result t = Ok x (** [no_nested_borrows::create_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 *) + Source: 'tests/src/no_nested_borrows.rs', lines 509:0-509:43 *) let create_id_type (t : Type0) (x : t) : result (idType_t t) = Ok x diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index b8fbcff0..262fc79e 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -538,27 +538,44 @@ def read_then_incr (x : U32) : Result (U32 × U32) := Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 -/ def Tuple (T1 T2 : Type) := T1 × T2 -/- [no_nested_borrows::use_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 -/ -def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) := +/- [no_nested_borrows::read_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:40 -/ +def read_tuple (x : (U32 × U32)) : Result U32 := + let (i, _) := x + Result.ok i + +/- [no_nested_borrows::update_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 -/ +def update_tuple (x : (U32 × U32)) : Result (U32 × U32) := + let (_, i) := x + Result.ok (1#u32, i) + +/- [no_nested_borrows::read_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/ +def read_tuple_struct (x : Tuple U32 U32) : Result U32 := + Result.ok x.#0 + +/- [no_nested_borrows::update_tuple_struct]: + Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/ +def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) := Result.ok (1#u32, x.#1) /- [no_nested_borrows::create_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/ def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) := Result.ok (x, y) /- [no_nested_borrows::IdType] - Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 503:0-503:20 -/ @[reducible] def IdType (T : Type) := T /- [no_nested_borrows::use_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 505:0-505:40 -/ def use_id_type (T : Type) (x : IdType T) : Result T := Result.ok x /- [no_nested_borrows::create_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 509:0-509:43 -/ def create_id_type (T : Type) (x : T) : Result (IdType T) := Result.ok x diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index 11c4a695..20f8efea 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -479,7 +479,19 @@ pub fn read_then_incr(x: &mut u32) -> u32 { pub struct Tuple<T1, T2>(T1, T2); -pub fn use_tuple_struct(x: &mut Tuple<u32, u32>) { +pub fn read_tuple(x: &(u32, u32)) -> u32 { + x.0 +} + +pub fn update_tuple(x: &mut (u32, u32)) { + x.0 = 1; +} + +pub fn read_tuple_struct(x: &Tuple<u32, u32>) -> u32 { + x.0 +} + +pub fn update_tuple_struct(x: &mut Tuple<u32, u32>) { x.0 = 1; } |