Fill out more of the primitives file, attempt at type classes for scalar_cast

1 files changed, 26 insertions, 2 deletions

diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean
index 3f1d13f1..0a51aacd 100644
--- a/backends/lean/primitives.lean
+++ b/backends/lean/primitives.lean
@@ -1,5 +1,6 @@
 import Lean
 import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
 
 -------------
 -- PRELUDE --
@@ -140,7 +141,7 @@ def USize.checked_add (n: USize) (m: USize): result USize :=
 def USize.checked_rem (n: USize) (m: USize): result USize :=
   if h: m > 0 then
     .ret ⟨ n.val % m.val, by
-      have h1: m.val < USize.size := m.val.isLt
+      have h1: ↑m.val < USize.size := m.val.isLt
       have h2: n.val.val % m.val.val < m.val.val := @Nat.mod_lt n.val m.val h
       apply Nat.lt_trans h2 h1
     ⟩
@@ -156,13 +157,36 @@ def USize.checked_mul (n: USize) (m: USize): result USize :=
 def USize.checked_div (n: USize) (m: USize): result USize :=
   if m > 0 then
     .ret ⟨ n.val / m.val, by
-      have h1: n.val < USize.size := n.val.isLt
+      have h1: ↑n.val < USize.size := n.val.isLt
       have h2: n.val.val / m.val.val <= n.val.val := @Nat.div_le_self n.val m.val
       apply Nat.lt_of_le_of_lt h2 h1
     ⟩
   else
     .fail integerOverflow
 
+class MachineInteger (t: Type) where
+  size: Nat
+  val: t -> Fin size
+  ofNatCore: (n:Nat) -> LT.lt n size -> t
+
+set_option hygiene false in
+run_cmd
+  for typeName in [`UInt8, `UInt16, `UInt32, `UInt64, `USize].map Lean.mkIdent do
+  Lean.Elab.Command.elabCommand (← `(
+    namespace $typeName
+    instance: MachineInteger $typeName where
+      size := size
+      val := val
+      ofNatCore := ofNatCore
+    end $typeName
+  ))
+
+def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): result dst :=
+  if h: MachineInteger.val x < MachineInteger.size dst then
+    .ret (MachineInteger.ofNatCore (MachineInteger.val x).val h)
+  else
+    .fail integerOverflow
+
 -- One needs to perform a little bit of reasoning in order to successfully
 -- inject constants into USize, so we provide a general-purpose macro