add support for more casts from and to BitsN types (#548)

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

libs/prelude/Prelude/Types.idr

@@ -689,6 +689,22 @@ export
 Cast Nat Integer where
   cast = natToInteger
 
+export
+Cast Bits8 Integer where
+  cast = prim__cast_Bits8Integer
+
+export
+Cast Bits16 Integer where
+  cast = prim__cast_Bits16Integer
+
+export
+Cast Bits32 Integer where
+  cast = prim__cast_Bits32Integer
+
+export
+Cast Bits64 Integer where
+  cast = prim__cast_Bits64Integer
+
 -- To Int
 
 export
@@ -711,6 +727,22 @@ export
 Cast Nat Int where
   cast = fromInteger . natToInteger
 
+export
+Cast Bits8 Int where
+  cast = prim__cast_Bits8Int
+
+export
+Cast Bits16 Int where
+  cast = prim__cast_Bits16Int
+
+export
+Cast Bits32 Int where
+  cast = prim__cast_Bits32Int
+
+export
+Cast Bits64 Int where
+  cast = prim__cast_Bits64Int
+
 -- To Char
 
 export
@@ -735,6 +767,98 @@ export
 Cast Nat Double where
   cast = prim__cast_IntegerDouble . natToInteger
 
+
+-- To Bits8
+
+export
+Cast Int Bits8 where
+  cast = prim__cast_IntBits8
+
+export
+Cast Integer Bits8 where
+  cast = prim__cast_IntegerBits8
+
+export
+Cast Bits16 Bits8 where
+  cast = prim__cast_Bits16Bits8
+
+export
+Cast Bits32 Bits8 where
+  cast = prim__cast_Bits32Bits8
+
+export
+Cast Bits64 Bits8 where
+  cast = prim__cast_Bits64Bits8
+
+
+-- To Bits16
+
+export
+Cast Int Bits16 where
+  cast = prim__cast_IntBits16
+
+export
+Cast Integer Bits16 where
+  cast = prim__cast_IntegerBits16
+
+export
+Cast Bits8 Bits16 where
+  cast = prim__cast_Bits8Bits16
+
+export
+Cast Bits32 Bits16 where
+  cast = prim__cast_Bits32Bits16
+
+export
+Cast Bits64 Bits16 where
+  cast = prim__cast_Bits64Bits16
+
+
+-- To Bits32
+
+export
+Cast Int Bits32 where
+  cast = prim__cast_IntBits32
+
+export
+Cast Integer Bits32 where
+  cast = prim__cast_IntegerBits32
+
+export
+Cast Bits8 Bits32 where
+  cast = prim__cast_Bits8Bits32
+
+export
+Cast Bits16 Bits32 where
+  cast = prim__cast_Bits16Bits32
+
+export
+Cast Bits64 Bits32 where
+  cast = prim__cast_Bits64Bits32
+
+-- To Bits64
+
+export
+Cast Int Bits64 where
+  cast = prim__cast_IntBits64
+
+export
+Cast Integer Bits64 where
+  cast = prim__cast_IntegerBits64
+
+export
+Cast Bits8 Bits64 where
+  cast = prim__cast_Bits8Bits64
+
+export
+Cast Bits16 Bits64 where
+  cast = prim__cast_Bits16Bits64
+
+export
+Cast Bits32 Bits64 where
+  cast = prim__cast_Bits32Bits64
+
+
 ------------
 -- RANGES --
 ------------

src/Compiler/ES/ES.idr

@@ -246,10 +246,33 @@ jsOp (Cast StringType IntegerType) [x] = jsIntegerOfString x
 jsOp (Cast IntegerType IntType) [x] = boundedInt 63 x
 jsOp (Cast IntType IntegerType) [x] = pure x
 jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"
+
+jsOp (Cast IntType Bits8Type) [x] = boundedUInt 8 x
+jsOp (Cast IntType Bits16Type) [x] = boundedUInt 16 x
+jsOp (Cast IntType Bits32Type) [x] = boundedUInt 32 x
+jsOp (Cast IntType Bits64Type) [x] = boundedUInt 64 x
+
 jsOp (Cast IntegerType Bits8Type) [x] = boundedUInt 8 x
 jsOp (Cast IntegerType Bits16Type) [x] = boundedUInt 16 x
 jsOp (Cast IntegerType Bits32Type) [x] = boundedUInt 32 x
 jsOp (Cast IntegerType Bits64Type) [x] = boundedUInt 64 x
+
+jsOp (Cast Bits8Type Bits16Type) [x] = pure x
+jsOp (Cast Bits8Type Bits32Type) [x] = pure x
+jsOp (Cast Bits8Type Bits64Type) [x] = pure x
+
+jsOp (Cast Bits16Type Bits8Type) [x] = boundedUInt 8 x
+jsOp (Cast Bits16Type Bits32Type) [x] = pure x
+jsOp (Cast Bits16Type Bits64Type) [x] = pure x
+
+jsOp (Cast Bits32Type Bits8Type) [x] = boundedUInt 8 x
+jsOp (Cast Bits32Type Bits16Type) [x] = boundedUInt 16 x
+jsOp (Cast Bits32Type Bits64Type) [x] = pure x
+
+jsOp (Cast Bits64Type Bits8Type) [x] = boundedUInt 8 x
+jsOp (Cast Bits64Type Bits16Type) [x] = boundedUInt 16 x
+jsOp (Cast Bits64Type Bits32Type) [x] = boundedUInt 32 x
+
 jsOp (Cast ty StringType) [x] = pure $ "(''+" ++ x ++ ")"
 jsOp (Cast ty ty2) [x] = jsCrashExp $ "invalid cast: + " ++ show ty ++ " + ' -> ' + " ++ show ty2
 jsOp BelieveMe [_,_,x] = pure x

src/Compiler/Scheme/Common.idr

@@ -158,11 +158,33 @@ schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x]
 schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
 schOp (Cast CharType IntType) [x] = op "char->integer" [x]
 
