From f028981e5ace4ec06e6e98dc27b43b61bce83760 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stefan=20H=C3=B6ck?= Date: Mon, 10 May 2021 13:17:09 +0200 Subject: [PATCH] [ fix #801 ] Use Number for up to 32 bit integers on JS backends (#1375) --- CHANGELOG.md | 6 + CONTRIBUTORS | 1 + src/Compiler/ES/ES.idr | 251 +++++++++++++++++++++++++---------- tests/Main.idr | 2 + tests/chez/bitops/BitOps.idr | 205 ++++++++++++++++++++++++++++ tests/chez/bitops/expected | 2 + tests/chez/bitops/input | 2 + tests/chez/bitops/run | 3 + tests/node/bitops/BitOps.idr | 205 ++++++++++++++++++++++++++++ tests/node/bitops/expected | 2 + tests/node/bitops/input | 2 + tests/node/bitops/run | 3 + 12 files changed, 611 insertions(+), 73 deletions(-) create mode 100644 tests/chez/bitops/BitOps.idr create mode 100644 tests/chez/bitops/expected create mode 100644 tests/chez/bitops/input create mode 100644 tests/chez/bitops/run create mode 100644 tests/node/bitops/BitOps.idr create mode 100644 tests/node/bitops/expected create mode 100644 tests/node/bitops/input create mode 100644 tests/node/bitops/run diff --git a/CHANGELOG.md b/CHANGELOG.md index efa5aa133..40e14a27e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,12 @@ Compiler changes: order to not block the Racket runtime when `sleep` is called. * Added `--profile` flag, which generates profile data if supported by a back end. Currently supported by the Chez and Racket back ends. +* Javascript codegens now use `Number` to represent up to 32 bit precision + signed and unsigned integers. `Int32` still goes via `BigInt` for + multiplication to avoid precision issues when getting results larger + than `Number.MAX_SAFE_INTEGER`. `Bits32` goes via `BigInt` for + multiplication for the same reason as well as for all bitops, since `Number` + uses signed 32 bit integers for those. Library changes: diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 77c79252a..4e26a9b5e 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -50,6 +50,7 @@ Rohit Grover Rui Barreiro Ruslan Feizerahmanov Simon Chatterjee +Stefan Höck tensorknower69 then0rTh Theo Butler diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index 6b7a76184..dc0340852 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -120,102 +120,172 @@ jsCrashExp message = n <- addConstToPreamble "crashExp" "x=>{throw new IdrisError(x)}" pure $ n ++ "("++ message ++ ")" -jsIntegerOfString : {auto c : Ref ESs ESSt} -> String -> Core String -jsIntegerOfString x = +toBigInt : String -> String +toBigInt e = "BigInt(" ++ e ++ ")" + +fromBigInt : String -> String +fromBigInt e = "Number(" ++ e ++ ")" + +useBigInt' : Int -> Bool +useBigInt' = (> 32) + +useBigInt : IntKind -> Bool +useBigInt (Signed $ P x) = useBigInt' x +useBigInt (Signed Unlimited) = True +useBigInt (Unsigned x) = useBigInt' x + +jsBigIntOfString : {auto c : Ref ESs ESSt} -> String -> Core String +jsBigIntOfString x = do - n <- addConstToPreamble "integerOfString" "s=>{const idx = s.indexOf('.'); return idx === -1 ? BigInt(s) : BigInt(s.slice(0, idx));}" + n <- addConstToPreamble "bigIntOfString" "s=>{const idx = s.indexOf('.'); return idx === -1 ? BigInt(s) : BigInt(s.slice(0, idx));}" pure $ n ++ "(" ++ x ++ ")" +jsNumberOfString : {auto c : Ref ESs ESSt} -> String -> Core String +jsNumberOfString x = pure $ "parseFloat(" ++ x ++ ")" + +jsIntOfString : {auto c : Ref ESs ESSt} -> IntKind -> String -> Core String +jsIntOfString k = if useBigInt k then jsBigIntOfString else jsNumberOfString + nSpaces : Nat -> String nSpaces n = pack $ List.replicate n ' ' binOp : String -> String -> String -> String binOp o lhs rhs = "(" ++ lhs ++ " " ++ o ++ " " ++ rhs ++ ")" -toBigInt : String -> String -toBigInt e = "BigInt(" ++ e ++ ")" +adjInt : Int -> String -> String +adjInt bits = if useBigInt' bits then toBigInt else id -fromBigInt : String -> String -fromBigInt e = "Number(" ++ e ++ ")" +toInt : IntKind -> String -> String +toInt k = if useBigInt k then toBigInt else id -jsIntegerOfChar : String -> String -jsIntegerOfChar s = toBigInt (s++ ".codePointAt(0)") +fromInt : IntKind -> String -> String +fromInt k = if useBigInt k then fromBigInt else id -jsIntegerOfDouble : String -> String -jsIntegerOfDouble s = toBigInt $ "Math.trunc(" ++ s ++ ")" +jsIntOfChar : IntKind -> String -> String +jsIntOfChar k s = toInt k $ s ++ ".codePointAt(0)" + +jsIntOfDouble : IntKind -> String -> String +jsIntOfDouble k s = toInt k $ "Math.trunc(" ++ s ++ ")" jsAnyToString : String -> String jsAnyToString s = "(''+" ++ s ++ ")" +-- Valid unicode code poing range is [0,1114111], therefore, +-- we calculate the remainder modulo 1114112 (= 17 * 2^16). +jsCharOfInt : {auto c : Ref ESs ESSt} -> IntKind -> String -> Core String +jsCharOfInt k e = + do fn <- addConstToPreamble + ("truncToChar") + ("x=>(x >= 0 && x <= 55295) || (x >= 57344 && x <= 1114111) ? x : 0") + pure $ "String.fromCodePoint(" ++ fn ++ "(" ++ fromInt k e ++ "))" -makeIntBound : {auto c : Ref ESs ESSt} -> Int -> Core String -makeIntBound bits = addConstToPreamble ("int_bound_" ++ show bits) ("BigInt(2) ** BigInt("++ show bits ++") ") +makeIntBound : {auto c : Ref ESs ESSt} -> + (isBigInt : Bool) -> Int -> Core String +makeIntBound isBigInt bits = + let f = if isBigInt then toBigInt else id + name = if isBigInt then "bigint_bound_" else "int_bound_" + in addConstToPreamble (name ++ show bits) (f "2" ++ " ** "++ f (show bits)) -truncateInt : {auto c : Ref ESs ESSt} -> Int -> String -> Core String -truncateInt bits e = +truncateIntWithBitMask : {auto c : Ref ESs ESSt} -> Int -> String -> Core String +truncateIntWithBitMask bits e = let bs = show bits - in do - mn <- addConstToPreamble ("int_mask_neg_" ++ bs) - ("BigInt(-1) << BigInt(" ++ bs ++")") - mp <- addConstToPreamble ("int_mask_pos_" ++ bs) - ("(BigInt(1) << BigInt(" ++ bs ++")) - BigInt(1)") + f = adjInt bits + in do ib <- makeIntBound (useBigInt' bits) bits + mn <- addConstToPreamble ("int_mask_neg_" ++ bs) ("-" ++ ib) + mp <- addConstToPreamble ("int_mask_pos_" ++ bs) (ib ++ " - " ++ f "1") pure $ concat {t = List} - [ "((", mn, " & ", e, ") == BigInt(0) ? " - , "(", e, " & ", mp, ") : " - , "(", e, " | ", mn, ")" + [ "((", ib, " & ", e, ") == " ++ ib ++ " ? " + , "(", e, " | ", mn, ") : " + , "(", e, " & ", mp, ")" , ")" ] --- Valid unicode code poing range is [0,1114111], therefore, --- we calculate the remainder modulo 1114112 (= 17 * 2^16). -truncChar : {auto c : Ref ESs ESSt} -> String -> Core String -truncChar e = - do fn <- addConstToPreamble ("truncToChar") ("x=>(x >= 0 && x <= 55295) || (x >= 57344 && x <= 1114111) ? x : 0") - pure $ "String.fromCodePoint(" ++ fn ++ "(" ++ fromBigInt e ++ "))" +-- We can't determine `isBigInt` from the given number of bits, since +-- when casting from BigInt to Number we need to truncate the BigInt +-- first, otherwise we might lose precision +boundedInt : {auto c : Ref ESs ESSt} -> + (isBigInt : Bool) -> Int -> String -> Core String +boundedInt isBigInt bits e = + let name = if isBigInt then "truncToBigInt" else "truncToInt" + in do n <- makeIntBound isBigInt bits + fn <- addConstToPreamble + (name ++ show bits) + ("x=>(x<(-" ++ n ++ ")||(x>=" ++ n ++ "))?x%" ++ n ++ ":x") + pure $ fn ++ "(" ++ e ++ ")" -boundedInt : {auto c : Ref ESs ESSt} -> Int -> String -> Core String -boundedInt bits e = - do - n <- makeIntBound bits - fn <- addConstToPreamble ("truncToInt"++show bits) ("x=>(x<(-" ++ n ++ ")||(x>=" ++ n ++ "))?x%" ++ n ++ ":x") - pure $ fn ++ "(" ++ e ++ ")" +boundedUInt : {auto c : Ref ESs ESSt} -> + (isBigInt : Bool) -> Int -> String -> Core String +boundedUInt isBigInt bits e = + let name = if isBigInt then "truncToUBigInt" else "truncToUInt" + in do n <- makeIntBound isBigInt bits + fn <- addConstToPreamble + (name ++ show bits) + ("x=>{const m = x%" ++ n ++ ";return m>=0?m:m+" ++ n ++ "}") + pure $ fn ++ "(" ++ e ++ ")" -boundedUInt : {auto c : Ref ESs ESSt} -> Int -> String -> Core String -boundedUInt bits e = - do - n <- makeIntBound bits - fn <- addConstToPreamble ("truncToUInt"++show bits) ("x=>{const m = x%" ++ n ++ ";return m>=0?m:m+" ++ n ++ "}") - pure $ fn ++ "(" ++ e ++ ")" +boundedIntOp : {auto c : Ref ESs ESSt} -> + Int -> String -> String -> String -> Core String +boundedIntOp bits o lhs rhs = + boundedInt (useBigInt' bits) bits (binOp o lhs rhs) -boundedIntOp : {auto c : Ref ESs ESSt} -> Int -> String -> String -> String -> Core String -boundedIntOp bits o lhs rhs = boundedInt bits (binOp o lhs rhs) +boundedIntBitOp : {auto c : Ref ESs ESSt} -> + Int -> String -> String -> String -> Core String +boundedIntBitOp bits o lhs rhs = truncateIntWithBitMask bits (binOp o lhs rhs) -boundedIntBitOp : {auto c : Ref ESs ESSt} -> Int -> String -> String -> String -> Core String -boundedIntBitOp bits o lhs rhs = truncateInt bits (binOp o lhs rhs) - -boundedUIntOp : {auto c : Ref ESs ESSt} -> Int -> String -> String -> String -> Core String -boundedUIntOp bits o lhs rhs = boundedUInt bits (binOp o lhs rhs) +boundedUIntOp : {auto c : Ref ESs ESSt} -> + Int -> String -> String -> String -> Core String +boundedUIntOp bits o lhs rhs = + boundedUInt (useBigInt' bits) bits (binOp o lhs rhs) boolOp : String -> String -> String -> String boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? BigInt(1) : BigInt(0))" jsConstant : {auto c : Ref ESs ESSt} -> Constant -> Core String jsConstant (I i) = pure $ show i ++ "n" -jsConstant (I8 i) = pure $ show i ++ "n" -jsConstant (I16 i) = pure $ show i ++ "n" -jsConstant (I32 i) = pure $ show i ++ "n" +jsConstant (I8 i) = pure $ show i +jsConstant (I16 i) = pure $ show i +jsConstant (I32 i) = pure $ show i jsConstant (I64 i) = pure $ show i ++ "n" jsConstant (BI i) = pure $ show i ++ "n" jsConstant (Str s) = pure $ jsString s jsConstant (Ch c) = pure $ jsString $ Data.Strings.singleton c jsConstant (Db f) = pure $ show f jsConstant WorldVal = addConstToPreamble "idrisworld" "Symbol('idrisworld')"; -jsConstant (B8 i) = pure $ show i ++ "n" -jsConstant (B16 i) = pure $ show i ++ "n" -jsConstant (B32 i) = pure $ show i ++ "n" +jsConstant (B8 i) = pure $ show i +jsConstant (B16 i) = pure $ show i +jsConstant (B32 i) = pure $ show i jsConstant (B64 i) = pure $ show i ++ "n" jsConstant ty = throw (InternalError $ "Unsuported constant " ++ show ty) +-- For multiplication of 32bit integers (signed or unsigned), +-- we go via BigInt and back, otherwise the calculation is +-- susceptible to rounding error, since we might exceed `MAX_SAFE_INTEGER`. +mult : {auto c : Ref ESs ESSt} + -> Maybe IntKind + -> (x : String) + -> (y : String) + -> Core String +mult (Just $ Signed $ P 32) x y = + fromBigInt <$> boundedInt True 31 (binOp "*" (toBigInt x) (toBigInt y)) + +mult (Just $ Unsigned 32) x y = + fromBigInt <$> boundedUInt True 32 (binOp "*" (toBigInt x) (toBigInt y)) + +mult (Just $ Signed $ P n) x y = boundedIntOp (n-1) "*" x y +mult (Just $ Unsigned n) x y = boundedUIntOp n "*" x y +mult _ x y = pure $ binOp "*" x y + +div : {auto c : Ref ESs ESSt} + -> Maybe IntKind + -> (x : String) + -> (y : String) + -> Core String +div (Just k) x y = + if useBigInt k then pure $ binOp "/" x y + else pure $ jsIntOfDouble k (x ++ " / " ++ y) +div Nothing x y = pure $ binOp "/" x y + + -- Creates the definition of a binary arithmetic operation. -- Rounding / truncation behavior is determined from the -- `IntKind`. @@ -231,6 +301,9 @@ arithOp _ op x y = pure $ binOp op x y -- Same as `arithOp` but for bitwise operations that might -- go out of the valid range. +-- Note: Bitwise operations on `Number` work correctly for +-- 32bit *signed* integers. For `Bits32` we therefore go via `BigInt` +-- in order not having to deal with all kinds of negativity nastiness. bitOp : {auto c : Ref ESs ESSt} -> Maybe IntKind -> (op : String) @@ -238,43 +311,75 @@ bitOp : {auto c : Ref ESs ESSt} -> (y : String) -> Core String bitOp (Just $ Signed $ P n) op x y = boundedIntBitOp (n-1) op x y +bitOp (Just $ Unsigned 32) op x y = + fromBigInt <$> boundedUInt True 32 (binOp op (toBigInt x) (toBigInt y)) bitOp (Just $ Unsigned n) op x y = boundedUIntOp n op x y bitOp _ op x y = pure $ binOp op x y constPrimitives : {auto c : Ref ESs ESSt} -> ConstantPrimitives constPrimitives = MkConstantPrimitives { - charToInt = \k => truncInt k . jsIntegerOfChar - , intToChar = \_ => truncChar - , stringToInt = \k,s => jsIntegerOfString s >>= truncInt k + charToInt = \k => truncInt (useBigInt k) k . jsIntOfChar k + , intToChar = \k => jsCharOfInt k + , stringToInt = \k,s => jsIntOfString k s >>= truncInt (useBigInt k) k , intToString = \_ => pure . jsAnyToString - , doubleToInt = \k => truncInt k . jsIntegerOfDouble - , intToDouble = \_ => pure . fromBigInt + , doubleToInt = \k => truncInt (useBigInt k) k . jsIntOfDouble k + , intToDouble = \k => pure . fromInt k , intToInt = intImpl } - where truncInt : IntKind -> String -> Core String - truncInt (Signed Unlimited) = pure - truncInt (Signed $ P n) = boundedInt (n-1) - truncInt (Unsigned n) = boundedUInt n + where truncInt : (isBigInt : Bool) -> IntKind -> String -> Core String + truncInt b (Signed Unlimited) = pure + truncInt b (Signed $ P n) = boundedInt b (n-1) + truncInt b (Unsigned n) = boundedUInt b n + shrink : IntKind -> IntKind -> String -> String + shrink k1 k2 = case (useBigInt k1, useBigInt k2) of + (True, False) => fromBigInt + _ => id + + expand : IntKind -> IntKind -> String -> String + expand k1 k2 = case (useBigInt k1, useBigInt k2) of + (False,True) => toBigInt + _ => id + + -- when going from BigInt to Number, we must make + -- sure to first truncate the BigInt, otherwise we + -- might get rounding issues intImpl : IntKind -> IntKind -> String -> Core String - intImpl _ (Signed Unlimited) = pure - intImpl (Signed m) k@(Signed n) = if n >= m then pure else truncInt k - intImpl (Signed _) k@(Unsigned n) = truncInt k - intImpl (Unsigned m) k@(Unsigned n) = if n >= m then pure else truncInt k + intImpl k1 k2 s = + let expanded = expand k1 k2 s + shrunk = shrink k1 k2 <$> truncInt (useBigInt k1) k2 s + in case (k1,k2) of + (_, Signed Unlimited) => pure $ expanded + (Signed m, Signed n) => + if n >= m then pure expanded else shrunk - -- Only if the precision of the target is greater - -- than the one of the source, there is no need to cast. - intImpl (Unsigned m) k@(Signed n) = if n > P m then pure else truncInt k + (Signed _, Unsigned n) => + case (useBigInt k1, useBigInt k2) of + (False,True) => truncInt True k2 (toBigInt s) + _ => shrunk + + (Unsigned m, Unsigned n) => + if n >= m then pure expanded else shrunk + + -- Only if the precision of the target is greater + -- than the one of the source, there is no need to cast. + (Unsigned m, Signed n) => + if n > P m then pure expanded else shrunk jsOp : {auto c : Ref ESs ESSt} -> PrimFn arity -> Vect arity String -> Core String jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y jsOp (Sub ty) [x, y] = arithOp (intKind ty) "-" x y -jsOp (Mul ty) [x, y] = arithOp (intKind ty) "*" x y -jsOp (Div ty) [x, y] = arithOp (intKind ty) "/" x y +jsOp (Mul ty) [x, y] = mult (intKind ty) x y +jsOp (Div ty) [x, y] = div (intKind ty) x y jsOp (Mod ty) [x, y] = arithOp (intKind ty) "%" x y jsOp (Neg ty) [x] = pure $ "(-(" ++ x ++ "))" +jsOp (ShiftL Int32Type) [x, y] = pure $ binOp "<<" x y jsOp (ShiftL ty) [x, y] = bitOp (intKind ty) "<<" x y +jsOp (ShiftR Int32Type) [x, y] = pure $ binOp ">>" x y jsOp (ShiftR ty) [x, y] = bitOp (intKind ty) ">>" x y +jsOp (BAnd Bits32Type) [x, y] = pure . fromBigInt $ binOp "&" (toBigInt x) (toBigInt y) +jsOp (BOr Bits32Type) [x, y] = pure . fromBigInt $ binOp "|" (toBigInt x) (toBigInt y) +jsOp (BXOr Bits32Type) [x, y] = pure . fromBigInt $ binOp "^" (toBigInt x) (toBigInt y) jsOp (BAnd ty) [x, y] = pure $ binOp "&" x y jsOp (BOr ty) [x, y] = pure $ binOp "|" x y jsOp (BXOr ty) [x, y] = pure $ binOp "^" x y @@ -307,7 +412,7 @@ jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")" jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")" jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")" -jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")" +jsOp (Cast StringType DoubleType) [x] = jsNumberOfString x jsOp (Cast ty StringType) [x] = pure $ jsAnyToString x jsOp (Cast ty ty2) [x] = castInt constPrimitives ty ty2 x jsOp BelieveMe [_,_,x] = pure x diff --git a/tests/Main.idr b/tests/Main.idr index 5c2851bfd..2f411c478 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -205,6 +205,7 @@ chezTests = MkTestPool [Chez] , "chez025", "chez026", "chez027", "chez028", "chez029", "chez030" , "chez031", "chez032" , "futures001" + , "bitops" , "casts" , "newints" , "semaphores001" @@ -239,6 +240,7 @@ nodeTests = MkTestPool [Node] , "node017", "node018", "node019", "node021", "node022", "node023" , "node024", "node025" -- , "node14", "node020" + , "bitops" , "casts" , "newints" , "reg001" diff --git a/tests/chez/bitops/BitOps.idr b/tests/chez/bitops/BitOps.idr new file mode 100644 index 000000000..9353c662d --- /dev/null +++ b/tests/chez/bitops/BitOps.idr @@ -0,0 +1,205 @@ +import Data.List + +-------------------------------------------------------------------------------- +-- Int8 +-------------------------------------------------------------------------------- + +Show Int8 where + show = prim__cast_Int8String + +public export +Eq Int8 where + x == y = intToBool (prim__eq_Int8 x y) + +Num Int8 where + (+) = prim__add_Int8 + (*) = prim__mul_Int8 + fromInteger = prim__cast_IntegerInt8 + +Neg Int8 where + (-) = prim__sub_Int8 + negate = prim__sub_Int8 0 + +-------------------------------------------------------------------------------- +-- Int16 +-------------------------------------------------------------------------------- + +Show Int16 where + show = prim__cast_Int16String + +public export +Eq Int16 where + x == y = intToBool (prim__eq_Int16 x y) + +Num Int16 where + (+) = prim__add_Int16 + (*) = prim__mul_Int16 + fromInteger = prim__cast_IntegerInt16 + +Neg Int16 where + (-) = prim__sub_Int16 + negate = prim__sub_Int16 0 + +-------------------------------------------------------------------------------- +-- Int32 +-------------------------------------------------------------------------------- + +Show Int32 where + show = prim__cast_Int32String + +public export +Eq Int32 where + x == y = intToBool (prim__eq_Int32 x y) + +Num Int32 where + (+) = prim__add_Int32 + (*) = prim__mul_Int32 + fromInteger = prim__cast_IntegerInt32 + +Neg Int32 where + (-) = prim__sub_Int32 + negate = prim__sub_Int32 0 + +-------------------------------------------------------------------------------- +-- Int64 +-------------------------------------------------------------------------------- + +Show Int64 where + show = prim__cast_Int64String + +public export +Eq Int64 where + x == y = intToBool (prim__eq_Int64 x y) + +Num Int64 where + (+) = prim__add_Int64 + (*) = prim__mul_Int64 + fromInteger = prim__cast_IntegerInt64 + +Neg Int64 where + (-) = prim__sub_Int64 + negate = prim__sub_Int64 0 + +-------------------------------------------------------------------------------- +-- Tests +-------------------------------------------------------------------------------- + +showTpe : Type -> String +showTpe Bits16 = "Bits16" +showTpe Bits32 = "Bits32" +showTpe Bits64 = "Bits64" +showTpe Bits8 = "Bits8" +showTpe Int = "Int" +showTpe Int16 = "Int16" +showTpe Int32 = "Int32" +showTpe Int64 = "Int64" +showTpe Int8 = "Int8" +showTpe Integer = "Integer" +showTpe _ = "unknown type" + +testOp : (a: Type) -> (Show a, Eq a) + => (opName : String) + -> (op : a -> a -> a) + -> List (a,a,a) + -> List String +testOp a n op = mapMaybe doTest + where doTest : (a,a,a) -> Maybe String + doTest (x,y,res) = + let myRes = op x y + in if myRes == res then Nothing + else Just $ #"Invalid result for \#{n} on \#{showTpe a}. "# + ++ #"Inputs: \#{show x}, \#{show y}. "# + ++ #"Expected \#{show res} but got \#{show myRes}."# + +results : List String +results = + testOp Int8 "shl" prim__shl_Int8 + [(0,7,0),(1,1,2),(1,3,8),(1,7,-128),(-1,7,-128)] + ++ testOp Int8 "shr" prim__shr_Int8 + [(0,7,0),(1,1,0),(-128,1,-64),(127,3,15),(-1,3,-1)] + ++ testOp Int8 "and" prim__and_Int8 + [(127,0,0),(-128,0,0),(23,-1,23),(-128,-1,-128),(15,8,8)] + ++ testOp Int8 "or" prim__or_Int8 + [(127,0,127),(-128,-1,-1),(23,-1,-1),(15,64,79)] + ++ testOp Int8 "xor" prim__xor_Int8 + [(127,0,127),(-128,-1,127),(127,-1,-128),(15,64,79),(15,1,14)] + + ++ testOp Bits8 "shl" prim__shl_Bits8 + [(0,7,0),(1,1,2),(1,3,8),(1,7,128),(255,7,128)] + ++ testOp Bits8 "shr" prim__shr_Bits8 + [(0,7,0),(1,1,0),(255,1,127),(127,3,15),(255,3,31)] + ++ testOp Bits8 "and" prim__and_Bits8 + [(127,0,0),(255,0,0),(23,255,23),(128,255,128),(15,8,8)] + ++ testOp Bits8 "or" prim__or_Bits8 + [(127,0,127),(128,255,255),(23,255,255),(15,64,79)] + ++ testOp Bits8 "xor" prim__xor_Bits8 + [(127,0,127),(128,255,127),(127,255,128),(15,64,79),(15,1,14)] + + ++ testOp Int16 "shl" prim__shl_Int16 + [(0,15,0),(1,1,2),(1,4,16),(1,15,-0x8000),(-1,15,-0x8000)] + ++ testOp Int16 "shr" prim__shr_Int16 + [(0,15,0),(1,1,0),(-0x8000,1,-0x4000),(0x7fff,3,0x0fff),(-1,3,-1)] + ++ testOp Int16 "and" prim__and_Int16 + [(0x7fff,0,0),(-0x8000,0,0),(23,-1,23),(-0x8000,-1,-0x8000),(15,8,8)] + ++ testOp Int16 "or" prim__or_Int16 + [(127,0,127),(-0x8000,-1,-1),(23,-1,-1),(15,64,79)] + ++ testOp Int16 "xor" prim__xor_Int16 + [(127,0,127),(-0x8000,-1,0x7fff),(0x7fff,-1,-0x8000),(15,64,79),(15,1,14)] + + ++ testOp Bits16 "shl" prim__shl_Bits16 + [(0,15,0),(1,1,2),(1,4,16),(1,15,0x8000),(0xffff,15,0x8000)] + ++ testOp Bits16 "shr" prim__shr_Bits16 + [(0,15,0),(1,1,0),(0xffff,1,0x7fff),(0x7fff,3,0x0fff),(0xffff,3,0x1fff)] + ++ testOp Bits16 "and" prim__and_Bits16 + [(0x7fff,0,0),(0xffff,0,0),(23,0xffff,23),(0x8000,0xffff,0x8000),(15,8,8)] + ++ testOp Bits16 "or" prim__or_Bits16 + [(0x7fff,0,0x7fff),(0x8000,0xffff,0xffff),(23,0xffff,0xffff),(15,64,79)] + ++ testOp Bits16 "xor" prim__xor_Bits16 + [(0x7fff,0,0x7fff),(0x8000,0xffff,0x7fff),(0x7fff,0xffff,0x8000),(15,64,79),(15,1,14)] + + ++ testOp Int32 "shl" prim__shl_Int32 + [(0,31,0),(1,1,2),(1,4,16),(1,31,-0x80000000),(-1,31,-0x80000000)] + ++ testOp Int32 "shr" prim__shr_Int32 + [(0,31,0),(1,1,0),(-0x80000000,1,-0x40000000),(0x7fffffff,3,0x0fffffff),(-1,3,-1)] + ++ testOp Int32 "and" prim__and_Int32 + [(0x7fffffff,0,0),(-0x80000000,0,0),(23,-1,23),(-0x80000000,-1,-0x80000000),(31,8,8)] + ++ testOp Int32 "or" prim__or_Int32 + [(127,0,127),(-0x80000000,-1,-1),(23,-1,-1),(31,64,95)] + ++ testOp Int32 "xor" prim__xor_Int32 + [(127,0,127),(-0x80000000,-1,0x7fffffff),(0x7fffffff,-1,-0x80000000),(15,64,79),(15,1,14)] + + ++ testOp Bits32 "shl" prim__shl_Bits32 + [(0,31,0),(1,1,2),(1,4,16),(1,31,0x80000000),(0xffffffff,31,0x80000000)] + ++ testOp Bits32 "shr" prim__shr_Bits32 + [(0,31,0),(1,1,0),(0xffffffff,1,0x7fffffff),(0x7fffffff,3,0x0fffffff),(0xffffffff,3,0x1fffffff)] + ++ testOp Bits32 "and" prim__and_Bits32 + [(0x7fffffff,0,0),(0xffffffff,0,0),(23,0xffffffff,23),(0x80000000,0xffffffff,0x80000000),(15,8,8)] + ++ testOp Bits32 "or" prim__or_Bits32 + [(0x7fffffff,0,0x7fffffff),(0x80000000,0xffffffff,0xffffffff),(23,0xffffffff,0xffffffff),(15,64,79)] + ++ testOp Bits32 "xor" prim__xor_Bits32 + [(0x7fffffff,0,0x7fffffff),(0x80000000,0xffffffff,0x7fffffff),(0x7fffffff,0xffffffff,0x80000000),(15,64,79),(15,1,14)] + + ++ testOp Int64 "shl" prim__shl_Int64 + [(0,63,0),(1,1,2),(1,4,16),(1,63,-0x8000000000000000),(-1,63,-0x8000000000000000)] + ++ testOp Int64 "shr" prim__shr_Int64 + [(0,63,0),(1,1,0),(-0x8000000000000000,1,-0x4000000000000000),(0x7fffffffffffffff,3,0x0fffffffffffffff),(-1,3,-1)] + ++ testOp Int64 "and" prim__and_Int64 + [(0x7fffffffffffffff,0,0),(-0x8000000000000000,0,0),(23,-1,23),(-0x8000000000000000,-1,-0x8000000000000000),(63,8,8)] + ++ testOp Int64 "or" prim__or_Int64 + [(127,0,127),(-0x8000000000000000,-1,-1),(23,-1,-1),(63,64,127)] + ++ testOp Int64 "xor" prim__xor_Int64 + [(127,0,127),(-0x8000000000000000,-1,0x7fffffffffffffff),(0x7fffffffffffffff,-1,-0x8000000000000000),(15,64,79),(15,1,14)] + + ++ testOp Bits64 "shl" prim__shl_Bits64 + [(0,63,0),(1,1,2),(1,4,16),(1,63,0x8000000000000000),(0xffffffffffffffff,63,0x8000000000000000)] + ++ testOp Bits64 "shr" prim__shr_Bits64 + [(0,63,0),(1,1,0),(0xffffffffffffffff,1,0x7fffffffffffffff),(0x7fffffffffffffff,3,0x0fffffffffffffff),(0xffffffffffffffff,3,0x1fffffffffffffff)] + ++ testOp Bits64 "and" prim__and_Bits64 + [(0x7fffffffffffffff,0,0),(0xffffffffffffffff,0,0),(23,0xffffffffffffffff,23),(0x8000000000000000,0xffffffffffffffff,0x8000000000000000),(15,8,8)] + ++ testOp Bits64 "or" prim__or_Bits64 + [(0x7fffffffffffffff,0,0x7fffffffffffffff),(0x8000000000000000,0xffffffffffffffff,0xffffffffffffffff),(23,0xffffffffffffffff,0xffffffffffffffff),(15,64,79)] + ++ testOp Bits64 "xor" prim__xor_Bits64 + [(0x7fffffffffffffff,0,0x7fffffffffffffff),(0x8000000000000000,0xffffffffffffffff,0x7fffffffffffffff),(0x7fffffffffffffff,0xffffffffffffffff,0x8000000000000000),(15,64,79),(15,1,14)] + +main : IO () +main = traverse_ putStrLn results diff --git a/tests/chez/bitops/expected b/tests/chez/bitops/expected new file mode 100644 index 000000000..8848f88cd --- /dev/null +++ b/tests/chez/bitops/expected @@ -0,0 +1,2 @@ +1/1: Building BitOps (BitOps.idr) +Main> Main> Bye for now! diff --git a/tests/chez/bitops/input b/tests/chez/bitops/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/chez/bitops/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/chez/bitops/run b/tests/chez/bitops/run new file mode 100644 index 000000000..c275366d8 --- /dev/null +++ b/tests/chez/bitops/run @@ -0,0 +1,3 @@ +$1 --no-banner --no-color --console-width 0 BitOps.idr < input + +rm -rf build diff --git a/tests/node/bitops/BitOps.idr b/tests/node/bitops/BitOps.idr new file mode 100644 index 000000000..9353c662d --- /dev/null +++ b/tests/node/bitops/BitOps.idr @@ -0,0 +1,205 @@ +import Data.List + +-------------------------------------------------------------------------------- +-- Int8 +-------------------------------------------------------------------------------- + +Show Int8 where + show = prim__cast_Int8String + +public export +Eq Int8 where + x == y = intToBool (prim__eq_Int8 x y) + +Num Int8 where + (+) = prim__add_Int8 + (*) = prim__mul_Int8 + fromInteger = prim__cast_IntegerInt8 + +Neg Int8 where + (-) = prim__sub_Int8 + negate = prim__sub_Int8 0 + +-------------------------------------------------------------------------------- +-- Int16 +-------------------------------------------------------------------------------- + +Show Int16 where + show = prim__cast_Int16String + +public export +Eq Int16 where + x == y = intToBool (prim__eq_Int16 x y) + +Num Int16 where + (+) = prim__add_Int16 + (*) = prim__mul_Int16 + fromInteger = prim__cast_IntegerInt16 + +Neg Int16 where + (-) = prim__sub_Int16 + negate = prim__sub_Int16 0 + +-------------------------------------------------------------------------------- +-- Int32 +-------------------------------------------------------------------------------- + +Show Int32 where + show = prim__cast_Int32String + +public export +Eq Int32 where + x == y = intToBool (prim__eq_Int32 x y) + +Num Int32 where + (+) = prim__add_Int32 + (*) = prim__mul_Int32 + fromInteger = prim__cast_IntegerInt32 + +Neg Int32 where + (-) = prim__sub_Int32 + negate = prim__sub_Int32 0 + +-------------------------------------------------------------------------------- +-- Int64 +-------------------------------------------------------------------------------- + +Show Int64 where + show = prim__cast_Int64String + +public export +Eq Int64 where + x == y = intToBool (prim__eq_Int64 x y) + +Num Int64 where + (+) = prim__add_Int64 + (*) = prim__mul_Int64 + fromInteger = prim__cast_IntegerInt64 + +Neg Int64 where + (-) = prim__sub_Int64 + negate = prim__sub_Int64 0 + +-------------------------------------------------------------------------------- +-- Tests +-------------------------------------------------------------------------------- + +showTpe : Type -> String +showTpe Bits16 = "Bits16" +showTpe Bits32 = "Bits32" +showTpe Bits64 = "Bits64" +showTpe Bits8 = "Bits8" +showTpe Int = "Int" +showTpe Int16 = "Int16" +showTpe Int32 = "Int32" +showTpe Int64 = "Int64" +showTpe Int8 = "Int8" +showTpe Integer = "Integer" +showTpe _ = "unknown type" + +testOp : (a: Type) -> (Show a, Eq a) + => (opName : String) + -> (op : a -> a -> a) + -> List (a,a,a) + -> List String +testOp a n op = mapMaybe doTest + where doTest : (a,a,a) -> Maybe String + doTest (x,y,res) = + let myRes = op x y + in if myRes == res then Nothing + else Just $ #"Invalid result for \#{n} on \#{showTpe a}. "# + ++ #"Inputs: \#{show x}, \#{show y}. "# + ++ #"Expected \#{show res} but got \#{show myRes}."# + +results : List String +results = + testOp Int8 "shl" prim__shl_Int8 + [(0,7,0),(1,1,2),(1,3,8),(1,7,-128),(-1,7,-128)] + ++ testOp Int8 "shr" prim__shr_Int8 + [(0,7,0),(1,1,0),(-128,1,-64),(127,3,15),(-1,3,-1)] + ++ testOp Int8 "and" prim__and_Int8 + [(127,0,0),(-128,0,0),(23,-1,23),(-128,-1,-128),(15,8,8)] + ++ testOp Int8 "or" prim__or_Int8 + [(127,0,127),(-128,-1,-1),(23,-1,-1),(15,64,79)] + ++ testOp Int8 "xor" prim__xor_Int8 + [(127,0,127),(-128,-1,127),(127,-1,-128),(15,64,79),(15,1,14)] + + ++ testOp Bits8 "shl" prim__shl_Bits8 + [(0,7,0),(1,1,2),(1,3,8),(1,7,128),(255,7,128)] + ++ testOp Bits8 "shr" prim__shr_Bits8 + [(0,7,0),(1,1,0),(255,1,127),(127,3,15),(255,3,31)] + ++ testOp Bits8 "and" prim__and_Bits8 + [(127,0,0),(255,0,0),(23,255,23),(128,255,128),(15,8,8)] + ++ testOp Bits8 "or" prim__or_Bits8 + [(127,0,127),(128,255,255),(23,255,255),(15,64,79)] + ++ testOp Bits8 "xor" prim__xor_Bits8 + [(127,0,127),(128,255,127),(127,255,128),(15,64,79),(15,1,14)] + + ++ testOp Int16 "shl" prim__shl_Int16 + [(0,15,0),(1,1,2),(1,4,16),(1,15,-0x8000),(-1,15,-0x8000)] + ++ testOp Int16 "shr" prim__shr_Int16 + [(0,15,0),(1,1,0),(-0x8000,1,-0x4000),(0x7fff,3,0x0fff),(-1,3,-1)] + ++ testOp Int16 "and" prim__and_Int16 + [(0x7fff,0,0),(-0x8000,0,0),(23,-1,23),(-0x8000,-1,-0x8000),(15,8,8)] + ++ testOp Int16 "or" prim__or_Int16 + [(127,0,127),(-0x8000,-1,-1),(23,-1,-1),(15,64,79)] + ++ testOp Int16 "xor" prim__xor_Int16 + [(127,0,127),(-0x8000,-1,0x7fff),(0x7fff,-1,-0x8000),(15,64,79),(15,1,14)] + + ++ testOp Bits16 "shl" prim__shl_Bits16 + [(0,15,0),(1,1,2),(1,4,16),(1,15,0x8000),(0xffff,15,0x8000)] + ++ testOp Bits16 "shr" prim__shr_Bits16 + [(0,15,0),(1,1,0),(0xffff,1,0x7fff),(0x7fff,3,0x0fff),(0xffff,3,0x1fff)] + ++ testOp Bits16 "and" prim__and_Bits16 + [(0x7fff,0,0),(0xffff,0,0),(23,0xffff,23),(0x8000,0xffff,0x8000),(15,8,8)] + ++ testOp Bits16 "or" prim__or_Bits16 + [(0x7fff,0,0x7fff),(0x8000,0xffff,0xffff),(23,0xffff,0xffff),(15,64,79)] + ++ testOp Bits16 "xor" prim__xor_Bits16 + [(0x7fff,0,0x7fff),(0x8000,0xffff,0x7fff),(0x7fff,0xffff,0x8000),(15,64,79),(15,1,14)] + + ++ testOp Int32 "shl" prim__shl_Int32 + [(0,31,0),(1,1,2),(1,4,16),(1,31,-0x80000000),(-1,31,-0x80000000)] + ++ testOp Int32 "shr" prim__shr_Int32 + [(0,31,0),(1,1,0),(-0x80000000,1,-0x40000000),(0x7fffffff,3,0x0fffffff),(-1,3,-1)] + ++ testOp Int32 "and" prim__and_Int32 + [(0x7fffffff,0,0),(-0x80000000,0,0),(23,-1,23),(-0x80000000,-1,-0x80000000),(31,8,8)] + ++ testOp Int32 "or" prim__or_Int32 + [(127,0,127),(-0x80000000,-1,-1),(23,-1,-1),(31,64,95)] + ++ testOp Int32 "xor" prim__xor_Int32 + [(127,0,127),(-0x80000000,-1,0x7fffffff),(0x7fffffff,-1,-0x80000000),(15,64,79),(15,1,14)] + + ++ testOp Bits32 "shl" prim__shl_Bits32 + [(0,31,0),(1,1,2),(1,4,16),(1,31,0x80000000),(0xffffffff,31,0x80000000)] + ++ testOp Bits32 "shr" prim__shr_Bits32 + [(0,31,0),(1,1,0),(0xffffffff,1,0x7fffffff),(0x7fffffff,3,0x0fffffff),(0xffffffff,3,0x1fffffff)] + ++ testOp Bits32 "and" prim__and_Bits32 + [(0x7fffffff,0,0),(0xffffffff,0,0),(23,0xffffffff,23),(0x80000000,0xffffffff,0x80000000),(15,8,8)] + ++ testOp Bits32 "or" prim__or_Bits32 + [(0x7fffffff,0,0x7fffffff),(0x80000000,0xffffffff,0xffffffff),(23,0xffffffff,0xffffffff),(15,64,79)] + ++ testOp Bits32 "xor" prim__xor_Bits32 + [(0x7fffffff,0,0x7fffffff),(0x80000000,0xffffffff,0x7fffffff),(0x7fffffff,0xffffffff,0x80000000),(15,64,79),(15,1,14)] + + ++ testOp Int64 "shl" prim__shl_Int64 + [(0,63,0),(1,1,2),(1,4,16),(1,63,-0x8000000000000000),(-1,63,-0x8000000000000000)] + ++ testOp Int64 "shr" prim__shr_Int64 + [(0,63,0),(1,1,0),(-0x8000000000000000,1,-0x4000000000000000),(0x7fffffffffffffff,3,0x0fffffffffffffff),(-1,3,-1)] + ++ testOp Int64 "and" prim__and_Int64 + [(0x7fffffffffffffff,0,0),(-0x8000000000000000,0,0),(23,-1,23),(-0x8000000000000000,-1,-0x8000000000000000),(63,8,8)] + ++ testOp Int64 "or" prim__or_Int64 + [(127,0,127),(-0x8000000000000000,-1,-1),(23,-1,-1),(63,64,127)] + ++ testOp Int64 "xor" prim__xor_Int64 + [(127,0,127),(-0x8000000000000000,-1,0x7fffffffffffffff),(0x7fffffffffffffff,-1,-0x8000000000000000),(15,64,79),(15,1,14)] + + ++ testOp Bits64 "shl" prim__shl_Bits64 + [(0,63,0),(1,1,2),(1,4,16),(1,63,0x8000000000000000),(0xffffffffffffffff,63,0x8000000000000000)] + ++ testOp Bits64 "shr" prim__shr_Bits64 + [(0,63,0),(1,1,0),(0xffffffffffffffff,1,0x7fffffffffffffff),(0x7fffffffffffffff,3,0x0fffffffffffffff),(0xffffffffffffffff,3,0x1fffffffffffffff)] + ++ testOp Bits64 "and" prim__and_Bits64 + [(0x7fffffffffffffff,0,0),(0xffffffffffffffff,0,0),(23,0xffffffffffffffff,23),(0x8000000000000000,0xffffffffffffffff,0x8000000000000000),(15,8,8)] + ++ testOp Bits64 "or" prim__or_Bits64 + [(0x7fffffffffffffff,0,0x7fffffffffffffff),(0x8000000000000000,0xffffffffffffffff,0xffffffffffffffff),(23,0xffffffffffffffff,0xffffffffffffffff),(15,64,79)] + ++ testOp Bits64 "xor" prim__xor_Bits64 + [(0x7fffffffffffffff,0,0x7fffffffffffffff),(0x8000000000000000,0xffffffffffffffff,0x7fffffffffffffff),(0x7fffffffffffffff,0xffffffffffffffff,0x8000000000000000),(15,64,79),(15,1,14)] + +main : IO () +main = traverse_ putStrLn results diff --git a/tests/node/bitops/expected b/tests/node/bitops/expected new file mode 100644 index 000000000..8848f88cd --- /dev/null +++ b/tests/node/bitops/expected @@ -0,0 +1,2 @@ +1/1: Building BitOps (BitOps.idr) +Main> Main> Bye for now! diff --git a/tests/node/bitops/input b/tests/node/bitops/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/bitops/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/bitops/run b/tests/node/bitops/run new file mode 100644 index 000000000..0ee1f73d5 --- /dev/null +++ b/tests/node/bitops/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner --no-color --console-width 0 BitOps.idr < input + +rm -rf build