[ refactor ] use proper int types for Constant (#1964)

* [ refactor ] user proper int types for Constant

* [ cleanup ] declare standalone TTC implementations for BitsN/IntN

Rather than doing the casting inline, have the (en/de)coding all
side by side in one place

* [ cleanup ] remove duplicated code

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>

idris2api.ipkg

@@ -152,6 +152,7 @@ modules =
     Libraries.Data.List1,
     Libraries.Data.NameMap,
     Libraries.Data.PosMap,
+    Libraries.Data.Primitives,
     Libraries.Data.SortedMap,
     Libraries.Data.SortedSet,
     Libraries.Data.String.Extra,

libs/base/Decidable/Equality.idr

@@ -128,12 +128,10 @@ DecEq a => DecEq (List1 a) where
 -- for computation in a higher order setting.
 
 
---------------------------------------------------------------------------------
+||| An unsafe decidable equality implementation based on boolean equality.
--- Int
+||| Useful for builtin types.
---------------------------------------------------------------------------------
-
 public export
-implementation DecEq Int where
+[FromEq] Eq a => DecEq a where
     decEq x y = case x == y of -- Blocks if x or y not concrete
                      True => Yes primitiveEq
                      False => No primitiveNotEq
@@ -142,153 +140,95 @@ implementation DecEq Int where
              primitiveNotEq : forall x, y . Not (x = y)
              primitiveNotEq prf = believe_me {b = Void} ()
 
+--------------------------------------------------------------------------------
+-- Int
+--------------------------------------------------------------------------------
+
+public export
+DecEq Int where
+    decEq = decEq @{FromEq}
+
 --------------------------------------------------------------------------------
 -- Bits8
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Bits8 where
+DecEq Bits8 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Bits16
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Bits16 where
+DecEq Bits16 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Bits32
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Bits32 where
+DecEq Bits32 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Bits64
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Bits64 where
+DecEq Bits64 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Int8
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Int8 where
+DecEq Int8 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Int16
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Int16 where
+DecEq Int16 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Int32
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Int32 where
+DecEq Int32 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Int64
 --------------------------------------------------------------------------------
 
 public export
-implementation DecEq Int64 where
+DecEq Int64 where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Char
 --------------------------------------------------------------------------------
 public export
-implementation DecEq Char where
+DecEq Char where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- Integer
 --------------------------------------------------------------------------------
 public export
-implementation DecEq Integer where
+DecEq Integer where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()
 
 --------------------------------------------------------------------------------
 -- String
 --------------------------------------------------------------------------------
 public export
-implementation DecEq String where
+DecEq String where
-    decEq x y = case x == y of -- Blocks if x or y not concrete
+    decEq = decEq @{FromEq}
-                     True => Yes primitiveEq
-                     False => No primitiveNotEq
-       where primitiveEq : forall x, y . x = y
-             primitiveEq = believe_me (Refl {x})
-             primitiveNotEq : forall x, y . Not (x = y)
-             primitiveNotEq prf = believe_me {b = Void} ()

src/Compiler/RefC/RefC.idr

@@ -109,8 +109,8 @@ showIntMin x = if x == -9223372036854775808
     then "INT64_MIN"
     else "INT64_C("++ show x ++")"
 
-showIntegerMin : Integer -> String
+showInt64Min : Int64 -> String
-showIntegerMin x = if x == -9223372036854775808
+showInt64Min x = if x == -9223372036854775808
     then "INT64_MIN"
     else "INT64_C("++ show x ++")"
 
@@ -119,7 +119,7 @@ cConstant (I x) = "(Value*)makeInt64("++ showIntMin x ++")"
 cConstant (I8 x) = "(Value*)makeInt8(INT8_C("++ show x ++"))"
 cConstant (I16 x) = "(Value*)makeInt16(INT16_C("++ show x ++"))"
 cConstant (I32 x) = "(Value*)makeInt32(INT32_C("++ show x ++"))"
-cConstant (I64 x) = "(Value*)makeInt64("++ showIntegerMin x ++")"
+cConstant (I64 x) = "(Value*)makeInt64("++ showInt64Min x ++")"
 cConstant (BI x) = "(Value*)makeIntegerLiteral(\""++ show x ++"\")"
 cConstant (Db x) = "(Value*)makeDouble("++ show x ++")"
 cConstant (Ch x) = "(Value*)makeChar("++ escapeChar x ++")"
@@ -440,16 +440,16 @@ const2Integer : Constant -> Integer -> Integer
 const2Integer c i =
     case c of
         (I x) => cast x
-        (I8 x) => x
+        (I8 x) => cast x
-        (I16 x) => x
+        (I16 x) => cast x
-        (I32 x) => x
+        (I32 x) => cast x
-        (I64 x) => x
+        (I64 x) => cast x
-        (BI x) => x
+        (BI x) => cast x
         (Ch x) => cast x
         (B8 x) => cast x
         (B16 x) => cast x
         (B32 x) => cast x
-        (B64 x) => x
+        (B64 x) => cast x
         _ => i
 
 

src/Core/Binary.idr

@@ -33,7 +33,7 @@ import public Libraries.Utils.Binary
 ||| (Increment this when changing anything in the data format)
 export
 ttcVersion : Int
-ttcVersion = 64
+ttcVersion = 65
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Binary/Prims.idr

@@ -388,6 +388,46 @@ TTC Integer where
                       pure (fromLimbs val)
               _ => corrupt "Integer"
 
+export
+TTC Bits8 where
+  toBuf b x = toBuf b $ cast {to = Int} x
+  fromBuf b = cast {from = Int} <$> fromBuf b
+
+export
+TTC Bits16 where
+  toBuf b x = toBuf b $ cast {to = Int} x
+  fromBuf b = cast {from = Int} <$> fromBuf b
+
+export
+TTC Bits32 where
+  toBuf b x = toBuf b $ cast {to = Integer} x
+  fromBuf b = cast {from = Integer} <$> fromBuf b
+
+export
+TTC Bits64 where
+  toBuf b x = toBuf b $ cast {to = Integer} x
+  fromBuf b = cast {from = Integer} <$> fromBuf b
+
+export
+TTC Int8 where
+  toBuf b x = toBuf b $ cast {to = Int} x
+  fromBuf b = cast {from = Int} <$> fromBuf b
+
+export
+TTC Int16 where
+  toBuf b x = toBuf b $ cast {to = Int} x
+  fromBuf b = cast {from = Int} <$> fromBuf b
+
+export
+TTC Int32 where
+  toBuf b x = toBuf b $ cast {to = Int} x
+  fromBuf b = cast {from = Int} <$> fromBuf b
+
+export
+TTC Int64 where
+  toBuf b x = toBuf b $ cast {to = Integer} x
+  fromBuf b = cast {from = Integer} <$> fromBuf b
+
 export
 TTC Nat where
   toBuf b val = toBuf b (cast {to=Integer} val)
@@ -429,4 +469,3 @@ hashFileWith (Just sha256sum) fileName
     osEscape = if isWindows
       then id
       else escapeStringUnix
-

src/Core/Hash.idr

@@ -32,6 +32,38 @@ export
 Hashable Int where
   hash = id
 
+export
+Hashable Int8 where
+  hash = cast
+
+export
+Hashable Int16 where
+  hash = cast
+
+export
+Hashable Int32 where
+  hash = cast
+
+export
+Hashable Int64 where
+  hash = cast
+
+export
+Hashable Bits8 where
+  hash = cast
+
+export
+Hashable Bits16 where
+  hash = cast
+
+export
+Hashable Bits32 where
+  hash = cast
+
+export
+Hashable Bits64 where
+  hash = cast
+
 export
 Hashable Integer where
   hash = fromInteger

src/Core/Primitives.idr

@@ -47,162 +47,85 @@ castString _ = Nothing
 
 castInteger : Vect 1 (NF vars) -> Maybe (NF vars)
 castInteger [NPrimVal fc (I i)] = Just (NPrimVal fc (BI (cast i)))
-castInteger [NPrimVal fc (I8 i)] = Just (NPrimVal fc (BI i))
+castInteger [NPrimVal fc (I8 i)] = Just (NPrimVal fc (BI (cast i)))
-castInteger [NPrimVal fc (I16 i)] = Just (NPrimVal fc (BI i))
+castInteger [NPrimVal fc (I16 i)] = Just (NPrimVal fc (BI (cast i)))
-castInteger [NPrimVal fc (I32 i)] = Just (NPrimVal fc (BI i))
+castInteger [NPrimVal fc (I32 i)] = Just (NPrimVal fc (BI (cast i)))
-castInteger [NPrimVal fc (I64 i)] = Just (NPrimVal fc (BI i))
+castInteger [NPrimVal fc (I64 i)] = Just (NPrimVal fc (BI (cast i)))
 castInteger [NPrimVal fc (B8 i)] = Just (NPrimVal fc (BI (cast i)))
 castInteger [NPrimVal fc (B16 i)] = Just (NPrimVal fc (BI (cast i)))
 castInteger [NPrimVal fc (B32 i)] = Just (NPrimVal fc (BI (cast i)))
-castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI i))
+castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI (cast i)))
 castInteger [NPrimVal fc (Ch i)] = Just (NPrimVal fc (BI (cast (cast {to=Int} i))))
 castInteger [NPrimVal fc (Db i)] = Just (NPrimVal fc (BI (cast i)))
 castInteger [NPrimVal fc (Str i)] = Just (NPrimVal fc (BI (cast i)))
 castInteger _ = Nothing
 
 castInt : Vect 1 (NF vars) -> Maybe (NF vars)
