From 703261b6c8ad680a925ae0550117a85d9dfa40fe Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 25 Apr 2024 13:42:23 +0200 Subject: Update the tests for External --- tests/coq/misc/External_Funs.v | 77 +++++++----------------- tests/coq/misc/External_FunsExternal.v | 21 +++---- tests/coq/misc/External_FunsExternal_Template.v | 30 ++++----- tests/coq/misc/External_Types.v | 10 +++ tests/coq/misc/External_TypesExternal.v | 5 +- tests/coq/misc/External_TypesExternal_Template.v | 8 +-- tests/coq/misc/Primitives.v | 75 +++++++++++++++++++++++ 7 files changed, 134 insertions(+), 92 deletions(-) (limited to 'tests/coq') 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 *) +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}::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#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}::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#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] *) -- cgit v1.2.3 From e739bde5ee916af9c0c2dcf186173edba1585e4f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 25 Apr 2024 13:53:32 +0200 Subject: Regenerate the Primitives files --- tests/coq/arrays/Primitives.v | 75 ++++++++++++++++++++++++++++++++++ tests/coq/betree/Primitives.v | 75 ++++++++++++++++++++++++++++++++++ tests/coq/demo/Primitives.v | 75 ++++++++++++++++++++++++++++++++++ tests/coq/hashmap/Primitives.v | 75 ++++++++++++++++++++++++++++++++++ tests/coq/hashmap_on_disk/Primitives.v | 75 ++++++++++++++++++++++++++++++++++ tests/coq/traits/Primitives.v | 75 ++++++++++++++++++++++++++++++++++ 6 files changed, 450 insertions(+) (limited to 'tests/coq') 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/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] *) -- cgit v1.2.3