summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives.lean3
-rw-r--r--backends/lean/Base/Primitives/Alloc.lean2
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean2
-rw-r--r--backends/lean/Base/Primitives/Core.lean (renamed from backends/lean/Base/Primitives/CoreOps.lean)23
-rw-r--r--backends/lean/Base/Primitives/CoreConvertNum.lean277
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean79
-rw-r--r--backends/lean/Base/Primitives/Vec.lean39
-rw-r--r--compiler/Extract.ml13
-rw-r--r--compiler/ExtractBuiltin.ml262
-rw-r--r--compiler/ExtractTypes.ml15
-rw-r--r--compiler/TranslateCore.ml19
11 files changed, 674 insertions, 60 deletions
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 7196d2ec..f80c2004 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -4,4 +4,5 @@ import Base.Primitives.Scalar
import Base.Primitives.ArraySlice
import Base.Primitives.Vec
import Base.Primitives.Alloc
-import Base.Primitives.CoreOps
+import Base.Primitives.Core
+import Base.Primitives.CoreConvertNum
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 15fe1ff9..1b15d36d 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -1,6 +1,6 @@
import Lean
import Base.Primitives.Base
-import Base.Primitives.CoreOps
+import Base.Primitives.Core
open Primitives
open Result
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 91ca7284..157f9df1 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic.Linarith
import Base.IList
import Base.Primitives.Scalar
import Base.Primitives.Range
-import Base.Primitives.CoreOps
+import Base.Primitives.Core
import Base.Arith
import Base.Progress.Base
diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/Core.lean
index 1736bfa6..99f65985 100644
--- a/backends/lean/Base/Primitives/CoreOps.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -4,7 +4,13 @@ import Base.Primitives.Base
open Primitives
open Result
-namespace core.ops
+namespace core
+
+/- Trait declaration: [core::convert::From] -/
+structure convert.From (Self T : Type) where
+ from_ : T → Result Self
+
+namespace ops -- core.ops
namespace index -- core.ops.index
@@ -32,4 +38,17 @@ structure DerefMut (Self : Type) where
end deref -- core.ops.deref
-end core.ops
+end ops -- core.ops
+
+/- Trait declaration: [core::clone::Clone] -/
+structure clone.Clone (Self : Type) where
+ clone : Self → Result Self
+
+/- [core::clone::impls::{(core::clone::Clone for bool)#19}::clone] -/
+def clone.impls.CloneBool.clone (b : Bool) : Bool := b
+
+def clone.CloneBool : clone.Clone Bool := {
+ clone := fun b => ok (clone.impls.CloneBool.clone b)
+}
+
+end core
diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
new file mode 100644
index 00000000..eb456a96
--- /dev/null
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -0,0 +1,277 @@
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.Linarith
+import Base.IList
+import Base.Primitives.Scalar
+import Base.Primitives.ArraySlice
+import Base.Arith
+import Base.Progress.Base
+
+namespace Primitives
+
+open Result Error
+
+namespace core.convert
+
+namespace num -- core.convert.num
+
+-- Conversions
+def FromUsizeBool.from (b : Bool) : Usize :=
+ if b then 1#usize else 0#usize
+
+def FromU8Bool.from (b : Bool) : U8 :=
+ if b then 1#u8 else 0#u8
+
+def FromU16Bool.from (b : Bool) : U16 :=
+ if b then 1#u16 else 0#u16
+
+def FromU32Bool.from (b : Bool) : U32 :=
+ if b then 1#u32 else 0#u32
+
+def FromU64Bool.from (b : Bool) : U64 :=
+ if b then 1#u64 else 0#u64
+
+def FromU128Bool.from (b : Bool) : U128 :=
+ if b then 1#u128 else 0#u128
+
+def FromIsizeBool.from (b : Bool) : Isize :=
+ if b then 1#isize else 0#isize
+
+def FromI8Bool.from (b : Bool) : I8 :=
+ if b then 1#i8 else 0#i8
+
+def FromI16Bool.from (b : Bool) : I16 :=
+ if b then 1#i16 else 0#i16
+
+def FromI32Bool.from (b : Bool) : I32 :=
+ if b then 1#i32 else 0#i32
+
+def FromI64Bool.from (b : Bool) : I64 :=
+ if b then 1#i64 else 0#i64
+
+def FromI128Bool.from (b : Bool) : I128 :=
+ if b then 1#i128 else 0#i128
+
+def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromUsizeU16.from (x : U16) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromUsizeU32.from (x : U32) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromUsizeUsize.from (x : Usize) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU8U8.from (x : U8) : U8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU16U8.from (x : U8) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU16U16.from (x : U16) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU32U8.from (x : U8) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU32U16.from (x : U16) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU32U32.from (x : U32) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU64U8.from (x : U8) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU64U16.from (x : U16) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU64U32.from (x : U32) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU64U64.from (x : U64) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU128U8.from (x : U8) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U16.from (x : U16) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U32.from (x : U32) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U64.from (x : U64) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U128.from (x : U128) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromIsizeI8.from (x : I8) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromIsizeI16.from (x : I16) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromIsizeI32.from (x : I32) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromIsizeIsize.from (x : Isize) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI8I8.from (x : I8) : I8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI16I8.from (x : I8) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI16I16.from (x : I16) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI32I8.from (x : I8) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI32I16.from (x : I16) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI32I32.from (x : I32) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI64I8.from (x : I8) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI64I16.from (x : I16) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI64I32.from (x : I32) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI64I64.from (x : I64) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI128I8.from (x : I8) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I16.from (x : I16) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I32.from (x : I32) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I64.from (x : I64) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I128.from (x : I128) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+end num -- core.convert.num
+
+def FromUsizeU8 : core.convert.From Usize U8 := {
+ from_ := fun x => ok (num.FromUsizeU8.from x)
+}
+
+def FromUsizeU16 : core.convert.From Usize U16 := {
+ from_ := fun x => ok (num.FromUsizeU16.from x)
+}
+
+def FromUsizeU32 : core.convert.From Usize U32 := {
+ from_ := fun x => ok (num.FromUsizeU32.from x)
+}
+
+def FromUsizeUsize : core.convert.From Usize Usize := {
+ from_ := fun x => ok (num.FromUsizeUsize.from x)
+}
+
+def FromU8U8 : core.convert.From U8 U8 := {
+ from_ := fun x => ok (num.FromU8U8.from x)
+}
+
+def FromU16U8 : core.convert.From U16 U8 := {
+ from_ := fun x => ok (num.FromU16U8.from x)
+}
+
+def FromU16U16 : core.convert.From U16 U16 := {
+ from_ := fun x => ok (num.FromU16U16.from x)
+}
+
+def FromU32U8 : core.convert.From U32 U8 := {
+ from_ := fun x => ok (num.FromU32U8.from x)
+}
+
+def FromU32U16 : core.convert.From U32 U16 := {
+ from_ := fun x => ok (num.FromU32U16.from x)
+}
+
+def FromU32U32 : core.convert.From U32 U32 := {
+ from_ := fun x => ok (num.FromU32U32.from x)
+}
+
+def FromU64U8 : core.convert.From U64 U8 := {
+ from_ := fun x => ok (num.FromU64U8.from x)
+}
+
+def FromU64U16 : core.convert.From U64 U16 := {
+ from_ := fun x => ok (num.FromU64U16.from x)
+}
+
+def FromU64U32 : core.convert.From U64 U32 := {
+ from_ := fun x => ok (num.FromU64U32.from x)
+}
+
+def FromU64U64 : core.convert.From U64 U64 := {
+ from_ := fun x => ok (num.FromU64U64.from x)
+}
+
+def FromU128U8 : core.convert.From U128 U8 := {
+ from_ := fun x => ok (num.FromU128U8.from x)
+}
+
+def FromU128U16 : core.convert.From U128 U16 := {
+ from_ := fun x => ok (num.FromU128U16.from x)
+}
+
+def FromU128U32 : core.convert.From U128 U32 := {
+ from_ := fun x => ok (num.FromU128U32.from x)
+}
+
+def FromU128U64 : core.convert.From U128 U64 := {
+ from_ := fun x => ok (num.FromU128U64.from x)
+}
+
+def FromU128U128 : core.convert.From U128 U128 := {
+ from_ := fun x => ok (num.FromU128U128.from x)
+}
+
+def FromIsizeI8 : core.convert.From Isize I8 := {
+ from_ := fun x => ok (num.FromIsizeI8.from x)
+}
+
+def FromIsizeI16 : core.convert.From Isize I16 := {
+ from_ := fun x => ok (num.FromIsizeI16.from x)
+}
+
+def FromIsizeI32 : core.convert.From Isize I32 := {
+ from_ := fun x => ok (num.FromIsizeI32.from x)
+}
+
+def FromIsizeIsize : core.convert.From Isize Isize := {
+ from_ := fun x => ok (num.FromIsizeIsize.from x)
+}
+
+def FromI8I8 : core.convert.From I8 I8 := {
+ from_ := fun x => ok (num.FromI8I8.from x)
+}
+
+def FromI16I8 : core.convert.From I16 I8 := {
+ from_ := fun x => ok (num.FromI16I8.from x)
+}
+
+def FromI16I16 : core.convert.From I16 I16 := {
+ from_ := fun x => ok (num.FromI16I16.from x)
+}
+
+def FromI32I8 : core.convert.From I32 I8 := {
+ from_ := fun x => ok (num.FromI32I8.from x)
+}
+
+def FromI32I16 : core.convert.From I32 I16 := {
+ from_ := fun x => ok (num.FromI32I16.from x)
+}
+
+def FromI32I32 : core.convert.From I32 I32 := {
+ from_ := fun x => ok (num.FromI32I32.from x)
+}
+
+def FromI64I8 : core.convert.From I64 I8 := {
+ from_ := fun x => ok (num.FromI64I8.from x)
+}
+
+def FromI64I16 : core.convert.From I64 I16 := {
+ from_ := fun x => ok (num.FromI64I16.from x)
+}
+
+def FromI64I32 : core.convert.From I64 I32 := {
+ from_ := fun x => ok (num.FromI64I32.from x)
+}
+
+def FromI64I64 : core.convert.From I64 I64 := {
+ from_ := fun x => ok (num.FromI64I64.from x)
+}
+
+def FromI128I8 : core.convert.From I128 I8 := {
+ from_ := fun x => ok (num.FromI128I8.from x)
+}
+
+def FromI128I16 : core.convert.From I128 I16 := {
+ from_ := fun x => ok (num.FromI128I16.from x)
+}
+
+def FromI128I32 : core.convert.From I128 I32 := {
+ from_ := fun x => ok (num.FromI128I32.from x)
+}
+
+def FromI128I64 : core.convert.From I128 I64 := {
+ from_ := fun x => ok (num.FromI128I64.from x)
+}
+
+def FromI128I128 : core.convert.From I128 I128 := {
+ from_ := fun x => ok (num.FromI128I128.from x)
+}
+
+-- to_le_bytes
+def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry
+
+-- to_be_bytes
+def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
+
+end core.convert
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 8de2b3f2..b8d93d30 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -2,6 +2,7 @@ import Lean
import Lean.Meta.Tactic.Simp
import Mathlib.Tactic.Linarith
import Base.Primitives.Base
+import Base.Primitives.Core
import Base.Diverge.Base
import Base.Progress.Base
import Base.Arith.Int
@@ -1393,4 +1394,82 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
@[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
simp [eq_equiv]
+-- Leading zeros
+def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry
+def core.num.U8.leading_zeros (x : U8) : U32 := sorry
+def core.num.U16.leading_zeros (x : U16) : U32 := sorry
+def core.num.U32.leading_zeros (x : U32) : U32 := sorry
+def core.num.U64.leading_zeros (x : U64) : U32 := sorry
+def core.num.U128.leading_zeros (x : U128) : U32 := sorry
+
+def core.num.Isize.leading_zeros (x : Isize) : U32 := sorry
+def core.num.I8.leading_zeros (x : I8) : U32 := sorry
+def core.num.I16.leading_zeros (x : I16) : U32 := sorry
+def core.num.I32.leading_zeros (x : I32) : U32 := sorry
+def core.num.I64.leading_zeros (x : I64) : U32 := sorry
+def core.num.I128.leading_zeros (x : I128) : U32 := sorry
+
+-- Clone
+def core.clone.impls.CloneUsize.clone (x : Usize) : Usize := x
+def core.clone.impls.CloneU8.clone (x : U8) : U8 := x
+def core.clone.impls.CloneU16.clone (x : U16) : U16 := x
+def core.clone.impls.CloneU32.clone (x : U32) : U32 := x
+def core.clone.impls.CloneU64.clone (x : U64) : U64 := x
+def core.clone.impls.CloneU128.clone (x : U128) : U128 := x
+
+def core.clone.impls.CloneIsize.clone (x : Isize) : Isize := x
+def core.clone.impls.CloneI8.clone (x : I8) : I8 := x
+def core.clone.impls.CloneI16.clone (x : I16) : I16 := x
+def core.clone.impls.CloneI32.clone (x : I32) : I32 := x
+def core.clone.impls.CloneI64.clone (x : I64) : I64 := x
+def core.clone.impls.CloneI128.clone (x : I128) : I128 := x
+
+def core.clone.CloneUsize : core.clone.Clone Usize := {
+ clone := fun x => ok (core.clone.impls.CloneUsize.clone x)
+}
+
+def core.clone.CloneU8 : core.clone.Clone U8 := {
+ clone := fun x => ok (core.clone.impls.CloneU8.clone x)
+}
+
+def core.clone.CloneU16 : core.clone.Clone U16 := {
+ clone := fun x => ok (core.clone.impls.CloneU16.clone x)
+}
+
+def core.clone.CloneU32 : core.clone.Clone U32 := {
+ clone := fun x => ok (core.clone.impls.CloneU32.clone x)
+}
+
+def core.clone.CloneU64 : core.clone.Clone U64 := {
+ clone := fun x => ok (core.clone.impls.CloneU64.clone x)
+}
+
+def core.clone.CloneU128 : core.clone.Clone U128 := {
+ clone := fun x => ok (core.clone.impls.CloneU128.clone x)
+}
+
+def core.clone.CloneIsize : core.clone.Clone Isize := {
+ clone := fun x => ok (core.clone.impls.CloneIsize.clone x)
+}
+
+def core.clone.CloneI8 : core.clone.Clone I8 := {
+ clone := fun x => ok (core.clone.impls.CloneI8.clone x)
+}
+
+def core.clone.CloneI16 : core.clone.Clone I16 := {
+ clone := fun x => ok (core.clone.impls.CloneI16.clone x)
+}
+
+def core.clone.CloneI32 : core.clone.Clone I32 := {
+ clone := fun x => ok (core.clone.impls.CloneI32.clone x)
+}
+
+def core.clone.CloneI64 : core.clone.Clone I64 := {
+ clone := fun x => ok (core.clone.impls.CloneI64.clone x)
+}
+
+def core.clone.CloneI128 : core.clone.Clone I128 := {
+ clone := fun x => ok (core.clone.impls.CloneI128.clone x)
+}
+
end Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 8e2d65a8..5ed7b606 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -182,4 +182,43 @@ theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
end alloc.vec
+/-- [alloc::slice::{@Slice<T>}::to_vec] -/
+def alloc.slice.Slice.to_vec
+ (T : Type) (cloneInst : core.clone.Clone T) (s : Slice T) : Result (alloc.vec.Vec T) :=
+ -- TODO: we need a monadic map
+ sorry
+
+/-- [core::slice::{@Slice<T>}::reverse] -/
+def core.slice.Slice.reverse (T : Type) (s : Slice T) : Slice T :=
+ ⟨ s.val.reverse, by sorry ⟩
+
+def alloc.vec.Vec.with_capacity (T : Type) (s : Usize) : alloc.vec.Vec T := Vec.new T
+
+/- [alloc::vec::{(core::ops::deref::Deref for alloc::vec::Vec<T, A>)#9}::deref]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2624:4-2624:27
+ Name pattern: alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref -/
+def alloc.vec.DerefVec.deref (T : Type) (v : Vec T) : Slice T :=
+ ⟨ v.val, v.property ⟩
+
+def core.ops.deref.DerefVec (T : Type) : core.ops.deref.Deref (alloc.vec.Vec T) := {
+ Target := Slice T
+ deref := fun v => ok (alloc.vec.DerefVec.deref T v)
+}
+
+/- [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec<T, A>)#10}::deref_mut]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2632:4-2632:39
+ Name pattern: alloc::vec::{core::ops::deref::DerefMut<alloc::vec::Vec<@T, @A>>}::deref_mut -/
+def alloc.vec.DerefMutVec.deref_mut (T : Type) (v : alloc.vec.Vec T) :
+ Result ((Slice T) × (Slice T → Result (alloc.vec.Vec T))) :=
+ ok (⟨ v.val, v.property ⟩, λ s => ok ⟨ s.val, s.property ⟩)
+
+/- Trait implementation: [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec<T, A>)#10}]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2630:0-2630:49
+ Name pattern: core::ops::deref::DerefMut<alloc::vec::Vec<@Self, @>> -/
+def core.ops.deref.DerefMutVec (T : Type) :
+ core.ops.deref.DerefMut (alloc.vec.Vec T) := {
+ derefInst := core.ops.deref.DerefVec T
+ deref_mut := alloc.vec.DerefMutVec.deref_mut T
+}
+
end Primitives
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 6eeef772..8efb59fb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2644,14 +2644,19 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- (let name =
+ (let name, generics =
if !Config.extract_external_name_patterns && not impl.is_local then
- Some impl.llbc_name
- else None
+ let decl_id = impl.impl_trait.trait_decl_id in
+ let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
+ let decl_ref = impl.llbc_impl_trait in
+ ( Some trait_decl.llbc_name,
+ Some (trait_decl.llbc_generics, decl_ref.decl_generics) )
+ else (None, None)
in
extract_comment_with_span ctx fmt
[ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
- name impl.meta.span);
+ (* TODO: why option option for the generics? Looks like a bug in OCaml!? *)
+ name ?generics:(Some generics) impl.meta.span);
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 3ba8d11d..a9b939b5 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -10,6 +10,22 @@ include ExtractName (* TODO: only open? *)
let log = Logging.builtin_log
+let all_int_names =
+ [
+ "usize";
+ "u8";
+ "u16";
+ "u32";
+ "u64";
+ "u128";
+ "isize";
+ "i8";
+ "i16";
+ "i32";
+ "i64";
+ "i128";
+ ]
+
(** Small utility to memoize some computations *)
let mk_memoized (f : unit -> 'a) : unit -> 'a =
let r = ref None in
@@ -215,6 +231,28 @@ let builtin_types_map = mk_memoized mk_builtin_types_map
type builtin_fun_info = { extract_name : string } [@@deriving show]
+let int_and_smaller_list : (string * string) list =
+ let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in
+ let int_names = List.rev [ "i8"; "i16"; "i32"; "i64"; "i128" ] in
+ let rec compute_pairs l =
+ match l with
+ | [] -> []
+ | x :: l -> List.map (fun y -> (x, y)) (x :: l) @ compute_pairs l
+ in
+ [
+ (* Usize *)
+ ("usize", "u8");
+ ("usize", "u16");
+ ("usize", "u32");
+ ("usize", "usize");
+ (* Isize *)
+ ("isize", "i8");
+ ("isize", "i16");
+ ("isize", "i32");
+ ("isize", "isize");
+ ]
+ @ compute_pairs uint_names @ compute_pairs int_names
+
(** The assumed functions.
The optional list of booleans is filtering information for the type
@@ -245,20 +283,7 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
(pattern * bool list option * builtin_fun_info) list =
List.map
(fun ty -> mk_fun (rust_name ty) (Some (extract_name ty)) None)
- [
- "usize";
- "u8";
- "u16";
- "u32";
- "u64";
- "u128";
- "isize";
- "i8";
- "i16";
- "i32";
- "i64";
- "i128";
- ]
+ all_int_names
in
[
mk_fun "core::mem::replace" None None;
@@ -344,6 +369,20 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
"core::slice::index::{core::slice::index::SliceIndex<usize, \
[@T]>}::index_mut"
(Some "core_slice_index_Slice_index_mut") None;
+ mk_fun "alloc::slice::{[@T]}::to_vec" (Some "alloc.slice.Slice.to_vec") None;
+ mk_fun
+ "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity"
+ (Some "alloc.vec.Vec.with_capacity") None;
+ mk_fun "core::slice::{[@T]}::reverse" (Some "core.slice.Slice.reverse") None;
+ mk_fun
+ "alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref"
+ (Some "alloc.vec.DerefVec.deref")
+ (Some [ true; false ]);
+ mk_fun
+ "alloc::vec::{core::ops::deref::DerefMut<alloc::vec::Vec<@T, \
+ @A>>}::deref_mut"
+ (Some "alloc.vec.DerefMutVec.deref_mut")
+ (Some [ true; false ]);
]
@ List.flatten
(List.map
@@ -353,6 +392,52 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
(fun ty ->
StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op))
[ "add"; "sub"; "mul"; "div"; "rem" ])
+ (* From<INT, bool> *)
+ @ mk_scalar_fun
+ (fun ty ->
+ "core::convert::num::{core::convert::From<" ^ ty ^ ", bool>}::from")
+ (fun ty ->
+ "core.convert.num.From"
+ ^ StringUtils.capitalize_first_letter ty
+ ^ "Bool.from")
+ (* From<INT, INT> *)
+ @ List.map
+ (fun (big, small) ->
+ mk_fun
+ ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
+ ^ ">}::from")
+ (Some
+ ("core.convert.num.From"
+ ^ StringUtils.capitalize_first_letter big
+ ^ StringUtils.capitalize_first_letter small
+ ^ ".from"))
+ None)
+ int_and_smaller_list
+ (* Leading zeros *)
+ @ mk_scalar_fun
+ (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
+ (fun ty ->
+ "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros")
+ (* to_le_bytes *)
+ @ mk_scalar_fun
+ (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes")
+ (fun ty ->
+ "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes")
+ (* to_be_bytes *)
+ @ mk_scalar_fun
+ (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes")
+ (fun ty ->
+ "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes")
+ (* Clone<bool> *)
+ @ [
+ mk_fun "core::clone::impls::{core::clone::Clone<bool>}::clone"
+ (Some "core.clone.CloneBool.clone") None;
+ ]
+ (* Clone<INT> *)
+ @ mk_scalar_fun
+ (fun ty -> "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
+ (fun ty ->
+ "core.clone.Clone" ^ StringUtils.capitalize_first_letter ty ^ ".clone")
let mk_builtin_funs_map () =
let m =
@@ -370,36 +455,57 @@ let builtin_funs_map = mk_memoized mk_builtin_funs_map
type effect_info = { can_fail : bool; stateful : bool }
let builtin_fun_effects =
- let int_names =
- [
- "usize";
- "u8";
- "u16";
- "u32";
- "u64";
- "u128";
- "isize";
- "i8";
- "i16";
- "i32";
- "i64";
- "i128";
- ]
- in
let int_ops =
[ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ]
in
let int_funs =
List.map
(fun int_name ->
+ List.map (fun op -> "core::num::" ^ "{" ^ int_name ^ "}::" ^ op) int_ops)
+ all_int_names
+ @ List.map
+ (fun op ->
+ List.map
+ (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
+ all_int_names)
+ [ "add"; "sub"; "mul"; "div"; "rem" ]
+ (* From<INT, bool> *)
+ @ [
List.map
- (fun op ->
- "core::num::" ^ "{"
- ^ StringUtils.capitalize_first_letter int_name
- ^ "}::" ^ op)
- int_ops)
- int_names
+ (fun int_name ->
+ "core::convert::num::{core::convert::From<" ^ int_name
+ ^ ", bool>}::from")
+ all_int_names;
+ ]
+ (* From<INT, INT> *)
+ @ [
+ List.map
+ (fun (big, small) ->
+ "core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
+ ^ ">}::from")
+ int_and_smaller_list;
+ ]
+ (* Leading zeros *)
+ @ [
+ List.map
+ (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
+ all_int_names;
+ ]
+ (* to_{le,be}_bytes *)
+ @ List.map
+ (fun ty ->
+ let pre = "core::num::{" ^ ty ^ "}::" in
+ [ pre ^ "to_le_bytes"; pre ^ "to_be_bytes" ])
+ all_int_names
+ (* clone *)
+ @ [
+ List.map
+ (fun ty ->
+ "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
+ all_int_names;
+ ]
in
+
let int_funs = List.concat int_funs in
let no_fail_no_state_funs =
[
@@ -409,6 +515,10 @@ let builtin_fun_effects =
"alloc::vec::{alloc::vec::Vec<@T, @A>}::len";
"core::mem::replace";
"core::mem::take";
+ "core::clone::impls::{core::clone::Clone<bool>}::clone";
+ "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity";
+ "core::slice::{[@T]}::reverse";
+ "alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref";
]
@ int_funs
in
@@ -454,7 +564,9 @@ type builtin_trait_decl_info = {
let builtin_trait_decls_info () =
let mk_trait (rust_name : string) ?(extract_name : string option = None)
?(parent_clauses : string list = []) ?(types : string list = [])
- ?(methods : string list = []) () : builtin_trait_decl_info =
+ ?(methods : string list = [])
+ ?(methods_with_extract : (string * string) list option = None) () :
+ builtin_trait_decl_info =
let rust_name = parse_pattern rust_name in
let extract_name =
match extract_name with
@@ -482,16 +594,22 @@ let builtin_trait_decls_info () =
List.map mk_type types
in
let methods =
- let mk_method item_name =
- (* TODO: factor out with builtin_funs_info *)
- let basename =
- if !record_fields_short_names then item_name
- else extract_name ^ "_" ^ item_name
- in
- let fwd = { extract_name = basename } in
- (item_name, fwd)
- in
- List.map mk_method methods
+ match methods_with_extract with
+ | None ->
+ let mk_method item_name =
+ (* TODO: factor out with builtin_funs_info *)
+ let basename =
+ if !record_fields_short_names then item_name
+ else extract_name ^ "_" ^ item_name
+ in
+ let fwd = { extract_name = basename } in
+ (item_name, fwd)
+ in
+ List.map mk_method methods
+ | Some methods ->
+ List.map
+ (fun (item_name, extract_name) -> (item_name, { extract_name }))
+ methods
in
{
rust_name;
@@ -531,6 +649,12 @@ let builtin_trait_decls_info () =
"index_mut";
]
();
+ (* From *)
+ mk_trait "core::convert::From"
+ ~methods_with_extract:(Some [ ("from", "from_") ])
+ ();
+ (* Clone *)
+ mk_trait "core::clone::Clone" ~methods:[ "clone" ] ();
]
let mk_builtin_trait_decls_map () =
@@ -601,7 +725,51 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexMutInst")
~filter:(Some [ true; true; false ])
();
+ (* core::clone::impls::{core::clone::Clone for bool} *)
+ fmt "core::clone::Clone<bool>" ~extract_name:(Some "core::clone::CloneBool")
+ ();
+ fmt "core::ops::deref::Deref<alloc::vec::Vec<@Self, @>>"
+ ~extract_name:(Some "alloc.vec.DerefVec")
+ ~filter:(Some [ true; false ])
+ ();
+ fmt "core::ops::deref::DerefMut<alloc::vec::Vec<@Self, @>>"
+ ~extract_name:(Some "alloc.vec.DerefMutVec")
+ ~filter:(Some [ true; false ])
+ ();
]
+ (* From<INT, bool> *)
+ @ List.map
+ (fun ty ->
+ fmt
+ ("core::convert::From<" ^ ty ^ ", bool>")
+ ~extract_name:
+ (Some
+ ("core.convert.From"
+ ^ StringUtils.capitalize_first_letter ty
+ ^ "Bool"))
+ ())
+ all_int_names
+ (* From<INT, INT> *)
+ @ List.map
+ (fun (big, small) ->
+ fmt
+ ("core::convert::From<" ^ big ^ ", " ^ small ^ ">")
+ ~extract_name:
+ (Some
+ ("core.convert.From"
+ ^ StringUtils.capitalize_first_letter big
+ ^ StringUtils.capitalize_first_letter small))
+ ())
+ int_and_smaller_list
+ (* Clone<INT> *)
+ @ List.map
+ (fun ty ->
+ fmt
+ ("core::clone::Clone<" ^ ty ^ ">")
+ ~extract_name:
+ (Some ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty))
+ ())
+ all_int_names
let mk_builtin_trait_impls_map () =
let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 1c3657a3..c2eb8da0 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1141,7 +1141,9 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
F.pp_close_box fmt ()
let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
- (sl : string list) (name : Types.name option) (span : Meta.span) : unit =
+ (sl : string list) (name : Types.name option)
+ ?(generics : (Types.generic_params * Types.generic_args) option = None)
+ (span : Meta.span) : unit =
let file = match span.file with Virtual s | Local s -> s in
let loc_to_string (l : Meta.loc) : string =
string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -1151,10 +1153,15 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
^ loc_to_string span.end_loc
in
let name =
- match name with
- | None -> []
- | Some name ->
+ match (name, generics) with
+ | None, _ -> []
+ | Some name, None ->
[ "Name pattern: " ^ name_to_pattern_string ctx.trans_ctx name ]
+ | Some name, Some (params, args) ->
+ [
+ "Name pattern: "
+ ^ name_with_generics_to_pattern_string ctx.trans_ctx name params args;
+ ]
in
extract_comment fmt (sl @ [ span ] @ name)
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index 3e4c7375..688cbe34 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -91,3 +91,22 @@ let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string =
in
let pat = Charon.NameMatcher.name_to_pattern mctx c n in
Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
+
+let name_with_generics_to_pattern_string (ctx : trans_ctx) (n : Types.name)
+ (params : Types.generic_params) (args : Types.generic_args) : string =
+ let mctx : Charon.NameMatcher.ctx =
+ {
+ type_decls = ctx.type_ctx.type_decls;
+ global_decls = ctx.global_ctx.global_decls;
+ fun_decls = ctx.fun_ctx.fun_decls;
+ trait_decls = ctx.trait_decls_ctx.trait_decls;
+ trait_impls = ctx.trait_impls_ctx.trait_impls;
+ }
+ in
+ let c : Charon.NameMatcher.to_pat_config =
+ { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+ in
+ let pat =
+ Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args
+ in
+ Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:49:08 +0000