-castInt [NPrimVal fc (I8 i)] = Just (NPrimVal fc (I (fromInteger i)))
+castInt [NPrimVal fc (I8 i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (I16 i)] = Just (NPrimVal fc (I (fromInteger i)))
+castInt [NPrimVal fc (I16 i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (I32 i)] = Just (NPrimVal fc (I (fromInteger i)))
+castInt [NPrimVal fc (I32 i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (I64 i)] = Just (NPrimVal fc (I (fromInteger i)))
+castInt [NPrimVal fc (I64 i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (fromInteger i)))
+castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I i))
+castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I i))
+castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I i))
+castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I (cast i)))
-castInt [NPrimVal fc (B64 i)] = Just (NPrimVal fc (I (fromInteger i)))
+castInt [NPrimVal fc (B64 i)] = Just (NPrimVal fc (I (cast i)))
 castInt [NPrimVal fc (Db i)] = Just (NPrimVal fc (I (cast i)))
 castInt [NPrimVal fc (Ch i)] = Just (NPrimVal fc (I (cast i)))
 castInt [NPrimVal fc (Str i)] = Just (NPrimVal fc (I (cast i)))
 castInt _ = Nothing
 
-b8max : Int
-b8max = 0x100
-
-b16max : Int
-b16max = 0x10000
-
-b32max : Int
-b32max = 0x100000000
-
-b64max : Integer
-b64max = 18446744073709551616 -- 0x10000000000000000
-
-bitCastWrap : Ord a => Integral a => (i : a) -> (max : a) -> a
-bitCastWrap i max
-    = if i >= 0 -- oops, we don't have `rem` yet!
-        then i `mod` max
-        else max + i `mod` max
-
-bit8CastWrap : (i : Int) -> Int
-bit8CastWrap i = bitCastWrap i b8max
-
-bit16CastWrap : (i : Int) -> Int
-bit16CastWrap i = bitCastWrap i b16max
-
-bit32CastWrap : (i : Int) -> Int
-bit32CastWrap i = bitCastWrap i b32max
-
-bit64CastWrap : (i : Integer) -> Integer
-bit64CastWrap i = bitCastWrap i b64max
-
-int8max : Integer
-int8max = 0x80
-
-int16max : Integer
-int16max = 0x8000
-
-int32max : Integer
-int32max = 0x80000000
-
-int64max : Integer
-int64max = 0x8000000000000000
-
-intCastWrap : (i : Integer) -> (max : Integer) -> Integer
-intCastWrap i max =
-  let max2 = 2*max
-      i2   = i `mod` max2
-      i3   = if i2 < 0 then i2 + max2 else i2
-   in if i3 >= max then i3 - max2 else i3
-
-int8CastWrap : (i : Integer) -> Integer
-int8CastWrap i = intCastWrap i int8max
-
-int16CastWrap : (i : Integer) -> Integer
-int16CastWrap i = intCastWrap i int16max
-
-int32CastWrap : (i : Integer) -> Integer
-int32CastWrap i = intCastWrap i int32max
-
-int64CastWrap : (i : Integer) -> Integer
-int64CastWrap i = intCastWrap i int64max
-
 constantIntegerValue : Constant -> Maybe Integer
 constantIntegerValue (I i)   = Just $ cast i
