summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Config.ml11
-rw-r--r--compiler/SymbolicToPure.ml2
-rw-r--r--tests/coq/misc/NoNestedBorrows.v33
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst29
-rw-r--r--tests/lean/NoNestedBorrows.lean35
-rw-r--r--tests/src/no_nested_borrows.rs14
6 files changed, 96 insertions, 28 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index cb2c86ad..584635bc 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -362,16 +362,19 @@ let variant_concatenate_type_name = ref true
ex.:
{[
// Rust
- struct Foo(u32)
+ struct Foo(u32, u32)
// OCaml
- type Foo = (u32)
+ type Foo = u32 * u32
]}
*)
let use_tuple_structs = ref true
-let backend_has_tuple_projectors () =
- match backend () with Lean -> true | Coq | FStar | HOL4 -> false
+let backend_has_tuple_projectors backend =
+ match backend with Lean -> true | Coq | FStar | HOL4 -> false
+
+(** Toggle the use of tuple projectors *)
+let use_tuple_projectors = ref false
(** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do
we use better projector syntax? *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3975107a..87f1128d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2916,7 +2916,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
at once (`let (a, b, c) = x in`) *)
|| TypesUtils.type_decl_from_type_id_is_tuple_struct
ctx.type_ctx.type_infos type_id
- && not (Config.backend_has_tuple_projectors ())
+ && not !Config.use_tuple_projectors
in
if use_let_with_cons then
(* Introduce a let binding which expands the ADT *)
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..f0438050 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -538,27 +538,46 @@ 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) :=
- Result.ok (1#u32, x.#1)
+/- [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 :=
+ let (i, _) := x
+ Result.ok i
+
+/- [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) :=
+ let (_, i) := x
+ Result.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 -/
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 07:48:35 +0000