summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/External_Funs.v77
-rw-r--r--tests/coq/misc/External_FunsExternal.v21
-rw-r--r--tests/coq/misc/External_FunsExternal_Template.v30
-rw-r--r--tests/coq/misc/External_Types.v10
-rw-r--r--tests/coq/misc/External_TypesExternal.v5
-rw-r--r--tests/coq/misc/External_TypesExternal_Template.v8
-rw-r--r--tests/coq/misc/Primitives.v75
-rw-r--r--tests/fstar/misc/External.Funs.fst64
-rw-r--r--tests/fstar/misc/External.FunsExternal.fsti28
-rw-r--r--tests/fstar/misc/External.Types.fst7
-rw-r--r--tests/fstar/misc/External.TypesExternal.fsti8
-rw-r--r--tests/fstar/misc/Primitives.fst75
-rw-r--r--tests/lean/External/Funs.lean72
-rw-r--r--tests/lean/External/FunsExternal.lean23
-rw-r--r--tests/lean/External/FunsExternal_Template.lean23
-rw-r--r--tests/lean/External/Types.lean6
-rw-r--r--tests/lean/External/TypesExternal.lean17
-rw-r--r--tests/lean/External/TypesExternal_Template.lean8
18 files changed, 320 insertions, 237 deletions
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 41d4a7bd..c4f70f75 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -12,64 +12,33 @@ Require Import External_FunsExternal.
Include External_FunsExternal.
Module External_Funs.
-(** [external::swap]:
- Source: 'src/external.rs', lines 6:0-6:46 *)
-Definition swap
- (T : Type) (x : T) (y : T) (st : state) : result (state * (T * T)) :=
- core_mem_swap T x y st
+(** Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+ Name pattern: core::marker::Copy<u32> *)
+Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {|
+ core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst := core_clone_CloneU32;
+|}.
+
+(** [external::use_get]:
+ Source: 'src/external.rs', lines 5:0-5:37 *)
+Definition use_get
+ (rc : core_cell_Cell_t u32) (st : state) : result (state * u32) :=
+ core_cell_Cell_get u32 core_marker_CopyU32 rc st
.
-(** [external::test_new_non_zero_u32]:
- Source: 'src/external.rs', lines 11:0-11:60 *)
-Definition test_new_non_zero_u32
- (x : u32) (st : state) : result (state * core_num_nonzero_NonZeroU32_t) :=
- p <- core_num_nonzero_NonZeroU32_new x st;
- let (st1, o) := p in
- core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st1
-.
-
-(** [external::test_vec]:
- Source: 'src/external.rs', lines 17:0-17:17 *)
-Definition test_vec : result unit :=
- _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Ok tt
-.
-
-(** Unit test for [external::test_vec] *)
-Check (test_vec )%return.
-
-(** [external::custom_swap]:
- Source: 'src/external.rs', lines 24:0-24:66 *)
-Definition custom_swap
- (T : Type) (x : T) (y : T) (st : state) :
- result (state * (T * (T -> state -> result (state * (T * T)))))
+(** [external::incr]:
+ Source: 'src/external.rs', lines 9:0-9:31 *)
+Definition incr
+ (rc : core_cell_Cell_t u32) (st : state) :
+ result (state * (core_cell_Cell_t u32))
:=
- p <- core_mem_swap T x y st;
- let (st1, p1) := p in
- let (x1, y1) := p1 in
- let back := fun (ret : T) (st2 : state) => Ok (st2, (ret, y1)) in
- Ok (st1, (x1, back))
-.
-
-(** [external::test_custom_swap]:
- Source: 'src/external.rs', lines 29:0-29:59 *)
-Definition test_custom_swap
- (x : u32) (y : u32) (st : state) : result (state * (u32 * u32)) :=
- p <- custom_swap u32 x y st;
- let (st1, p1) := p in
- let (_, custom_swap_back) := p1 in
- p2 <- custom_swap_back 1%u32 st1;
- let (_, p3) := p2 in
- let (x1, y1) := p3 in
- Ok (st1, (x1, y1))
-.
-
-(** [external::test_swap_non_zero]:
- Source: 'src/external.rs', lines 35:0-35:44 *)
-Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
- p <- swap u32 x 0%u32 st;
+ p <- core_cell_Cell_get_mut u32 rc st;
let (st1, p1) := p in
- let (x1, _) := p1 in
- if x1 s= 0%u32 then Fail_ Failure else Ok (st1, x1)
+ let (i, get_mut_back) := p1 in
+ i1 <- u32_add i 1%u32;
+ p2 <- get_mut_back i1 st1;
+ let (_, rc1) := p2 in
+ Ok (st1, rc1)
.
End External_Funs.
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index 39f4a60e..a25d9c33 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -9,22 +9,15 @@ Require Export External_Types.
Include External_Types.
Module External_FunsExternal.
-(** [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Definition core_mem_swap (T : Type) (x : T) (y : T) (s : state) :=
- Ok (s, (y, x))
+Axiom core_cell_Cell_get :
+ forall(T : Type) (markerCopyInst : core_marker_Copy_t T),
+ core_cell_Cell_t T -> state -> result (state * T)
.
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
-Axiom core_num_nonzero_NonZeroU32_new
- : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-Axiom core_option_Option_unwrap :
- forall(T : Type), option T -> state -> result (state * T)
+Axiom core_cell_Cell_get_mut :
+ forall(T : Type),
+ core_cell_Cell_t T -> state -> result (state * (T * (T -> state ->
+ result (state * (core_cell_Cell_t T)))))
.
End External_FunsExternal.
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 24dd2d47..b3e4a129 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -11,25 +11,21 @@ Require Import External_Types.
Include External_Types.
Module External_FunsExternal_Template.
-(** [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
- Name pattern: core::mem::swap *)
-Axiom core_mem_swap :
- forall(T : Type), T -> T -> state -> result (state * (T * T))
+(** [core::cell::{core::cell::Cell<T>#10}::get]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
+Axiom core_cell_Cell_get :
+ forall(T : Type) (markerCopyInst : core_marker_Copy_t T),
+ core_cell_Cell_t T -> state -> result (state * T)
.
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
- Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
-Axiom core_num_nonzero_NonZeroU32_new
- : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
- Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-Axiom core_option_Option_unwrap :
- forall(T : Type), option T -> state -> result (state * T)
+(** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
+Axiom core_cell_Cell_get_mut :
+ forall(T : Type),
+ core_cell_Cell_t T -> state -> result (state * (T * (T -> state ->
+ result (state * (core_cell_Cell_t T)))))
.
End External_FunsExternal_Template.
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
index b42c2ecf..5b233c62 100644
--- a/tests/coq/misc/External_Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -10,4 +10,14 @@ Require Import External_TypesExternal.
Include External_TypesExternal.
Module External_Types.
+(** Trait declaration: [core::marker::Copy]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+ Name pattern: core::marker::Copy *)
+Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t {
+ core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst : core_clone_Clone Self;
+}.
+
+Arguments mkcore_marker_Copy_t { _ }.
+Arguments core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst { _ }.
+
End External_Types.
diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v
index 734c66e5..6bb2b1db 100644
--- a/tests/coq/misc/External_TypesExternal.v
+++ b/tests/coq/misc/External_TypesExternal.v
@@ -8,9 +8,8 @@ Import ListNotations.
Local Open Scope Primitives_scope.
Module External_TypesExternal.
-(** [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
+(** [core::cell::Cell] *)
+Axiom core_cell_Cell_t : forall (T : Type), Type.
(** The state type used in the state-error monad *)
Axiom state : Type.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index 7d6af202..87b1c826 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -9,10 +9,10 @@ Import ListNotations.
Local Open Scope Primitives_scope.
Module External_TypesExternal_Template.
-(** [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
- Name pattern: core::num::nonzero::NonZeroU32 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
+(** [core::cell::Cell]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+ Name pattern: core::cell::Cell *)
+Axiom core_cell_Cell_t : forall (T : Type), Type.
(** The state type used in the state-error monad *)
Axiom state : Type.
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index e84d65ce..5ffda12f 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -489,6 +489,81 @@ Definition core_i64_max := i64_max %i64.
Definition core_i128_max := i64_max %i128.
Axiom core_isize_max : isize. (** TODO *)
+(*** core *)
+
+(** Trait declaration: [core::clone::Clone] *)
+Record core_clone_Clone (self : Type) := {
+ clone : self -> result self
+}.
+
+Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b.
+
+Definition core_clone_CloneBool : core_clone_Clone bool := {|
+ clone := fun b => Ok (core_clone_impls_CloneBool_clone b)
+|}.
+
+Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x.
+Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x.
+Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x.
+Definition core_clone_impls_CloneU32_clone (x : u32) : u32 := x.
+Definition core_clone_impls_CloneU64_clone (x : u64) : u64 := x.
+Definition core_clone_impls_CloneU128_clone (x : u128) : u128 := x.
+
+Definition core_clone_impls_CloneIsize_clone (x : isize) : isize := x.
+Definition core_clone_impls_CloneI8_clone (x : i8) : i8 := x.
+Definition core_clone_impls_CloneI16_clone (x : i16) : i16 := x.
+Definition core_clone_impls_CloneI32_clone (x : i32) : i32 := x.
+Definition core_clone_impls_CloneI64_clone (x : i64) : i64 := x.
+Definition core_clone_impls_CloneI128_clone (x : i128) : i128 := x.
+
+Definition core_clone_CloneUsize : core_clone_Clone usize := {|
+ clone := fun x => Ok (core_clone_impls_CloneUsize_clone x)
+|}.
+
+Definition core_clone_CloneU8 : core_clone_Clone u8 := {|
+ clone := fun x => Ok (core_clone_impls_CloneU8_clone x)
+|}.
+
+Definition core_clone_CloneU16 : core_clone_Clone u16 := {|
+ clone := fun x => Ok (core_clone_impls_CloneU16_clone x)
+|}.
+
+Definition core_clone_CloneU32 : core_clone_Clone u32 := {|
+ clone := fun x => Ok (core_clone_impls_CloneU32_clone x)
+|}.
+
+Definition core_clone_CloneU64 : core_clone_Clone u64 := {|
+ clone := fun x => Ok (core_clone_impls_CloneU64_clone x)
+|}.
+
+Definition core_clone_CloneU128 : core_clone_Clone u128 := {|
+ clone := fun x => Ok (core_clone_impls_CloneU128_clone x)
+|}.
+
+Definition core_clone_CloneIsize : core_clone_Clone isize := {|
+ clone := fun x => Ok (core_clone_impls_CloneIsize_clone x)
+|}.
+
+Definition core_clone_CloneI8 : core_clone_Clone i8 := {|
+ clone := fun x => Ok (core_clone_impls_CloneI8_clone x)
+|}.
+
+Definition core_clone_CloneI16 : core_clone_Clone i16 := {|
+ clone := fun x => Ok (core_clone_impls_CloneI16_clone x)
+|}.
+
+Definition core_clone_CloneI32 : core_clone_Clone i32 := {|
+ clone := fun x => Ok (core_clone_impls_CloneI32_clone x)
+|}.
+
+Definition core_clone_CloneI64 : core_clone_Clone i64 := {|
+ clone := fun x => Ok (core_clone_impls_CloneI64_clone x)
+|}.
+
+Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
+ clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
+|}.
+
(*** core::ops *)
(* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index d4247b8f..d8457ce3 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -7,48 +7,26 @@ include External.FunsExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [external::swap]:
- Source: 'src/external.rs', lines 6:0-6:46 *)
-let swap (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & t)) =
- core_mem_swap t x y st
-
-(** [external::test_new_non_zero_u32]:
- Source: 'src/external.rs', lines 11:0-11:60 *)
-let test_new_non_zero_u32
- (x : u32) (st : state) : result (state & core_num_nonzero_NonZeroU32_t) =
- let* (st1, o) = core_num_nonzero_NonZeroU32_new x st in
- core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st1
-
-(** [external::test_vec]:
- Source: 'src/external.rs', lines 17:0-17:17 *)
-let test_vec : result unit =
- let* _ = alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0 in Ok ()
-
-(** Unit test for [external::test_vec] *)
-let _ = assert_norm (test_vec = Ok ())
-
-(** [external::custom_swap]:
- Source: 'src/external.rs', lines 24:0-24:66 *)
-let custom_swap
- (t : Type0) (x : t) (y : t) (st : state) :
- result (state & (t & (t -> state -> result (state & (t & t)))))
+(** Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+ Name pattern: core::marker::Copy<u32> *)
+let core_marker_CopyU32 : core_marker_Copy_t u32 = {
+ cloneCloneInst = core_clone_CloneU32;
+}
+
+(** [external::use_get]:
+ Source: 'src/external.rs', lines 5:0-5:37 *)
+let use_get (rc : core_cell_Cell_t u32) (st : state) : result (state & u32) =
+ core_cell_Cell_get u32 core_marker_CopyU32 rc st
+
+(** [external::incr]:
+ Source: 'src/external.rs', lines 9:0-9:31 *)
+let incr
+ (rc : core_cell_Cell_t u32) (st : state) :
+ result (state & (core_cell_Cell_t u32))
=
- let* (st1, (x1, y1)) = core_mem_swap t x y st in
- let back = fun ret st2 -> Ok (st2, (ret, y1)) in
- Ok (st1, (x1, back))
-
-(** [external::test_custom_swap]:
- Source: 'src/external.rs', lines 29:0-29:59 *)
-let test_custom_swap
- (x : u32) (y : u32) (st : state) : result (state & (u32 & u32)) =
- let* (st1, (_, custom_swap_back)) = custom_swap u32 x y st in
- let* (_, (x1, y1)) = custom_swap_back 1 st1 in
- Ok (st1, (x1, y1))
-
-(** [external::test_swap_non_zero]:
- Source: 'src/external.rs', lines 35:0-35:44 *)
-let test_swap_non_zero (x : u32) (st : state) : result (state & u32) =
- let* (st1, p) = swap u32 x 0 st in
- let (x1, _) = p in
- if x1 = 0 then Fail Failure else Ok (st1, x1)
+ let* (st1, (i, get_mut_back)) = core_cell_Cell_get_mut u32 rc st in
+ let* i1 = u32_add i 1 in
+ let* (_, rc1) = get_mut_back i1 st1 in
+ Ok (st1, rc1)
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index 4c1c58b7..9436cf86 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -6,20 +6,18 @@ include External.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
- Name pattern: core::mem::swap *)
-val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
+(** [core::cell::{core::cell::Cell<T>#10}::get]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
+val core_cell_Cell_get
+ (t : Type0) (markerCopyInst : core_marker_Copy_t t) :
+ core_cell_Cell_t t -> state -> result (state & t)
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
- Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
-val core_num_nonzero_NonZeroU32_new
- : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
-
-(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
- Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-val core_option_Option_unwrap
- (t : Type0) : option t -> state -> result (state & t)
+(** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
+val core_cell_Cell_get_mut
+ (t : Type0) :
+ core_cell_Cell_t t -> state -> result (state & (t & (t -> state -> result
+ (state & (core_cell_Cell_t t)))))
diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst
index 4fbcec47..143f24dd 100644
--- a/tests/fstar/misc/External.Types.fst
+++ b/tests/fstar/misc/External.Types.fst
@@ -6,3 +6,10 @@ include External.TypesExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+(** Trait declaration: [core::marker::Copy]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+ Name pattern: core::marker::Copy *)
+noeq type core_marker_Copy_t (self : Type0) = {
+ cloneCloneInst : core_clone_Clone self;
+}
+
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 45174c7e..c0b7e43f 100644
--- a/tests/fstar/misc/External.TypesExternal.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -5,10 +5,10 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
- Name pattern: core::num::nonzero::NonZeroU32 *)
-val core_num_nonzero_NonZeroU32_t : Type0
+(** [core::cell::Cell]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+ Name pattern: core::cell::Cell *)
+val core_cell_Cell_t (t : Type0) : Type0
(** The state type used in the state-error monad *)
val state : Type0
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index acdb09dc..c7c9f9db 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -465,6 +465,81 @@ let i64_shr #ty = scalar_shr #I64 #ty
let i128_shr #ty = scalar_shr #I128 #ty
let isize_shr #ty = scalar_shr #Isize #ty
+(*** core *)
+
+/// Trait declaration: [core::clone::Clone]
+noeq type core_clone_Clone (self : Type0) = {
+ clone : self → result self
+}
+
+let core_clone_impls_CloneBool_clone (b : bool) : bool = b
+
+let core_clone_CloneBool : core_clone_Clone bool = {
+ clone = fun b -> Ok (core_clone_impls_CloneBool_clone b)
+}
+
+let core_clone_impls_CloneUsize_clone (x : usize) : usize = x
+let core_clone_impls_CloneU8_clone (x : u8) : u8 = x
+let core_clone_impls_CloneU16_clone (x : u16) : u16 = x
+let core_clone_impls_CloneU32_clone (x : u32) : u32 = x
+let core_clone_impls_CloneU64_clone (x : u64) : u64 = x
+let core_clone_impls_CloneU128_clone (x : u128) : u128 = x
+
+let core_clone_impls_CloneIsize_clone (x : isize) : isize = x
+let core_clone_impls_CloneI8_clone (x : i8) : i8 = x
+let core_clone_impls_CloneI16_clone (x : i16) : i16 = x
+let core_clone_impls_CloneI32_clone (x : i32) : i32 = x
+let core_clone_impls_CloneI64_clone (x : i64) : i64 = x
+let core_clone_impls_CloneI128_clone (x : i128) : i128 = x
+
+let core_clone_CloneUsize : core_clone_Clone usize = {
+ clone = fun x -> Ok (core_clone_impls_CloneUsize_clone x)
+}
+
+let core_clone_CloneU8 : core_clone_Clone u8 = {
+ clone = fun x -> Ok (core_clone_impls_CloneU8_clone x)
+}
+
+let core_clone_CloneU16 : core_clone_Clone u16 = {
+ clone = fun x -> Ok (core_clone_impls_CloneU16_clone x)
+}
+
+let core_clone_CloneU32 : core_clone_Clone u32 = {
+ clone = fun x -> Ok (core_clone_impls_CloneU32_clone x)
+}
+
+let core_clone_CloneU64 : core_clone_Clone u64 = {
+ clone = fun x -> Ok (core_clone_impls_CloneU64_clone x)
+}
+
+let core_clone_CloneU128 : core_clone_Clone u128 = {
+ clone = fun x -> Ok (core_clone_impls_CloneU128_clone x)
+}
+
+let core_clone_CloneIsize : core_clone_Clone isize = {
+ clone = fun x -> Ok (core_clone_impls_CloneIsize_clone x)
+}
+
+let core_clone_CloneI8 : core_clone_Clone i8 = {
+ clone = fun x -> Ok (core_clone_impls_CloneI8_clone x)
+}
+
+let core_clone_CloneI16 : core_clone_Clone i16 = {
+ clone = fun x -> Ok (core_clone_impls_CloneI16_clone x)
+}
+
+let core_clone_CloneI32 : core_clone_Clone i32 = {
+ clone = fun x -> Ok (core_clone_impls_CloneI32_clone x)
+}
+
+let core_clone_CloneI64 : core_clone_Clone i64 = {
+ clone = fun x -> Ok (core_clone_impls_CloneI64_clone x)
+}
+
+let core_clone_CloneI128 : core_clone_Clone i128 = {
+ clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
+}
+
(*** core::ops *)
// Trait declaration: [core::ops::index::Index]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 78e0f95c..20c4b8e5 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -7,58 +7,28 @@ open Primitives
namespace external
-/- [external::swap]:
- Source: 'src/external.rs', lines 6:0-6:46 -/
-def swap
- (T : Type) (x : T) (y : T) (st : State) : Result (State × (T × T)) :=
- core.mem.swap T x y st
-
-/- [external::test_new_non_zero_u32]:
- Source: 'src/external.rs', lines 11:0-11:60 -/
-def test_new_non_zero_u32
- (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) :=
- do
- let (st1, o) ← core.num.nonzero.NonZeroU32.new x st
- core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st1
-
-/- [external::test_vec]:
- Source: 'src/external.rs', lines 17:0-17:17 -/
-def test_vec : Result Unit :=
- do
- let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32
- Result.ok ()
-
-/- Unit test for [external::test_vec] -/
-#assert (test_vec == Result.ok ())
-
-/- [external::custom_swap]:
- Source: 'src/external.rs', lines 24:0-24:66 -/
-def custom_swap
- (T : Type) (x : T) (y : T) (st : State) :
- Result (State × (T × (T → State → Result (State × (T × T)))))
+/- Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+ Name pattern: core::marker::Copy<u32> -/
+def core.marker.CopyU32 : core.marker.Copy U32 := {
+ cloneCloneInst := core.clone.CloneU32
+}
+
+/- [external::use_get]:
+ Source: 'src/external.rs', lines 5:0-5:37 -/
+def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) :=
+ core.cell.Cell.get U32 core.marker.CopyU32 rc st
+
+/- [external::incr]:
+ Source: 'src/external.rs', lines 9:0-9:31 -/
+def incr
+ (rc : core.cell.Cell U32) (st : State) :
+ Result (State × (core.cell.Cell U32))
:=
do
- let (st1, (x1, y1)) ← core.mem.swap T x y st
- let back := fun ret st2 => Result.ok (st2, (ret, y1))
- Result.ok (st1, (x1, back))
-
-/- [external::test_custom_swap]:
- Source: 'src/external.rs', lines 29:0-29:59 -/
-def test_custom_swap
- (x : U32) (y : U32) (st : State) : Result (State × (U32 × U32)) :=
- do
- let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st
- let (_, (x1, y1)) ← custom_swap_back 1#u32 st1
- Result.ok (st1, (x1, y1))
-
-/- [external::test_swap_non_zero]:
- Source: 'src/external.rs', lines 35:0-35:44 -/
-def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
- do
- let (st1, p) ← swap U32 x 0#u32 st
- let (x1, _) := p
- if x1 = 0#u32
- then Result.fail .panic
- else Result.ok (st1, x1)
+ let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st
+ let i1 ← i + 1#u32
+ let (_, rc1) ← get_mut_back i1 st1
+ Result.ok (st1, rc1)
end external
diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean
index b6efc65f..28ba2077 100644
--- a/tests/lean/External/FunsExternal.lean
+++ b/tests/lean/External/FunsExternal.lean
@@ -4,19 +4,14 @@ import External.Types
open Primitives
open external
--- TODO: fill those bodies
+/- [core::cell::{core::cell::Cell<T>#10}::get]: -/
+def core.cell.Cell.get
+ (T : Type) (markerCopyInst : core.marker.Copy T) (c : core.cell.Cell T) (s : State) :
+ Result (State × T) :=
+ sorry
-/- [core::mem::swap] -/
-def core.mem.swap
- (T : Type) : T → T → State → Result (State × (T × T)) :=
- fun x y s => .ok (s, (y, x))
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]: -/
+def core.cell.Cell.get_mut (T : Type) (c : core.cell.Cell T) (s : State) :
+ Result (State × (T × (T → State → Result (State × (core.cell.Cell T))))) :=
+ sorry
-/- [core::num::nonzero::NonZeroU32::{14}::new] -/
-def core.num.nonzero.NonZeroU32.new :
- U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) :=
- fun _ _ => .fail .panic
-
-/- [core::option::Option::{0}::unwrap] -/
-def core.option.Option.unwrap
- (T : Type) : Option T → State → Result (State × T) :=
- fun _ _ => .fail .panic
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index f0e771f7..a6163c96 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -6,15 +6,18 @@ import External.Types
open Primitives
open external
-/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
- Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
-axiom core.num.nonzero.NonZeroU32.new
- : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
+/- [core::cell::{core::cell::Cell<T>#10}::get]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
+axiom core.cell.Cell.get
+ (T : Type) (markerCopyInst : core.marker.Copy T) :
+ core.cell.Cell T → State → Result (State × T)
-/- [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
- Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
-axiom core.option.Option.unwrap
- (T : Type) : Option T → State → Result (State × T)
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
+axiom core.cell.Cell.get_mut
+ (T : Type) :
+ core.cell.Cell T → State → Result (State × (T × (T → State → Result
+ (State × (core.cell.Cell T)))))
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 961f3e8a..5d4cfc77 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -6,4 +6,10 @@ open Primitives
namespace external
+/- Trait declaration: [core::marker::Copy]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+ Name pattern: core::marker::Copy -/
+structure core.marker.Copy (Self : Type) where
+ cloneCloneInst : core.clone.Clone Self
+
end external
diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean
index 7c30f792..d0f5a0cc 100644
--- a/tests/lean/External/TypesExternal.lean
+++ b/tests/lean/External/TypesExternal.lean
@@ -1,11 +1,20 @@
-- [external]: external types.
import Base
-open Primitives
+open Lean Primitives
/- [core::num::nonzero::NonZeroU32]
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+structure core.cell.Cell (T : Type) :=
+ id : Nat
-/- The state type used in the state-error monad -/
-axiom State : Type
+def CellValue := (T:Type) × T
+
+/- The state type used in the state-error monad
+ TODO: we tried the following definition, but it makes State a Type 1, leading
+ to type errors later:
+
+ structure State :=
+ cells : AssocList Nat CellValue
+ -/
+axiom State : Type
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 84245531..2e6ed6e0 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -4,10 +4,10 @@
import Base
open Primitives
-/- [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
- Name pattern: core::num::nonzero::NonZeroU32 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+/- [core::cell::Cell]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+ Name pattern: core::cell::Cell -/
+axiom core.cell.Cell (T : Type) : Type
/- The state type used in the state-error monad -/
axiom State : Type
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 11:47:32 +0000