-constantIntegerValue (I8 i)   = Just i
+constantIntegerValue (I8 i)   = Just $ cast i
-constantIntegerValue (I16 i)   = Just i
+constantIntegerValue (I16 i)   = Just $ cast i
-constantIntegerValue (I32 i)   = Just i
+constantIntegerValue (I32 i)   = Just $ cast i
-constantIntegerValue (I64 i)   = Just i
+constantIntegerValue (I64 i)   = Just $ cast i
 constantIntegerValue (BI i)  = Just i
 constantIntegerValue (B8 i)  = Just $ cast i
 constantIntegerValue (B16 i) = Just $ cast i
 constantIntegerValue (B32 i) = Just $ cast i
-constantIntegerValue (B64 i) = Just i
+constantIntegerValue (B64 i) = Just $ cast i
 constantIntegerValue _       = Nothing
 
 castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
-castBits8 [NPrimVal fc constant] = do
+castBits8 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . B8 . cast <$> constantIntegerValue constant
-    let wrapped = bitCastWrap value (cast b8max)
-    pure (NPrimVal fc (B8 (cast wrapped)))
 castBits8 _ = Nothing
 
 castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)
-castBits16 [NPrimVal fc constant] = do
+castBits16 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . B16 . cast <$> constantIntegerValue constant
-    let wrapped = bitCastWrap value (cast b16max)
-    pure (NPrimVal fc (B16 (cast wrapped)))
 castBits16 _ = Nothing
 
 castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
-castBits32 [NPrimVal fc constant] = do
+castBits32 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . B32 . cast <$> constantIntegerValue constant
-    let wrapped = bitCastWrap value (cast b32max)
-    pure (NPrimVal fc (B32 (cast wrapped)))
 castBits32 _ = Nothing
 
 castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
-castBits64 [NPrimVal fc constant] = do
+castBits64 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . B64 . cast <$> constantIntegerValue constant
-    let wrapped = bitCastWrap value b64max
-    pure (NPrimVal fc (B64 wrapped))
 castBits64 _ = Nothing
 
 castInt8 : Vect 1 (NF vars) -> Maybe (NF vars)
-castInt8 [NPrimVal fc constant] = do
+castInt8 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . I8 . cast <$> constantIntegerValue constant
-    let wrapped = int8CastWrap value
-    pure (NPrimVal fc (I8 wrapped))
 castInt8 _ = Nothing
 
 castInt16 : Vect 1 (NF vars) -> Maybe (NF vars)
-castInt16 [NPrimVal fc constant] = do
+castInt16 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . I16 . cast <$> constantIntegerValue constant
-    let wrapped = int16CastWrap value
-    pure (NPrimVal fc (I16 wrapped))
 castInt16 _ = Nothing
 
 castInt32 : Vect 1 (NF vars) -> Maybe (NF vars)
-castInt32 [NPrimVal fc constant] = do
+castInt32 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . I32 . cast <$> constantIntegerValue constant
-    let wrapped = int32CastWrap value
-    pure (NPrimVal fc (I32 wrapped))
 castInt32 _ = Nothing
 
 castInt64 : Vect 1 (NF vars) -> Maybe (NF vars)
-castInt64 [NPrimVal fc constant] = do
+castInt64 [NPrimVal fc constant] =
-    value <- constantIntegerValue constant
+    NPrimVal fc . I64 . cast <$> constantIntegerValue constant
-    let wrapped = int64CastWrap value
-    pure (NPrimVal fc (I64 wrapped))
 castInt64 _ = Nothing
 
 castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
@@ -211,12 +134,25 @@ castDouble [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Db (cast i)))
 castDouble [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Db (cast i)))
 castDouble [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Db (cast i)))
 castDouble [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Db (cast i)))
