Update Primitives.lean

1 files changed, 58 insertions, 90 deletions

diff --git a/backends/lean/Primitives.lean b/backends/lean/Primitives.lean
index 6401bca2..e5634bfe 100644
--- a/backends/lean/Primitives.lean
+++ b/backends/lean/Primitives.lean
@@ -325,18 +325,20 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re
   Scalar.tryMk tgt_ty x.val
 
 -- The scalar types
-def Isize := Scalar .Isize
-def I8    := Scalar .I8
-def I16   := Scalar .I16
-def I32   := Scalar .I32
-def I64   := Scalar .I64
-def I128  := Scalar .I128
-def Usize := Scalar .Usize
-def U8    := Scalar .U8
-def U16   := Scalar .U16
-def U32   := Scalar .U32
-def U64   := Scalar .U64
-def U128  := Scalar .U128
+-- We declare the definitions as reducible so that Lean can unfold them (useful
+-- for type class resolution for instance).
+@[reducible] def Isize := Scalar .Isize
+@[reducible] def I8    := Scalar .I8
+@[reducible] def I16   := Scalar .I16
+@[reducible] def I32   := Scalar .I32
+@[reducible] def I64   := Scalar .I64
+@[reducible] def I128  := Scalar .I128
+@[reducible] def Usize := Scalar .Usize
+@[reducible] def U8    := Scalar .U8
+@[reducible] def U16   := Scalar .U16
+@[reducible] def U32   := Scalar .U32
+@[reducible] def U64   := Scalar .U64
+@[reducible] def U128  := Scalar .U128
 
 -- TODO: below: not sure this is the best way.
 -- Should we rather overload operations like +, -, etc.?
@@ -345,84 +347,50 @@ def U128  := Scalar .U128
 -- read the file, which is not supposed to change a lot)
 
 -- Negation
-def Isize.neg := @Scalar.neg .Isize
-def I8.neg    := @Scalar.neg .I8
-def I16.neg   := @Scalar.neg .I16
-def I32.neg   := @Scalar.neg .I32
-def I64.neg   := @Scalar.neg .I64
-def I128.neg  := @Scalar.neg .I128
 
--- Division
-def Isize.div := @Scalar.div .Isize
-def I8.div    := @Scalar.div .I8
-def I16.div   := @Scalar.div .I16
-def I32.div   := @Scalar.div .I32
-def I64.div   := @Scalar.div .I64
-def I128.div  := @Scalar.div .I128
-def Usize.div := @Scalar.div .Usize
-def U8.div    := @Scalar.div .U8
-def U16.div   := @Scalar.div .U16
-def U32.div   := @Scalar.div .U32
-def U64.div   := @Scalar.div .U64
-def U128.div  := @Scalar.div .U128
+/--
+Remark: there is no heterogeneous negation in the Lean prelude: we thus introduce
+one here.
 
--- Remainder
-def Isize.rem := @Scalar.rem .Isize
-def I8.rem    := @Scalar.rem .I8
-def I16.rem   := @Scalar.rem .I16
-def I32.rem   := @Scalar.rem .I32
-def I64.rem   := @Scalar.rem .I64
-def I128.rem  := @Scalar.rem .I128
-def Usize.rem := @Scalar.rem .Usize
-def U8.rem    := @Scalar.rem .U8
-def U16.rem   := @Scalar.rem .U16
-def U32.rem   := @Scalar.rem .U32
-def U64.rem   := @Scalar.rem .U64
-def U128.rem  := @Scalar.rem .U128
+The notation typeclass for heterogeneous addition.
+This enables the notation `- a : β` where `a : α`.
+-/
+class HNeg (α : Type u) (β : outParam (Type v)) where
+  /-- `- a` computes the negation of `a`.
+  The meaning of this notation is type-dependent. -/
+  hNeg : α → β
+
+prefix:75  "-"   => HNeg.hNeg
+
+instance : HNeg Isize (Result Isize) where hNeg x := Scalar.neg x
+instance : HNeg I8 (Result I8) where hNeg x := Scalar.neg x
+instance : HNeg I16 (Result I16) where hNeg x := Scalar.neg x
+instance : HNeg I32 (Result I32) where hNeg x := Scalar.neg x
+instance : HNeg I64 (Result I64) where hNeg x := Scalar.neg x
+instance : HNeg I128 (Result I128) where hNeg x := Scalar.neg x
 
 -- Addition
