diff options
Diffstat (limited to '')
32 files changed, 1297 insertions, 223 deletions
diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v index e84d65ce..5ffda12f 100644 --- a/tests/coq/arrays/Primitives.v +++ b/tests/coq/arrays/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/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v index e84d65ce..5ffda12f 100644 --- a/tests/coq/betree/Primitives.v +++ b/tests/coq/betree/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/coq/demo/Primitives.v b/tests/coq/demo/Primitives.v index e84d65ce..5ffda12f 100644 --- a/tests/coq/demo/Primitives.v +++ b/tests/coq/demo/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/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v index e84d65ce..5ffda12f 100644 --- a/tests/coq/hashmap/Primitives.v +++ b/tests/coq/hashmap/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/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v index e84d65ce..5ffda12f 100644 --- a/tests/coq/hashmap_on_disk/Primitives.v +++ b/tests/coq/hashmap_on_disk/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/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 8658236f..b3e4a129 100644 --- a/tests/coq/misc/External_FunsExternal_Template.v +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -11,18 +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::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/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v index e84d65ce..5ffda12f 100644 --- a/tests/coq/traits/Primitives.v +++ b/tests/coq/traits/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/arrays/Primitives.fst b/tests/fstar/arrays/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/arrays/Primitives.fst +++ b/tests/fstar/arrays/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/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/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/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/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/fstar/demo/Primitives.fst b/tests/fstar/demo/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/demo/Primitives.fst +++ b/tests/fstar/demo/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/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/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/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/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/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 64d6d883..9436cf86 100644 --- a/tests/fstar/misc/External.FunsExternal.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -6,14 +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::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/fstar/traits/Primitives.fst b/tests/fstar/traits/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/traits/Primitives.fst +++ b/tests/fstar/traits/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/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 57b334fa..0c31b9bc 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -238,11 +238,11 @@ divergent def betree.Node.apply_upserts betree.Node.apply_upserts msgs1 (some v) key st else do - let v ← core.option.Option.unwrap U64 prev + let (st1, v) ← core.option.Option.unwrap U64 prev st let msgs1 ← betree.List.push_front (U64 × betree.Message) msgs (key, betree.Message.Insert v) - Result.ok (st, (v, msgs1)) + Result.ok (st1, (v, msgs1)) /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 3bdd70e3..20c4b8e5 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -7,59 +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 - let o1 ← core.option.Option.unwrap core.num.nonzero.NonZeroU32 o - Result.ok (st1, o1) - -/- [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 7adf0922..c3e8dd79 100644 --- a/tests/lean/External/FunsExternal.lean +++ b/tests/lean/External/FunsExternal.lean @@ -4,14 +4,13 @@ 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::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::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 diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index 34b0552a..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::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 - (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 + (T : Type) (markerCopyInst : core.marker.Copy T) : + core.cell.Cell 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)) +/- [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 |