+castDouble [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Db (cast i)))
+castDouble [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Db (cast i)))
+castDouble [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Db (cast i)))
+castDouble [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Db (cast i)))
 castDouble [NPrimVal fc (BI i)] = Just (NPrimVal fc (Db (cast i)))
 castDouble [NPrimVal fc (Str i)] = Just (NPrimVal fc (Db (cast i)))
 castDouble _ = Nothing
 
 castChar : Vect 1 (NF vars) -> Maybe (NF vars)
 castChar [NPrimVal fc (I i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Ch (cast i)))
+castChar [NPrimVal fc (BI i)] = Just (NPrimVal fc (Ch (cast i)))
 castChar _ = Nothing
 
 strLength : Vect 1 (NF vars) -> Maybe (NF vars)
@@ -266,14 +202,14 @@ strSubstr _ = Nothing
 add : Constant -> Constant -> Maybe Constant
 add (BI x) (BI y) = pure $ BI (x + y)
 add (I x) (I y) = pure $ I (x + y)
-add (I8 x) (I8 y) = pure $ I8 (int8CastWrap $ x + y)
+add (I8 x) (I8 y) = pure $ I8 (x + y)
-add (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x + y)
+add (I16 x) (I16 y) = pure $ I16 (x + y)
-add (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x + y)
+add (I32 x) (I32 y) = pure $ I32 (x + y)
-add (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ x + y)
+add (I64 x) (I64 y) = pure $ I64 (x + y)
-add (B8 x) (B8 y) = pure $ B8 $ (x + y) `mod` b8max
+add (B8 x) (B8 y) = pure $ B8 (x + y)
-add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` b16max
+add (B16 x) (B16 y) = pure $ B16 (x + y)
-add (B32 x) (B32 y) = pure $ B32 $ (x + y) `mod` b32max
+add (B32 x) (B32 y) = pure $ B32 (x + y)
-add (B64 x) (B64 y) = pure $ B64 $ (x + y) `mod` b64max
+add (B64 x) (B64 y) = pure $ B64 (x + y)
 add (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x + cast y))
 add (Db x) (Db y) = pure $ Db (x + y)
 add _ _ = Nothing
@@ -281,29 +217,29 @@ add _ _ = Nothing
 sub : Constant -> Constant -> Maybe Constant
 sub (BI x) (BI y) = pure $ BI (x - y)
 sub (I x) (I y) = pure $ I (x - y)
-sub (I8 x) (I8 y) = pure $ I8 (int8CastWrap $ x - y)
+sub (I8 x) (I8 y) = pure $ I8 (x - y)
-sub (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x - y)
+sub (I16 x) (I16 y) = pure $ I16 (x - y)
-sub (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x - y)
+sub (I32 x) (I32 y) = pure $ I32 (x - y)
-sub (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ x - y)
+sub (I64 x) (I64 y) = pure $ I64 (x - y)
-sub (B8 x) (B8 y) = pure $ B8 (bit8CastWrap $ x - y)
+sub (B8 x) (B8 y) = pure $ B8 (x - y)
-sub (B16 x) (B16 y) = pure $ B16 (bit16CastWrap $ x - y)
+sub (B16 x) (B16 y) = pure $ B16 (x - y)
-sub (B32 x) (B32 y) = pure $ B32 (bit32CastWrap $ x - y)
+sub (B32 x) (B32 y) = pure $ B32 (x - y)
-sub (B64 x) (B64 y) = pure $ B64 (bit64CastWrap $ x - y)
+sub (B64 x) (B64 y) = pure $ B64 (x - y)
 sub (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x - cast y))
 sub (Db x) (Db y) = pure $ Db (x - y)
 sub _ _ = Nothing
 
 mul : Constant -> Constant -> Maybe Constant
 mul (BI x) (BI y) = pure $ BI (x * y)
-mul (B8 x) (B8 y) = pure $ B8 $ (x * y) `mod` b8max
+mul (B8 x) (B8 y) = pure $ B8 (x * y)
-mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` b16max
+mul (B16 x) (B16 y) = pure $ B16 (x * y)
-mul (B32 x) (B32 y) = pure $ B32 $ (x * y) `mod` b32max
+mul (B32 x) (B32 y) = pure $ B32 (x * y)
-mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` b64max
+mul (B64 x) (B64 y) = pure $ B64 (x * y)
 mul (I x) (I y) = pure $ I (x * y)
-mul (I8 x) (I8 y) = pure $ I8 (int8CastWrap $ x * y)
+mul (I8 x) (I8 y) = pure $ I8 (x * y)
-mul (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x * y)
+mul (I16 x) (I16 y) = pure $ I16 (x * y)
-mul (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x * y)
+mul (I32 x) (I32 y) = pure $ I32 (x * y)
-mul (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ x * y)
+mul (I64 x) (I64 y) = pure $ I64 (x * y)
 mul (Db x) (Db y) = pure $ Db (x * y)
 mul _ _ = Nothing
 
@@ -313,21 +249,21 @@ div (BI x) (BI y) = pure $ BI (assert_total (x `div` y))
 div (I x) (I 0) = Nothing
 div (I x) (I y) = pure $ I (assert_total (x `div` y))
 div (I8 x) (I8 0) = Nothing
-div (I8 x) (I8 y) = pure $ I8 (int8CastWrap $ assert_total (x `div` y))
+div (I8 x) (I8 y) = pure $ I8 (assert_total (x `div` y))
 div (I16 x) (I16 0) = Nothing
-div (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ assert_total (x `div` y))
+div (I16 x) (I16 y) = pure $ I16 (assert_total (x `div` y))
 div (I32 x) (I32 0) = Nothing
-div (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ assert_total (x `div` y))
+div (I32 x) (I32 y) = pure $ I32 (assert_total (x `div` y))
 div (I64 x) (I64 0) = Nothing
-div (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ assert_total (x `div` y))
+div (I64 x) (I64 y) = pure $ I64 (assert_total (x `div` y))
 div (B8 x) (B8 0) = Nothing
-div (B8 x) (B8 y) = pure $ B8 (bit8CastWrap $ assert_total (x `div` y))
+div (B8 x) (B8 y) = pure $ B8 (assert_total (x `div` y))
 div (B16 x) (B16 0) = Nothing
-div (B16 x) (B16 y) = pure $ B16 (bit16CastWrap $ assert_total (x `div` y))
+div (B16 x) (B16 y) = pure $ B16 (assert_total (x `div` y))
 div (B32 x) (B32 0) = Nothing
-div (B32 x) (B32 y) = pure $ B32 (bit32CastWrap $ assert_total (x `div` y))
+div (B32 x) (B32 y) = pure $ B32 (assert_total (x `div` y))
 div (B64 x) (B64 0) = Nothing
-div (B64 x) (B64 y) = pure $ B64 (bit64CastWrap $ assert_total (x `div` y))
+div (B64 x) (B64 y) = pure $ B64 (assert_total (x `div` y))
 div (Db x) (Db y) = pure $ Db (x / y)
 div _ _ = Nothing
 
@@ -337,109 +273,98 @@ mod (BI x) (BI y) = pure $ BI (assert_total (x `mod` y))
 mod (I x) (I 0) = Nothing
 mod (I x) (I y) = pure $ I (assert_total (x `mod` y))
 mod (I8 x) (I8 0) = Nothing
-mod (I8 x) (I8 y) = pure $ I8 (int8CastWrap $ assert_total (x `mod` y))
+mod (I8 x) (I8 y) = pure $ I8 (assert_total (x `mod` y))
 mod (I16 x) (I16 0) = Nothing
-mod (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ assert_total (x `mod` y))
+mod (I16 x) (I16 y) = pure $ I16 (assert_total (x `mod` y))
 mod (I32 x) (I32 0) = Nothing
-mod (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ assert_total (x `mod` y))
+mod (I32 x) (I32 y) = pure $ I32 (assert_total (x `mod` y))
 mod (I64 x) (I64 0) = Nothing
-mod (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ assert_total (x `mod` y))
+mod (I64 x) (I64 y) = pure $ I64 (assert_total (x `mod` y))
 mod (B8 x) (B8 0) = Nothing
-mod (B8 x) (B8 y) = pure $ B8 (bit8CastWrap $ assert_total (x `mod` y))
+mod (B8 x) (B8 y) = pure $ B8 (assert_total (x `mod` y))
 mod (B16 x) (B16 0) = Nothing
-mod (B16 x) (B16 y) = pure $ B16 (bit16CastWrap $ assert_total (x `mod` y))
+mod (B16 x) (B16 y) = pure $ B16 (assert_total (x `mod` y))
 mod (B32 x) (B32 0) = Nothing
-mod (B32 x) (B32 y) = pure $ B32 (bit32CastWrap $ assert_total (x `mod` y))
+mod (B32 x) (B32 y) = pure $ B32 (assert_total (x `mod` y))
 mod (B64 x) (B64 0) = Nothing
-mod (B64 x) (B64 y) = pure $ B64 (bit64CastWrap $ assert_total (x `mod` y))
+mod (B64 x) (B64 y) = pure $ B64 (assert_total (x `mod` y))
 mod _ _ = Nothing
 
--- Make sure a signed integer stays within bounds after a
--- bitwise shift operation. If, after the shift, the highest bit
--- is set, treat the result as a negative number, computing its
--- twos complement, otherwise treat it as a positive number,
--- truncating all bits above the highest one.
-signedShift : (i : Integer) -> (max : Integer) -> Integer
-signedShift i max =
-  if prim__and_Integer i max == 0
-     then prim__and_Integer i (max - 1) -- treat as positive number: highest bit unset
-     else prim__or_Integer i (-max)     -- treat as negative number: highest bit set
-
 shiftl : Constant -> Constant -> Maybe Constant
 shiftl (I x) (I y) = pure $ I (prim__shl_Int x y)
-shiftl (I8 x) (I8 y) = pure $ I8 (signedShift (prim__shl_Integer x y) int8max)
+shiftl (I8 x) (I8 y) = pure $ I8 (prim__shl_Int8 x y)
-shiftl (I16 x) (I16 y) = pure $ I16 (signedShift (prim__shl_Integer x y) int16max)
+shiftl (I16 x) (I16 y) = pure $ I16 (prim__shl_Int16 x y)
-shiftl (I32 x) (I32 y) = pure $ I32 (signedShift (prim__shl_Integer x y) int32max)
+shiftl (I32 x) (I32 y) = pure $ I32 (prim__shl_Int32 x y)
-shiftl (I64 x) (I64 y) = pure $ I64 (signedShift (prim__shl_Integer x y) int64max)
+shiftl (I64 x) (I64 y) = pure $ I64 (prim__shl_Int64 x y)
 shiftl (BI x) (BI y) = pure $ BI (prim__shl_Integer x y)
-shiftl (B8 x) (B8 y) = pure $ B8 $ (prim__shl_Int x y) `mod` b8max
+shiftl (B8 x) (B8 y) = pure $ B8 (prim__shl_Bits8 x y)
-shiftl (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` b16max
+shiftl (B16 x) (B16 y) = pure $ B16 (prim__shl_Bits16 x y)
-shiftl (B32 x) (B32 y) = pure $ B32 $ (prim__shl_Int x y) `mod` b32max
+shiftl (B32 x) (B32 y) = pure $ B32 (prim__shl_Bits32 x y)
-shiftl (B64 x) (B64 y) = pure $ B64 $ (prim__shl_Integer x y) `mod` b64max
+shiftl (B64 x) (B64 y) = pure $ B64 (prim__shl_Bits64 x y)
 shiftl _ _ = Nothing
 
 shiftr : Constant -> Constant -> Maybe Constant
 shiftr (I x) (I y) = pure $ I (prim__shr_Int x y)
