mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-23 22:22:07 +03:00
[ new ] Add Int(8/16/32/64) (#1352)
This adds new `Int8`, `Int16`, `Int32` and `Int64` data types to the compiler, thus working towards properly specified integer types as discussed in #1048. In addition, the following changes / corrections are made: * Support casts from `Char`, `String`, and `Double` to all integer types (and back). This fixes #1270. * Make sure that all casts to limited-precision integers are properly bounds checked (this was not the case so far for casts from `String` and `Double` to `Int`) * Add a thorough set of tests to make sure all bounds checks work correctly for all supported casts and arithmetic operations
This commit is contained in:
Stefan Höck
GitHub
parent
e972a23126
commit
6cdf05f1ec
46
.github/workflows/ci-macos-combined.yml
vendored
46
.github/workflows/ci-macos-combined.yml
vendored
@ -65,26 +65,26 @@ jobs:
|
||||
|
||||
# this gambit test is really slow so se run it separately
|
||||
|
||||
test-gambit:
|
||||
needs: build-bootstrap-chez
|
||||
runs-on: macos-latest
|
||||
steps:
|
||||
- name: Checkout
|
||||
uses: actions/checkout@v2
|
||||
- name: Download Idris2 Artifact
|
||||
uses: actions/download-artifact@v2
|
||||
with:
|
||||
name: installed-bootstrapped-idris2-chez
|
||||
path: ~/.idris2/
|
||||
- name: Install build dependencies
|
||||
run: |
|
||||
brew install chezscheme
|
||||
brew install coreutils
|
||||
brew install gambit-scheme
|
||||
CURRENTDIR=$(find /usr/local/Cellar/gambit-scheme -type l -name current)
|
||||
echo "::add-path::${CURRENTDIR}/bin"
|
||||
echo "::add-path::$HOME/.idris2/bin"
|
||||
chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
|
||||
- name: Test gambit
|
||||
run: cd tests/gambit/bitops001/ && ./run idris2
|
||||
shell: bash
|
||||
# test-gambit:
|
||||
# needs: build-bootstrap-chez
|
||||
# runs-on: macos-latest
|
||||
# steps:
|
||||
# - name: Checkout
|
||||
# uses: actions/checkout@v2
|
||||
# - name: Download Idris2 Artifact
|
||||
# uses: actions/download-artifact@v2
|
||||
# with:
|
||||
# name: installed-bootstrapped-idris2-chez
|
||||
# path: ~/.idris2/
|
||||
# - name: Install build dependencies
|
||||
# run: |
|
||||
# brew install chezscheme
|
||||
# brew install coreutils
|
||||
# brew install gambit-scheme
|
||||
# CURRENTDIR=$(find /usr/local/Cellar/gambit-scheme -type l -name current)
|
||||
# echo "::add-path::${CURRENTDIR}/bin"
|
||||
# echo "::add-path::$HOME/.idris2/bin"
|
||||
# chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
|
||||
# - name: Test gambit
|
||||
# run: cd tests/gambit/bitops001/ && ./run idris2
|
||||
# shell: bash
|
||||
|
||||
@ -449,3 +449,37 @@ pathLookup candidates
|
||||
x <- candidates,
|
||||
y <- extensions ]
|
||||
firstExists candidates
|
||||
|
||||
||| Cast implementations. Values of `ConstantPrimitives` can
|
||||
||| be used in a call to `castInt`, which then determines
|
||||
||| the cast implementation based on the given pair of
|
||||
||| constants.
|
||||
public export
|
||||
record ConstantPrimitives where
|
||||
constructor MkConstantPrimitives
|
||||
charToInt : IntKind -> String -> Core String
|
||||
intToChar : IntKind -> String -> Core String
|
||||
stringToInt : IntKind -> String -> Core String
|
||||
intToString : IntKind -> String -> Core String
|
||||
doubleToInt : IntKind -> String -> Core String
|
||||
intToDouble : IntKind -> String -> Core String
|
||||
intToInt : IntKind -> IntKind -> String -> Core String
|
||||
|
||||
||| Implements casts from and to integral types by using
|
||||
||| the implementations from the provided `ConstantPrimitives`.
|
||||
export
|
||||
castInt : ConstantPrimitives
|
||||
-> Constant
|
||||
-> Constant
|
||||
-> String
|
||||
-> Core String
|
||||
castInt p from to x =
|
||||
case ((from, intKind from), (to, intKind to)) of
|
||||
((CharType, _) , (_, Just k)) => p.charToInt k x
|
||||
((StringType, _), (_, Just k)) => p.stringToInt k x
|
||||
((DoubleType, _), (_, Just k)) => p.doubleToInt k x
|
||||
((_, Just k), (CharType, _)) => p.intToChar k x
|
||||
((_, Just k), (StringType, _)) => p.intToString k x
|
||||
((_, Just k), (DoubleType, _)) => p.intToDouble k x
|
||||
((_, Just k1), (_, Just k2)) => p.intToInt k1 k2 x
|
||||
_ => throw $ InternalError $ "invalid cast: + " ++ show from ++ " + ' -> ' + " ++ show to
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
module Compiler.ES.ES
|
||||
|
||||
import Compiler.Common
|
||||
import Compiler.ES.Imperative
|
||||
import Libraries.Utils.Hex
|
||||
import Data.List1
|
||||
@ -137,16 +138,19 @@ toBigInt e = "BigInt(" ++ e ++ ")"
|
||||
fromBigInt : String -> String
|
||||
fromBigInt e = "Number(" ++ e ++ ")"
|
||||
|
||||
jsIntegerOfChar : String -> String
|
||||
jsIntegerOfChar s = toBigInt (s++ ".codePointAt(0)")
|
||||
|
||||
jsIntegerOfDouble : String -> String
|
||||
jsIntegerOfDouble s = toBigInt $ "Math.trunc(" ++ s ++ ")"
|
||||
|
||||
jsAnyToString : String -> String
|
||||
jsAnyToString s = "(''+" ++ s ++ ")"
|
||||
|
||||
|
||||
makeIntBound : {auto c : Ref ESs ESSt} -> Int -> Core String
|
||||
makeIntBound bits = addConstToPreamble ("int_bound_" ++ show bits) ("BigInt(2) ** BigInt("++ show bits ++") ")
|
||||
|
||||
boundedInt : {auto c : Ref ESs ESSt} -> Int -> String -> Core String
|
||||
boundedInt bits e =
|
||||
do
|
||||
n <- makeIntBound bits
|
||||
pure $ "(" ++ e ++ " % " ++ n ++ ")"
|
||||
|
||||
truncateInt : {auto c : Ref ESs ESSt} -> Int -> String -> Core String
|
||||
truncateInt bits e =
|
||||
let bs = show bits
|
||||
@ -162,10 +166,24 @@ truncateInt bits e =
|
||||
, ")"
|
||||
]
|
||||
|
||||
-- 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 ++ "))"
|
||||
|
||||
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} -> Int -> String -> Core String
|
||||
boundedUInt bits e =
|
||||
do
|
||||
n <- makeIntBound bits
|
||||
n <- makeIntBound bits
|
||||
fn <- addConstToPreamble ("truncToUInt"++show bits) ("x=>{const m = x%" ++ n ++ ";return m>=0?m:m+" ++ n ++ "}")
|
||||
pure $ fn ++ "(" ++ e ++ ")"
|
||||
|
||||
@ -183,6 +201,10 @@ 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 (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
|
||||
@ -203,9 +225,9 @@ arithOp : {auto c : Ref ESs ESSt}
|
||||
-> (x : String)
|
||||
-> (y : String)
|
||||
-> Core String
|
||||
arithOp (Just $ Signed $ P n) op x y = boundedIntOp (n-1) op x y
|
||||
arithOp (Just $ Unsigned $ P n) op x y = boundedUIntOp n op x y
|
||||
arithOp _ op x y = pure $ binOp op x y
|
||||
arithOp (Just $ Signed $ P n) op x y = boundedIntOp (n-1) op x y
|
||||
arithOp (Just $ Unsigned n) op x y = boundedUIntOp n op x y
|
||||
arithOp _ op x y = pure $ binOp op x y
|
||||
|
||||
-- Same as `arithOp` but for bitwise operations that might
|
||||
-- go out of the valid range.
|
||||
@ -215,33 +237,34 @@ bitOp : {auto c : Ref ESs ESSt}
|
||||
-> (x : String)
|
||||
-> (y : String)
|
||||
-> Core String
|
||||
bitOp (Just $ Signed $ P n) op x y = boundedIntBitOp (n-1) op x y
|
||||
bitOp (Just $ Unsigned $ P n) op x y = boundedUIntOp n op x y
|
||||
bitOp _ op x y = pure $ binOp op x y
|
||||
bitOp (Just $ Signed $ P n) op x y = boundedIntBitOp (n-1) op x y
|
||||
bitOp (Just $ Unsigned n) op x y = boundedUIntOp n op x y
|
||||
bitOp _ op x y = pure $ binOp op x y
|
||||
|
||||
castInt : {auto c : Ref ESs ESSt}
|
||||
-> Constant
|
||||
-> Constant
|
||||
-> String
|
||||
-> Core String
|
||||
castInt from to x =
|
||||
case (intKind from, intKind to) of
|
||||
(Just _, Just $ Signed Unlimited) => pure x
|
||||
constPrimitives : {auto c : Ref ESs ESSt} -> ConstantPrimitives
|
||||
constPrimitives = MkConstantPrimitives {
|
||||
charToInt = \k => truncInt k . jsIntegerOfChar
|
||||
, intToChar = \_ => truncChar
|
||||
, stringToInt = \k,s => jsIntegerOfString s >>= truncInt k
|
||||
, intToString = \_ => pure . jsAnyToString
|
||||
, doubleToInt = \k => truncInt k . jsIntegerOfDouble
|
||||
, intToDouble = \_ => pure . fromBigInt
|
||||
, intToInt = intImpl
|
||||
}
|
||||
where truncInt : IntKind -> String -> Core String
|
||||
truncInt (Signed Unlimited) = pure
|
||||
truncInt (Signed $ P n) = boundedInt (n-1)
|
||||
truncInt (Unsigned n) = boundedUInt n
|
||||
|
||||
(Just $ Signed m, Just $ Signed $ P n) =>
|
||||
if P n >= m then pure x else boundedInt (n-1) x
|
||||
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
|
||||
|
||||
-- Only if the precision of the target is greater
|
||||
-- than the one of the source, there is no need to cast.
|
||||
(Just $ Unsigned m, Just $ Signed $ P n) =>
|
||||
if P n > m then pure x else boundedInt (n-1) x
|
||||
|
||||
(Just $ Signed _, Just $ Unsigned $ P n) => boundedUInt n x
|
||||
|
||||
(Just $ Unsigned m, Just $ Unsigned $ P n) =>
|
||||
if P n >= m then pure x else boundedUInt n x
|
||||
|
||||
_ => throw $ InternalError $ "invalid cast: + " ++ show from ++ " + ' -> ' + " ++ show to
|
||||
-- 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
|
||||
|
||||
jsOp : {auto c : Ref ESs ESSt} -> PrimFn arity -> Vect arity String -> Core String
|
||||
jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y
|
||||
@ -284,20 +307,9 @@ jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")"
|
||||
jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")"
|
||||
jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")"
|
||||
|
||||
jsOp (Cast CharType IntType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
|
||||
jsOp (Cast CharType IntegerType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
|
||||
jsOp (Cast DoubleType IntType) [x] = boundedInt 63 $ "BigInt(Math.floor(" ++ x ++ "))"
|
||||
jsOp (Cast DoubleType IntegerType) [x] = pure $ "BigInt(Math.floor(" ++ x ++ "))"
|
||||
jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
|
||||
jsOp (Cast IntType DoubleType) [x] = pure $ "Number(" ++ x ++ ")"
|
||||
jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
|
||||
jsOp (Cast IntegerType DoubleType) [x] = pure $ "Number(" ++ x ++ ")"
|
||||
jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"
|
||||
jsOp (Cast StringType IntType) [x] = boundedInt 63 $ !(jsIntegerOfString x)
|
||||
jsOp (Cast StringType IntegerType) [x] = jsIntegerOfString x
|
||||
|
||||
jsOp (Cast ty StringType) [x] = pure $ "(''+" ++ x ++ ")"
|
||||
jsOp (Cast ty ty2) [x] = castInt ty ty2 x
|
||||
jsOp (Cast ty StringType) [x] = pure $ jsAnyToString x
|
||||
jsOp (Cast ty ty2) [x] = castInt constPrimitives ty ty2 x
|
||||
jsOp BelieveMe [_,_,x] = pure x
|
||||
jsOp (Crash) [_, msg] = jsCrashExp msg
|
||||
|
||||
|
||||
@ -58,125 +58,131 @@ boolop : String -> List String -> String
|
||||
boolop o args = "(or (and " ++ op o args ++ " 1) 0)"
|
||||
|
||||
add : Maybe IntKind -> String -> String -> String
|
||||
add (Just $ Signed $ P n) x y = op "b+" [x, y, show (n-1)]
|
||||
add (Just $ Unsigned $ P n) x y = op "b+" [x, y, show n]
|
||||
add (Just $ Signed $ P n) x y = op "bs+" [x, y, show (n-1)]
|
||||
add (Just $ Unsigned n) x y = op "bu+" [x, y, show n]
|
||||
add _ x y = op "+" [x, y]
|
||||
|
||||
sub : Maybe IntKind -> String -> String -> String
|
||||
sub (Just $ Signed $ P n) x y = op "b-" [x, y, show (n-1)]
|
||||
sub (Just $ Unsigned $ P n) x y = op "b-" [x, y, show n]
|
||||
sub (Just $ Signed $ P n) x y = op "bs-" [x, y, show (n-1)]
|
||||
sub (Just $ Unsigned n) x y = op "bu-" [x, y, show n]
|
||||
sub _ x y = op "-" [x, y]
|
||||
|
||||
mul : Maybe IntKind -> String -> String -> String
|
||||
mul (Just $ Signed $ P n) x y = op "b*" [x, y, show (n-1)]
|
||||
mul (Just $ Unsigned $ P n) x y = op "b*" [x, y, show n]
|
||||
mul (Just $ Signed $ P n) x y = op "bs*" [x, y, show (n-1)]
|
||||
mul (Just $ Unsigned n) x y = op "bu*" [x, y, show n]
|
||||
mul _ x y = op "*" [x, y]
|
||||
|
||||
div : Maybe IntKind -> String -> String -> String
|
||||
div (Just $ Signed Unlimited) x y = op "quotient" [x, y]
|
||||
div (Just $ Signed $ P n) x y = op "b/" [x, y, show (n-1)]
|
||||
div (Just $ Unsigned $ P n) x y = op "b/" [x, y, show n]
|
||||
div (Just $ Signed $ P n) x y = op "bs/" [x, y, show (n-1)]
|
||||
div (Just $ Unsigned n) x y = op "bu/" [x, y, show n]
|
||||
div _ x y = op "/" [x, y]
|
||||
|
||||
shl : Maybe IntKind -> String -> String -> String
|
||||
shl (Just $ Signed $ P n) x y = op "blodwen-bits-shl-signed"
|
||||
[x, y, show (n-1)]
|
||||
shl (Just $ Unsigned $ P n) x y = op "blodwen-bits-shl" [x, y, show n]
|
||||
shl _ x y = op "blodwen-shl" [x, y]
|
||||
shl (Just $ Signed $ P n) x y = op "blodwen-bits-shl-signed"
|
||||
[x, y, show (n-1)]
|
||||
shl (Just $ Unsigned n) x y = op "blodwen-bits-shl" [x, y, show n]
|
||||
shl _ x y = op "blodwen-shl" [x, y]
|
||||
|
||||
castInt : Constant -> Constant -> String -> String
|
||||
castInt from to x =
|
||||
case (intKind from, intKind to) of
|
||||
(Just _, Just $ Signed Unlimited) => x
|
||||
|
||||
(Just $ Signed m, Just $ Signed $ P n) =>
|
||||
if P n >= m then x else op "blodwen-toSignedInt" [x,show (n-1)]
|
||||
constPrimitives : ConstantPrimitives
|
||||
constPrimitives = MkConstantPrimitives {
|
||||
charToInt = \k => pure . charTo k
|
||||
, intToChar = \_,x => pure $ op "cast-int-char" [x]
|
||||
, stringToInt = \k => pure . strTo k
|
||||
, intToString = \_,x => pure $ op "number->string" [x]
|
||||
, doubleToInt = \k => pure . dblTo k
|
||||
, intToDouble = \_,x => pure $ op "exact->inexact" [x]
|
||||
, intToInt = \k1,k2 => pure . intTo k1 k2
|
||||
}
|
||||
where charTo : IntKind -> String -> String
|
||||
charTo (Signed Unlimited) x = op "char->integer" [x]
|
||||
charTo (Signed $ P n) x = op "cast-char-boundedInt" [x, show (n-1)]
|
||||
charTo (Unsigned n) x = op "cast-char-boundedUInt" [x,show n]
|
||||
|
||||
-- Only if the precision of the target is greater
|
||||
-- than the one of the source, there is no need to cast.
|
||||
(Just $ Unsigned m, Just $ Signed $ P n) =>
|
||||
if P n > m then x else op "blodwen-toSignedInt" [x,show (n-1)]
|
||||
strTo : IntKind -> String -> String
|
||||
strTo (Signed Unlimited) x = op "cast-string-int" [x]
|
||||
strTo (Signed $ P n) x = op "cast-string-boundedInt" [x, show (n-1)]
|
||||
strTo (Unsigned n) x = op "cast-string-boundedUInt" [x,show n]
|
||||
|
||||
(Just $ Signed _, Just $ Unsigned $ P n) =>
|
||||
op "blodwen-toUnsignedInt" [x,show n]
|
||||
dblTo : IntKind -> String -> String
|
||||
dblTo (Signed Unlimited) x = op "exact-truncate" [x]
|
||||
dblTo (Signed $ P n) x = op "exact-truncate-boundedInt" [x, show (n-1)]
|
||||
dblTo (Unsigned n) x = op "exact-truncate-boundedUInt" [x,show n]
|
||||
|
||||
(Just $ Unsigned m, Just $ Unsigned $ P n) =>
|
||||
if P n >= m then x else op "blodwen-toUnsignedInt" [x,show n]
|
||||
intTo : IntKind -> IntKind -> String -> String
|
||||
intTo _ (Signed Unlimited) x = x
|
||||
intTo (Signed m) (Signed $ P n) x =
|
||||
if P n >= m then x else op "blodwen-toSignedInt" [x,show (n-1)]
|
||||
|
||||
_ => "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"
|
||||
-- Only if the precision of the target is greater
|
||||
-- than the one of the source, there is no need to cast.
|
||||
intTo (Unsigned m) (Signed $ P n) x =
|
||||
if n > m then x else op "blodwen-toSignedInt" [x,show (n-1)]
|
||||
|
||||
intTo (Signed _) (Unsigned n) x = op "blodwen-toUnsignedInt" [x,show n]
|
||||
|
||||
intTo (Unsigned m) (Unsigned n) x =
|
||||
if n >= m then x else op "blodwen-toUnsignedInt" [x,show n]
|
||||
|
||||
||| Generate scheme for a primitive function.
|
||||
schOp : PrimFn arity -> Vect arity String -> String
|
||||
schOp (Add ty) [x, y] = add (intKind ty) x y
|
||||
schOp (Sub ty) [x, y] = sub (intKind ty) x y
|
||||
schOp (Mul ty) [x, y] = mul (intKind ty) x y
|
||||
schOp (Div ty) [x, y] = div (intKind ty) x y
|
||||
schOp (Mod ty) [x, y] = op "remainder" [x, y]
|
||||
schOp (Neg ty) [x] = op "-" [x]
|
||||
schOp (ShiftL ty) [x, y] = shl (intKind ty) x y
|
||||
schOp (ShiftR ty) [x, y] = op "blodwen-shr" [x, y]
|
||||
schOp (BAnd ty) [x, y] = op "blodwen-and" [x, y]
|
||||
schOp (BOr ty) [x, y] = op "blodwen-or" [x, y]
|
||||
schOp (BXOr ty) [x, y] = op "blodwen-xor" [x, y]
|
||||
schOp (LT CharType) [x, y] = boolop "char<?" [x, y]
|
||||
schOp (LTE CharType) [x, y] = boolop "char<=?" [x, y]
|
||||
schOp (EQ CharType) [x, y] = boolop "char=?" [x, y]
|
||||
schOp (GTE CharType) [x, y] = boolop "char>=?" [x, y]
|
||||
schOp (GT CharType) [x, y] = boolop "char>?" [x, y]
|
||||
schOp (LT StringType) [x, y] = boolop "string<?" [x, y]
|
||||
schOp (LTE StringType) [x, y] = boolop "string<=?" [x, y]
|
||||
schOp (EQ StringType) [x, y] = boolop "string=?" [x, y]
|
||||
schOp (GTE StringType) [x, y] = boolop "string>=?" [x, y]
|
||||
schOp (GT StringType) [x, y] = boolop "string>?" [x, y]
|
||||
schOp (LT ty) [x, y] = boolop "<" [x, y]
|
||||
schOp (LTE ty) [x, y] = boolop "<=" [x, y]
|
||||
schOp (EQ ty) [x, y] = boolop "=" [x, y]
|
||||
schOp (GTE ty) [x, y] = boolop ">=" [x, y]
|
||||
schOp (GT ty) [x, y] = boolop ">" [x, y]
|
||||
schOp StrLength [x] = op "string-length" [x]
|
||||
schOp StrHead [x] = op "string-ref" [x, "0"]
|
||||
schOp StrTail [x] = op "substring" [x, "1", op "string-length" [x]]
|
||||
schOp StrIndex [x, i] = op "string-ref" [x, i]
|
||||
schOp StrCons [x, y] = op "string-cons" [x, y]
|
||||
schOp StrAppend [x, y] = op "string-append" [x, y]
|
||||
schOp StrReverse [x] = op "string-reverse" [x]
|
||||
schOp StrSubstr [x, y, z] = op "string-substr" [x, y, z]
|
||||
schOp : PrimFn arity -> Vect arity String -> Core String
|
||||
schOp (Add ty) [x, y] = pure $ add (intKind ty) x y
|
||||
schOp (Sub ty) [x, y] = pure $ sub (intKind ty) x y
|
||||
schOp (Mul ty) [x, y] = pure $ mul (intKind ty) x y
|
||||
schOp (Div ty) [x, y] = pure $ div (intKind ty) x y
|
||||
schOp (Mod ty) [x, y] = pure $ op "remainder" [x, y]
|
||||
schOp (Neg ty) [x] = pure $ op "-" [x]
|
||||
schOp (ShiftL ty) [x, y] = pure $ shl (intKind ty) x y
|
||||
schOp (ShiftR ty) [x, y] = pure $ op "blodwen-shr" [x, y]
|
||||
schOp (BAnd ty) [x, y] = pure $ op "blodwen-and" [x, y]
|
||||
schOp (BOr ty) [x, y] = pure $ op "blodwen-or" [x, y]
|
||||
schOp (BXOr ty) [x, y] = pure $ op "blodwen-xor" [x, y]
|
||||
schOp (LT CharType) [x, y] = pure $ boolop "char<?" [x, y]
|
||||
schOp (LTE CharType) [x, y] = pure $ boolop "char<=?" [x, y]
|
||||
schOp (EQ CharType) [x, y] = pure $ boolop "char=?" [x, y]
|
||||
schOp (GTE CharType) [x, y] = pure $ boolop "char>=?" [x, y]
|
||||
schOp (GT CharType) [x, y] = pure $ boolop "char>?" [x, y]
|
||||
schOp (LT StringType) [x, y] = pure $ boolop "string<?" [x, y]
|
||||
schOp (LTE StringType) [x, y] = pure $ boolop "string<=?" [x, y]
|
||||
schOp (EQ StringType) [x, y] = pure $ boolop "string=?" [x, y]
|
||||
schOp (GTE StringType) [x, y] = pure $ boolop "string>=?" [x, y]
|
||||
schOp (GT StringType) [x, y] = pure $ boolop "string>?" [x, y]
|
||||
schOp (LT ty) [x, y] = pure $ boolop "<" [x, y]
|
||||
schOp (LTE ty) [x, y] = pure $ boolop "<=" [x, y]
|
||||
schOp (EQ ty) [x, y] = pure $ boolop "=" [x, y]
|
||||
schOp (GTE ty) [x, y] = pure $ boolop ">=" [x, y]
|
||||
schOp (GT ty) [x, y] = pure $ boolop ">" [x, y]
|
||||
schOp StrLength [x] = pure $ op "string-length" [x]
|
||||
schOp StrHead [x] = pure $ op "string-ref" [x, "0"]
|
||||
schOp StrTail [x] = pure $ op "substring" [x, "1", op "string-length" [x]]
|
||||
schOp StrIndex [x, i] = pure $ op "string-ref" [x, i]
|
||||
schOp StrCons [x, y] = pure $ op "string-cons" [x, y]
|
||||
schOp StrAppend [x, y] = pure $ op "string-append" [x, y]
|
||||
schOp StrReverse [x] = pure $ op "string-reverse" [x]
|
||||
schOp StrSubstr [x, y, z] = pure $ op "string-substr" [x, y, z]
|
||||
|
||||
-- `e` is Euler's number, which approximates to: 2.718281828459045
|
||||
schOp DoubleExp [x] = op "flexp" [x] -- Base is `e`. Same as: `pow(e, x)`
|
||||
schOp DoubleLog [x] = op "fllog" [x] -- Base is `e`.
|
||||
schOp DoubleSin [x] = op "flsin" [x]
|
||||
schOp DoubleCos [x] = op "flcos" [x]
|
||||
schOp DoubleTan [x] = op "fltan" [x]
|
||||
schOp DoubleASin [x] = op "flasin" [x]
|
||||
schOp DoubleACos [x] = op "flacos" [x]
|
||||
schOp DoubleATan [x] = op "flatan" [x]
|
||||
schOp DoubleSqrt [x] = op "flsqrt" [x]
|
||||
schOp DoubleFloor [x] = op "flfloor" [x]
|
||||
schOp DoubleCeiling [x] = op "flceiling" [x]
|
||||
schOp DoubleExp [x] = pure $ op "flexp" [x] -- Base is `e`. Same as: `pow(e, x)`
|
||||
schOp DoubleLog [x] = pure $ op "fllog" [x] -- Base is `e`.
|
||||
schOp DoubleSin [x] = pure $ op "flsin" [x]
|
||||
schOp DoubleCos [x] = pure $ op "flcos" [x]
|
||||
schOp DoubleTan [x] = pure $ op "fltan" [x]
|
||||
schOp DoubleASin [x] = pure $ op "flasin" [x]
|
||||
schOp DoubleACos [x] = pure $ op "flacos" [x]
|
||||
schOp DoubleATan [x] = pure $ op "flatan" [x]
|
||||
schOp DoubleSqrt [x] = pure $ op "flsqrt" [x]
|
||||
schOp DoubleFloor [x] = pure $ op "flfloor" [x]
|
||||
schOp DoubleCeiling [x] = pure $ op "flceiling" [x]
|
||||
|
||||
schOp (Cast Bits16Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits32Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits64Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits8Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast CharType IntType) [x] = op "char->integer" [x]
|
||||
schOp (Cast CharType IntegerType) [x] = op "char->integer" [x]
|
||||
schOp (Cast CharType StringType) [x] = op "string" [x]
|
||||
schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x]
|
||||
schOp (Cast DoubleType IntegerType) [x] = op "exact-floor" [x]
|
||||
schOp (Cast DoubleType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast IntType CharType) [x] = op "cast-int-char" [x]
|
||||
schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x]
|
||||
schOp (Cast IntType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x]
|
||||
schOp (Cast IntegerType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]
|
||||
schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
|
||||
schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]
|
||||
schOp (Cast from to) [x] = castInt from to x
|
||||
schOp (Cast DoubleType StringType) [x] = pure $ op "number->string" [x]
|
||||
schOp (Cast CharType StringType) [x] = pure $ op "string" [x]
|
||||
schOp (Cast StringType DoubleType) [x] = pure $ op "cast-string-double" [x]
|
||||
|
||||
schOp BelieveMe [_,_,x] = x
|
||||
schOp Crash [_,msg] = "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))"
|
||||
schOp (Cast from to) [x] = castInt constPrimitives from to x
|
||||
|
||||
schOp BelieveMe [_,_,x] = pure x
|
||||
schOp Crash [_,msg] = pure $ "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))"
|
||||
|
||||
||| Extended primitives for the scheme backend, outside the standard set of primFn
|
||||
public export
|
||||
@ -236,6 +242,10 @@ mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- M
|
||||
|
||||
schConstant : (String -> String) -> Constant -> String
|
||||
schConstant _ (I x) = show x
|
||||
schConstant _ (I8 x) = show x
|
||||
schConstant _ (I16 x) = show x
|
||||
schConstant _ (I32 x) = show x
|
||||
schConstant _ (I64 x) = show x
|
||||
schConstant _ (BI x) = show x
|
||||
schConstant _ (B8 x) = show x
|
||||
schConstant _ (B16 x) = show x
|
||||
@ -249,6 +259,10 @@ schConstant _ (Ch x)
|
||||
schConstant _ (Db x) = show x
|
||||
schConstant _ WorldVal = "#f"
|
||||
schConstant _ IntType = "#t"
|
||||
schConstant _ Int8Type = "#t"
|
||||
schConstant _ Int16Type = "#t"
|
||||
schConstant _ Int32Type = "#t"
|
||||
schConstant _ Int64Type = "#t"
|
||||
schConstant _ IntegerType = "#t"
|
||||
schConstant _ Bits8Type = "#t"
|
||||
schConstant _ Bits16Type = "#t"
|
||||
@ -354,7 +368,7 @@ parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
|
||||
schExp i (NmCon fc x tag args)
|
||||
= pure $ schConstructor schString x tag !(traverse (schExp i) args)
|
||||
schExp i (NmOp fc op args)
|
||||
= pure $ schOp op !(schArgs i args)
|
||||
= schOp op !(schArgs i args)
|
||||
schExp i (NmExtPrim fc p args)
|
||||
= schExtPrim i (toPrim p) args
|
||||
schExp i (NmForce fc lr t) = pure $ "(" ++ !(schExp i t) ++ ")"
|
||||
|
||||
@ -102,6 +102,10 @@ mutual
|
||||
|
||||
chkConstant : FC -> Constant -> Term vars
|
||||
chkConstant fc (I x) = PrimVal fc IntType
|
||||
chkConstant fc (I8 x) = PrimVal fc Int8Type
|
||||
chkConstant fc (I16 x) = PrimVal fc Int16Type
|
||||
chkConstant fc (I32 x) = PrimVal fc Int32Type
|
||||
chkConstant fc (I64 x) = PrimVal fc Int64Type
|
||||
chkConstant fc (BI x) = PrimVal fc IntegerType
|
||||
chkConstant fc (B8 x) = PrimVal fc Bits8Type
|
||||
chkConstant fc (B16 x) = PrimVal fc Bits16Type
|
||||
|
||||
@ -32,6 +32,10 @@ unaryOp _ _ = Nothing
|
||||
|
||||
castString : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castString [NPrimVal fc (I i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (BI i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
@ -43,6 +47,10 @@ 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 (I16 i)] = Just (NPrimVal fc (BI i))
|
||||
castInteger [NPrimVal fc (I32 i)] = Just (NPrimVal fc (BI i))
|
||||
castInteger [NPrimVal fc (I64 i)] = Just (NPrimVal fc (BI 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)))
|
||||
@ -53,6 +61,10 @@ 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 (I16 i)] = Just (NPrimVal fc (I (fromInteger i)))
|
||||
castInt [NPrimVal fc (I32 i)] = Just (NPrimVal fc (I (fromInteger i)))
|
||||
castInt [NPrimVal fc (I64 i)] = Just (NPrimVal fc (I (fromInteger i)))
|
||||
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))
|
||||
@ -81,8 +93,42 @@ bitCastWrap i max
|
||||
then i `mod` max
|
||||
else max + i `mod` max
|
||||
|
||||
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
|
||||
= if i < negate max || i >= max
|
||||
then i `mod` max
|
||||
else i
|
||||
|
||||
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 (I16 i) = Just i
|
||||
constantIntegerValue (I32 i) = Just i
|
||||
constantIntegerValue (I64 i) = Just i
|
||||
constantIntegerValue (BI i) = Just i
|
||||
constantIntegerValue (B8 i) = Just $ cast i
|
||||
constantIntegerValue (B16 i) = Just $ cast i
|
||||
@ -118,8 +164,40 @@ castBits64 [NPrimVal fc constant] = do
|
||||
pure (NPrimVal fc (B64 wrapped))
|
||||
castBits64 _ = Nothing
|
||||
|
||||
castInt8 : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castInt8 [NPrimVal fc constant] = do
|
||||
value <- 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
|
||||
value <- 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
|
||||
value <- 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
|
||||
value <- constantIntegerValue constant
|
||||
let wrapped = int64CastWrap value
|
||||
pure (NPrimVal fc (I64 wrapped))
|
||||
castInt64 _ = Nothing
|
||||
|
||||
castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castDouble [NPrimVal fc (I i)] = Just (NPrimVal fc (Db (cast i)))
|
||||
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 (BI i)] = Just (NPrimVal fc (Db (cast i)))
|
||||
castDouble [NPrimVal fc (Str i)] = Just (NPrimVal fc (Db (cast i)))
|
||||
castDouble _ = Nothing
|
||||
@ -175,6 +253,10 @@ 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 (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x + y)
|
||||
add (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x + y)
|
||||
add (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ x + y)
|
||||
add (B8 x) (B8 y) = pure $ B8 $ (x + y) `mod` b8max
|
||||
add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` b16max
|
||||
add (B32 x) (B32 y) = pure $ B32 $ (x + y) `mod` b32max
|
||||
@ -186,6 +268,10 @@ 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 (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x - y)
|
||||
sub (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x - y)
|
||||
sub (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ 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
|
||||
@ -197,6 +283,10 @@ mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` b16max
|
||||
mul (B32 x) (B32 y) = pure $ B32 $ (x * y) `mod` b32max
|
||||
mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` b64max
|
||||
mul (I x) (I y) = pure $ I (x * y)
|
||||
mul (I8 x) (I8 y) = pure $ I8 (int8CastWrap $ x * y)
|
||||
mul (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x * y)
|
||||
mul (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x * y)
|
||||
mul (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ x * y)
|
||||
mul (Db x) (Db y) = pure $ Db (x * y)
|
||||
mul _ _ = Nothing
|
||||
|
||||
@ -205,6 +295,14 @@ div (BI x) (BI 0) = Nothing
|
||||
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 (I16 x) (I16 0) = Nothing
|
||||
div (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ 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 (I64 x) (I64 0) = Nothing
|
||||
div (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ assert_total (x `div` y))
|
||||
div (Db x) (Db y) = pure $ Db (x / y)
|
||||
div _ _ = Nothing
|
||||
|
||||
@ -213,10 +311,33 @@ mod (BI x) (BI 0) = Nothing
|
||||
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 (I16 x) (I16 0) = Nothing
|
||||
mod (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ 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 (I64 x) (I64 0) = Nothing
|
||||
mod (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ 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 (I16 x) (I16 y) = pure $ I16 (signedShift (prim__shl_Integer x y) int16max)
|
||||
shiftl (I32 x) (I32 y) = pure $ I32 (signedShift (prim__shl_Integer x y) int32max)
|
||||
shiftl (I64 x) (I64 y) = pure $ I64 (signedShift (prim__shl_Integer x y) int64max)
|
||||
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 (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` b16max
|
||||
@ -226,7 +347,10 @@ shiftl _ _ = Nothing
|
||||
|
||||
shiftr : Constant -> Constant -> Maybe Constant
|
||||
shiftr (I x) (I y) = pure $ I (prim__shr_Int x y)
|
||||
shiftr (BI x) (BI y) = pure $ BI (prim__shr_Integer x y)
|
||||
shiftr (I8 x) (I8 y) = pure $ I8 (signedShift (prim__shr_Integer x y) int8max)
|
||||
shiftr (I16 x) (I16 y) = pure $ I16 (signedShift (prim__shr_Integer x y) int16max)
|
||||
shiftr (I32 x) (I32 y) = pure $ I32 (signedShift (prim__shr_Integer x y) int32max)
|
||||
shiftr (I64 x) (I64 y) = pure $ I64 (signedShift (prim__shr_Integer x y) int64max)
|
||||
shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Int x y)
|
||||
shiftr (B16 x) (B16 y) = pure $ B16 $ (prim__shr_Int x y)
|
||||
shiftr (B32 x) (B32 y) = pure $ B32 $ (prim__shr_Int x y)
|
||||
@ -235,6 +359,10 @@ 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 (I16 x) (I16 y) = pure $ I16 (prim__and_Integer x y)
|
||||
band (I32 x) (I32 y) = pure $ I32 (prim__and_Integer x y)
|
||||
band (I64 x) (I64 y) = pure $ I64 (prim__and_Integer 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 (B16 x) (B16 y) = pure $ B16 (prim__and_Int x y)
|
||||
@ -244,6 +372,10 @@ 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 (I16 x) (I16 y) = pure $ I16 (prim__or_Integer x y)
|
||||
bor (I32 x) (I32 y) = pure $ I32 (prim__or_Integer x y)
|
||||
bor (I64 x) (I64 y) = pure $ I64 (prim__or_Integer 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 (B16 x) (B16 y) = pure $ B16 (prim__or_Int x y)
|
||||
@ -251,6 +383,8 @@ bor (B32 x) (B32 y) = pure $ B32 (prim__or_Int x y)
|
||||
bor (B64 x) (B64 y) = pure $ B64 (prim__or_Integer x y)
|
||||
bor _ _ = Nothing
|
||||
|
||||
-- TODO: Add implementations for
|
||||
-- Bits64, Integer, Int8, Int16, Int32, and Int64
|
||||
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)
|
||||
@ -261,6 +395,10 @@ 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 (I16 x) = pure . I16 $ int16CastWrap (-x)
|
||||
neg (I32 x) = pure . I32 $ int32CastWrap (-x)
|
||||
neg (I64 x) = pure . I64 $ int64CastWrap (-x)
|
||||
neg (Db x) = pure $ Db (-x)
|
||||
neg _ = Nothing
|
||||
|
||||
@ -270,6 +408,10 @@ toInt False = I 0
|
||||
|
||||
lt : Constant -> Constant -> Maybe Constant
|
||||
lt (I x) (I y) = pure $ toInt (x < y)
|
||||
lt (I8 x) (I8 y) = pure $ toInt (x < y)
|
||||
lt (I16 x) (I16 y) = pure $ toInt (x < y)
|
||||
lt (I32 x) (I32 y) = pure $ toInt (x < y)
|
||||
lt (I64 x) (I64 y) = pure $ toInt (x < y)
|
||||
lt (BI x) (BI y) = pure $ toInt (x < y)
|
||||
lt (B8 x) (B8 y) = pure $ toInt (x < y)
|
||||
lt (B16 x) (B16 y) = pure $ toInt (x < y)
|
||||
@ -282,6 +424,10 @@ lt _ _ = Nothing
|
||||
|
||||
lte : Constant -> Constant -> Maybe Constant
|
||||
lte (I x) (I y) = pure $ toInt (x <= y)
|
||||
lte (I8 x) (I8 y) = pure $ toInt (x <= y)
|
||||
lte (I16 x) (I16 y) = pure $ toInt (x <= y)
|
||||
lte (I32 x) (I32 y) = pure $ toInt (x <= y)
|
||||
lte (I64 x) (I64 y) = pure $ toInt (x <= y)
|
||||
lte (BI x) (BI y) = pure $ toInt (x <= y)
|
||||
lte (B8 x) (B8 y) = pure $ toInt (x <= y)
|
||||
lte (B16 x) (B16 y) = pure $ toInt (x <= y)
|
||||
@ -294,6 +440,10 @@ lte _ _ = Nothing
|
||||
|
||||
eq : Constant -> Constant -> Maybe Constant
|
||||
eq (I x) (I y) = pure $ toInt (x == y)
|
||||
eq (I8 x) (I8 y) = pure $ toInt (x == y)
|
||||
eq (I16 x) (I16 y) = pure $ toInt (x == y)
|
||||
eq (I32 x) (I32 y) = pure $ toInt (x == y)
|
||||
eq (I64 x) (I64 y) = pure $ toInt (x == y)
|
||||
eq (BI x) (BI y) = pure $ toInt (x == y)
|
||||
eq (B8 x) (B8 y) = pure $ toInt (x == y)
|
||||
eq (B16 x) (B16 y) = pure $ toInt (x == y)
|
||||
@ -306,6 +456,10 @@ eq _ _ = Nothing
|
||||
|
||||
gte : Constant -> Constant -> Maybe Constant
|
||||
gte (I x) (I y) = pure $ toInt (x >= y)
|
||||
gte (I8 x) (I8 y) = pure $ toInt (x >= y)
|
||||
gte (I16 x) (I16 y) = pure $ toInt (x >= y)
|
||||
gte (I32 x) (I32 y) = pure $ toInt (x >= y)
|
||||
gte (I64 x) (I64 y) = pure $ toInt (x >= y)
|
||||
gte (BI x) (BI y) = pure $ toInt (x >= y)
|
||||
gte (B8 x) (B8 y) = pure $ toInt (x >= y)
|
||||
gte (B16 x) (B16 y) = pure $ toInt (x >= y)
|
||||
@ -318,6 +472,10 @@ gte _ _ = Nothing
|
||||
|
||||
gt : Constant -> Constant -> Maybe Constant
|
||||
gt (I x) (I y) = pure $ toInt (x > y)
|
||||
gt (I8 x) (I8 y) = pure $ toInt (x > y)
|
||||
gt (I16 x) (I16 y) = pure $ toInt (x > y)
|
||||
gt (I32 x) (I32 y) = pure $ toInt (x > y)
|
||||
gt (I64 x) (I64 y) = pure $ toInt (x > y)
|
||||
gt (BI x) (BI y) = pure $ toInt (x > y)
|
||||
gt (B8 x) (B8 y) = pure $ toInt (x > y)
|
||||
gt (B16 x) (B16 y) = pure $ toInt (x > y)
|
||||
@ -413,6 +571,10 @@ crashTy
|
||||
|
||||
castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castTo IntType = castInt
|
||||
castTo Int8Type = castInt8
|
||||
castTo Int16Type = castInt16
|
||||
castTo Int32Type = castInt32
|
||||
castTo Int64Type = castInt64
|
||||
castTo IntegerType = castInteger
|
||||
castTo Bits8Type = castBits8
|
||||
castTo Bits16Type = castBits16
|
||||
@ -515,27 +677,46 @@ opName (Cast x y) = prim $ "cast_" ++ show x ++ show y
|
||||
opName BelieveMe = prim $ "believe_me"
|
||||
opName Crash = prim $ "crash"
|
||||
|
||||
integralTypes : List Constant
|
||||
integralTypes = [ IntType
|
||||
, Int8Type
|
||||
, Int16Type
|
||||
, Int32Type
|
||||
, Int64Type
|
||||
, IntegerType
|
||||
, Bits8Type
|
||||
, Bits16Type
|
||||
, Bits32Type
|
||||
, Bits64Type
|
||||
]
|
||||
|
||||
numTypes : List Constant
|
||||
numTypes = integralTypes ++ [DoubleType]
|
||||
|
||||
primTypes : List Constant
|
||||
primTypes = numTypes ++ [StringType, CharType]
|
||||
|
||||
export
|
||||
allPrimitives : List Prim
|
||||
allPrimitives =
|
||||
map (\t => MkPrim (Add t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Sub t) (arithTy t) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Mul t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, DoubleType] ++
|
||||
map (\t => MkPrim (Div t) (arithTy t) notCovering) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, DoubleType] ++
|
||||
map (\t => MkPrim (Mod t) (arithTy t) notCovering) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (Neg t) (predTy t t) isTotal) [IntType, IntegerType, DoubleType] ++
|
||||
map (\t => MkPrim (ShiftL t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (ShiftR t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (Add t) (arithTy t) isTotal) numTypes ++
|
||||
map (\t => MkPrim (Sub t) (arithTy t) isTotal) numTypes ++
|
||||
map (\t => MkPrim (Mul t) (arithTy t) isTotal) numTypes ++
|
||||
map (\t => MkPrim (Neg t) (predTy t t) isTotal) numTypes ++
|
||||
map (\t => MkPrim (Div t) (arithTy t) notCovering) numTypes ++
|
||||
map (\t => MkPrim (Mod t) (arithTy t) notCovering) integralTypes ++
|
||||
|
||||
map (\t => MkPrim (BAnd t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (BOr t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (ShiftL t) (arithTy t) isTotal) integralTypes ++
|
||||
map (\t => MkPrim (ShiftR t) (arithTy t) isTotal) integralTypes ++
|
||||
map (\t => MkPrim (BAnd t) (arithTy t) isTotal) integralTypes ++
|
||||
map (\t => MkPrim (BOr t) (arithTy t) isTotal) integralTypes ++
|
||||
map (\t => MkPrim (BXOr t) (arithTy t) isTotal) integralTypes ++
|
||||
|
||||
map (\t => MkPrim (LT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (LTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (EQ t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (GTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (GT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
map (\t => MkPrim (LT t) (cmpTy t) isTotal) primTypes ++
|
||||
map (\t => MkPrim (LTE t) (cmpTy t) isTotal) primTypes ++
|
||||
map (\t => MkPrim (EQ t) (cmpTy t) isTotal) primTypes ++
|
||||
map (\t => MkPrim (GTE t) (cmpTy t) isTotal) primTypes ++
|
||||
map (\t => MkPrim (GT t) (cmpTy t) isTotal) primTypes ++
|
||||
|
||||
[MkPrim StrLength (predTy StringType IntType) isTotal,
|
||||
MkPrim StrHead (predTy StringType CharType) notCovering,
|
||||
@ -560,13 +741,13 @@ allPrimitives =
|
||||
MkPrim DoubleFloor doubleTy isTotal,
|
||||
MkPrim DoubleCeiling doubleTy isTotal] ++
|
||||
|
||||
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, 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) [IntType, IntegerType, Bits16Type, Bits32Type, Bits64Type] ++
|
||||
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) [IntType, IntegerType, Bits8Type, Bits16Type, Bits64Type] ++
|
||||
map (\t => MkPrim (Cast t Bits64Type) (predTy t Bits64Type) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type]
|
||||
-- support all combinations of primitive casts with the following
|
||||
-- exceptions: String -> Char, Double -> Char, Char -> Double
|
||||
[ MkPrim (Cast t1 t2) (predTy t1 t2) isTotal
|
||||
| t1 <- primTypes
|
||||
, t2 <- primTypes
|
||||
, t1 /= t2 &&
|
||||
(t1,t2) /= (StringType,CharType) &&
|
||||
(t1,t2) /= (DoubleType,CharType) &&
|
||||
(t1,t2) /= (CharType,DoubleType)
|
||||
]
|
||||
|
||||
@ -341,6 +341,18 @@ Reify Constant where
|
||||
(NS _ (UN "I"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (I x')
|
||||
(NS _ (UN "I8"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (I8 x')
|
||||
(NS _ (UN "I16"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (I16 x')
|
||||
(NS _ (UN "I32"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (I32 x')
|
||||
(NS _ (UN "I64"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (I64 x')
|
||||
(NS _ (UN "BI"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (BI x')
|
||||
@ -369,6 +381,14 @@ Reify Constant where
|
||||
=> pure WorldVal
|
||||
(NS _ (UN "IntType"), [])
|
||||
=> pure IntType
|
||||
(NS _ (UN "Int8Type"), [])
|
||||
=> pure Int8Type
|
||||
(NS _ (UN "Int16Type"), [])
|
||||
=> pure Int16Type
|
||||
(NS _ (UN "Int32Type"), [])
|
||||
=> pure Int32Type
|
||||
(NS _ (UN "Int64Type"), [])
|
||||
=> pure Int64Type
|
||||
(NS _ (UN "IntegerType"), [])
|
||||
=> pure IntegerType
|
||||
(NS _ (UN "Bits8Type"), [])
|
||||
@ -395,6 +415,18 @@ Reflect Constant where
|
||||
reflect fc defs lhs env (I x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "I") [x']
|
||||
reflect fc defs lhs env (I8 x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "I8") [x']
|
||||
reflect fc defs lhs env (I16 x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "I16") [x']
|
||||
reflect fc defs lhs env (I32 x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "I32") [x']
|
||||
reflect fc defs lhs env (I64 x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "I64") [x']
|
||||
reflect fc defs lhs env (BI x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "BI") [x']
|
||||
@ -423,6 +455,14 @@ Reflect Constant where
|
||||
= getCon fc defs (reflectiontt "WorldVal")
|
||||
reflect fc defs lhs env IntType
|
||||
= getCon fc defs (reflectiontt "IntType")
|
||||
reflect fc defs lhs env Int8Type
|
||||
= getCon fc defs (reflectiontt "Int8Type")
|
||||
reflect fc defs lhs env Int16Type
|
||||
= getCon fc defs (reflectiontt "Int16Type")
|
||||
reflect fc defs lhs env Int32Type
|
||||
= getCon fc defs (reflectiontt "Int32Type")
|
||||
reflect fc defs lhs env Int64Type
|
||||
= getCon fc defs (reflectiontt "Int64Type")
|
||||
reflect fc defs lhs env IntegerType
|
||||
= getCon fc defs (reflectiontt "IntegerType")
|
||||
reflect fc defs lhs env Bits8Type
|
||||
|
||||
@ -32,6 +32,10 @@ isCon _ = Nothing
|
||||
public export
|
||||
data Constant
|
||||
= I Int
|
||||
| I8 Integer -- reuse code from I64 with fewer casts
|
||||
| I16 Integer
|
||||
| I32 Integer
|
||||
| I64 Integer
|
||||
| BI Integer
|
||||
| B8 Int -- For now, since we don't have Bits types. We need to
|
||||
-- make sure the Integer remains in range
|
||||
@ -44,6 +48,10 @@ data Constant
|
||||
| WorldVal
|
||||
|
||||
| IntType
|
||||
| Int8Type
|
||||
| Int16Type
|
||||
| Int32Type
|
||||
| Int64Type
|
||||
| IntegerType
|
||||
| Bits8Type
|
||||
| Bits16Type
|
||||
@ -58,6 +66,10 @@ export
|
||||
isConstantType : Name -> Maybe Constant
|
||||
isConstantType (UN n) = case n of
|
||||
"Int" => Just IntType
|
||||
"Int8" => Just Int8Type
|
||||
"Int16" => Just Int16Type
|
||||
"Int32" => Just Int32Type
|
||||
"Int64" => Just Int64Type
|
||||
"Integer" => Just IntegerType
|
||||
"Bits8" => Just Bits8Type
|
||||
"Bits16" => Just Bits16Type
|
||||
@ -75,6 +87,18 @@ 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
|
||||
Yes Refl => Just Refl
|
||||
No contra => Nothing
|
||||
constantEq (I16 x) (I16 y) = case decEq x y of
|
||||
Yes Refl => Just Refl
|
||||
No contra => Nothing
|
||||
constantEq (I32 x) (I32 y) = case decEq x y of
|
||||
Yes Refl => Just Refl
|
||||
No contra => Nothing
|
||||
constantEq (I64 x) (I64 y) = case decEq x y of
|
||||
Yes Refl => Just Refl
|
||||
No contra => Nothing
|
||||
constantEq (BI x) (BI y) = case decEq x y of
|
||||
Yes Refl => Just Refl
|
||||
No contra => Nothing
|
||||
@ -87,6 +111,10 @@ constantEq (Ch x) (Ch y) = case decEq x y of
|
||||
constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
|
||||
constantEq WorldVal WorldVal = Just Refl
|
||||
constantEq IntType IntType = Just Refl
|
||||
constantEq Int8Type Int8Type = Just Refl
|
||||
constantEq Int16Type Int16Type = Just Refl
|
||||
constantEq Int32Type Int32Type = Just Refl
|
||||
constantEq Int64Type Int64Type = Just Refl
|
||||
constantEq IntegerType IntegerType = Just Refl
|
||||
constantEq StringType StringType = Just Refl
|
||||
constantEq CharType CharType = Just Refl
|
||||
@ -97,6 +125,10 @@ constantEq _ _ = Nothing
|
||||
export
|
||||
Show Constant where
|
||||
show (I x) = show x
|
||||
show (I8 x) = show x
|
||||
show (I16 x) = show x
|
||||
show (I32 x) = show x
|
||||
show (I64 x) = show x
|
||||
show (BI x) = show x
|
||||
show (B8 x) = show x
|
||||
show (B16 x) = show x
|
||||
@ -107,6 +139,10 @@ Show Constant where
|
||||
show (Db x) = show x
|
||||
show WorldVal = "%MkWorld"
|
||||
show IntType = "Int"
|
||||
show Int8Type = "Int8"
|
||||
show Int16Type = "Int16"
|
||||
show Int32Type = "Int32"
|
||||
show Int64Type = "Int64"
|
||||
show IntegerType = "Integer"
|
||||
show Bits8Type = "Bits8"
|
||||
show Bits16Type = "Bits16"
|
||||
@ -120,6 +156,10 @@ Show Constant where
|
||||
export
|
||||
Pretty Constant where
|
||||
pretty (I x) = pretty x
|
||||
pretty (I8 x) = pretty x
|
||||
pretty (I16 x) = pretty x
|
||||
pretty (I32 x) = pretty x
|
||||
pretty (I64 x) = pretty x
|
||||
pretty (BI x) = pretty x
|
||||
pretty (B8 x) = pretty x
|
||||
pretty (B16 x) = pretty x
|
||||
@ -130,6 +170,10 @@ Pretty Constant where
|
||||
pretty (Db x) = pretty x
|
||||
pretty WorldVal = pretty "%MkWorld"
|
||||
pretty IntType = pretty "Int"
|
||||
pretty Int8Type = pretty "Int8"
|
||||
pretty Int16Type = pretty "Int16"
|
||||
pretty Int32Type = pretty "Int32"
|
||||
pretty Int64Type = pretty "Int64"
|
||||
pretty IntegerType = pretty "Integer"
|
||||
pretty Bits8Type = pretty "Bits8"
|
||||
pretty Bits16Type = pretty "Bits16"
|
||||
@ -143,6 +187,10 @@ Pretty Constant where
|
||||
export
|
||||
Eq Constant where
|
||||
(I x) == (I y) = x == y
|
||||
(I8 x) == (I8 y) = x == y
|
||||
(I16 x) == (I16 y) = x == y
|
||||
(I32 x) == (I32 y) = x == y
|
||||
(I64 x) == (I64 y) = x == y
|
||||
(BI x) == (BI y) = x == y
|
||||
(B8 x) == (B8 y) = x == y
|
||||
(B16 x) == (B16 y) = x == y
|
||||
@ -153,6 +201,10 @@ Eq Constant where
|
||||
(Db x) == (Db y) = x == y
|
||||
WorldVal == WorldVal = True
|
||||
IntType == IntType = True
|
||||
Int8Type == Int8Type = True
|
||||
Int16Type == Int16Type = True
|
||||
Int32Type == Int32Type = True
|
||||
Int64Type == Int64Type = True
|
||||
IntegerType == IntegerType = True
|
||||
Bits8Type == Bits8Type = True
|
||||
Bits16Type == Bits16Type = True
|
||||
@ -178,6 +230,10 @@ constTag StringType = 9
|
||||
constTag CharType = 10
|
||||
constTag DoubleType = 11
|
||||
constTag WorldType = 12
|
||||
constTag Int8Type = 13
|
||||
constTag Int16Type = 14
|
||||
constTag Int32Type = 15
|
||||
constTag Int64Type = 16
|
||||
constTag _ = 0
|
||||
|
||||
||| Precision of integral types.
|
||||
@ -197,19 +253,30 @@ Ord Precision where
|
||||
compare Unlimited _ = GT
|
||||
compare _ Unlimited = LT
|
||||
|
||||
-- so far, we only support limited precision
|
||||
-- unsigned integers
|
||||
public export
|
||||
data IntKind = Signed Precision | Unsigned Precision
|
||||
data IntKind = Signed Precision | Unsigned Int
|
||||
|
||||
public export
|
||||
intKind : Constant -> Maybe IntKind
|
||||
intKind IntegerType = Just $ Signed Unlimited
|
||||
intKind Int8Type = Just . Signed $ P 8
|
||||
intKind Int16Type = Just . Signed $ P 16
|
||||
intKind Int32Type = Just . Signed $ P 32
|
||||
intKind Int64Type = Just . Signed $ P 64
|
||||
intKind IntType = Just . Signed $ P 64
|
||||
intKind Bits8Type = Just . Unsigned $ P 8
|
||||
intKind Bits16Type = Just . Unsigned $ P 16
|
||||
intKind Bits32Type = Just . Unsigned $ P 32
|
||||
intKind Bits64Type = Just . Unsigned $ P 64
|
||||
intKind Bits8Type = Just $ Unsigned 8
|
||||
intKind Bits16Type = Just $ Unsigned 16
|
||||
intKind Bits32Type = Just $ Unsigned 32
|
||||
intKind Bits64Type = Just $ Unsigned 64
|
||||
intKind _ = Nothing
|
||||
|
||||
public export
|
||||
precision : IntKind -> Precision
|
||||
precision (Signed p) = p
|
||||
precision (Unsigned p) = P p
|
||||
|
||||
-- All the internal operators, parameterised by their arity
|
||||
public export
|
||||
data PrimFn : Nat -> Type where
|
||||
|
||||
@ -137,6 +137,15 @@ TTC Constant where
|
||||
toBuf b DoubleType = tag 18
|
||||
toBuf b WorldType = tag 19
|
||||
|
||||
toBuf b (I32 x) = do tag 20; toBuf b x
|
||||
toBuf b (I64 x) = do tag 21; toBuf b x
|
||||
toBuf b Int32Type = tag 22
|
||||
toBuf b Int64Type = tag 23
|
||||
toBuf b (I8 x) = do tag 24; toBuf b x
|
||||
toBuf b (I16 x) = do tag 25; toBuf b x
|
||||
toBuf b Int8Type = tag 26
|
||||
toBuf b Int16Type = tag 27
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
0 => do x <- fromBuf b; pure (I x)
|
||||
@ -159,6 +168,14 @@ TTC Constant where
|
||||
17 => pure CharType
|
||||
18 => pure DoubleType
|
||||
19 => pure WorldType
|
||||
20 => do x <- fromBuf b; pure (I32 x)
|
||||
21 => do x <- fromBuf b; pure (I64 x)
|
||||
22 => pure Int32Type
|
||||
23 => pure Int64Type
|
||||
24 => do x <- fromBuf b; pure (I8 x)
|
||||
25 => do x <- fromBuf b; pure (I16 x)
|
||||
26 => pure Int8Type
|
||||
27 => pure Int16Type
|
||||
_ => corrupt "Constant"
|
||||
|
||||
export
|
||||
|
||||
@ -9,6 +9,8 @@ import Core.Options
|
||||
import Core.TT
|
||||
import Core.Unify
|
||||
|
||||
import Data.Maybe
|
||||
|
||||
import Libraries.Data.List.Extra
|
||||
import Libraries.Data.StringMap
|
||||
import Libraries.Data.String.Extra
|
||||
@ -578,11 +580,33 @@ mutual
|
||||
= do l' <- desugarTree side ps l
|
||||
r' <- desugarTree side ps r
|
||||
pure (IApp loc (IApp loc (IVar loc op) l') r')
|
||||
|
||||
-- negation is a special case, since we can't have an operator with
|
||||
-- two meanings otherwise
|
||||
--
|
||||
-- Note: In case of negated signed integer literals, we apply the
|
||||
-- negation directly. Otherwise, the literal might be
|
||||
-- truncated to 0 before being passed on to `negate`.
|
||||
desugarTree side ps (Pre loc (UN "-") $ Leaf $ PPrimVal fc c)
|
||||
= let newFC = fromMaybe EmptyFC (mergeFC loc fc)
|
||||
continue = desugarTree side ps . Leaf . PPrimVal newFC
|
||||
in case c of
|
||||
I x => continue $ I (-x)
|
||||
I8 x => continue $ I8 (-x)
|
||||
I16 x => continue $ I16 (-x)
|
||||
I32 x => continue $ I32 (-x)
|
||||
I64 x => continue $ I64 (-x)
|
||||
BI x => continue $ BI (-x)
|
||||
|
||||
-- not a signed integer literal. proceed by desugaring
|
||||
-- and applying to `negate`.
|
||||
_ => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c)
|
||||
pure (IApp loc (IVar loc (UN "negate")) arg')
|
||||
|
||||
desugarTree side ps (Pre loc (UN "-") arg)
|
||||
= do arg' <- desugarTree side ps arg
|
||||
pure (IApp loc (IVar loc (UN "negate")) arg')
|
||||
= do arg' <- desugarTree side ps arg
|
||||
pure (IApp loc (IVar loc (UN "negate")) arg')
|
||||
|
||||
desugarTree side ps (Pre loc op arg)
|
||||
= do arg' <- desugarTree side ps arg
|
||||
pure (IApp loc (IVar loc op) arg')
|
||||
|
||||
@ -232,4 +232,3 @@ equivTypes ty1 ty2 =
|
||||
(\err => pure False)
|
||||
when b $ logTerm "typesearch.equiv" 20 "Accepted: " ty1
|
||||
pure b
|
||||
|
||||
|
||||
@ -43,15 +43,9 @@ constant
|
||||
Just c' => Just (Ch c')
|
||||
DoubleLit d => Just (Db d)
|
||||
IntegerLit i => Just (BI i)
|
||||
Ident "Char" => Just CharType
|
||||
Ident "Double" => Just DoubleType
|
||||
Ident "Int" => Just IntType
|
||||
Ident "Integer" => Just IntegerType
|
||||
Ident "Bits8" => Just Bits8Type
|
||||
Ident "Bits16" => Just Bits16Type
|
||||
Ident "Bits32" => Just Bits32Type
|
||||
Ident "Bits64" => Just Bits64Type
|
||||
Ident "String" => Just StringType
|
||||
Ident s => isConstantType (UN s) >>=
|
||||
\case WorldType => Nothing
|
||||
c => Just c
|
||||
_ => Nothing)
|
||||
|
||||
documentation' : Rule String
|
||||
@ -250,8 +244,10 @@ holeName
|
||||
|
||||
reservedNames : List String
|
||||
reservedNames
|
||||
= ["Type", "Int", "Integer", "Bits8", "Bits16", "Bits32", "Bits64",
|
||||
"String", "Char", "Double", "Lazy", "Inf", "Force", "Delay"]
|
||||
= [ "Type", "Int", "Int8", "Int16", "Int32", "Int64", "Integer"
|
||||
, "Bits8", "Bits16", "Bits32", "Bits64"
|
||||
, "String", "Char", "Double", "Lazy", "Inf", "Force", "Delay"
|
||||
]
|
||||
|
||||
isNotReservedIdent : WithBounds String -> SourceEmptyRule ()
|
||||
isNotReservedIdent x
|
||||
|
||||
@ -7,6 +7,10 @@ import Core.TT
|
||||
export
|
||||
checkPrim : FC -> Constant -> (Term vars, Term vars)
|
||||
checkPrim fc (I i) = (PrimVal fc (I i), PrimVal fc IntType)
|
||||
checkPrim fc (I8 i) = (PrimVal fc (I8 i), PrimVal fc Int8Type)
|
||||
checkPrim fc (I16 i) = (PrimVal fc (I16 i), PrimVal fc Int16Type)
|
||||
checkPrim fc (I32 i) = (PrimVal fc (I32 i), PrimVal fc Int32Type)
|
||||
checkPrim fc (I64 i) = (PrimVal fc (I64 i), PrimVal fc Int64Type)
|
||||
checkPrim fc (BI i) = (PrimVal fc (BI i), PrimVal fc IntegerType)
|
||||
checkPrim fc (B8 i) = (PrimVal fc (B8 i), PrimVal fc Bits8Type)
|
||||
checkPrim fc (B16 i) = (PrimVal fc (B16 i), PrimVal fc Bits16Type)
|
||||
@ -18,6 +22,10 @@ checkPrim fc (Db d) = (PrimVal fc (Db d), PrimVal fc DoubleType)
|
||||
checkPrim fc WorldVal = (PrimVal fc WorldVal, PrimVal fc WorldType)
|
||||
|
||||
checkPrim fc IntType = (PrimVal fc IntType, TType fc)
|
||||
checkPrim fc Int8Type = (PrimVal fc Int8Type, TType fc)
|
||||
checkPrim fc Int16Type = (PrimVal fc Int16Type, TType fc)
|
||||
checkPrim fc Int32Type = (PrimVal fc Int32Type, TType fc)
|
||||
checkPrim fc Int64Type = (PrimVal fc Int64Type, TType fc)
|
||||
checkPrim fc IntegerType = (PrimVal fc IntegerType, TType fc)
|
||||
checkPrim fc Bits8Type = (PrimVal fc Bits8Type, TType fc)
|
||||
checkPrim fc Bits16Type = (PrimVal fc Bits16Type, TType fc)
|
||||
|
||||
@ -13,14 +13,34 @@
|
||||
((0) '())
|
||||
((1) (cons (vector-ref desc 2)
|
||||
(blodwen-read-args (vector-ref desc 3)))))))
|
||||
|
||||
(define blodwen-toSignedInt
|
||||
(lambda (x bits)
|
||||
(let ((ma (ash 1 bits)))
|
||||
(if (or (< x (- 0 ma))
|
||||
(>= x ma))
|
||||
(remainder x ma)
|
||||
x))))
|
||||
|
||||
(define blodwen-toUnsignedInt
|
||||
(lambda (x bits)
|
||||
(modulo x (ash 1 bits))))
|
||||
|
||||
(define bu+ (lambda (x y bits) (blodwen-toUnsignedInt (+ x y) bits)))
|
||||
(define bu- (lambda (x y bits) (blodwen-toUnsignedInt (- x y) bits)))
|
||||
(define bu* (lambda (x y bits) (blodwen-toUnsignedInt (* x y) bits)))
|
||||
(define bu/ (lambda (x y bits) (blodwen-toUnsignedInt (quotient x y) bits)))
|
||||
|
||||
(define bs+ (lambda (x y bits) (blodwen-toSignedInt (+ x y) bits)))
|
||||
(define bs- (lambda (x y bits) (blodwen-toSignedInt (- x y) bits)))
|
||||
(define bs* (lambda (x y bits) (blodwen-toSignedInt (* x y) bits)))
|
||||
(define bs/ (lambda (x y bits) (blodwen-toSignedInt (quotient x y) bits)))
|
||||
|
||||
(define b+ (lambda (x y bits) (remainder (+ x y) (ash 1 bits))))
|
||||
(define b- (lambda (x y bits) (remainder (- x y) (ash 1 bits))))
|
||||
(define b* (lambda (x y bits) (remainder (* x y) (ash 1 bits))))
|
||||
(define b/ (lambda (x y bits) (remainder (exact-floor (/ x y)) (ash 1 bits))))
|
||||
|
||||
(define blodwen-toSignedInt (lambda (x y) (modulo x (expt 2 y))))
|
||||
(define blodwen-toUnsignedInt (lambda (x y) (modulo x (expt 2 y))))
|
||||
|
||||
(define integer->bits8 (lambda (x) (modulo x (expt 2 8))))
|
||||
(define integer->bits16 (lambda (x) (modulo x (expt 2 16))))
|
||||
(define integer->bits32 (lambda (x) (modulo x (expt 2 32))))
|
||||
@ -42,6 +62,7 @@
|
||||
(define blodwen-bits-shl-signed (lambda (x y bits) (truncate-bits (ash x y) bits)))
|
||||
|
||||
(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))))
|
||||
(define blodwen-and (lambda (x y) (logand x y)))
|
||||
@ -57,18 +78,51 @@
|
||||
((equal? x "") "")
|
||||
((equal? (string-ref x 0) #\#) "")
|
||||
(else x))))
|
||||
|
||||
(define exact-floor
|
||||
(lambda (x)
|
||||
(inexact->exact (floor x))))
|
||||
|
||||
(define exact-truncate
|
||||
(lambda (x)
|
||||
(inexact->exact (truncate x))))
|
||||
|
||||
(define exact-truncate-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (exact-truncate x) y)))
|
||||
|
||||
(define exact-truncate-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (exact-truncate x) y)))
|
||||
|
||||
(define cast-char-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (char->integer x) y)))
|
||||
|
||||
(define cast-char-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (char->integer x) y)))
|
||||
|
||||
(define cast-string-int
|
||||
(lambda (x)
|
||||
(exact-floor (cast-num (string->number (destroy-prefix x))))))
|
||||
(exact-truncate (cast-num (string->number (destroy-prefix x))))))
|
||||
|
||||
(define cast-string-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (cast-string-int x) y)))
|
||||
|
||||
(define cast-string-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (cast-string-int x) y)))
|
||||
|
||||
(define cast-int-char
|
||||
(lambda (x)
|
||||
(if (and (>= x 0)
|
||||
(<= x #x10ffff))
|
||||
(if (or
|
||||
(and (>= x 0) (<= x #xd7ff))
|
||||
(and (>= x #xe000) (<= x #x10ffff)))
|
||||
(integer->char x)
|
||||
0)))
|
||||
(integer->char 0))))
|
||||
|
||||
(define cast-string-double
|
||||
(lambda (x)
|
||||
(cast-num (string->number (destroy-prefix x)))))
|
||||
|
||||
@ -14,6 +14,28 @@
|
||||
(cons (vector-ref desc 2)
|
||||
(blodwen-read-args (vector-ref desc 3)))))
|
||||
|
||||
(define blodwen-toSignedInt
|
||||
(lambda (x bits)
|
||||
(let ((ma (arithmetic-shift 1 bits)))
|
||||
(if (or (< x (- 0 ma))
|
||||
(>= x ma))
|
||||
(remainder x ma)
|
||||
x))))
|
||||
|
||||
(define blodwen-toUnsignedInt
|
||||
(lambda (x bits)
|
||||
(modulo x (arithmetic-shift 1 bits))))
|
||||
|
||||
(define bu+ (lambda (x y bits) (blodwen-toUnsignedInt (+ x y) bits)))
|
||||
(define bu- (lambda (x y bits) (blodwen-toUnsignedInt (- x y) bits)))
|
||||
(define bu* (lambda (x y bits) (blodwen-toUnsignedInt (* x y) bits)))
|
||||
(define bu/ (lambda (x y bits) (blodwen-toUnsignedInt (quotient x y) bits)))
|
||||
|
||||
(define bs+ (lambda (x y bits) (blodwen-toSignedInt (+ x y) bits)))
|
||||
(define bs- (lambda (x y bits) (blodwen-toSignedInt (- x y) bits)))
|
||||
(define bs* (lambda (x y bits) (blodwen-toSignedInt (* x y) bits)))
|
||||
(define bs/ (lambda (x y bits) (blodwen-toSignedInt (quotient x y) bits)))
|
||||
|
||||
(define-macro (b+ x y bits)
|
||||
(if (exact-integer? bits)
|
||||
`(remainder (+ ,x ,y) ,(arithmetic-shift 1 bits))
|
||||
@ -31,9 +53,6 @@
|
||||
`(remainder (floor (/ ,x ,y)) ,(arithmetic-shift 1 bits))
|
||||
`(remainder (floor (/ ,x ,y)) (arithmetic-shift 1 ,bits))))
|
||||
|
||||
(define blodwen-toSignedInt (lambda (x y) (modulo x (expt 2 y))))
|
||||
(define blodwen-toUnsignedInt (lambda (x y) (modulo x (expt 2 y))))
|
||||
|
||||
(define integer->bits8 (lambda (x) (modulo x (expt 2 8))))
|
||||
(define integer->bits16 (lambda (x) (modulo x (expt 2 16))))
|
||||
(define integer->bits32 (lambda (x) (modulo x (expt 2 32))))
|
||||
@ -70,6 +89,34 @@
|
||||
`(let ((,s ,x))
|
||||
(if (flonum? ,s) (##flonum->exact-int ,s) (##floor ,s)))))
|
||||
|
||||
(define exact-truncate
|
||||
(lambda (x)
|
||||
(inexact->exact (truncate x))))
|
||||
|
||||
(define exact-truncate-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (exact-truncate x) y)))
|
||||
|
||||
(define exact-truncate-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (exact-truncate x) y)))
|
||||
|
||||
(define cast-char-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (char->integer x) y)))
|
||||
|
||||
(define cast-char-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (char->integer x) y)))
|
||||
|
||||
(define cast-string-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (cast-string-int x) y)))
|
||||
|
||||
(define cast-string-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (cast-string-int x) y)))
|
||||
|
||||
;; TODO Convert to macro
|
||||
(define (cast-string-double x)
|
||||
(define (cast-num x)
|
||||
@ -79,7 +126,7 @@
|
||||
(cast-num (string->number (destroy-prefix x))))
|
||||
|
||||
(define-macro (cast-string-int x)
|
||||
`(exact-floor (cast-string-double ,x)))
|
||||
`(exact-truncate (cast-string-double ,x)))
|
||||
|
||||
(define (from-idris-list xs)
|
||||
(if (= (vector-ref xs 0) 0)
|
||||
|
||||
@ -10,14 +10,34 @@
|
||||
((0) '())
|
||||
((1) (cons (vector-ref desc 2)
|
||||
(blodwen-read-args (vector-ref desc 3)))))))
|
||||
|
||||
(define blodwen-toSignedInt
|
||||
(lambda (x bits)
|
||||
(let ((ma (arithmetic-shift 1 bits)))
|
||||
(if (or (< x (- 0 ma))
|
||||
(>= x ma))
|
||||
(remainder x ma)
|
||||
x))))
|
||||
|
||||
(define blodwen-toUnsignedInt
|
||||
(lambda (x bits)
|
||||
(modulo x (arithmetic-shift 1 bits))))
|
||||
|
||||
(define bu+ (lambda (x y bits) (blodwen-toUnsignedInt (+ x y) bits)))
|
||||
(define bu- (lambda (x y bits) (blodwen-toUnsignedInt (- x y) bits)))
|
||||
(define bu* (lambda (x y bits) (blodwen-toUnsignedInt (* x y) bits)))
|
||||
(define bu/ (lambda (x y bits) (blodwen-toUnsignedInt (quotient x y) bits)))
|
||||
|
||||
(define bs+ (lambda (x y bits) (blodwen-toSignedInt (+ x y) bits)))
|
||||
(define bs- (lambda (x y bits) (blodwen-toSignedInt (- x y) bits)))
|
||||
(define bs* (lambda (x y bits) (blodwen-toSignedInt (* x y) bits)))
|
||||
(define bs/ (lambda (x y bits) (blodwen-toSignedInt (quotient x y) bits)))
|
||||
|
||||
(define b+ (lambda (x y bits) (remainder (+ x y) (arithmetic-shift 1 bits))))
|
||||
(define b- (lambda (x y bits) (remainder (- x y) (arithmetic-shift 1 bits))))
|
||||
(define b* (lambda (x y bits) (remainder (* x y) (arithmetic-shift 1 bits))))
|
||||
(define b/ (lambda (x y bits) (remainder (exact-floor (/ x y)) (arithmetic-shift 1 bits))))
|
||||
|
||||
(define blodwen-toSignedInt (lambda (x y) (modulo x (expt 2 y))))
|
||||
(define blodwen-toUnsignedInt (lambda (x y) (modulo x (expt 2 y))))
|
||||
|
||||
(define integer->bits8 (lambda (x) (modulo x (expt 2 8))))
|
||||
(define integer->bits16 (lambda (x) (modulo x (expt 2 16))))
|
||||
(define integer->bits32 (lambda (x) (modulo x (expt 2 32))))
|
||||
@ -37,6 +57,10 @@
|
||||
(define blodwen-or (lambda (x y) (bitwise-ior x y)))
|
||||
(define blodwen-xor (lambda (x y) (bitwise-xor x y)))
|
||||
|
||||
(define exact-floor
|
||||
(lambda (x)
|
||||
(inexact->exact (floor x))))
|
||||
|
||||
(define truncate-bits
|
||||
(lambda (x bits)
|
||||
(if (bitwise-bit-set? x bits)
|
||||
@ -46,6 +70,38 @@
|
||||
(define blodwen-bits-shl-signed
|
||||
(lambda (x y bits) (truncate-bits (arithmetic-shift x y) bits)))
|
||||
|
||||
(define exact-truncate
|
||||
(lambda (x)
|
||||
(inexact->exact (truncate x))))
|
||||
|
||||
(define exact-truncate-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (exact-truncate x) y)))
|
||||
|
||||
(define exact-truncate-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (exact-truncate x) y)))
|
||||
|
||||
(define cast-char-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (char->integer x) y)))
|
||||
|
||||
(define cast-char-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (char->integer x) y)))
|
||||
|
||||
(define cast-string-int
|
||||
(lambda (x)
|
||||
(exact-truncate (cast-num (string->number (destroy-prefix x))))))
|
||||
|
||||
(define cast-string-boundedInt
|
||||
(lambda (x y)
|
||||
(blodwen-toSignedInt (cast-string-int x) y)))
|
||||
|
||||
(define cast-string-boundedUInt
|
||||
(lambda (x y)
|
||||
(blodwen-toUnsignedInt (cast-string-int x) y)))
|
||||
|
||||
(define cast-num
|
||||
(lambda (x)
|
||||
(if (number? x) x 0)))
|
||||
@ -55,15 +111,15 @@
|
||||
((equal? x "") "")
|
||||
((equal? (string-ref x 0) #\#) "")
|
||||
(else x))))
|
||||
(define cast-string-int
|
||||
(lambda (x)
|
||||
(exact-floor (cast-num (string->number (destroy-prefix x))))))
|
||||
|
||||
(define cast-int-char
|
||||
(lambda (x)
|
||||
(if (and (>= x 0)
|
||||
(<= x #x10ffff))
|
||||
(if (or
|
||||
(and (>= x 0) (<= x #xd7ff))
|
||||
(and (>= x #xe000) (<= x #x10ffff)))
|
||||
(integer->char x)
|
||||
0)))
|
||||
(integer->char 0))))
|
||||
|
||||
(define cast-string-double
|
||||
(lambda (x)
|
||||
(cast-num (string->number (destroy-prefix x)))))
|
||||
|
||||
@ -202,6 +202,8 @@ chezTests = MkTestPool [Chez]
|
||||
, "chez025", "chez026", "chez027", "chez028", "chez029", "chez030"
|
||||
, "chez031", "chez032"
|
||||
, "futures001"
|
||||
, "casts"
|
||||
, "newints"
|
||||
, "semaphores001"
|
||||
, "semaphores002"
|
||||
, "perf001"
|
||||
@ -234,6 +236,8 @@ nodeTests = MkTestPool [Node]
|
||||
, "node017", "node018", "node019", "node021", "node022", "node023"
|
||||
, "node024", "node025"
|
||||
-- , "node14", "node020"
|
||||
, "casts"
|
||||
, "newints"
|
||||
, "reg001"
|
||||
, "syntax001"
|
||||
, "tailrec001"
|
||||
|
||||
690
tests/chez/casts/Casts.idr
Normal file
690
tests/chez/casts/Casts.idr
Normal file
@ -0,0 +1,690 @@
|
||||
--
|
||||
-- Primitive casts: Specification
|
||||
--
|
||||
-- a. Unsigned integers
|
||||
--
|
||||
-- Unsigned integers with a precision of x bit have a valid
|
||||
-- range of [0,2^x - 1]. When casting from another integral type of value y,
|
||||
-- the value is checked for being in bounds, and if it is not, the
|
||||
-- unsigned remainder modulo 2^x of y is returned.
|
||||
--
|
||||
-- When casting from a `Double`, the value is first truncated towards 0,
|
||||
-- before applying the inbounds check and (if necessary) calculating
|
||||
-- the unsigned remainder modulo 2^x.
|
||||
--
|
||||
-- When casting from a `String`, the value is first converted to a floating
|
||||
-- point number by the backend and then truncated as described above.
|
||||
--
|
||||
-- Example: For `Bits8` the valid range is [0,255]. Below are some
|
||||
-- example casts.
|
||||
--
|
||||
-- cast {from = Integer} {to = Bits8} 12 = 12
|
||||
-- cast {from = Integer} {to = Bits8} 256 = 0
|
||||
-- cast {from = Integer} {to = Bits8} 259 = 3
|
||||
-- cast {from = Integer} {to = Bits8} (-2) = 254
|
||||
-- cast {from = Double} {to = Bits8} (-12.001) = 244
|
||||
-- cast {from = Double} {to = Bits8} ("-12.001") = 244
|
||||
--
|
||||
-- b. Signed integers
|
||||
--
|
||||
-- Signed integers with a precision of x bit have a valid
|
||||
-- range of [-2^(x-1),2^(x-1) - 1]. When casting from another
|
||||
-- integral type of value y, the value is checked for being in bounds,
|
||||
-- and if it is not, the signed remainder modulo 2^(x-1) of y is returned.
|
||||
--
|
||||
-- When casting from a `Double`, the value is first truncated towards 0,
|
||||
-- before applying the inbounds check and (if necessary) calculating
|
||||
-- the signed remainder modulo 2^(x-1).
|
||||
--
|
||||
-- When casting from a `String`, the value is first converted to a floating
|
||||
-- point number by the backend and then truncated as described above.
|
||||
--
|
||||
-- Example: For `Int8` the valid range is [-128,127]. Below are some
|
||||
-- example casts.
|
||||
--
|
||||
-- cast {from = Integer} {to = Int8} 12 = 12
|
||||
-- cast {from = Integer} {to = Int8} 256 = 0
|
||||
-- cast {from = Integer} {to = Int8} 259 = 4
|
||||
-- cast {from = Integer} {to = Int8} (-128) = (-128)
|
||||
-- cast {from = Integer} {to = Int8} (-129) = (-1)
|
||||
-- cast {from = Double} {to = Int8} (-12.001) = (-12)
|
||||
-- cast {from = Double} {to = Int8} ("-12.001") = (-12)
|
||||
--
|
||||
-- b. Characters
|
||||
--
|
||||
-- Casts from all integral types to `Char` are supported. Note however,
|
||||
-- that only casts in the non-surrogate range are supported, that is
|
||||
-- values in the ranges [0,0xd7ff] and [0xe000,0x10ffff], or, in decimal
|
||||
-- notation, [0,55295] and [57344,1114111].
|
||||
--
|
||||
-- All casts from integer types to `Char` are therefore submitted to a
|
||||
-- bounds check, and, in case the value is out of bounds, are converted to `'\0'`.
|
||||
--
|
||||
--
|
||||
-- Test all casts from and to integral types.
|
||||
-- The `Cast` implementations in here should go to `Prelude`, once
|
||||
-- a new minor version of the compiler is released.
|
||||
--
|
||||
-- These tests verify also that the full range of integer literals
|
||||
-- is supported for every integral type.
|
||||
--
|
||||
-- Nothing fancy is being done here:
|
||||
-- All test cases have been hand-written.
|
||||
|
||||
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
|
||||
|
||||
Cast Int8 Bits8 where
|
||||
cast = prim__cast_Int8Bits8
|
||||
|
||||
Cast Int8 Bits16 where
|
||||
cast = prim__cast_Int8Bits16
|
||||
|
||||
Cast Int8 Bits32 where
|
||||
cast = prim__cast_Int8Bits32
|
||||
|
||||
Cast Int8 Bits64 where
|
||||
cast = prim__cast_Int8Bits64
|
||||
|
||||
Cast Int8 Int16 where
|
||||
cast = prim__cast_Int8Int16
|
||||
|
||||
Cast Int8 Int32 where
|
||||
cast = prim__cast_Int8Int32
|
||||
|
||||
Cast Int8 Int64 where
|
||||
cast = prim__cast_Int8Int64
|
||||
|
||||
Cast Int8 Int where
|
||||
cast = prim__cast_Int8Int
|
||||
|
||||
Cast Int8 Integer where
|
||||
cast = prim__cast_Int8Integer
|
||||
|
||||
Cast Int8 String where
|
||||
cast = prim__cast_Int8String
|
||||
|
||||
Cast Int8 Char where
|
||||
cast = prim__cast_Int8Char
|
||||
|
||||
Cast Int8 Double where
|
||||
cast = prim__cast_Int8Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export
|
||||
Eq Int16 where
|
||||
x == y = intToBool (prim__eq_Int16 x y)
|
||||
|
||||
Show Int16 where
|
||||
show = prim__cast_Int16String
|
||||
|
||||
Num Int16 where
|
||||
(+) = prim__add_Int16
|
||||
(*) = prim__mul_Int16
|
||||
fromInteger = prim__cast_IntegerInt16
|
||||
|
||||
Neg Int16 where
|
||||
(-) = prim__sub_Int16
|
||||
negate = prim__sub_Int16 0
|
||||
|
||||
Cast Int16 Bits8 where
|
||||
cast = prim__cast_Int16Bits8
|
||||
|
||||
Cast Int16 Bits16 where
|
||||
cast = prim__cast_Int16Bits16
|
||||
|
||||
Cast Int16 Bits32 where
|
||||
cast = prim__cast_Int16Bits32
|
||||
|
||||
Cast Int16 Bits64 where
|
||||
cast = prim__cast_Int16Bits64
|
||||
|
||||
Cast Int16 Int8 where
|
||||
cast = prim__cast_Int16Int8
|
||||
|
||||
Cast Int16 Int32 where
|
||||
cast = prim__cast_Int16Int32
|
||||
|
||||
Cast Int16 Int64 where
|
||||
cast = prim__cast_Int16Int64
|
||||
|
||||
Cast Int16 Int where
|
||||
cast = prim__cast_Int16Int
|
||||
|
||||
Cast Int16 Integer where
|
||||
cast = prim__cast_Int16Integer
|
||||
|
||||
Cast Int16 String where
|
||||
cast = prim__cast_Int16String
|
||||
|
||||
Cast Int16 Char where
|
||||
cast = prim__cast_Int16Char
|
||||
|
||||
Cast Int16 Double where
|
||||
cast = prim__cast_Int16Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- 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
|
||||
|
||||
Cast Int32 Bits8 where
|
||||
cast = prim__cast_Int32Bits8
|
||||
|
||||
Cast Int32 Bits16 where
|
||||
cast = prim__cast_Int32Bits16
|
||||
|
||||
Cast Int32 Bits32 where
|
||||
cast = prim__cast_Int32Bits32
|
||||
|
||||
Cast Int32 Bits64 where
|
||||
cast = prim__cast_Int32Bits64
|
||||
|
||||
Cast Int32 Int8 where
|
||||
cast = prim__cast_Int32Int8
|
||||
|
||||
Cast Int32 Int16 where
|
||||
cast = prim__cast_Int32Int16
|
||||
|
||||
Cast Int32 Int64 where
|
||||
cast = prim__cast_Int32Int64
|
||||
|
||||
Cast Int32 Int where
|
||||
cast = prim__cast_Int32Int
|
||||
|
||||
Cast Int32 Integer where
|
||||
cast = prim__cast_Int32Integer
|
||||
|
||||
Cast Int32 String where
|
||||
cast = prim__cast_Int32String
|
||||
|
||||
Cast Int32 Char where
|
||||
cast = prim__cast_Int32Char
|
||||
|
||||
Cast Int32 Double where
|
||||
cast = prim__cast_Int32Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- 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
|
||||
|
||||
Cast Int64 Bits8 where
|
||||
cast = prim__cast_Int64Bits8
|
||||
|
||||
Cast Int64 Bits16 where
|
||||
cast = prim__cast_Int64Bits16
|
||||
|
||||
Cast Int64 Bits32 where
|
||||
cast = prim__cast_Int64Bits32
|
||||
|
||||
Cast Int64 Bits64 where
|
||||
cast = prim__cast_Int64Bits64
|
||||
|
||||
Cast Int64 Int8 where
|
||||
cast = prim__cast_Int64Int8
|
||||
|
||||
Cast Int64 Int16 where
|
||||
cast = prim__cast_Int64Int16
|
||||
|
||||
Cast Int64 Int32 where
|
||||
cast = prim__cast_Int64Int32
|
||||
|
||||
Cast Int64 Int where
|
||||
cast = prim__cast_Int64Int
|
||||
|
||||
Cast Int64 Integer where
|
||||
cast = prim__cast_Int64Integer
|
||||
|
||||
Cast Int64 String where
|
||||
cast = prim__cast_Int64String
|
||||
|
||||
Cast Int64 Char where
|
||||
cast = prim__cast_Int64Char
|
||||
|
||||
Cast Int64 Double where
|
||||
cast = prim__cast_Int64Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Int Int8 where
|
||||
cast = prim__cast_IntInt8
|
||||
|
||||
Cast Int Int16 where
|
||||
cast = prim__cast_IntInt16
|
||||
|
||||
Cast Int Int32 where
|
||||
cast = prim__cast_IntInt32
|
||||
|
||||
Cast Int Int64 where
|
||||
cast = prim__cast_IntInt64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Integer
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Integer Int8 where
|
||||
cast = prim__cast_IntegerInt8
|
||||
|
||||
Cast Integer Int16 where
|
||||
cast = prim__cast_IntegerInt16
|
||||
|
||||
Cast Integer Int32 where
|
||||
cast = prim__cast_IntegerInt32
|
||||
|
||||
Cast Integer Int64 where
|
||||
cast = prim__cast_IntegerInt64
|
||||
|
||||
Cast Integer Char where
|
||||
cast = prim__cast_IntegerChar
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits8
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits8 Int8 where
|
||||
cast = prim__cast_Bits8Int8
|
||||
|
||||
Cast Bits8 Int16 where
|
||||
cast = prim__cast_Bits8Int16
|
||||
|
||||
Cast Bits8 Int32 where
|
||||
cast = prim__cast_Bits8Int32
|
||||
|
||||
Cast Bits8 Int64 where
|
||||
cast = prim__cast_Bits8Int64
|
||||
|
||||
Cast Bits8 String where
|
||||
cast = prim__cast_Bits8String
|
||||
|
||||
Cast Bits8 Char where
|
||||
cast = prim__cast_Bits8Char
|
||||
|
||||
Cast Bits8 Double where
|
||||
cast = prim__cast_Bits8Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits16 Int8 where
|
||||
cast = prim__cast_Bits16Int8
|
||||
|
||||
Cast Bits16 Int16 where
|
||||
cast = prim__cast_Bits16Int16
|
||||
|
||||
Cast Bits16 Int32 where
|
||||
cast = prim__cast_Bits16Int32
|
||||
|
||||
Cast Bits16 Int64 where
|
||||
cast = prim__cast_Bits16Int64
|
||||
|
||||
Cast Bits16 String where
|
||||
cast = prim__cast_Bits16String
|
||||
|
||||
Cast Bits16 Char where
|
||||
cast = prim__cast_Bits16Char
|
||||
|
||||
Cast Bits16 Double where
|
||||
cast = prim__cast_Bits16Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits32
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits32 Int8 where
|
||||
cast = prim__cast_Bits32Int8
|
||||
|
||||
Cast Bits32 Int16 where
|
||||
cast = prim__cast_Bits32Int16
|
||||
|
||||
Cast Bits32 Int32 where
|
||||
cast = prim__cast_Bits32Int32
|
||||
|
||||
Cast Bits32 Int64 where
|
||||
cast = prim__cast_Bits32Int64
|
||||
|
||||
Cast Bits32 String where
|
||||
cast = prim__cast_Bits32String
|
||||
|
||||
Cast Bits32 Char where
|
||||
cast = prim__cast_Bits32Char
|
||||
|
||||
Cast Bits32 Double where
|
||||
cast = prim__cast_Bits32Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits64
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits64 Int8 where
|
||||
cast = prim__cast_Bits64Int8
|
||||
|
||||
Cast Bits64 Int16 where
|
||||
cast = prim__cast_Bits64Int16
|
||||
|
||||
Cast Bits64 Int32 where
|
||||
cast = prim__cast_Bits64Int32
|
||||
|
||||
Cast Bits64 Int64 where
|
||||
cast = prim__cast_Bits64Int64
|
||||
|
||||
Cast Bits64 String where
|
||||
cast = prim__cast_Bits64String
|
||||
|
||||
Cast Bits64 Char where
|
||||
cast = prim__cast_Bits64Char
|
||||
|
||||
Cast Bits64 Double where
|
||||
cast = prim__cast_Bits64Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- String
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast String Bits8 where
|
||||
cast = prim__cast_StringBits8
|
||||
|
||||
Cast String Bits16 where
|
||||
cast = prim__cast_StringBits16
|
||||
|
||||
Cast String Bits32 where
|
||||
cast = prim__cast_StringBits32
|
||||
|
||||
Cast String Bits64 where
|
||||
cast = prim__cast_StringBits64
|
||||
|
||||
Cast String Int8 where
|
||||
cast = prim__cast_StringInt8
|
||||
|
||||
Cast String Int16 where
|
||||
cast = prim__cast_StringInt16
|
||||
|
||||
Cast String Int32 where
|
||||
cast = prim__cast_StringInt32
|
||||
|
||||
Cast String Int64 where
|
||||
cast = prim__cast_StringInt64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Double
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Double Bits8 where
|
||||
cast = prim__cast_DoubleBits8
|
||||
|
||||
Cast Double Bits16 where
|
||||
cast = prim__cast_DoubleBits16
|
||||
|
||||
Cast Double Bits32 where
|
||||
cast = prim__cast_DoubleBits32
|
||||
|
||||
Cast Double Bits64 where
|
||||
cast = prim__cast_DoubleBits64
|
||||
|
||||
Cast Double Int8 where
|
||||
cast = prim__cast_DoubleInt8
|
||||
|
||||
Cast Double Int16 where
|
||||
cast = prim__cast_DoubleInt16
|
||||
|
||||
Cast Double Int32 where
|
||||
cast = prim__cast_DoubleInt32
|
||||
|
||||
Cast Double Int64 where
|
||||
cast = prim__cast_DoubleInt64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Tests
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
showTpe : Type -> String
|
||||
showTpe Bits16 = "Bits16"
|
||||
showTpe Bits32 = "Bits32"
|
||||
showTpe Bits64 = "Bits64"
|
||||
showTpe Bits8 = "Bits8"
|
||||
showTpe Char = "Char"
|
||||
showTpe Double = "Double"
|
||||
showTpe Int = "Int"
|
||||
showTpe Int16 = "Int16"
|
||||
showTpe Int32 = "Int32"
|
||||
showTpe Int64 = "Int64"
|
||||
showTpe Int8 = "Int8"
|
||||
showTpe Integer = "Integer"
|
||||
showTpe String = "String"
|
||||
showTpe _ = "unknown type"
|
||||
|
||||
testCasts : (a: Type) -> (b : Type) -> (Cast a b, Show a, Show b, Eq b) =>
|
||||
List (a,b) -> List String
|
||||
testCasts a b = mapMaybe doTest
|
||||
where doTest : (a,b) -> Maybe String
|
||||
doTest (x,y) =
|
||||
let y2 = cast {to = b} x
|
||||
in if y == y2 then Nothing
|
||||
else Just $ #"Invalid cast from \#{showTpe a} to \#{showTpe b}: "#
|
||||
++ #"expected \#{show y} but got \#{show y2} when casting from \#{show x}"#
|
||||
|
||||
maxBits8 : Bits8
|
||||
maxBits8 = 0xff
|
||||
|
||||
maxBits16 : Bits16
|
||||
maxBits16 = 0xffff
|
||||
|
||||
maxBits32 : Bits32
|
||||
maxBits32 = 0xffffffff
|
||||
|
||||
maxBits64 : Bits64
|
||||
maxBits64 = 0xffffffffffffffff
|
||||
|
||||
results : List String
|
||||
results = testCasts Int8 Int16 [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Int32 [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Int64 [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Int [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Double [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 String [(-129,"-1"),(-128,"-128"),(0,"0"),(127,"127"),(128,"0")]
|
||||
++ testCasts Int8 Integer [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits8 [(-129,maxBits8),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits16 [(-129,maxBits16),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits32 [(-129,maxBits32),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits64 [(-129,maxBits64),(0,0),(127,127),(128,0)]
|
||||
|
||||
++ testCasts Int16 Int8 [(-32769,-1),(-32768,0),(0,0),(32767,127),(32768,0)]
|
||||
++ testCasts Int16 Int32 [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Int64 [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Int [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Double [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 String [(-32769,"-1"),(-32768,"-32768"),(0,"0"),(32767,"32767"),(32768,"0")]
|
||||
++ testCasts Int16 Integer [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits8 [(-32769,maxBits8),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits16 [(-32769,maxBits16),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits32 [(-32769,maxBits32),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits64 [(-32769,maxBits64),(0,0),(32767,32767),(32768,0)]
|
||||
|
||||
++ testCasts Int32 Int8 [(-2147483649,-1),(-2147483648,0),(0,0),(2147483647,0xff),(2147483648,0)]
|
||||
++ testCasts Int32 Int16 [(-2147483649,-1),(-2147483648,0),(0,0),(2147483647,0x7fff),(2147483648,0)]
|
||||
++ testCasts Int32 Int64 [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Int [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Double [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 String [(-2147483649,"-1"),(-2147483648,"-2147483648"),(0,"0"),(2147483647,"2147483647"),(2147483648,"0")]
|
||||
++ testCasts Int32 Integer [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits8 [(-2147483649,maxBits8),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits16 [(-2147483649,maxBits16),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits32 [(-2147483649,maxBits32),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits64 [(-2147483649,maxBits64),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
|
||||
++ testCasts Int64 Int8 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Int16 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Int32 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Int [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Double [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int64 String [(-9223372036854775809,"-1"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"0")]
|
||||
++ testCasts Int64 Integer [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits8 [(-9223372036854775809,maxBits8),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits16 [(-9223372036854775809,maxBits16),(0,0),(9223372036854775807,0xffff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits32 [(-9223372036854775809,maxBits32),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits64 [(-9223372036854775809,maxBits64),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
|
||||
++ testCasts Int Int8 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int Int16 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fff),(9223372036854775808,0)]
|
||||
++ testCasts Int Int32 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int Int64 [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int Double [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int String [(-9223372036854775809,"-1"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"0")]
|
||||
++ testCasts Int Integer [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits8 [(-9223372036854775809,maxBits8),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits16 [(-9223372036854775809,maxBits16),(0,0),(9223372036854775807,0xffff),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits32 [(-9223372036854775809,maxBits32),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits64 [(-9223372036854775809,maxBits64),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
|
||||
++ testCasts Integer Int8 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7f),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int16 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int32 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int64 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fffffffffffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fffffffffffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer String [(-170141183460469231731687303715884105729,"-170141183460469231731687303715884105729"),(-170141183460469231731687303715884105728,"-170141183460469231731687303715884105728"),(0,"0"),(170141183460469231731687303715884105727,"170141183460469231731687303715884105727"),(170141183460469231731687303715884105728,"170141183460469231731687303715884105728")]
|
||||
++ testCasts Integer Bits8 [(-170141183460469231731687303715884105729,maxBits8),(0,0),(170141183460469231731687303715884105727,0xff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Bits16 [(-170141183460469231731687303715884105729,maxBits16),(0,0),(170141183460469231731687303715884105727,0xffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Bits32 [(-170141183460469231731687303715884105729,maxBits32),(0,0),(170141183460469231731687303715884105727,0xffffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Bits64 [(-170141183460469231731687303715884105729,maxBits64),(0,0),(170141183460469231731687303715884105727,0xffffffffffffffff),(170141183460469231731687303715884105728,0)]
|
||||
|
||||
++ testCasts Bits8 Int8 [(0,0),(255,127),(256,0)]
|
||||
++ testCasts Bits8 Int16 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Int32 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Int64 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Int [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Double [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 String [(0,"0"),(255,"255"),(256,"0")]
|
||||
++ testCasts Bits8 Integer [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Bits16 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Bits32 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Bits64 [(0,0),(255,255),(256,0)]
|
||||
|
||||
++ testCasts Bits16 Int8 [(0,0),(0xffff,127),(0x10000,0)]
|
||||
++ testCasts Bits16 Int16 [(0,0),(0xffff,0x7fff),(0x10000,0)]
|
||||
++ testCasts Bits16 Int32 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Int64 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Int [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Double [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 String [(0,"0"),(0xffff,"65535"),(0x10000,"0")]
|
||||
++ testCasts Bits16 Integer [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Bits8 [(0,0),(0xffff,0xff),(0x10000,0)]
|
||||
++ testCasts Bits16 Bits32 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Bits64 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
|
||||
++ testCasts Bits32 Int8 [(0,0),(0xffffffff,127),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int16 [(0,0),(0xffffffff,0x7fff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int32 [(0,0),(0xffffffff,0x7fffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int64 [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Double [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 String [(0,"0"),(0xffffffff,"4294967295"),(0x100000000,"0")]
|
||||
++ testCasts Bits32 Integer [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Bits8 [(0,0),(0xffffffff,0xff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Bits16 [(0,0),(0xffffffff,0xffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Bits64 [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
|
||||
++ testCasts Bits64 Int8 [(0,0),(0xffffffffffffffff,127),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int16 [(0,0),(0xffffffffffffffff,0x7fff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int32 [(0,0),(0xffffffffffffffff,0x7fffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int64 [(0,0),(0xffffffffffffffff,0x7fffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int [(0,0),(0xffffffffffffffff,0x7fffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Double [(0,0),(0xffffffffffffffff,0xffffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 String [(0,"0"),(0xffffffffffffffff,"18446744073709551615"),(0x10000000000000000,"0")]
|
||||
++ testCasts Bits64 Integer [(0,0),(0xffffffffffffffff,0xffffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Bits8 [(0,0),(0xffffffffffffffff,0xff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Bits16 [(0,0),(0xffffffffffffffff,0xffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Bits32 [(0,0),(0xffffffffffffffff,0xffffffff),(0x10000000000000000,0)]
|
||||
|
||||
++ testCasts String Int8 [("-129",-1),("-128",-128),("0",0),("127",127), ("128",0)]
|
||||
++ testCasts String Int16 [("-32769",-1),("-32768",-32768),("0",0),("32767",32767), ("32768",0)]
|
||||
++ testCasts String Int32 [("-2147483649",-1),("-2147483648",-2147483648),("0",0),("2147483647",2147483647), ("2147483648",0)]
|
||||
++ testCasts String Int64 [("-9223372036854775809",-1),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",0)]
|
||||
++ testCasts String Int [("-9223372036854775809",-1),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",0)]
|
||||
++ testCasts String Integer [("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("0",0),("170141183460469231731687303715884105728",170141183460469231731687303715884105728)]
|
||||
++ testCasts String Bits8 [("0",0),("255",255), ("256",0)]
|
||||
++ testCasts String Bits16 [("0",0),("65535",65535), ("65536",0)]
|
||||
++ testCasts String Bits32 [("0",0),("4294967295",4294967295), ("4294967296",0)]
|
||||
++ testCasts String Bits64 [("0",0),("18446744073709551615",18446744073709551615), ("18446744073709551616",0)]
|
||||
|
||||
++ testCasts Double Int8 [(-129.0, -1),(-128.0,-128),(-12.001,-12),(12.001,12),(127.0,127),(128.0,0)]
|
||||
++ testCasts Double Int16 [(-32769.0, -1),(-32768.0,-32768),(-12.001,-12),(12.001,12),(32767.0,32767),(32768.0,0)]
|
||||
++ testCasts Double Int32 [(-2147483649.0, -1),(-2147483648.0,-2147483648),(-12.001,-12),(12.001,12),(2147483647.0,2147483647),(2147483648.0,0)]
|
||||
++ testCasts Double Int64 [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,0)]
|
||||
++ testCasts Double Int [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,0)]
|
||||
++ testCasts Double Bits8 [(0.0,0),(255.0,255), (256.0,0)]
|
||||
++ testCasts Double Bits16 [(0.0,0),(65535.0,65535), (65536.0,0)]
|
||||
++ testCasts Double Bits32 [(0.0,0),(4294967295.0,4294967295), (4294967296.0,0)]
|
||||
++ testCasts Double Bits64 [(0.0,0),(18446744073709551616.0,0)]
|
||||
|
||||
++ testCasts Int8 Char [(-1, '\x0'), (80, 'P')]
|
||||
++ testCasts Int16 Char [(-1, '\x0'), (80, 'P')]
|
||||
++ testCasts Int32 Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Int64 Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Int Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Bits8 Char [(80, 'P')]
|
||||
++ testCasts Bits16 Char [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000')]
|
||||
++ testCasts Bits32 Char [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Bits64 Char [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Integer Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Main
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
main : IO ()
|
||||
main = traverse_ putStrLn results
|
||||
2
tests/chez/casts/expected
Normal file
2
tests/chez/casts/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building Casts (Casts.idr)
|
||||
Main> Main> Bye for now!
|
||||
2
tests/chez/casts/input
Normal file
2
tests/chez/casts/input
Normal file
@ -0,0 +1,2 @@
|
||||
:exec main
|
||||
:q
|
||||
3
tests/chez/casts/run
Normal file
3
tests/chez/casts/run
Normal file
@ -0,0 +1,3 @@
|
||||
$1 --no-banner --no-color --console-width 0 Casts.idr < input
|
||||
|
||||
rm -rf build
|
||||
353
tests/chez/newints/IntOps.idr
Normal file
353
tests/chez/newints/IntOps.idr
Normal file
@ -0,0 +1,353 @@
|
||||
--
|
||||
-- Specification
|
||||
--
|
||||
-- a. Unsigned integers
|
||||
--
|
||||
-- Unsigned integers with a precision of x bit have a valid
|
||||
-- range of [0,2^x - 1]. They support all the usual arithmetic
|
||||
-- operations: +,*,-,div, and mod. If the result y of an operation
|
||||
-- is outside the valid range, the unsigned remainder modulo 2^x of y
|
||||
-- is returned instead. The same kind of truncation happens when
|
||||
-- other numeric types are cast to one of the unsigned integer
|
||||
-- types.
|
||||
--
|
||||
-- Example: For `Bits8` the valid range is [0,255]. Below are some
|
||||
-- example calculations. All numbers are considered to be of type `Bits8`
|
||||
-- unless specified otherwise:
|
||||
--
|
||||
-- 255 + 7 = 6
|
||||
-- 3 * 128 = 128
|
||||
-- (-1) = 255
|
||||
-- 7 - 10 = 253
|
||||
--
|
||||
-- b. Signed integers
|
||||
--
|
||||
-- Signed integers with a precision of x bit have a valid
|
||||
-- range of [-2^(x-1),2^(x-1) - 1]. They support all the usual arithmetic
|
||||
-- operations: +,*,-,div, and mod. If the result `y` of an operation
|
||||
-- is outside the valid range, the signed remainder modulo 2^x of `y`
|
||||
-- is returned instead. The same kind of truncation happens when
|
||||
-- other numeric types are cast to one of the signed integer
|
||||
-- types.
|
||||
--
|
||||
-- Example: For `Int8` the valid range is [-128,127]. Below are some
|
||||
-- example calculations. All numbers are considered to be of type `Int8`
|
||||
-- unless specified otherwise:
|
||||
--
|
||||
-- 127 + 7 = 6
|
||||
-- 3 * 64 = 64
|
||||
-- 2 * (-64) = (-128)
|
||||
-- (-129) = (-1)
|
||||
-- 7 - 10 = (-3)
|
||||
--
|
||||
import Data.List
|
||||
import Data.Stream
|
||||
|
||||
record IntType (a : Type) where
|
||||
constructor MkIntType
|
||||
name : String
|
||||
signed : Bool
|
||||
precision : Integer
|
||||
min : Integer
|
||||
max : Integer
|
||||
|
||||
intType : Bool -> String -> Integer -> IntType a
|
||||
intType True n p = let ma = prim__shl_Integer 1 (p - 1)
|
||||
in MkIntType n True p (negate ma) (ma - 1)
|
||||
intType False n p = let ma = prim__shl_Integer 1 p
|
||||
in MkIntType n False p 0 (ma - 1)
|
||||
|
||||
bits8 : IntType Bits8
|
||||
bits8 = intType False "Bits8" 8
|
||||
|
||||
bits16 : IntType Bits16
|
||||
bits16 = intType False "Bits16" 16
|
||||
|
||||
bits32 : IntType Bits32
|
||||
bits32 = intType False "Bits32" 32
|
||||
|
||||
bits64 : IntType Bits64
|
||||
bits64 = intType False "Bits64" 64
|
||||
|
||||
int8 : IntType Int8
|
||||
int8 = intType True "Int8" 8
|
||||
|
||||
int16 : IntType Int16
|
||||
int16 = intType True "Int16" 16
|
||||
|
||||
int32 : IntType Int32
|
||||
int32 = intType True "Int32" 32
|
||||
|
||||
int64 : IntType Int64
|
||||
int64 = intType True "Int64" 64
|
||||
|
||||
int : IntType Int
|
||||
int = intType True "Int" 64
|
||||
|
||||
record Op a where
|
||||
constructor MkOp
|
||||
name : String
|
||||
op : a -> a -> a
|
||||
opInt : Integer -> Integer -> Integer
|
||||
allowZero : Bool
|
||||
type : IntType a
|
||||
|
||||
add : Num a => IntType a -> Op a
|
||||
add = MkOp "+" (+) (+) True
|
||||
|
||||
sub : Neg a => IntType a -> Op a
|
||||
sub = MkOp "-" (-) (-) True
|
||||
|
||||
mul : Num a => IntType a -> Op a
|
||||
mul = MkOp "*" (*) (*) True
|
||||
|
||||
div : Integral a => IntType a -> Op a
|
||||
div = MkOp "div" (div) (div) False
|
||||
|
||||
mod : Integral a => IntType a -> Op a
|
||||
mod = MkOp "mod" (mod) (mod) False
|
||||
|
||||
|
||||
pairs : List (Integer,Integer)
|
||||
pairs = let -- [1,2,4,8,16,...,18446744073709551616]
|
||||
powsOf2 = take 65 (iterate (*2) 1)
|
||||
|
||||
-- powsOf2 ++ [0,1,3,7,...,18446744073709551615]
|
||||
naturals = powsOf2 ++ map (\x => x-1) powsOf2
|
||||
|
||||
-- positive and negative versions of naturals
|
||||
ints = naturals ++ map negate naturals
|
||||
|
||||
-- naturals paired with ints
|
||||
in [| (,) ints naturals |]
|
||||
|
||||
-- This check does the following: For a given binary operation `op`,
|
||||
-- calculate the result of applying the operation to all passed pairs
|
||||
-- of integers in `pairs` and check, with the given bit size, if
|
||||
-- the result is out of bounds. If it is, calculate the result
|
||||
-- modulo 2^bits. This gives the reference result as an `Integer`.
|
||||
--
|
||||
-- Now perform the same operation with the same input but for
|
||||
-- the integer type we'd like to check and cast the result back
|
||||
-- to an `Integer`. Create a nice error message for every pair
|
||||
-- that fails (returns an empty list if all goes well).
|
||||
check : (Num a, Cast a Integer) => Op a -> List String
|
||||
check (MkOp name op opInt allowZero $ MkIntType type signed bits mi ma) =
|
||||
let ps = if allowZero then pairs
|
||||
else filter ((0 /=) . checkBounds . snd) pairs
|
||||
in mapMaybe failing ps
|
||||
|
||||
where
|
||||
checkBounds : Integer -> Integer
|
||||
checkBounds n = let r1 = if n < mi || n > ma then n `mod` (ma + 1) else n
|
||||
in if not signed && r1 < 0
|
||||
then ma + r1 + 1
|
||||
else r1
|
||||
|
||||
failing : (Integer,Integer) -> Maybe String
|
||||
failing (x,y) =
|
||||
let resInteger = opInt x y
|
||||
resMod = checkBounds $ opInt (checkBounds x) (checkBounds y)
|
||||
resA = cast {to = Integer} (op (fromInteger x) (fromInteger y))
|
||||
in if resA == resMod
|
||||
then Nothing
|
||||
else Just #"Error when calculating \#{show x} \#{name} \#{show y} for \#{type}: Expected \#{show resMod} but got \#{show resA} (unrounded: \#{show resInteger})"#
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int8
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int8 where
|
||||
show = prim__cast_Int8String
|
||||
|
||||
Cast Int8 Integer where
|
||||
cast = prim__cast_Int8Integer
|
||||
|
||||
Num Int8 where
|
||||
(+) = prim__add_Int8
|
||||
(*) = prim__mul_Int8
|
||||
fromInteger = prim__cast_IntegerInt8
|
||||
|
||||
Neg Int8 where
|
||||
(-) = prim__sub_Int8
|
||||
negate = prim__sub_Int8 0
|
||||
|
||||
Integral Int8 where
|
||||
div = prim__div_Int8
|
||||
mod = prim__mod_Int8
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int16 where
|
||||
show = prim__cast_Int16String
|
||||
|
||||
Cast Int16 Integer where
|
||||
cast = prim__cast_Int16Integer
|
||||
|
||||
Num Int16 where
|
||||
(+) = prim__add_Int16
|
||||
(*) = prim__mul_Int16
|
||||
fromInteger = prim__cast_IntegerInt16
|
||||
|
||||
Neg Int16 where
|
||||
(-) = prim__sub_Int16
|
||||
negate = prim__sub_Int16 0
|
||||
|
||||
Integral Int16 where
|
||||
div = prim__div_Int16
|
||||
mod = prim__mod_Int16
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int32
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int32 where
|
||||
show = prim__cast_Int32String
|
||||
|
||||
Cast Int32 Integer where
|
||||
cast = prim__cast_Int32Integer
|
||||
|
||||
Num Int32 where
|
||||
(+) = prim__add_Int32
|
||||
(*) = prim__mul_Int32
|
||||
fromInteger = prim__cast_IntegerInt32
|
||||
|
||||
Neg Int32 where
|
||||
(-) = prim__sub_Int32
|
||||
negate = prim__sub_Int32 0
|
||||
|
||||
Integral Int32 where
|
||||
div = prim__div_Int32
|
||||
mod = prim__mod_Int32
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int64
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int64 where
|
||||
show = prim__cast_Int64String
|
||||
|
||||
Cast Int64 Integer where
|
||||
cast = prim__cast_Int64Integer
|
||||
|
||||
Num Int64 where
|
||||
(+) = prim__add_Int64
|
||||
(*) = prim__mul_Int64
|
||||
fromInteger = prim__cast_IntegerInt64
|
||||
|
||||
Neg Int64 where
|
||||
(-) = prim__sub_Int64
|
||||
negate = prim__sub_Int64 0
|
||||
|
||||
Integral Int64 where
|
||||
div = prim__div_Int64
|
||||
mod = prim__mod_Int64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits8
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits8 where
|
||||
(-) = prim__sub_Bits8
|
||||
negate = prim__sub_Bits8 0
|
||||
|
||||
Integral Bits8 where
|
||||
div = prim__div_Bits8
|
||||
mod = prim__mod_Bits8
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits16 where
|
||||
(-) = prim__sub_Bits16
|
||||
negate = prim__sub_Bits16 0
|
||||
|
||||
Integral Bits16 where
|
||||
div = prim__div_Bits16
|
||||
mod = prim__mod_Bits16
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits32
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits32 where
|
||||
(-) = prim__sub_Bits32
|
||||
negate = prim__sub_Bits32 0
|
||||
|
||||
Integral Bits32 where
|
||||
div = prim__div_Bits32
|
||||
mod = prim__mod_Bits32
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits64
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits64 where
|
||||
(-) = prim__sub_Bits64
|
||||
negate = prim__sub_Bits64 0
|
||||
|
||||
Integral Bits64 where
|
||||
div = prim__div_Bits64
|
||||
mod = prim__mod_Bits64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Main
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
main : IO ()
|
||||
main = do traverse_ putStrLn . check $ add int8
|
||||
traverse_ putStrLn . check $ sub int8
|
||||
traverse_ putStrLn . check $ mul int8
|
||||
traverse_ putStrLn . check $ div int8
|
||||
traverse_ putStrLn . check $ mod int8
|
||||
|
||||
traverse_ putStrLn . check $ add int16
|
||||
traverse_ putStrLn . check $ sub int16
|
||||
traverse_ putStrLn . check $ mul int16
|
||||
traverse_ putStrLn . check $ div int16
|
||||
traverse_ putStrLn . check $ mod int16
|
||||
|
||||
traverse_ putStrLn . check $ add int32
|
||||
traverse_ putStrLn . check $ sub int32
|
||||
traverse_ putStrLn . check $ mul int32
|
||||
traverse_ putStrLn . check $ div int32
|
||||
traverse_ putStrLn . check $ mod int32
|
||||
|
||||
traverse_ putStrLn . check $ add int64
|
||||
traverse_ putStrLn . check $ sub int64
|
||||
traverse_ putStrLn . check $ mul int64
|
||||
traverse_ putStrLn . check $ div int64
|
||||
traverse_ putStrLn . check $ mod int64
|
||||
|
||||
traverse_ putStrLn . check $ add int
|
||||
traverse_ putStrLn . check $ sub int
|
||||
traverse_ putStrLn . check $ mul int
|
||||
traverse_ putStrLn . check $ div int
|
||||
traverse_ putStrLn . check $ mod int
|
||||
|
||||
traverse_ putStrLn . check $ add bits8
|
||||
traverse_ putStrLn . check $ sub bits8
|
||||
traverse_ putStrLn . check $ mul bits8
|
||||
traverse_ putStrLn . check $ div bits8
|
||||
traverse_ putStrLn . check $ mod bits8
|
||||
|
||||
traverse_ putStrLn . check $ add bits16
|
||||
traverse_ putStrLn . check $ sub bits16
|
||||
traverse_ putStrLn . check $ mul bits16
|
||||
traverse_ putStrLn . check $ div bits16
|
||||
traverse_ putStrLn . check $ mod bits16
|
||||
|
||||
traverse_ putStrLn . check $ add bits32
|
||||
traverse_ putStrLn . check $ sub bits32
|
||||
traverse_ putStrLn . check $ mul bits32
|
||||
traverse_ putStrLn . check $ div bits32
|
||||
traverse_ putStrLn . check $ mod bits32
|
||||
|
||||
traverse_ putStrLn . check $ add bits64
|
||||
traverse_ putStrLn . check $ sub bits64
|
||||
traverse_ putStrLn . check $ mul bits64
|
||||
traverse_ putStrLn . check $ div bits64
|
||||
traverse_ putStrLn . check $ mod bits64
|
||||
2
tests/chez/newints/expected
Normal file
2
tests/chez/newints/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building IntOps (IntOps.idr)
|
||||
Main> Main> Bye for now!
|
||||
2
tests/chez/newints/input
Normal file
2
tests/chez/newints/input
Normal file
@ -0,0 +1,2 @@
|
||||
:exec main
|
||||
:q
|
||||
3
tests/chez/newints/run
Normal file
3
tests/chez/newints/run
Normal file
@ -0,0 +1,3 @@
|
||||
$1 --no-banner --no-color --console-width 0 IntOps.idr < input
|
||||
|
||||
rm -rf build
|
||||
@ -5,9 +5,9 @@ Main> 12
|
||||
Main> 12
|
||||
Main> "Negative Int"
|
||||
Main> -12
|
||||
Main> -13
|
||||
Main> -13
|
||||
Main> -13
|
||||
Main> -12
|
||||
Main> -12
|
||||
Main> -12
|
||||
Main> "Integer"
|
||||
Main> 12
|
||||
Main> 12
|
||||
@ -15,9 +15,9 @@ Main> 12
|
||||
Main> 12
|
||||
Main> "Negative Integer"
|
||||
Main> -12
|
||||
Main> -13
|
||||
Main> -13
|
||||
Main> -13
|
||||
Main> -12
|
||||
Main> -12
|
||||
Main> -12
|
||||
Main> "Double"
|
||||
Main> 12.0
|
||||
Main> 12.3
|
||||
|
||||
690
tests/node/casts/Casts.idr
Normal file
690
tests/node/casts/Casts.idr
Normal file
@ -0,0 +1,690 @@
|
||||
--
|
||||
-- Primitive casts: Specification
|
||||
--
|
||||
-- a. Unsigned integers
|
||||
--
|
||||
-- Unsigned integers with a precision of x bit have a valid
|
||||
-- range of [0,2^x - 1]. When casting from another integral type of value y,
|
||||
-- the value is checked for being in bounds, and if it is not, the
|
||||
-- unsigned remainder modulo 2^x of y is returned.
|
||||
--
|
||||
-- When casting from a `Double`, the value is first truncated towards 0,
|
||||
-- before applying the inbounds check and (if necessary) calculating
|
||||
-- the unsigned remainder modulo 2^x.
|
||||
--
|
||||
-- When casting from a `String`, the value is first converted to a floating
|
||||
-- point number by the backend and then truncated as described above.
|
||||
--
|
||||
-- Example: For `Bits8` the valid range is [0,255]. Below are some
|
||||
-- example casts.
|
||||
--
|
||||
-- cast {from = Integer} {to = Bits8} 12 = 12
|
||||
-- cast {from = Integer} {to = Bits8} 256 = 0
|
||||
-- cast {from = Integer} {to = Bits8} 259 = 3
|
||||
-- cast {from = Integer} {to = Bits8} (-2) = 254
|
||||
-- cast {from = Double} {to = Bits8} (-12.001) = 244
|
||||
-- cast {from = Double} {to = Bits8} ("-12.001") = 244
|
||||
--
|
||||
-- b. Signed integers
|
||||
--
|
||||
-- Signed integers with a precision of x bit have a valid
|
||||
-- range of [-2^(x-1),2^(x-1) - 1]. When casting from another
|
||||
-- integral type of value y, the value is checked for being in bounds,
|
||||
-- and if it is not, the signed remainder modulo 2^(x-1) of y is returned.
|
||||
--
|
||||
-- When casting from a `Double`, the value is first truncated towards 0,
|
||||
-- before applying the inbounds check and (if necessary) calculating
|
||||
-- the signed remainder modulo 2^(x-1).
|
||||
--
|
||||
-- When casting from a `String`, the value is first converted to a floating
|
||||
-- point number by the backend and then truncated as described above.
|
||||
--
|
||||
-- Example: For `Int8` the valid range is [-128,127]. Below are some
|
||||
-- example casts.
|
||||
--
|
||||
-- cast {from = Integer} {to = Int8} 12 = 12
|
||||
-- cast {from = Integer} {to = Int8} 256 = 0
|
||||
-- cast {from = Integer} {to = Int8} 259 = 4
|
||||
-- cast {from = Integer} {to = Int8} (-128) = (-128)
|
||||
-- cast {from = Integer} {to = Int8} (-129) = (-1)
|
||||
-- cast {from = Double} {to = Int8} (-12.001) = (-12)
|
||||
-- cast {from = Double} {to = Int8} ("-12.001") = (-12)
|
||||
--
|
||||
-- b. Characters
|
||||
--
|
||||
-- Casts from all integral types to `Char` are supported. Note however,
|
||||
-- that only casts in the non-surrogate range are supported, that is
|
||||
-- values in the ranges [0,0xd7ff] and [0xe000,0x10ffff], or, in decimal
|
||||
-- notation, [0,55295] and [57344,1114111].
|
||||
--
|
||||
-- All casts from integer types to `Char` are therefore submitted to a
|
||||
-- bounds check, and, in case the value is out of bounds, are converted to `'\0'`.
|
||||
--
|
||||
--
|
||||
-- Test all casts from and to integral types.
|
||||
-- The `Cast` implementations in here should go to `Prelude`, once
|
||||
-- a new minor version of the compiler is released.
|
||||
--
|
||||
-- These tests verify also that the full range of integer literals
|
||||
-- is supported for every integral type.
|
||||
--
|
||||
-- Nothing fancy is being done here:
|
||||
-- All test cases have been hand-written.
|
||||
|
||||
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
|
||||
|
||||
Cast Int8 Bits8 where
|
||||
cast = prim__cast_Int8Bits8
|
||||
|
||||
Cast Int8 Bits16 where
|
||||
cast = prim__cast_Int8Bits16
|
||||
|
||||
Cast Int8 Bits32 where
|
||||
cast = prim__cast_Int8Bits32
|
||||
|
||||
Cast Int8 Bits64 where
|
||||
cast = prim__cast_Int8Bits64
|
||||
|
||||
Cast Int8 Int16 where
|
||||
cast = prim__cast_Int8Int16
|
||||
|
||||
Cast Int8 Int32 where
|
||||
cast = prim__cast_Int8Int32
|
||||
|
||||
Cast Int8 Int64 where
|
||||
cast = prim__cast_Int8Int64
|
||||
|
||||
Cast Int8 Int where
|
||||
cast = prim__cast_Int8Int
|
||||
|
||||
Cast Int8 Integer where
|
||||
cast = prim__cast_Int8Integer
|
||||
|
||||
Cast Int8 String where
|
||||
cast = prim__cast_Int8String
|
||||
|
||||
Cast Int8 Char where
|
||||
cast = prim__cast_Int8Char
|
||||
|
||||
Cast Int8 Double where
|
||||
cast = prim__cast_Int8Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export
|
||||
Eq Int16 where
|
||||
x == y = intToBool (prim__eq_Int16 x y)
|
||||
|
||||
Show Int16 where
|
||||
show = prim__cast_Int16String
|
||||
|
||||
Num Int16 where
|
||||
(+) = prim__add_Int16
|
||||
(*) = prim__mul_Int16
|
||||
fromInteger = prim__cast_IntegerInt16
|
||||
|
||||
Neg Int16 where
|
||||
(-) = prim__sub_Int16
|
||||
negate = prim__sub_Int16 0
|
||||
|
||||
Cast Int16 Bits8 where
|
||||
cast = prim__cast_Int16Bits8
|
||||
|
||||
Cast Int16 Bits16 where
|
||||
cast = prim__cast_Int16Bits16
|
||||
|
||||
Cast Int16 Bits32 where
|
||||
cast = prim__cast_Int16Bits32
|
||||
|
||||
Cast Int16 Bits64 where
|
||||
cast = prim__cast_Int16Bits64
|
||||
|
||||
Cast Int16 Int8 where
|
||||
cast = prim__cast_Int16Int8
|
||||
|
||||
Cast Int16 Int32 where
|
||||
cast = prim__cast_Int16Int32
|
||||
|
||||
Cast Int16 Int64 where
|
||||
cast = prim__cast_Int16Int64
|
||||
|
||||
Cast Int16 Int where
|
||||
cast = prim__cast_Int16Int
|
||||
|
||||
Cast Int16 Integer where
|
||||
cast = prim__cast_Int16Integer
|
||||
|
||||
Cast Int16 String where
|
||||
cast = prim__cast_Int16String
|
||||
|
||||
Cast Int16 Char where
|
||||
cast = prim__cast_Int16Char
|
||||
|
||||
Cast Int16 Double where
|
||||
cast = prim__cast_Int16Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- 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
|
||||
|
||||
Cast Int32 Bits8 where
|
||||
cast = prim__cast_Int32Bits8
|
||||
|
||||
Cast Int32 Bits16 where
|
||||
cast = prim__cast_Int32Bits16
|
||||
|
||||
Cast Int32 Bits32 where
|
||||
cast = prim__cast_Int32Bits32
|
||||
|
||||
Cast Int32 Bits64 where
|
||||
cast = prim__cast_Int32Bits64
|
||||
|
||||
Cast Int32 Int8 where
|
||||
cast = prim__cast_Int32Int8
|
||||
|
||||
Cast Int32 Int16 where
|
||||
cast = prim__cast_Int32Int16
|
||||
|
||||
Cast Int32 Int64 where
|
||||
cast = prim__cast_Int32Int64
|
||||
|
||||
Cast Int32 Int where
|
||||
cast = prim__cast_Int32Int
|
||||
|
||||
Cast Int32 Integer where
|
||||
cast = prim__cast_Int32Integer
|
||||
|
||||
Cast Int32 String where
|
||||
cast = prim__cast_Int32String
|
||||
|
||||
Cast Int32 Char where
|
||||
cast = prim__cast_Int32Char
|
||||
|
||||
Cast Int32 Double where
|
||||
cast = prim__cast_Int32Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- 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
|
||||
|
||||
Cast Int64 Bits8 where
|
||||
cast = prim__cast_Int64Bits8
|
||||
|
||||
Cast Int64 Bits16 where
|
||||
cast = prim__cast_Int64Bits16
|
||||
|
||||
Cast Int64 Bits32 where
|
||||
cast = prim__cast_Int64Bits32
|
||||
|
||||
Cast Int64 Bits64 where
|
||||
cast = prim__cast_Int64Bits64
|
||||
|
||||
Cast Int64 Int8 where
|
||||
cast = prim__cast_Int64Int8
|
||||
|
||||
Cast Int64 Int16 where
|
||||
cast = prim__cast_Int64Int16
|
||||
|
||||
Cast Int64 Int32 where
|
||||
cast = prim__cast_Int64Int32
|
||||
|
||||
Cast Int64 Int where
|
||||
cast = prim__cast_Int64Int
|
||||
|
||||
Cast Int64 Integer where
|
||||
cast = prim__cast_Int64Integer
|
||||
|
||||
Cast Int64 String where
|
||||
cast = prim__cast_Int64String
|
||||
|
||||
Cast Int64 Char where
|
||||
cast = prim__cast_Int64Char
|
||||
|
||||
Cast Int64 Double where
|
||||
cast = prim__cast_Int64Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Int Int8 where
|
||||
cast = prim__cast_IntInt8
|
||||
|
||||
Cast Int Int16 where
|
||||
cast = prim__cast_IntInt16
|
||||
|
||||
Cast Int Int32 where
|
||||
cast = prim__cast_IntInt32
|
||||
|
||||
Cast Int Int64 where
|
||||
cast = prim__cast_IntInt64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Integer
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Integer Int8 where
|
||||
cast = prim__cast_IntegerInt8
|
||||
|
||||
Cast Integer Int16 where
|
||||
cast = prim__cast_IntegerInt16
|
||||
|
||||
Cast Integer Int32 where
|
||||
cast = prim__cast_IntegerInt32
|
||||
|
||||
Cast Integer Int64 where
|
||||
cast = prim__cast_IntegerInt64
|
||||
|
||||
Cast Integer Char where
|
||||
cast = prim__cast_IntegerChar
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits8
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits8 Int8 where
|
||||
cast = prim__cast_Bits8Int8
|
||||
|
||||
Cast Bits8 Int16 where
|
||||
cast = prim__cast_Bits8Int16
|
||||
|
||||
Cast Bits8 Int32 where
|
||||
cast = prim__cast_Bits8Int32
|
||||
|
||||
Cast Bits8 Int64 where
|
||||
cast = prim__cast_Bits8Int64
|
||||
|
||||
Cast Bits8 String where
|
||||
cast = prim__cast_Bits8String
|
||||
|
||||
Cast Bits8 Char where
|
||||
cast = prim__cast_Bits8Char
|
||||
|
||||
Cast Bits8 Double where
|
||||
cast = prim__cast_Bits8Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits16 Int8 where
|
||||
cast = prim__cast_Bits16Int8
|
||||
|
||||
Cast Bits16 Int16 where
|
||||
cast = prim__cast_Bits16Int16
|
||||
|
||||
Cast Bits16 Int32 where
|
||||
cast = prim__cast_Bits16Int32
|
||||
|
||||
Cast Bits16 Int64 where
|
||||
cast = prim__cast_Bits16Int64
|
||||
|
||||
Cast Bits16 String where
|
||||
cast = prim__cast_Bits16String
|
||||
|
||||
Cast Bits16 Char where
|
||||
cast = prim__cast_Bits16Char
|
||||
|
||||
Cast Bits16 Double where
|
||||
cast = prim__cast_Bits16Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits32
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits32 Int8 where
|
||||
cast = prim__cast_Bits32Int8
|
||||
|
||||
Cast Bits32 Int16 where
|
||||
cast = prim__cast_Bits32Int16
|
||||
|
||||
Cast Bits32 Int32 where
|
||||
cast = prim__cast_Bits32Int32
|
||||
|
||||
Cast Bits32 Int64 where
|
||||
cast = prim__cast_Bits32Int64
|
||||
|
||||
Cast Bits32 String where
|
||||
cast = prim__cast_Bits32String
|
||||
|
||||
Cast Bits32 Char where
|
||||
cast = prim__cast_Bits32Char
|
||||
|
||||
Cast Bits32 Double where
|
||||
cast = prim__cast_Bits32Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits64
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Bits64 Int8 where
|
||||
cast = prim__cast_Bits64Int8
|
||||
|
||||
Cast Bits64 Int16 where
|
||||
cast = prim__cast_Bits64Int16
|
||||
|
||||
Cast Bits64 Int32 where
|
||||
cast = prim__cast_Bits64Int32
|
||||
|
||||
Cast Bits64 Int64 where
|
||||
cast = prim__cast_Bits64Int64
|
||||
|
||||
Cast Bits64 String where
|
||||
cast = prim__cast_Bits64String
|
||||
|
||||
Cast Bits64 Char where
|
||||
cast = prim__cast_Bits64Char
|
||||
|
||||
Cast Bits64 Double where
|
||||
cast = prim__cast_Bits64Double
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- String
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast String Bits8 where
|
||||
cast = prim__cast_StringBits8
|
||||
|
||||
Cast String Bits16 where
|
||||
cast = prim__cast_StringBits16
|
||||
|
||||
Cast String Bits32 where
|
||||
cast = prim__cast_StringBits32
|
||||
|
||||
Cast String Bits64 where
|
||||
cast = prim__cast_StringBits64
|
||||
|
||||
Cast String Int8 where
|
||||
cast = prim__cast_StringInt8
|
||||
|
||||
Cast String Int16 where
|
||||
cast = prim__cast_StringInt16
|
||||
|
||||
Cast String Int32 where
|
||||
cast = prim__cast_StringInt32
|
||||
|
||||
Cast String Int64 where
|
||||
cast = prim__cast_StringInt64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Double
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Cast Double Bits8 where
|
||||
cast = prim__cast_DoubleBits8
|
||||
|
||||
Cast Double Bits16 where
|
||||
cast = prim__cast_DoubleBits16
|
||||
|
||||
Cast Double Bits32 where
|
||||
cast = prim__cast_DoubleBits32
|
||||
|
||||
Cast Double Bits64 where
|
||||
cast = prim__cast_DoubleBits64
|
||||
|
||||
Cast Double Int8 where
|
||||
cast = prim__cast_DoubleInt8
|
||||
|
||||
Cast Double Int16 where
|
||||
cast = prim__cast_DoubleInt16
|
||||
|
||||
Cast Double Int32 where
|
||||
cast = prim__cast_DoubleInt32
|
||||
|
||||
Cast Double Int64 where
|
||||
cast = prim__cast_DoubleInt64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Tests
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
showTpe : Type -> String
|
||||
showTpe Bits16 = "Bits16"
|
||||
showTpe Bits32 = "Bits32"
|
||||
showTpe Bits64 = "Bits64"
|
||||
showTpe Bits8 = "Bits8"
|
||||
showTpe Char = "Char"
|
||||
showTpe Double = "Double"
|
||||
showTpe Int = "Int"
|
||||
showTpe Int16 = "Int16"
|
||||
showTpe Int32 = "Int32"
|
||||
showTpe Int64 = "Int64"
|
||||
showTpe Int8 = "Int8"
|
||||
showTpe Integer = "Integer"
|
||||
showTpe String = "String"
|
||||
showTpe _ = "unknown type"
|
||||
|
||||
testCasts : (a: Type) -> (b : Type) -> (Cast a b, Show a, Show b, Eq b) =>
|
||||
List (a,b) -> List String
|
||||
testCasts a b = mapMaybe doTest
|
||||
where doTest : (a,b) -> Maybe String
|
||||
doTest (x,y) =
|
||||
let y2 = cast {to = b} x
|
||||
in if y == y2 then Nothing
|
||||
else Just $ #"Invalid cast from \#{showTpe a} to \#{showTpe b}: "#
|
||||
++ #"expected \#{show y} but got \#{show y2} when casting from \#{show x}"#
|
||||
|
||||
maxBits8 : Bits8
|
||||
maxBits8 = 0xff
|
||||
|
||||
maxBits16 : Bits16
|
||||
maxBits16 = 0xffff
|
||||
|
||||
maxBits32 : Bits32
|
||||
maxBits32 = 0xffffffff
|
||||
|
||||
maxBits64 : Bits64
|
||||
maxBits64 = 0xffffffffffffffff
|
||||
|
||||
results : List String
|
||||
results = testCasts Int8 Int16 [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Int32 [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Int64 [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Int [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Double [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 String [(-129,"-1"),(-128,"-128"),(0,"0"),(127,"127"),(128,"0")]
|
||||
++ testCasts Int8 Integer [(-129,-1),(-128,-128),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits8 [(-129,maxBits8),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits16 [(-129,maxBits16),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits32 [(-129,maxBits32),(0,0),(127,127),(128,0)]
|
||||
++ testCasts Int8 Bits64 [(-129,maxBits64),(0,0),(127,127),(128,0)]
|
||||
|
||||
++ testCasts Int16 Int8 [(-32769,-1),(-32768,0),(0,0),(32767,127),(32768,0)]
|
||||
++ testCasts Int16 Int32 [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Int64 [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Int [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Double [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 String [(-32769,"-1"),(-32768,"-32768"),(0,"0"),(32767,"32767"),(32768,"0")]
|
||||
++ testCasts Int16 Integer [(-32769,-1),(-32768,-32768),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits8 [(-32769,maxBits8),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits16 [(-32769,maxBits16),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits32 [(-32769,maxBits32),(0,0),(32767,32767),(32768,0)]
|
||||
++ testCasts Int16 Bits64 [(-32769,maxBits64),(0,0),(32767,32767),(32768,0)]
|
||||
|
||||
++ testCasts Int32 Int8 [(-2147483649,-1),(-2147483648,0),(0,0),(2147483647,0xff),(2147483648,0)]
|
||||
++ testCasts Int32 Int16 [(-2147483649,-1),(-2147483648,0),(0,0),(2147483647,0x7fff),(2147483648,0)]
|
||||
++ testCasts Int32 Int64 [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Int [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Double [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 String [(-2147483649,"-1"),(-2147483648,"-2147483648"),(0,"0"),(2147483647,"2147483647"),(2147483648,"0")]
|
||||
++ testCasts Int32 Integer [(-2147483649,-1),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits8 [(-2147483649,maxBits8),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits16 [(-2147483649,maxBits16),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits32 [(-2147483649,maxBits32),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
++ testCasts Int32 Bits64 [(-2147483649,maxBits64),(0,0),(2147483647,2147483647),(2147483648,0)]
|
||||
|
||||
++ testCasts Int64 Int8 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Int16 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Int32 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Int [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Double [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int64 String [(-9223372036854775809,"-1"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"0")]
|
||||
++ testCasts Int64 Integer [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits8 [(-9223372036854775809,maxBits8),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits16 [(-9223372036854775809,maxBits16),(0,0),(9223372036854775807,0xffff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits32 [(-9223372036854775809,maxBits32),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int64 Bits64 [(-9223372036854775809,maxBits64),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
|
||||
++ testCasts Int Int8 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int Int16 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fff),(9223372036854775808,0)]
|
||||
++ testCasts Int Int32 [(-9223372036854775809,-1),(-9223372036854775808,0),(0,0),(9223372036854775807,0x7fffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int Int64 [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int Double [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int String [(-9223372036854775809,"-1"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"0")]
|
||||
++ testCasts Int Integer [(-9223372036854775809,-1),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits8 [(-9223372036854775809,maxBits8),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits16 [(-9223372036854775809,maxBits16),(0,0),(9223372036854775807,0xffff),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits32 [(-9223372036854775809,maxBits32),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)]
|
||||
++ testCasts Int Bits64 [(-9223372036854775809,maxBits64),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,0)]
|
||||
|
||||
++ testCasts Integer Int8 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7f),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int16 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int32 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int64 [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fffffffffffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Int [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,0x7fffffffffffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer String [(-170141183460469231731687303715884105729,"-170141183460469231731687303715884105729"),(-170141183460469231731687303715884105728,"-170141183460469231731687303715884105728"),(0,"0"),(170141183460469231731687303715884105727,"170141183460469231731687303715884105727"),(170141183460469231731687303715884105728,"170141183460469231731687303715884105728")]
|
||||
++ testCasts Integer Bits8 [(-170141183460469231731687303715884105729,maxBits8),(0,0),(170141183460469231731687303715884105727,0xff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Bits16 [(-170141183460469231731687303715884105729,maxBits16),(0,0),(170141183460469231731687303715884105727,0xffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Bits32 [(-170141183460469231731687303715884105729,maxBits32),(0,0),(170141183460469231731687303715884105727,0xffffffff),(170141183460469231731687303715884105728,0)]
|
||||
++ testCasts Integer Bits64 [(-170141183460469231731687303715884105729,maxBits64),(0,0),(170141183460469231731687303715884105727,0xffffffffffffffff),(170141183460469231731687303715884105728,0)]
|
||||
|
||||
++ testCasts Bits8 Int8 [(0,0),(255,127),(256,0)]
|
||||
++ testCasts Bits8 Int16 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Int32 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Int64 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Int [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Double [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 String [(0,"0"),(255,"255"),(256,"0")]
|
||||
++ testCasts Bits8 Integer [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Bits16 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Bits32 [(0,0),(255,255),(256,0)]
|
||||
++ testCasts Bits8 Bits64 [(0,0),(255,255),(256,0)]
|
||||
|
||||
++ testCasts Bits16 Int8 [(0,0),(0xffff,127),(0x10000,0)]
|
||||
++ testCasts Bits16 Int16 [(0,0),(0xffff,0x7fff),(0x10000,0)]
|
||||
++ testCasts Bits16 Int32 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Int64 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Int [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Double [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 String [(0,"0"),(0xffff,"65535"),(0x10000,"0")]
|
||||
++ testCasts Bits16 Integer [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Bits8 [(0,0),(0xffff,0xff),(0x10000,0)]
|
||||
++ testCasts Bits16 Bits32 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
++ testCasts Bits16 Bits64 [(0,0),(0xffff,0xffff),(0x10000,0)]
|
||||
|
||||
++ testCasts Bits32 Int8 [(0,0),(0xffffffff,127),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int16 [(0,0),(0xffffffff,0x7fff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int32 [(0,0),(0xffffffff,0x7fffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int64 [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Int [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Double [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 String [(0,"0"),(0xffffffff,"4294967295"),(0x100000000,"0")]
|
||||
++ testCasts Bits32 Integer [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Bits8 [(0,0),(0xffffffff,0xff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Bits16 [(0,0),(0xffffffff,0xffff),(0x100000000,0)]
|
||||
++ testCasts Bits32 Bits64 [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
|
||||
|
||||
++ testCasts Bits64 Int8 [(0,0),(0xffffffffffffffff,127),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int16 [(0,0),(0xffffffffffffffff,0x7fff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int32 [(0,0),(0xffffffffffffffff,0x7fffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int64 [(0,0),(0xffffffffffffffff,0x7fffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Int [(0,0),(0xffffffffffffffff,0x7fffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Double [(0,0),(0xffffffffffffffff,0xffffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 String [(0,"0"),(0xffffffffffffffff,"18446744073709551615"),(0x10000000000000000,"0")]
|
||||
++ testCasts Bits64 Integer [(0,0),(0xffffffffffffffff,0xffffffffffffffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Bits8 [(0,0),(0xffffffffffffffff,0xff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Bits16 [(0,0),(0xffffffffffffffff,0xffff),(0x10000000000000000,0)]
|
||||
++ testCasts Bits64 Bits32 [(0,0),(0xffffffffffffffff,0xffffffff),(0x10000000000000000,0)]
|
||||
|
||||
++ testCasts String Int8 [("-129",-1),("-128",-128),("0",0),("127",127), ("128",0)]
|
||||
++ testCasts String Int16 [("-32769",-1),("-32768",-32768),("0",0),("32767",32767), ("32768",0)]
|
||||
++ testCasts String Int32 [("-2147483649",-1),("-2147483648",-2147483648),("0",0),("2147483647",2147483647), ("2147483648",0)]
|
||||
++ testCasts String Int64 [("-9223372036854775809",-1),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",0)]
|
||||
++ testCasts String Int [("-9223372036854775809",-1),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",0)]
|
||||
++ testCasts String Integer [("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("0",0),("170141183460469231731687303715884105728",170141183460469231731687303715884105728)]
|
||||
++ testCasts String Bits8 [("0",0),("255",255), ("256",0)]
|
||||
++ testCasts String Bits16 [("0",0),("65535",65535), ("65536",0)]
|
||||
++ testCasts String Bits32 [("0",0),("4294967295",4294967295), ("4294967296",0)]
|
||||
++ testCasts String Bits64 [("0",0),("18446744073709551615",18446744073709551615), ("18446744073709551616",0)]
|
||||
|
||||
++ testCasts Double Int8 [(-129.0, -1),(-128.0,-128),(-12.001,-12),(12.001,12),(127.0,127),(128.0,0)]
|
||||
++ testCasts Double Int16 [(-32769.0, -1),(-32768.0,-32768),(-12.001,-12),(12.001,12),(32767.0,32767),(32768.0,0)]
|
||||
++ testCasts Double Int32 [(-2147483649.0, -1),(-2147483648.0,-2147483648),(-12.001,-12),(12.001,12),(2147483647.0,2147483647),(2147483648.0,0)]
|
||||
++ testCasts Double Int64 [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,0)]
|
||||
++ testCasts Double Int [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,0)]
|
||||
++ testCasts Double Bits8 [(0.0,0),(255.0,255), (256.0,0)]
|
||||
++ testCasts Double Bits16 [(0.0,0),(65535.0,65535), (65536.0,0)]
|
||||
++ testCasts Double Bits32 [(0.0,0),(4294967295.0,4294967295), (4294967296.0,0)]
|
||||
++ testCasts Double Bits64 [(0.0,0),(18446744073709551616.0,0)]
|
||||
|
||||
++ testCasts Int8 Char [(-1, '\x0'), (80, 'P')]
|
||||
++ testCasts Int16 Char [(-1, '\x0'), (80, 'P')]
|
||||
++ testCasts Int32 Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Int64 Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Int Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Bits8 Char [(80, 'P')]
|
||||
++ testCasts Bits16 Char [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000')]
|
||||
++ testCasts Bits32 Char [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Bits64 Char [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
++ testCasts Integer Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Main
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
main : IO ()
|
||||
main = traverse_ putStrLn results
|
||||
2
tests/node/casts/expected
Normal file
2
tests/node/casts/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building Casts (Casts.idr)
|
||||
Main> Main> Bye for now!
|
||||
2
tests/node/casts/input
Normal file
2
tests/node/casts/input
Normal file
@ -0,0 +1,2 @@
|
||||
:exec main
|
||||
:q
|
||||
3
tests/node/casts/run
Normal file
3
tests/node/casts/run
Normal file
@ -0,0 +1,3 @@
|
||||
$1 --cg node --no-banner --no-color --console-width 0 Casts.idr < input
|
||||
|
||||
rm -rf build
|
||||
359
tests/node/newints/IntOps.idr
Normal file
359
tests/node/newints/IntOps.idr
Normal file
@ -0,0 +1,359 @@
|
||||
--
|
||||
-- Specification
|
||||
--
|
||||
-- a. Unsigned integers
|
||||
--
|
||||
-- Unsigned integers with a precision of x bit have a valid
|
||||
-- range of [0,2^x - 1]. They support all the usual arithmetic
|
||||
-- operations: +,*,-,div, and mod. If the result y of an operation
|
||||
-- is outside the valid range, the unsigned remainder modulo 2^x of y
|
||||
-- is returned instead. The same kind of truncation happens when
|
||||
-- other numeric types are cast to one of the unsigned integer
|
||||
-- types.
|
||||
--
|
||||
-- Example: For `Bits8` the valid range is [0,255]. Below are some
|
||||
-- example calculations. All numbers are considered to be of type `Bits8`
|
||||
-- unless specified otherwise:
|
||||
--
|
||||
-- 255 + 7 = 6
|
||||
-- 3 * 128 = 128
|
||||
-- (-1) = 255
|
||||
-- 7 - 10 = 253
|
||||
--
|
||||
-- b. Signed integers
|
||||
--
|
||||
-- Signed integers with a precision of x bit have a valid
|
||||
-- range of [-2^(x-1),2^(x-1) - 1]. They support all the usual arithmetic
|
||||
-- operations: +,*,-,div, and mod. If the result `y` of an operation
|
||||
-- is outside the valid range, the signed remainder modulo 2^x of `y`
|
||||
-- is returned instead. The same kind of truncation happens when
|
||||
-- other numeric types are cast to one of the signed integer
|
||||
-- types.
|
||||
--
|
||||
-- Example: For `Int8` the valid range is [-128,127]. Below are some
|
||||
-- example calculations. All numbers are considered to be of type `Int8`
|
||||
-- unless specified otherwise:
|
||||
--
|
||||
-- 127 + 7 = 6
|
||||
-- 3 * 64 = 64
|
||||
-- 2 * (-64) = (-128)
|
||||
-- (-129) = (-1)
|
||||
-- 7 - 10 = (-3)
|
||||
--
|
||||
import Data.List
|
||||
import Data.Stream
|
||||
|
||||
record IntType (a : Type) where
|
||||
constructor MkIntType
|
||||
name : String
|
||||
signed : Bool
|
||||
precision : Integer
|
||||
min : Integer
|
||||
max : Integer
|
||||
|
||||
intType : Bool -> String -> Integer -> IntType a
|
||||
intType True n p = let ma = prim__shl_Integer 1 (p - 1)
|
||||
in MkIntType n True p (negate ma) (ma - 1)
|
||||
intType False n p = let ma = prim__shl_Integer 1 p
|
||||
in MkIntType n False p 0 (ma - 1)
|
||||
|
||||
bits8 : IntType Bits8
|
||||
bits8 = intType False "Bits8" 8
|
||||
|
||||
bits16 : IntType Bits16
|
||||
bits16 = intType False "Bits16" 16
|
||||
|
||||
bits32 : IntType Bits32
|
||||
bits32 = intType False "Bits32" 32
|
||||
|
||||
bits64 : IntType Bits64
|
||||
bits64 = intType False "Bits64" 64
|
||||
|
||||
int8 : IntType Int8
|
||||
int8 = intType True "Int8" 8
|
||||
|
||||
int16 : IntType Int16
|
||||
int16 = intType True "Int16" 16
|
||||
|
||||
int32 : IntType Int32
|
||||
int32 = intType True "Int32" 32
|
||||
|
||||
int64 : IntType Int64
|
||||
int64 = intType True "Int64" 64
|
||||
|
||||
int : IntType Int
|
||||
int = intType True "Int" 64
|
||||
|
||||
record Op a where
|
||||
constructor MkOp
|
||||
name : String
|
||||
op : a -> a -> a
|
||||
opInt : Integer -> Integer -> Integer
|
||||
allowZero : Bool
|
||||
type : IntType a
|
||||
|
||||
add : Num a => IntType a -> Op a
|
||||
add = MkOp "+" (+) (+) True
|
||||
|
||||
sub : Neg a => IntType a -> Op a
|
||||
sub = MkOp "-" (-) (-) True
|
||||
|
||||
mul : Num a => IntType a -> Op a
|
||||
mul = MkOp "*" (*) (*) True
|
||||
|
||||
div : Integral a => IntType a -> Op a
|
||||
div = MkOp "div" (div) (div) False
|
||||
|
||||
mod : Integral a => IntType a -> Op a
|
||||
mod = MkOp "mod" (mod) (mod) False
|
||||
|
||||
|
||||
pairs : List (Integer,Integer)
|
||||
pairs = let -- [1,2,4,8,16,...,18446744073709551616]
|
||||
powsOf2 = take 65 (iterate (*2) 1)
|
||||
|
||||
-- powsOf2 ++ [0,1,3,7,...,18446744073709551615]
|
||||
naturals = powsOf2 ++ map (\x => x-1) powsOf2
|
||||
|
||||
-- positive and negative versions of naturals
|
||||
ints = naturals ++ map negate naturals
|
||||
|
||||
-- naturals paired with ints
|
||||
in [| (,) ints naturals |]
|
||||
|
||||
filterTailRec : (a -> Bool) -> List a -> List a
|
||||
filterTailRec p = run Nil
|
||||
where run : List a -> List a -> List a
|
||||
run res [] = res
|
||||
run res (h :: t) = if p h then run (h :: res) t else run res t
|
||||
|
||||
-- This check does the following: For a given binary operation `op`,
|
||||
-- calculate the result of applying the operation to all passed pairs
|
||||
-- of integers in `pairs` and check, with the given bit size, if
|
||||
-- the result is out of bounds. If it is, calculate the result
|
||||
-- modulo 2^bits. This gives the reference result as an `Integer`.
|
||||
--
|
||||
-- Now perform the same operation with the same input but for
|
||||
-- the integer type we'd like to check and cast the result back
|
||||
-- to an `Integer`. Create a nice error message for every pair
|
||||
-- that fails (returns an empty list if all goes well).
|
||||
check : (Num a, Cast a Integer) => Op a -> List String
|
||||
check (MkOp name op opInt allowZero $ MkIntType type signed bits mi ma) =
|
||||
let ps = if allowZero then pairs
|
||||
else filterTailRec ((0 /=) . checkBounds . snd) pairs
|
||||
in mapMaybe failing ps
|
||||
|
||||
where
|
||||
checkBounds : Integer -> Integer
|
||||
checkBounds n = let r1 = if n < mi || n > ma then n `mod` (ma + 1) else n
|
||||
in if not signed && r1 < 0
|
||||
then ma + r1 + 1
|
||||
else r1
|
||||
|
||||
failing : (Integer,Integer) -> Maybe String
|
||||
failing (x,y) =
|
||||
let resInteger = opInt x y
|
||||
resMod = checkBounds $ opInt (checkBounds x) (checkBounds y)
|
||||
resA = cast {to = Integer} (op (fromInteger x) (fromInteger y))
|
||||
in if resA == resMod
|
||||
then Nothing
|
||||
else Just #"Error when calculating \#{show x} \#{name} \#{show y} for \#{type}: Expected \#{show resMod} but got \#{show resA} (unrounded: \#{show resInteger})"#
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int8
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int8 where
|
||||
show = prim__cast_Int8String
|
||||
|
||||
Cast Int8 Integer where
|
||||
cast = prim__cast_Int8Integer
|
||||
|
||||
Num Int8 where
|
||||
(+) = prim__add_Int8
|
||||
(*) = prim__mul_Int8
|
||||
fromInteger = prim__cast_IntegerInt8
|
||||
|
||||
Neg Int8 where
|
||||
(-) = prim__sub_Int8
|
||||
negate = prim__sub_Int8 0
|
||||
|
||||
Integral Int8 where
|
||||
div = prim__div_Int8
|
||||
mod = prim__mod_Int8
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int16 where
|
||||
show = prim__cast_Int16String
|
||||
|
||||
Cast Int16 Integer where
|
||||
cast = prim__cast_Int16Integer
|
||||
|
||||
Num Int16 where
|
||||
(+) = prim__add_Int16
|
||||
(*) = prim__mul_Int16
|
||||
fromInteger = prim__cast_IntegerInt16
|
||||
|
||||
Neg Int16 where
|
||||
(-) = prim__sub_Int16
|
||||
negate = prim__sub_Int16 0
|
||||
|
||||
Integral Int16 where
|
||||
div = prim__div_Int16
|
||||
mod = prim__mod_Int16
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int32
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int32 where
|
||||
show = prim__cast_Int32String
|
||||
|
||||
Cast Int32 Integer where
|
||||
cast = prim__cast_Int32Integer
|
||||
|
||||
Num Int32 where
|
||||
(+) = prim__add_Int32
|
||||
(*) = prim__mul_Int32
|
||||
fromInteger = prim__cast_IntegerInt32
|
||||
|
||||
Neg Int32 where
|
||||
(-) = prim__sub_Int32
|
||||
negate = prim__sub_Int32 0
|
||||
|
||||
Integral Int32 where
|
||||
div = prim__div_Int32
|
||||
mod = prim__mod_Int32
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Int64
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Show Int64 where
|
||||
show = prim__cast_Int64String
|
||||
|
||||
Cast Int64 Integer where
|
||||
cast = prim__cast_Int64Integer
|
||||
|
||||
Num Int64 where
|
||||
(+) = prim__add_Int64
|
||||
(*) = prim__mul_Int64
|
||||
fromInteger = prim__cast_IntegerInt64
|
||||
|
||||
Neg Int64 where
|
||||
(-) = prim__sub_Int64
|
||||
negate = prim__sub_Int64 0
|
||||
|
||||
Integral Int64 where
|
||||
div = prim__div_Int64
|
||||
mod = prim__mod_Int64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits8
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits8 where
|
||||
(-) = prim__sub_Bits8
|
||||
negate = prim__sub_Bits8 0
|
||||
|
||||
Integral Bits8 where
|
||||
div = prim__div_Bits8
|
||||
mod = prim__mod_Bits8
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits16
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits16 where
|
||||
(-) = prim__sub_Bits16
|
||||
negate = prim__sub_Bits16 0
|
||||
|
||||
Integral Bits16 where
|
||||
div = prim__div_Bits16
|
||||
mod = prim__mod_Bits16
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits32
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits32 where
|
||||
(-) = prim__sub_Bits32
|
||||
negate = prim__sub_Bits32 0
|
||||
|
||||
Integral Bits32 where
|
||||
div = prim__div_Bits32
|
||||
mod = prim__mod_Bits32
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Bits64
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Neg Bits64 where
|
||||
(-) = prim__sub_Bits64
|
||||
negate = prim__sub_Bits64 0
|
||||
|
||||
Integral Bits64 where
|
||||
div = prim__div_Bits64
|
||||
mod = prim__mod_Bits64
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Main
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
main : IO ()
|
||||
main = do traverse_ putStrLn . check $ add int8
|
||||
traverse_ putStrLn . check $ sub int8
|
||||
traverse_ putStrLn . check $ mul int8
|
||||
traverse_ putStrLn . check $ div int8
|
||||
traverse_ putStrLn . check $ mod int8
|
||||
|
||||
traverse_ putStrLn . check $ add int16
|
||||
traverse_ putStrLn . check $ sub int16
|
||||
traverse_ putStrLn . check $ mul int16
|
||||
traverse_ putStrLn . check $ div int16
|
||||
traverse_ putStrLn . check $ mod int16
|
||||
|
||||
traverse_ putStrLn . check $ add int32
|
||||
traverse_ putStrLn . check $ sub int32
|
||||
traverse_ putStrLn . check $ mul int32
|
||||
traverse_ putStrLn . check $ div int32
|
||||
traverse_ putStrLn . check $ mod int32
|
||||
|
||||
traverse_ putStrLn . check $ add int64
|
||||
traverse_ putStrLn . check $ sub int64
|
||||
traverse_ putStrLn . check $ mul int64
|
||||
traverse_ putStrLn . check $ div int64
|
||||
traverse_ putStrLn . check $ mod int64
|
||||
|
||||
traverse_ putStrLn . check $ add int
|
||||
traverse_ putStrLn . check $ sub int
|
||||
traverse_ putStrLn . check $ mul int
|
||||
traverse_ putStrLn . check $ div int
|
||||
traverse_ putStrLn . check $ mod int
|
||||
|
||||
traverse_ putStrLn . check $ add bits8
|
||||
traverse_ putStrLn . check $ sub bits8
|
||||
traverse_ putStrLn . check $ mul bits8
|
||||
traverse_ putStrLn . check $ div bits8
|
||||
traverse_ putStrLn . check $ mod bits8
|
||||
|
||||
traverse_ putStrLn . check $ add bits16
|
||||
traverse_ putStrLn . check $ sub bits16
|
||||
traverse_ putStrLn . check $ mul bits16
|
||||
traverse_ putStrLn . check $ div bits16
|
||||
traverse_ putStrLn . check $ mod bits16
|
||||
|
||||
traverse_ putStrLn . check $ add bits32
|
||||
traverse_ putStrLn . check $ sub bits32
|
||||
traverse_ putStrLn . check $ mul bits32
|
||||
traverse_ putStrLn . check $ div bits32
|
||||
traverse_ putStrLn . check $ mod bits32
|
||||
|
||||
traverse_ putStrLn . check $ add bits64
|
||||
traverse_ putStrLn . check $ sub bits64
|
||||
traverse_ putStrLn . check $ mul bits64
|
||||
traverse_ putStrLn . check $ div bits64
|
||||
traverse_ putStrLn . check $ mod bits64
|
||||
2
tests/node/newints/expected
Normal file
2
tests/node/newints/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building IntOps (IntOps.idr)
|
||||
Main> Main> Bye for now!
|
||||
2
tests/node/newints/input
Normal file
2
tests/node/newints/input
Normal file
@ -0,0 +1,2 @@
|
||||
:exec main
|
||||
:q
|
||||
3
tests/node/newints/run
Normal file
3
tests/node/newints/run
Normal file
@ -0,0 +1,3 @@
|
||||
$1 --cg node --no-banner --no-color --console-width 0 IntOps.idr < input
|
||||
|
||||
rm -rf build
|
||||
@ -2,5 +2,5 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Just [a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [k = Main.Z]) [a = Integer]) 1) (Main.Vect.Nil [a = Integer])))
|
||||
Yaffle> ((Main.MkInfer [a = (Main.List.List Integer)]) (((Main.List.Cons [a = Integer]) 1) (Main.List.Nil [a = Integer])))
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved209 ?Main.{a:62}_[]), ($resolved189 ?Main.{a:62}_[])]
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved383 ?Main.{a:62}_[]), ($resolved363 ?Main.{a:62}_[])]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,7 +2,7 @@ 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} => ($resolved205 {b:27}[1] {a:26}[0] $resolved187 ($resolved196 {a:26}[0]) ($resolved196 {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} => ($resolved379 {b:27}[1] {a:26}[0] $resolved361 ($resolved370 {a:26}[0]) ($resolved370 {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:
|
||||
|
||||
@ -2,6 +2,6 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.lookup: All cases covered
|
||||
Yaffle> Main.lookup':
|
||||
($resolved236 [__] [__] ($resolved202 [__]) {_:62})
|
||||
($resolved410 [__] [__] ($resolved376 [__]) {_:62})
|
||||
Yaffle> Main.lookup'': Calls non covering function Main.lookup'
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -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:191} unifies with ?{P:m:191}_[]
|
||||
Dot2.yaff:15:28--15:30:Pattern variable {P:n:365} unifies with ?{P:m:365}_[]
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot3.yaff:18:1--19:1:When elaborating left hand side of Main.addBaz3:
|
||||
Dot3.yaff:18:10--18:15:Can't match on ($resolved183 ?{P:x:196}_[] ?{P:x:196}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved183 ?Main.{_:13}_[] ?Main.{_:14}_[])
|
||||
Dot3.yaff:18:10--18:15:Can't match on ($resolved357 ?{P:x:370}_[] ?{P:x:370}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved357 ?Main.{_:13}_[] ?Main.{_:14}_[])
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot4.yaff:17:1--18:1:When elaborating left hand side of Main.addBaz4:
|
||||
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:198}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
|
||||
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:372}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user