+schOp (Cast IntType Bits8Type) [x] = op "integer->bits8" [x]
+schOp (Cast IntType Bits16Type) [x] = op "integer->bits16" [x]
+schOp (Cast IntType Bits32Type) [x] = op "integer->bits32" [x]
+schOp (Cast IntType Bits64Type) [x] = op "integer->bits64" [x]
+
 schOp (Cast IntegerType Bits8Type) [x] = op "integer->bits8" [x]
 schOp (Cast IntegerType Bits16Type) [x] = op "integer->bits16" [x]
 schOp (Cast IntegerType Bits32Type) [x] = op "integer->bits32" [x]
 schOp (Cast IntegerType Bits64Type) [x] = op "integer->bits64" [x]
 
+schOp (Cast Bits8Type Bits16Type) [x] = x
+schOp (Cast Bits8Type Bits32Type) [x] = x
+schOp (Cast Bits8Type Bits64Type) [x] = x
+
+schOp (Cast Bits16Type Bits8Type) [x] = op "bits16->bits8" [x]
+schOp (Cast Bits16Type Bits32Type) [x] = x
+schOp (Cast Bits16Type Bits64Type) [x] = x
+
+schOp (Cast Bits32Type Bits8Type) [x] = op "bits32->bits8" [x]
+schOp (Cast Bits32Type Bits16Type) [x] = op "bits32->bits16" [x]
+schOp (Cast Bits32Type Bits64Type) [x] = x
+
+schOp (Cast Bits64Type Bits8Type) [x] = op "bits64->bits8" [x]
+schOp (Cast Bits64Type Bits16Type) [x] = op "bits64->bits16" [x]
+schOp (Cast Bits64Type Bits32Type) [x] = op "bits64->bits32" [x]
+
+
 schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x]
 schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x]
 schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]

src/Core/Primitives.idr

@@ -57,6 +57,7 @@ castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (fromInteger i)))
 castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I i))
 castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I i))
 castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I i))
+castInt [NPrimVal fc (B64 i)] = Just (NPrimVal fc (I (fromInteger 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)))
@@ -74,32 +75,47 @@ b32max = 0x100000000
 b64max : Integer
 b64max = 18446744073709551616 -- 0x10000000000000000
 
-castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
+bitCastWrap : (i : Integer) -> (max : Integer) -> Integer
-castBits8 [NPrimVal fc (BI i)]
+bitCastWrap i max
     = if i >= 0 -- oops, we don't have `rem` yet!
-          then Just (NPrimVal fc (B8 (fromInteger i `mod` b8max)))
+        then i `mod` max
-          else Just (NPrimVal fc (B8 (b8max + fromInteger i `mod` b8max)))
+        else max + i `mod` max
+
+constantIntegerValue : Constant -> Maybe Integer
+constantIntegerValue (I 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 _       = Nothing
+
+castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
+castBits8 [NPrimVal fc constant] = do
+    value <- 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 (BI i)]
+castBits16 [NPrimVal fc constant] = do
-    = if i >= 0 -- oops, we don't have `rem` yet!
+    value <- constantIntegerValue constant
-          then Just (NPrimVal fc (B8 (fromInteger i `mod` b16max)))
+    let wrapped = bitCastWrap value (cast b16max)
-          else Just (NPrimVal fc (B8 (b16max + fromInteger i `mod` b16max)))
+    pure (NPrimVal fc (B16 (cast wrapped)))
 castBits16 _ = Nothing
 
 castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
-castBits32 [NPrimVal fc (BI i)]
+castBits32 [NPrimVal fc constant] = do
-    = if i >= 0 -- oops, we don't have `rem` yet!
+    value <- constantIntegerValue constant
-          then Just (NPrimVal fc (B8 (fromInteger i `mod` b32max)))
+    let wrapped = bitCastWrap value (cast b32max)
-          else Just (NPrimVal fc (B8 (b32max + fromInteger i `mod` b32max)))
+    pure (NPrimVal fc (B32 (cast wrapped)))
 castBits32 _ = Nothing
 
 castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
-castBits64 [NPrimVal fc (BI i)]
+castBits64 [NPrimVal fc constant] = do
-    = if i >= 0 -- oops, we don't have `rem` yet!
+    value <- constantIntegerValue constant
-          then Just (NPrimVal fc (B64 (i `mod` b64max)))
+    let wrapped = bitCastWrap value b64max
-          else Just (NPrimVal fc (B64 (b64max + i `mod` b64max)))
+    pure (NPrimVal fc (B64 wrapped))
 castBits64 _ = Nothing
 
 castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