-shiftr (I8 x) (I8 y) = pure $ I8 (signedShift (prim__shr_Integer x y) int8max)
+shiftr (I8 x) (I8 y) = pure $ I8 (prim__shr_Int8 x y)
-shiftr (I16 x) (I16 y) = pure $ I16 (signedShift (prim__shr_Integer x y) int16max)
+shiftr (I16 x) (I16 y) = pure $ I16 (prim__shr_Int16 x y)
-shiftr (I32 x) (I32 y) = pure $ I32 (signedShift (prim__shr_Integer x y) int32max)
+shiftr (I32 x) (I32 y) = pure $ I32 (prim__shr_Int32 x y)
-shiftr (I64 x) (I64 y) = pure $ I64 (signedShift (prim__shr_Integer x y) int64max)
+shiftr (I64 x) (I64 y) = pure $ I64 (prim__shr_Int64 x y)
-shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Int x y)
+shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Bits8 x y)
-shiftr (B16 x) (B16 y) = pure $ B16 $ (prim__shr_Int x y)
+shiftr (B16 x) (B16 y) = pure $ B16 (prim__shr_Bits16 x y)
-shiftr (B32 x) (B32 y) = pure $ B32 $ (prim__shr_Int x y)
+shiftr (B32 x) (B32 y) = pure $ B32 (prim__shr_Bits32 x y)
-shiftr (B64 x) (B64 y) = pure $ B64 $ (prim__shr_Integer x y)
+shiftr (B64 x) (B64 y) = pure $ B64 (prim__shr_Bits64 x y)
 shiftr _ _ = Nothing
 
 band : Constant -> Constant -> Maybe Constant
 band (I x) (I y) = pure $ I (prim__and_Int x y)