-def Isize.add := @Scalar.add .Isize
-def I8.add    := @Scalar.add .I8
-def I16.add   := @Scalar.add .I16
-def I32.add   := @Scalar.add .I32
-def I64.add   := @Scalar.add .I64
-def I128.add  := @Scalar.add .I128
-def Usize.add := @Scalar.add .Usize
-def U8.add    := @Scalar.add .U8
-def U16.add   := @Scalar.add .U16
-def U32.add   := @Scalar.add .U32
-def U64.add   := @Scalar.add .U64
-def U128.add  := @Scalar.add .U128
+instance {ty} : HAdd (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hAdd x y := Scalar.add x y
 
 -- Substraction
-def Isize.sub := @Scalar.sub .Isize
-def I8.sub    := @Scalar.sub .I8
-def I16.sub   := @Scalar.sub .I16
-def I32.sub   := @Scalar.sub .I32
-def I64.sub   := @Scalar.sub .I64
-def I128.sub  := @Scalar.sub .I128
-def Usize.sub := @Scalar.sub .Usize
-def U8.sub    := @Scalar.sub .U8
-def U16.sub   := @Scalar.sub .U16
-def U32.sub   := @Scalar.sub .U32
-def U64.sub   := @Scalar.sub .U64
-def U128.sub  := @Scalar.sub .U128
+instance {ty} : HSub (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hSub x y := Scalar.sub x y
 
 -- Multiplication
-def Isize.mul := @Scalar.mul .Isize
-def I8.mul    := @Scalar.mul .I8
-def I16.mul   := @Scalar.mul .I16
-def I32.mul   := @Scalar.mul .I32
-def I64.mul   := @Scalar.mul .I64
-def I128.mul  := @Scalar.mul .I128
-def Usize.mul := @Scalar.mul .Usize
-def U8.mul    := @Scalar.mul .U8
-def U16.mul   := @Scalar.mul .U16
-def U32.mul   := @Scalar.mul .U32
-def U64.mul   := @Scalar.mul .U64
-def U128.mul  := @Scalar.mul .U128
+instance {ty} : HMul (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hMul x y := Scalar.mul x y
+
+-- Division
+instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hDiv x y := Scalar.div x y
+
+-- Remainder
+instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hMod x y := Scalar.rem x y
 
 -- ofIntCore
+-- TODO: typeclass?
 def Isize.ofIntCore := @Scalar.ofIntCore .Isize
 def I8.ofIntCore    := @Scalar.ofIntCore .I8
 def I16.ofIntCore   := @Scalar.ofIntCore .I16
@@ -436,7 +404,8 @@ def U32.ofIntCore   := @Scalar.ofIntCore .U32
 def U64.ofIntCore   := @Scalar.ofIntCore .U64
 def U128.ofIntCore  := @Scalar.ofIntCore .U128
 
--- ofInt
+--  ofInt
+-- TODO: typeclass?
 def Isize.ofInt := @Scalar.ofInt .Isize
 def I8.ofInt    := @Scalar.ofInt .I8
 def I16.ofInt   := @Scalar.ofInt .I16
@@ -450,6 +419,14 @@ def U32.ofInt   := @Scalar.ofInt .U32
 def U64.ofInt   := @Scalar.ofInt .U64
 def U128.ofInt  := @Scalar.ofInt .U128
 
+-- Comparisons
+instance {ty} : LT (Scalar ty) where
+  lt a b := LT.lt a.val b.val
+
+instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val
+
+instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt ..
+instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe ..
 
 theorem Scalar.eq_of_val_eq {ty} : ∀ {i j : Scalar ty}, Eq i.val j.val → Eq i j
   | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl
@@ -466,15 +443,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
     | isTrue h  => isTrue (Scalar.eq_of_val_eq h)
     | isFalse h => isFalse (Scalar.ne_of_val_ne h)
 
-instance {ty} : LT (Scalar ty) where
-  lt a b := LT.lt a.val b.val
-
-instance {ty} : LE (Scalar ty) where
-  le a b := LE.le a.val b.val
-
-instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt ..
-instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe ..
-
 def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
 
 -- -- We now define a type class that subsumes the various machine integer types, so