@@ -544,11 +560,11 @@ allPrimitives =
 
     map (\t => MkPrim (Cast t StringType) (predTy t StringType) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
     map (\t => MkPrim (Cast t IntegerType) (predTy t IntegerType) isTotal) [StringType, IntType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
-    map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, Bits8Type, Bits16Type, Bits32Type, CharType, DoubleType] ++
+    map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
     map (\t => MkPrim (Cast t DoubleType) (predTy t DoubleType) isTotal) [StringType, IntType, IntegerType] ++
     map (\t => MkPrim (Cast t CharType) (predTy t CharType) isTotal) [StringType, IntType] ++
 
-    map (\t => MkPrim (Cast t Bits8Type) (predTy t Bits8Type) isTotal) [IntegerType] ++
+    map (\t => MkPrim (Cast t Bits8Type) (predTy t Bits8Type) isTotal) [IntType, IntegerType, Bits16Type, Bits32Type, Bits64Type] ++
-    map (\t => MkPrim (Cast t Bits16Type) (predTy t Bits16Type) isTotal) [IntegerType] ++
+    map (\t => MkPrim (Cast t Bits16Type) (predTy t Bits16Type) isTotal) [IntType, IntegerType, Bits8Type, Bits32Type, Bits64Type] ++
-    map (\t => MkPrim (Cast t Bits32Type) (predTy t Bits32Type) isTotal) [IntegerType] ++
+    map (\t => MkPrim (Cast t Bits32Type) (predTy t Bits32Type) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits64Type] ++
-    map (\t => MkPrim (Cast t Bits64Type) (predTy t Bits64Type) isTotal) [IntegerType]
+    map (\t => MkPrim (Cast t Bits64Type) (predTy t Bits64Type) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type]

support/chez/support.ss

@@ -23,6 +23,13 @@
 (define integer->bits32 (lambda (x) (modulo x (expt 2 32))))
 (define integer->bits64 (lambda (x) (modulo x (expt 2 64))))
 
+(define bits16->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits32->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits32->bits16 (lambda (x) (modulo x (expt 2 16))))
+(define bits64->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits64->bits16 (lambda (x) (modulo x (expt 2 16))))
+(define bits64->bits32 (lambda (x) (modulo x (expt 2 32))))
+
 (define blodwen-bits-shl (lambda (x y bits) (remainder (ash x y) (ash 1 bits))))
 (define blodwen-shl (lambda (x y) (ash x y)))
 (define blodwen-shr (lambda (x y) (ash x (- y))))

support/gambit/support.scm

@@ -36,6 +36,13 @@
 (define integer->bits32 (lambda (x) (modulo x (expt 2 32))))
 (define integer->bits64 (lambda (x) (modulo x (expt 2 64))))
 
+(define bits16->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits32->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits32->bits16 (lambda (x) (modulo x (expt 2 16))))
+(define bits64->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits64->bits16 (lambda (x) (modulo x (expt 2 16))))
+(define bits64->bits32 (lambda (x) (modulo x (expt 2 32))))
+
 (define-macro (blodwen-and . args) `(bitwise-and ,@args))
 (define-macro (blodwen-or . args) `(bitwise-ior ,@args))
 (define-macro (blodwen-xor . args) `(bitwise-xor ,@args))

support/racket/support.rkt

@@ -20,6 +20,13 @@
 (define integer->bits32 (lambda (x) (modulo x (expt 2 32))))
 (define integer->bits64 (lambda (x) (modulo x (expt 2 64))))
 
+(define bits16->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits32->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits32->bits16 (lambda (x) (modulo x (expt 2 16))))
+(define bits64->bits8 (lambda (x) (modulo x (expt 2 8))))
+(define bits64->bits16 (lambda (x) (modulo x (expt 2 16))))
+(define bits64->bits32 (lambda (x) (modulo x (expt 2 32))))
+
 (define blodwen-bits-shl (lambda (x y bits) (remainder (arithmetic-shift x y) (arithmetic-shift 1 bits))))
 (define blodwen-shl (lambda (x y) (arithmetic-shift x y)))
 (define blodwen-shr (lambda (x y) (arithmetic-shift x (- y))))

tests/Main.idr

@@ -41,7 +41,7 @@ idrisTests
        "basic026", "basic027", "basic028", "basic029", "basic030",
        "basic031", "basic032", "basic033", "basic034", "basic035",
        "basic036", "basic037", "basic038", "basic039", "basic040",
-       "basic041", "basic042",
+       "basic041", "basic042", "basic043",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
@@ -125,14 +125,14 @@ chezTests
       "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
       "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
       "chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
-      "chez025", "chez026", "chez027", "chez028",
+      "chez025", "chez026", "chez027", "chez028", "chez029",
       "reg001"]
 
 nodeTests : List String
 nodeTests
   = [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
     , "node011", "node012", "node015", "node017", "node018", "node019" -- node014
-    , "node021" --, "node020"
+    , "node021", "node022" --, "node020"
     , "reg001"
     , "syntax001"
     , "tailrec001"

tests/chez/chez029/BitCasts.idr

@@ -0,0 +1,95 @@
+-- Tests to check that casting between integer types works as expected
+-- 
+-- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
+-- same and should all have the same output.
+
+--
+-- Widening should not have any effect
+--
+
+bits8WideningNoEffect : List String
+bits8WideningNoEffect = [
+    show $ cast {from = Bits8} {to = Bits16} 123,
+    show $ cast {from = Bits8} {to = Bits32} 123,
+    show $ cast {from = Bits8} {to = Bits64} 123,
+    show $ cast {from = Bits8} {to = Int} 123,
+    show $ cast {from = Bits8} {to = Integer} 123
+]
+
+bits16WideningNoEffect : List String
+bits16WideningNoEffect = [
+    show $ cast {from = Bits16} {to = Bits32} 1234,
+    show $ cast {from = Bits16} {to = Bits64} 1234,
+    show $ cast {from = Bits16} {to = Int} 1234,
+    show $ cast {from = Bits16} {to = Integer} 1234
+]
+
+bits32WideningNoEffect : List String
+bits32WideningNoEffect = [
+    show $ cast {from = Bits32} {to = Bits64} 1234567,
+    show $ cast {from = Bits32} {to = Int} 1234567,
+    show $ cast {from = Bits32} {to = Integer} 1234567
+]
+
+--
+-- Narrowing
+--
+
+b8max : Integer
+b8max = 0x100
+
+b16max : Integer
+b16max = 0x10000
+
+b32max : Integer
+b32max = 0x100000000
+
+b64max : Integer
+b64max = 18446744073709551616 -- 0x10000000000000000
+
+
+narrowFromInteger : List String
+narrowFromInteger = [
+    show $ cast {from = Integer} {to = Bits8} (b8max + 134),
+    show $ cast {from = Integer} {to = Bits16} (b16max + 134),
+    show $ cast {from = Integer} {to = Bits32} (b32max + 134),
+    show $ cast {from = Integer} {to = Bits64} (b64max + 134)
+]
+
+narrowFromInt : List String
+narrowFromInt = [
+    show $ cast {from = Int} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Int} {to = Bits16} (cast (b16max + 134)),
+    show $ cast {from = Int} {to = Bits32} (cast (b32max + 134)),
+    show $ cast {from = Int} {to = Bits64} (cast (b64max + 134))
+]
+
+narrowFromBits64 : List String
+narrowFromBits64 = [
+    show $ cast {from = Bits64} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Bits64} {to = Bits16} (cast (b16max + 134)),
+    show $ cast {from = Bits64} {to = Bits32} (cast (b32max + 134))
+]
+
+narrowFromBits32 : List String
+narrowFromBits32 = [
+    show $ cast {from = Bits32} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Bits32} {to = Bits16} (cast (b16max + 134))
+]
+
+narrowFromBits16 : List String
+narrowFromBits16 = [
+    show $ cast {from = Bits16} {to = Bits8} (cast (b8max + 134))
+]
+
+--
+-- Negative numbers
+--
+
+negativeNumberCast : List String
+negativeNumberCast = [
+    show $ cast {to = Bits8} (-19),
+    show $ cast {to = Bits16} (-19),
+    show $ cast {to = Bits32} (-19),
+    show $ cast {to = Bits64} (-19)
+]

tests/chez/chez029/expected

@@ -0,0 +1,11 @@
+1/1: Building BitCasts (BitCasts.idr)
+Main> ["123", "123", "123", "123", "123"]
+Main> ["1234", "1234", "1234", "1234"]
+Main> ["1234567", "1234567", "1234567"]
+Main> ["134", "134", "134", "134"]
+Main> ["134", "134", "134", "134"]
+Main> ["134", "134", "134"]
+Main> ["134", "134"]
+Main> ["134"]
+Main> ["237", "65517", "4294967277", "18446744073709551597"]
+Main> Bye for now!

tests/chez/chez029/input

@@ -0,0 +1,10 @@
+bits8WideningNoEffect
+bits16WideningNoEffect
+bits32WideningNoEffect
+narrowFromInteger
+narrowFromInt
+narrowFromBits64
+narrowFromBits32
+narrowFromBits16
+negativeNumberCast
+:q

tests/chez/chez029/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 BitCasts.idr < input
+
+rm -rf build

tests/idris2/basic043/BitCasts.idr

@@ -0,0 +1,95 @@
+-- Tests to check that casting between integer types works as expected
+-- 
+-- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
+-- same and should all have the same output.
+
+--
+-- Widening should not have any effect
+--
+
+bits8WideningNoEffect : List String
+bits8WideningNoEffect = [
+    show $ cast {from = Bits8} {to = Bits16} 123,
+    show $ cast {from = Bits8} {to = Bits32} 123,
+    show $ cast {from = Bits8} {to = Bits64} 123,
+    show $ cast {from = Bits8} {to = Int} 123,
+    show $ cast {from = Bits8} {to = Integer} 123
+]
+
+bits16WideningNoEffect : List String
+bits16WideningNoEffect = [
+    show $ cast {from = Bits16} {to = Bits32} 1234,
+    show $ cast {from = Bits16} {to = Bits64} 1234,
+    show $ cast {from = Bits16} {to = Int} 1234,
+    show $ cast {from = Bits16} {to = Integer} 1234
+]
+
+bits32WideningNoEffect : List String
+bits32WideningNoEffect = [
+    show $ cast {from = Bits32} {to = Bits64} 1234567,
+    show $ cast {from = Bits32} {to = Int} 1234567,
+    show $ cast {from = Bits32} {to = Integer} 1234567
+]
+
+--
+-- Narrowing
+--
+
+b8max : Integer
+b8max = 0x100
+
+b16max : Integer
+b16max = 0x10000
+
+b32max : Integer
+b32max = 0x100000000
+
+b64max : Integer
+b64max = 18446744073709551616 -- 0x10000000000000000
+
+
+narrowFromInteger : List String
+narrowFromInteger = [
+    show $ cast {from = Integer} {to = Bits8} (b8max + 134),
+    show $ cast {from = Integer} {to = Bits16} (b16max + 134),
+    show $ cast {from = Integer} {to = Bits32} (b32max + 134),
+    show $ cast {from = Integer} {to = Bits64} (b64max + 134)
+]
+
+narrowFromInt : List String
+narrowFromInt = [
+    show $ cast {from = Int} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Int} {to = Bits16} (cast (b16max + 134)),
+    show $ cast {from = Int} {to = Bits32} (cast (b32max + 134)),
+    show $ cast {from = Int} {to = Bits64} (cast (b64max + 134))
+]
+
+narrowFromBits64 : List String
+narrowFromBits64 = [
+    show $ cast {from = Bits64} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Bits64} {to = Bits16} (cast (b16max + 134)),
+    show $ cast {from = Bits64} {to = Bits32} (cast (b32max + 134))
+]
+
+narrowFromBits32 : List String
+narrowFromBits32 = [
+    show $ cast {from = Bits32} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Bits32} {to = Bits16} (cast (b16max + 134))
+]
+
+narrowFromBits16 : List String
+narrowFromBits16 = [
+    show $ cast {from = Bits16} {to = Bits8} (cast (b8max + 134))
+]
+
+--
+-- Negative numbers
+--
+
+negativeNumberCast : List String
+negativeNumberCast = [
+    show $ cast {to = Bits8} (-19),
+    show $ cast {to = Bits16} (-19),
+    show $ cast {to = Bits32} (-19),
+    show $ cast {to = Bits64} (-19)
+]

tests/idris2/basic043/expected

@@ -0,0 +1,11 @@
+1/1: Building BitCasts (BitCasts.idr)
+Main> ["123", "123", "123", "123", "123"]
+Main> ["1234", "1234", "1234", "1234"]
+Main> ["1234567", "1234567", "1234567"]
+Main> ["134", "134", "134", "134"]
+Main> ["134", "134", "134", "134"]
+Main> ["134", "134", "134"]
+Main> ["134", "134"]
+Main> ["134"]
+Main> ["237", "65517", "4294967277", "18446744073709551597"]
+Main> Bye for now!

tests/idris2/basic043/input

@@ -0,0 +1,10 @@
+bits8WideningNoEffect
+bits16WideningNoEffect
+bits32WideningNoEffect
+narrowFromInteger
+narrowFromInt
+narrowFromBits64
+narrowFromBits32
+narrowFromBits16
+negativeNumberCast
+:q

tests/idris2/basic043/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 BitCasts.idr < input
+
+rm -rf build

tests/node/node022/BitCasts.idr

@@ -0,0 +1,95 @@
+-- Tests to check that casting between integer types works as expected
+-- 
+-- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
+-- same and should all have the same output.
+
+--
+-- Widening should not have any effect
+--
+
+bits8WideningNoEffect : List String
+bits8WideningNoEffect = [
+    show $ cast {from = Bits8} {to = Bits16} 123,
+    show $ cast {from = Bits8} {to = Bits32} 123,
+    show $ cast {from = Bits8} {to = Bits64} 123,
+    show $ cast {from = Bits8} {to = Int} 123,
+    show $ cast {from = Bits8} {to = Integer} 123
+]
+
+bits16WideningNoEffect : List String
+bits16WideningNoEffect = [
+    show $ cast {from = Bits16} {to = Bits32} 1234,
+    show $ cast {from = Bits16} {to = Bits64} 1234,
+    show $ cast {from = Bits16} {to = Int} 1234,
+    show $ cast {from = Bits16} {to = Integer} 1234
+]
+
+bits32WideningNoEffect : List String
+bits32WideningNoEffect = [
+    show $ cast {from = Bits32} {to = Bits64} 1234567,
+    show $ cast {from = Bits32} {to = Int} 1234567,
+    show $ cast {from = Bits32} {to = Integer} 1234567
+]
+
+--
+-- Narrowing
+--
+
+b8max : Integer
+b8max = 0x100
+
+b16max : Integer
+b16max = 0x10000
+
+b32max : Integer
+b32max = 0x100000000
+
+b64max : Integer
+b64max = 18446744073709551616 -- 0x10000000000000000
+
+
+narrowFromInteger : List String
+narrowFromInteger = [
+    show $ cast {from = Integer} {to = Bits8} (b8max + 134),
+    show $ cast {from = Integer} {to = Bits16} (b16max + 134),
+    show $ cast {from = Integer} {to = Bits32} (b32max + 134),
+    show $ cast {from = Integer} {to = Bits64} (b64max + 134)
+]
+
+narrowFromInt : List String
+narrowFromInt = [
+    show $ cast {from = Int} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Int} {to = Bits16} (cast (b16max + 134)),
+    show $ cast {from = Int} {to = Bits32} (cast (b32max + 134)),
+    show $ cast {from = Int} {to = Bits64} (cast (b64max + 134))
+]
+
+narrowFromBits64 : List String
+narrowFromBits64 = [
+    show $ cast {from = Bits64} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Bits64} {to = Bits16} (cast (b16max + 134)),
+    show $ cast {from = Bits64} {to = Bits32} (cast (b32max + 134))
+]
+
+narrowFromBits32 : List String
+narrowFromBits32 = [
+    show $ cast {from = Bits32} {to = Bits8} (cast (b8max + 134)),
+    show $ cast {from = Bits32} {to = Bits16} (cast (b16max + 134))
+]
+
+narrowFromBits16 : List String
+narrowFromBits16 = [
+    show $ cast {from = Bits16} {to = Bits8} (cast (b8max + 134))
+]
+
+--
+-- Negative numbers
+--
+
+negativeNumberCast : List String
+negativeNumberCast = [
+    show $ cast {to = Bits8} (-19),
+    show $ cast {to = Bits16} (-19),
+    show $ cast {to = Bits32} (-19),
+    show $ cast {to = Bits64} (-19)
+]

tests/node/node022/expected

@@ -0,0 +1,11 @@
+1/1: Building BitCasts (BitCasts.idr)
+Main> ["123", "123", "123", "123", "123"]
+Main> ["1234", "1234", "1234", "1234"]
+Main> ["1234567", "1234567", "1234567"]
+Main> ["134", "134", "134", "134"]
+Main> ["134", "134", "134", "134"]
+Main> ["134", "134", "134"]
+Main> ["134", "134"]
+Main> ["134"]
+Main> ["237", "65517", "4294967277", "18446744073709551597"]
+Main> Bye for now!

tests/node/node022/input

@@ -0,0 +1,10 @@
+bits8WideningNoEffect
+bits16WideningNoEffect
+bits32WideningNoEffect
+narrowFromInteger
+narrowFromInt
+narrowFromBits64
+narrowFromBits32
+narrowFromBits16
+negativeNumberCast
+:q

tests/node/node022/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner --no-color --console-width 0 BitCasts.idr < input
+
+rm -rf build

tests/ttimp/basic006/expected

@@ -2,5 +2,5 @@ Processing as TTImp
 Written TTC
 Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
 Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
-Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved190 ?Main.{a:62}_[]), ($resolved170 ?Main.{a:62}_[])]
+Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved207 ?Main.{a:62}_[]), ($resolved187 ?Main.{a:62}_[])]
 Yaffle> Bye for now!

tests/ttimp/coverage001/expected

@@ -2,10 +2,10 @@ Processing as TTImp
 Written TTC
 Yaffle> Bye for now!
 Processing as TTImp
-Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved186 {b:27}[1] {a:26}[0] $resolved168 ($resolved177 {a:26}[0]) ($resolved177 {b:27}[1])) is not a valid impossible pattern because it typechecks
+Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved203 {b:27}[1] {a:26}[0] $resolved185 ($resolved194 {a:26}[0]) ($resolved194 {b:27}[1])) is not a valid impossible pattern because it typechecks
 Yaffle> Bye for now!
 Processing as TTImp
 Vect3.yaff:25:1--26:1:Not a valid impossible pattern:
-	Vect3.yaff:25:9--25:11:When unifying: $resolved167 and ($resolved175 ?Main.{n:21}_[] ?Main.{b:19}_[])
+	Vect3.yaff:25:9--25:11:When unifying: $resolved184 and ($resolved192 ?Main.{n:21}_[] ?Main.{b:19}_[])
-	Vect3.yaff:25:9--25:11:Type mismatch: $resolved167 and ($resolved175 ?Main.{n:21}_[] ?Main.{b:19}_[])
+	Vect3.yaff:25:9--25:11:Type mismatch: $resolved184 and ($resolved192 ?Main.{n:21}_[] ?Main.{b:19}_[])
 Yaffle> Bye for now!

tests/ttimp/coverage002/expected

@@ -2,6 +2,6 @@ Processing as TTImp
 Written TTC
 Yaffle> Main.lookup: All cases covered
 Yaffle> Main.lookup':
-($resolved217 [__] [__] ($resolved183 [__]) {_:62})
+($resolved234 [__] [__] ($resolved200 [__]) {_:62})
 Yaffle> Main.lookup'': Calls non covering function Main.lookup'
 Yaffle> Bye for now!

tests/ttimp/dot001/expected

@@ -3,13 +3,13 @@ Written TTC
 Yaffle> Bye for now!
 Processing as TTImp
 Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
-Dot2.yaff:15:28--15:30:Pattern variable {P:n:172} unifies with ?{P:m:172}_[]
+Dot2.yaff:15:28--15:30:Pattern variable {P:n:189} unifies with ?{P:m:189}_[]
 Yaffle> Bye for now!
 Processing as TTImp
 Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
-Dot3.yaff:18:10--18:15:Can't match on ($resolved164 ?{P:x:177}_[] ?{P:x:177}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved164 ?Main.{_:13}_[] ?Main.{_:14}_[])
+Dot3.yaff:18:10--18:15:Can't match on ($resolved181 ?{P:x:194}_[] ?{P:x:194}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved181 ?Main.{_:13}_[] ?Main.{_:14}_[])
 Yaffle> Bye for now!
 Processing as TTImp
 Dot4.yaff:17:1--19:1:When elaborating left hand side of Main.addBaz4:
-Dot4.yaff:17:33--17:34:Can't match on ?{P:x:179}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
+Dot4.yaff:17:33--17:34:Can't match on ?{P:x:196}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
 Yaffle> Bye for now!

tests/ttimp/eta002/expected

@@ -1,5 +1,5 @@
 Processing as TTImp
 Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
-Eta.yaff:16:10--17:1:When unifying: ($resolved169 ?Main.{b:18}_[] ?Main.{b:18}_[] \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved179 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved179 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and ($resolved169 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved178)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved178)) $resolved179 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved179 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
+Eta.yaff:16:10--17:1:When unifying: ($resolved186 ?Main.{b:18}_[] ?Main.{b:18}_[] \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved196 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved196 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and ($resolved186 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved195)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved195)) $resolved196 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved196 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
 	Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
 Yaffle> Bye for now!