-band (I8 x) (I8 y) = pure $ I8 (prim__and_Integer x y)
+band (I8 x) (I8 y) = pure $ I8 (prim__and_Int8 x y)
-band (I16 x) (I16 y) = pure $ I16 (prim__and_Integer x y)
+band (I16 x) (I16 y) = pure $ I16 (prim__and_Int16 x y)
-band (I32 x) (I32 y) = pure $ I32 (prim__and_Integer x y)
+band (I32 x) (I32 y) = pure $ I32 (prim__and_Int32 x y)
-band (I64 x) (I64 y) = pure $ I64 (prim__and_Integer x y)
+band (I64 x) (I64 y) = pure $ I64 (prim__and_Int64 x y)
 band (BI x) (BI y) = pure $ BI (prim__and_Integer x y)
-band (B8 x) (B8 y) = pure $ B8 (prim__and_Int x y)
+band (B8 x) (B8 y) = pure $ B8 (prim__and_Bits8 x y)
-band (B16 x) (B16 y) = pure $ B16 (prim__and_Int x y)
+band (B16 x) (B16 y) = pure $ B16 (prim__and_Bits16 x y)
-band (B32 x) (B32 y) = pure $ B32 (prim__and_Int x y)
+band (B32 x) (B32 y) = pure $ B32 (prim__and_Bits32 x y)
-band (B64 x) (B64 y) = pure $ B64 (prim__and_Integer x y)
+band (B64 x) (B64 y) = pure $ B64 (prim__and_Bits64 x y)
 band _ _ = Nothing
 
 bor : Constant -> Constant -> Maybe Constant
 bor (I x) (I y) = pure $ I (prim__or_Int x y)
-bor (I8 x) (I8 y) = pure $ I8 (prim__or_Integer x y)
+bor (I8 x) (I8 y) = pure $ I8 (prim__or_Int8 x y)
-bor (I16 x) (I16 y) = pure $ I16 (prim__or_Integer x y)
+bor (I16 x) (I16 y) = pure $ I16 (prim__or_Int16 x y)
-bor (I32 x) (I32 y) = pure $ I32 (prim__or_Integer x y)
+bor (I32 x) (I32 y) = pure $ I32 (prim__or_Int32 x y)
-bor (I64 x) (I64 y) = pure $ I64 (prim__or_Integer x y)
+bor (I64 x) (I64 y) = pure $ I64 (prim__or_Int64 x y)
 bor (BI x) (BI y) = pure $ BI (prim__or_Integer x y)
-bor (B8 x) (B8 y) = pure $ B8 (prim__or_Int x y)
+bor (B8 x) (B8 y) = pure $ B8 (prim__or_Bits8 x y)
-bor (B16 x) (B16 y) = pure $ B16 (prim__or_Int x y)
+bor (B16 x) (B16 y) = pure $ B16 (prim__or_Bits16 x y)
-bor (B32 x) (B32 y) = pure $ B32 (prim__or_Int x y)
+bor (B32 x) (B32 y) = pure $ B32 (prim__or_Bits32 x y)
-bor (B64 x) (B64 y) = pure $ B64 (prim__or_Integer x y)
+bor (B64 x) (B64 y) = pure $ B64 (prim__or_Bits64 x y)
 bor _ _ = Nothing
 
 bxor : Constant -> Constant -> Maybe Constant
 bxor (I x) (I y) = pure $ I (prim__xor_Int x y)
