summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/coq/Primitives.v75
-rw-r--r--backends/fstar/Primitives.fst75
-rw-r--r--backends/lean/Base/Primitives/Base.lean4
3 files changed, 154 insertions, 0 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index e84d65ce..5ffda12f 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/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/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index acdb09dc..c7c9f9db 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/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/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index ac4fd340..d682e926 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -135,6 +135,10 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
----------
@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a × a := (x, x)
+/- [core::option::Option::take] -/
+@[simp] def Option.take (T: Type) (self: Option T): Option T × Option T := (self, .none)
+/- [core::mem::swap] -/
+@[simp] def core.mem.swap (T: Type) (a b: T): T × T := (b, a)
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/