Add more definitions to the Lean library

5 files changed, 200 insertions, 0 deletions

diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean
index f67da7d7..99f65985 100644
--- a/backends/lean/Base/Primitives/Core.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -40,4 +40,15 @@ end deref -- core.ops.deref
 
 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
index d76fba37..eb456a96 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -258,6 +258,20 @@ 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 9eb5a794..b8d93d30 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1409,4 +1409,67 @@ 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/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index ac7a4a24..a9b939b5 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -369,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
@@ -404,6 +418,26 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
       (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 =
@@ -457,6 +491,19 @@ let builtin_fun_effects =
           (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
@@ -468,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
@@ -602,6 +653,8 @@ let builtin_trait_decls_info () =
     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 () =
@@ -672,6 +725,17 @@ 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
@@ -697,6 +761,15 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
                ^ 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