-bxor (B8 x) (B8 y) = pure $ B8 (prim__xor_Int x y)
+bxor (B8 x) (B8 y) = pure $ B8 (prim__xor_Bits8 x y)
-bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Int x y)
+bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Bits16 x y)
-bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Int x y)
+bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Bits32 x y)
-bxor (B64 x) (B64 y) = pure $ B64 (prim__xor_Integer x y)
+bxor (B64 x) (B64 y) = pure $ B64 (prim__xor_Bits64 x y)
-bxor (I8 x) (I8 y) = pure $ I8 (prim__xor_Integer x y)
+bxor (I8 x) (I8 y) = pure $ I8 (prim__xor_Int8 x y)
-bxor (I16 x) (I16 y) = pure $ I16 (prim__xor_Integer x y)
+bxor (I16 x) (I16 y) = pure $ I16 (prim__xor_Int16 x y)
-bxor (I32 x) (I32 y) = pure $ I32 (prim__xor_Integer x y)
+bxor (I32 x) (I32 y) = pure $ I32 (prim__xor_Int32 x y)
-bxor (I64 x) (I64 y) = pure $ I64 (prim__xor_Integer x y)
+bxor (I64 x) (I64 y) = pure $ I64 (prim__xor_Int64 x y)
 bxor (BI x) (BI y) = pure $ BI (prim__xor_Integer x y)
 bxor _ _ = Nothing
 
 neg : Constant -> Maybe Constant
 neg (BI x) = pure $ BI (-x)
 neg (I x) = pure $ I (-x)
-neg (I8 x) = pure . I8 $ int8CastWrap (-x)
+neg (I8 x) = pure $ I8 (-x)
-neg (I16 x) = pure . I16 $ int16CastWrap (-x)
+neg (I16 x) = pure $ I16 (-x)
-neg (I32 x) = pure . I32 $ int32CastWrap (-x)
+neg (I32 x) = pure $ I32 (-x)
-neg (I64 x) = pure . I64 $ int64CastWrap (-x)
+neg (I64 x) = pure $ I64 (-x)
-neg (B8 x) = pure . B8 $ bit8CastWrap (-x)
+neg (B8 x) = pure $ B8 (-x)
-neg (B16 x) = pure . B16 $ bit16CastWrap (-x)
+neg (B16 x) = pure $ B16 (-x)
-neg (B32 x) = pure . B32 $ bit32CastWrap (-x)
+neg (B32 x) = pure $ B32 (-x)
-neg (B64 x) = pure . B64 $ bit64CastWrap (-x)
+neg (B64 x) = pure $ B64 (-x)
 neg (Db x) = pure $ Db (-x)
 neg _ = Nothing
 

src/Core/Reflect.idr

@@ -103,6 +103,78 @@ export
 Reflect Int where
   reflect fc defs lhs env x = pure (PrimVal fc (I x))
 
+export
+Reify Int8 where
+  reify defs (NPrimVal _ (I8 v)) = pure v
+  reify defs val = cantReify val "Int8"
+
+export
+Reflect Int8 where
+  reflect fc defs lhs env x = pure (PrimVal fc (I8 x))
+
+export
+Reify Int16 where
+  reify defs (NPrimVal _ (I16 v)) = pure v
+  reify defs val = cantReify val "Int16"
+
+export
+Reflect Int16 where
+  reflect fc defs lhs env x = pure (PrimVal fc (I16 x))
+
+export
+Reify Int32 where
+  reify defs (NPrimVal _ (I32 v)) = pure v
+  reify defs val = cantReify val "Int32"
+
+export
+Reflect Int32 where
+  reflect fc defs lhs env x = pure (PrimVal fc (I32 x))
+
+export
+Reify Int64 where
+  reify defs (NPrimVal _ (I64 v)) = pure v
+  reify defs val = cantReify val "Int64"
+
+export
+Reflect Int64 where
+  reflect fc defs lhs env x = pure (PrimVal fc (I64 x))
+
+export
+Reify Bits8 where
+  reify defs (NPrimVal _ (B8 v)) = pure v
+  reify defs val = cantReify val "Bits8"
+
+export
+Reflect Bits8 where
+  reflect fc defs lhs env x = pure (PrimVal fc (B8 x))
+
+export
+Reify Bits16 where
+  reify defs (NPrimVal _ (B16 v)) = pure v
+  reify defs val = cantReify val "Bits16"
+
+export
+Reflect Bits16 where
+  reflect fc defs lhs env x = pure (PrimVal fc (B16 x))
+
+export
+Reify Bits32 where
+  reify defs (NPrimVal _ (B32 v)) = pure v
+  reify defs val = cantReify val "Bits32"
+
+export
+Reflect Bits32 where
+  reflect fc defs lhs env x = pure (PrimVal fc (B32 x))
+
+export
+Reify Bits64 where
+  reify defs (NPrimVal _ (B64 v)) = pure v
+  reify defs val = cantReify val "Bits64"
+
+export
+Reflect Bits64 where
+  reflect fc defs lhs env x = pure (PrimVal fc (B64 x))
+
 export
 Reify Integer where
   reify defs (NPrimVal _ (BI v)) = pure v

src/Core/TT.idr

@@ -9,6 +9,7 @@ import Data.Vect
 import Decidable.Equality
 
 import Libraries.Data.NameMap
+import Libraries.Data.Primitives
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
 
@@ -45,20 +46,19 @@ Show KindedName where show = show . rawName
 
 public export
 data Constant
-    = I Int
+    = I   Int
-    | I8 Integer -- reuse code from I64 with fewer casts
+    | I8  Int8
-    | I16 Integer
+    | I16 Int16
-    | I32 Integer
+    | I32 Int32
-    | I64 Integer
+    | I64 Int64
-    | BI Integer
+    | BI  Integer
-    | B8 Int -- For now, since we don't have Bits types. We need to
+    | B8  Bits8
-                -- make sure the Integer remains in range
+    | B16 Bits16
-    | B16 Int
+    | B32 Bits32
-    | B32 Int
+    | B64 Bits64
-    | B64 Integer
     | Str String
-    | Ch Char
+    | Ch  Char
-    | Db Double
+    | Db  Double
     | WorldVal
 
     | IntType
@@ -128,21 +128,35 @@ isPrimType CharType    = True
 isPrimType DoubleType  = True
 isPrimType WorldType   = True
 
+-- TODO : The `TempXY` instances can be removed after the next release
+--        (see also `Libraries.Data.Primitives`)
 export
 constantEq : (x, y : Constant) -> Maybe (x = y)
 constantEq (I x) (I y) = case decEq x y of
                               Yes Refl => Just Refl
                               No contra => Nothing
-constantEq (I8 x) (I8 y) = case decEq x y of
+constantEq (I8 x) (I8 y) = case decEq @{TempI8} x y of
                                   Yes Refl => Just Refl
                                   No contra => Nothing
-constantEq (I16 x) (I16 y) = case decEq x y of
+constantEq (I16 x) (I16 y) = case decEq @{TempI16} x y of
                                   Yes Refl => Just Refl
                                   No contra => Nothing
-constantEq (I32 x) (I32 y) = case decEq x y of
+constantEq (I32 x) (I32 y) = case decEq @{TempI32} x y of
                                   Yes Refl => Just Refl
                                   No contra => Nothing
-constantEq (I64 x) (I64 y) = case decEq x y of
+constantEq (I64 x) (I64 y) = case decEq @{TempI64} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B8 x) (B8 y) = case decEq @{TempB8} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B16 x) (B16 y) = case decEq @{TempB16} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B32 x) (B32 y) = case decEq @{TempB32} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B64 x) (B64 y) = case decEq @{TempB64} x y of
                                   Yes Refl => Just Refl
                                   No contra => Nothing
 constantEq (BI x) (BI y) = case decEq x y of

src/Libraries/Data/Primitives.idr

@@ -0,0 +1,81 @@
+||| TODO : This was interduced after v0.5.1. After the next minor release,
+|||        this can be removed and the instances from `base` can be used.
+module Libraries.Data.Primitives
+
+import public Decidable.Equality.Core as Decidable.Equality
+
+%default total
+
+public export
+[FromEq] Eq a => DecEq a where
+    decEq x y = case x == y of -- Blocks if x or y not concrete
+                     True => Yes primitiveEq
+                     False => No primitiveNotEq
+       where primitiveEq : forall x, y . x = y
+             primitiveEq = believe_me (Refl {x})
+             primitiveNotEq : forall x, y . Not (x = y)
+             primitiveNotEq prf = believe_me {b = Void} ()
+
+--------------------------------------------------------------------------------
+-- Bits8
+--------------------------------------------------------------------------------
+
+public export
+[TempB8] DecEq Bits8 where
+    decEq = decEq @{FromEq}
+
+--------------------------------------------------------------------------------
+-- Bits16
+--------------------------------------------------------------------------------
+
+public export
+[TempB16] DecEq Bits16 where
+    decEq = decEq @{FromEq}
+
+--------------------------------------------------------------------------------
+-- Bits32
+--------------------------------------------------------------------------------
+
+public export
+[TempB32] DecEq Bits32 where
+    decEq = decEq @{FromEq}
+
+--------------------------------------------------------------------------------
+-- Bits64
+--------------------------------------------------------------------------------
+
+public export
+[TempB64] DecEq Bits64 where
+    decEq = decEq @{FromEq}
+
+--------------------------------------------------------------------------------
+-- Int8
+--------------------------------------------------------------------------------
+
+public export
+[TempI8] DecEq Int8 where
+    decEq = decEq @{FromEq}
+
+--------------------------------------------------------------------------------
+-- Int16
+--------------------------------------------------------------------------------
+
+public export
+[TempI16] DecEq Int16 where
+    decEq = decEq @{FromEq}
+
+--------------------------------------------------------------------------------
+-- Int32
+--------------------------------------------------------------------------------
+
+public export
+[TempI32] DecEq Int32 where
+    decEq = decEq @{FromEq}
+
+--------------------------------------------------------------------------------
+-- Int64
+--------------------------------------------------------------------------------
+
+public export
+[TempI64] DecEq Int64 where
+    decEq = decEq @{FromEq}

src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr

@@ -424,6 +424,10 @@ export Pretty Bits8 where pretty = unsafeTextWithoutNewLines . show
 export Pretty Bits16 where pretty = unsafeTextWithoutNewLines . show
 export Pretty Bits32 where pretty = unsafeTextWithoutNewLines . show
 export Pretty Bits64 where pretty = unsafeTextWithoutNewLines . show
+export Pretty Int8 where pretty = unsafeTextWithoutNewLines . show
+export Pretty Int16 where pretty = unsafeTextWithoutNewLines . show
+export Pretty Int32 where pretty = unsafeTextWithoutNewLines . show
+export Pretty Int64 where pretty = unsafeTextWithoutNewLines . show
 
 export
 (Pretty a, Pretty b) => Pretty (a, b) where

src/Libraries/Utils/Scheme.idr

@@ -305,6 +305,62 @@ Scheme Int where
   fromScheme (IntegerVal x) = Just (cast x)
   fromScheme _ = Nothing
 
+export
+Scheme Int8 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme Int16 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme Int32 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme Int64 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme Bits8 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme Bits16 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme Bits32 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme Bits64 where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
 export
 Scheme String where
   toScheme x = StringVal x