mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-23 22:22:07 +03:00
[ refactor ] Cleanup integral primops (#1211)
This commit is contained in:
parent
d32daaf36a
commit
bbea929cf3
@ -194,50 +194,64 @@ jsConstant (B32 i) = pure $ show i ++ "n"
|
||||
jsConstant (B64 i) = pure $ show i ++ "n"
|
||||
jsConstant ty = throw (InternalError $ "Unsuported constant " ++ show ty)
|
||||
|
||||
-- Creates the definition of a binary arithmetic operation.
|
||||
-- Rounding / truncation behavior is determined from the
|
||||
-- `IntKind`.
|
||||
arithOp : {auto c : Ref ESs ESSt}
|
||||
-> Maybe IntKind
|
||||
-> (op : String)
|
||||
-> (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
|
||||
|
||||
-- Same as `arithOp` but for bitwise operations that might
|
||||
-- go out of the valid range.
|
||||
bitOp : {auto c : Ref ESs ESSt}
|
||||
-> Maybe IntKind
|
||||
-> (op : String)
|
||||
-> (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
|
||||
|
||||
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
|
||||
|
||||
(Just $ Signed m, Just $ Signed $ P n) =>
|
||||
if P n >= m then pure x else boundedInt (n-1) x
|
||||
|
||||
-- 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
|
||||
|
||||
jsOp : {auto c : Ref ESs ESSt} -> PrimFn arity -> Vect arity String -> Core String
|
||||
jsOp (Add IntType) [x, y] = pure $ !(boundedIntOp 63 "+" x y)
|
||||
jsOp (Sub IntType) [x, y] = pure $ !(boundedIntOp 63 "-" x y)
|
||||
jsOp (Mul IntType) [x, y] = pure $ !(boundedIntOp 63 "*" x y)
|
||||
jsOp (Div IntType) [x, y] = pure $ !(boundedIntOp 63 "/" x y)
|
||||
jsOp (Mod IntType) [x, y] = pure $ !(boundedIntOp 63 "%" x y)
|
||||
jsOp (Add Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "+" x y)
|
||||
jsOp (Sub Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "-" x y)
|
||||
jsOp (Mul Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "*" x y)
|
||||
jsOp (Div Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "/" x y)
|
||||
jsOp (Mod Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "%" x y)
|
||||
jsOp (Add Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "+" x y)
|
||||
jsOp (Sub Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "-" x y)
|
||||
jsOp (Mul Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "*" x y)
|
||||
jsOp (Div Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "/" x y)
|
||||
jsOp (Mod Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "%" x y)
|
||||
jsOp (Add Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "+" x y)
|
||||
jsOp (Sub Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "-" x y)
|
||||
jsOp (Mul Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "*" x y)
|
||||
jsOp (Div Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "/" x y)
|
||||
jsOp (Mod Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "%" x y)
|
||||
jsOp (Add Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "+" x y)
|
||||
jsOp (Sub Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "-" x y)
|
||||
jsOp (Mul Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "*" x y)
|
||||
jsOp (Div Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "/" x y)
|
||||
jsOp (Mod Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "%" x y)
|
||||
jsOp (Add ty) [x, y] = pure $ binOp "+" x y
|
||||
jsOp (Sub ty) [x, y] = pure $ binOp "-" x y
|
||||
jsOp (Mul ty) [x, y] = pure $ binOp "*" x y
|
||||
jsOp (Div ty) [x, y] = pure $ binOp "/" x y
|
||||
jsOp (Mod ty) [x, y] = pure $ binOp "%" x y
|
||||
jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y
|
||||
jsOp (Sub ty) [x, y] = arithOp (intKind ty) "-" x y
|
||||
jsOp (Mul ty) [x, y] = arithOp (intKind ty) "*" x y
|
||||
jsOp (Div ty) [x, y] = arithOp (intKind ty) "/" x y
|
||||
jsOp (Mod ty) [x, y] = arithOp (intKind ty) "%" x y
|
||||
jsOp (Neg ty) [x] = pure $ "(-(" ++ x ++ "))"
|
||||
jsOp (ShiftL IntType) [x, y] = pure $ !(boundedIntBitOp 63 "<<" x y)
|
||||
jsOp (ShiftL Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "<<" x y)
|
||||
jsOp (ShiftL Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "<<" x y)
|
||||
jsOp (ShiftL Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "<<" x y)
|
||||
jsOp (ShiftL Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "<<" x y)
|
||||
jsOp (ShiftL ty) [x, y] = pure $ binOp "<<" x y
|
||||
jsOp (ShiftR IntType) [x, y] = pure $ !(boundedIntBitOp 63 ">>" x y)
|
||||
jsOp (ShiftR Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 ">>" x y)
|
||||
jsOp (ShiftR Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 ">>" x y)
|
||||
jsOp (ShiftR Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 ">>" x y)
|
||||
jsOp (ShiftR Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 ">>" x y)
|
||||
jsOp (ShiftR ty) [x, y] = pure $ binOp ">>" x y
|
||||
jsOp (ShiftL ty) [x, y] = bitOp (intKind ty) "<<" x y
|
||||
jsOp (ShiftR ty) [x, y] = bitOp (intKind ty) ">>" x y
|
||||
jsOp (BAnd ty) [x, y] = pure $ binOp "&" x y
|
||||
jsOp (BOr ty) [x, y] = pure $ binOp "|" x y
|
||||
jsOp (BXOr ty) [x, y] = pure $ binOp "^" x y
|
||||
@ -270,58 +284,20 @@ jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")"
|
||||
jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")"
|
||||
jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")"
|
||||
|
||||
jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
|
||||
jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt 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 IntegerType IntType) [x] = boundedInt 63 x
|
||||
jsOp (Cast IntType IntegerType) [x] = pure x
|
||||
jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"
|
||||
|
||||
jsOp (Cast Bits8Type IntType) [x] = pure x
|
||||
jsOp (Cast Bits16Type IntType) [x] = pure x
|
||||
jsOp (Cast Bits32Type IntType) [x] = pure x
|
||||
jsOp (Cast Bits64Type IntType) [x] = pure x
|
||||
|
||||
jsOp (Cast Bits8Type IntegerType) [x] = pure x
|
||||
jsOp (Cast Bits16Type IntegerType) [x] = pure x
|
||||
jsOp (Cast Bits32Type IntegerType) [x] = pure x
|
||||
jsOp (Cast Bits64Type IntegerType) [x] = pure x
|
||||
|
||||
jsOp (Cast IntType Bits8Type) [x] = boundedUInt 8 x
|
||||
jsOp (Cast IntType Bits16Type) [x] = boundedUInt 16 x
|
||||
jsOp (Cast IntType Bits32Type) [x] = boundedUInt 32 x
|
||||
jsOp (Cast IntType Bits64Type) [x] = boundedUInt 64 x
|
||||
|
||||
jsOp (Cast IntegerType Bits8Type) [x] = boundedUInt 8 x
|
||||
jsOp (Cast IntegerType Bits16Type) [x] = boundedUInt 16 x
|
||||
jsOp (Cast IntegerType Bits32Type) [x] = boundedUInt 32 x
|
||||
jsOp (Cast IntegerType Bits64Type) [x] = boundedUInt 64 x
|
||||
|
||||
jsOp (Cast Bits8Type Bits16Type) [x] = pure x
|
||||
jsOp (Cast Bits8Type Bits32Type) [x] = pure x
|
||||
jsOp (Cast Bits8Type Bits64Type) [x] = pure x
|
||||
|
||||
jsOp (Cast Bits16Type Bits8Type) [x] = boundedUInt 8 x
|
||||
jsOp (Cast Bits16Type Bits32Type) [x] = pure x
|
||||
jsOp (Cast Bits16Type Bits64Type) [x] = pure x
|
||||
|
||||
jsOp (Cast Bits32Type Bits8Type) [x] = boundedUInt 8 x
|
||||
jsOp (Cast Bits32Type Bits16Type) [x] = boundedUInt 16 x
|
||||
jsOp (Cast Bits32Type Bits64Type) [x] = pure x
|
||||
|
||||
jsOp (Cast Bits64Type Bits8Type) [x] = boundedUInt 8 x
|
||||
jsOp (Cast Bits64Type Bits16Type) [x] = boundedUInt 16 x
|
||||
jsOp (Cast Bits64Type Bits32Type) [x] = boundedUInt 32 x
|
||||
|
||||
jsOp (Cast ty StringType) [x] = pure $ "(''+" ++ x ++ ")"
|
||||
jsOp (Cast ty ty2) [x] = jsCrashExp $ jsString $ "invalid cast: + " ++ show ty ++ " + ' -> ' + " ++ show ty2
|
||||
jsOp (Cast ty ty2) [x] = castInt ty ty2 x
|
||||
jsOp BelieveMe [_,_,x] = pure x
|
||||
jsOp (Crash) [_, msg] = jsCrashExp msg
|
||||
|
||||
|
@ -57,41 +57,63 @@ op o args = "(" ++ o ++ " " ++ showSep " " args ++ ")"
|
||||
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 _ 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 _ 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 _ 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 _ 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]
|
||||
|
||||
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)]
|
||||
|
||||
-- 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)]
|
||||
|
||||
(Just $ Signed _, Just $ Unsigned $ P n) =>
|
||||
op "blodwen-toUnsignedInt" [x,show n]
|
||||
|
||||
(Just $ Unsigned m, Just $ Unsigned $ P n) =>
|
||||
if P n >= m then x else op "blodwen-toUnsignedInt" [x,show n]
|
||||
|
||||
_ => "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"
|
||||
|
||||
||| Generate scheme for a primitive function.
|
||||
schOp : PrimFn arity -> Vect arity String -> String
|
||||
schOp (Add IntType) [x, y] = op "b+" [x, y, "63"]
|
||||
schOp (Sub IntType) [x, y] = op "b-" [x, y, "63"]
|
||||
schOp (Mul IntType) [x, y] = op "b*" [x, y, "63"]
|
||||
schOp (Div IntType) [x, y] = op "b/" [x, y, "63"]
|
||||
schOp (Add Bits8Type) [x, y] = op "b+" [x, y, "8"]
|
||||
schOp (Sub Bits8Type) [x, y] = op "b-" [x, y, "8"]
|
||||
schOp (Mul Bits8Type) [x, y] = op "b*" [x, y, "8"]
|
||||
schOp (Div Bits8Type) [x, y] = op "b/" [x, y, "8"]
|
||||
schOp (Add Bits16Type) [x, y] = op "b+" [x, y, "16"]
|
||||
schOp (Sub Bits16Type) [x, y] = op "b-" [x, y, "16"]
|
||||
schOp (Mul Bits16Type) [x, y] = op "b*" [x, y, "16"]
|
||||
schOp (Div Bits16Type) [x, y] = op "b/" [x, y, "16"]
|
||||
schOp (Add Bits32Type) [x, y] = op "b+" [x, y, "32"]
|
||||
schOp (Sub Bits32Type) [x, y] = op "b-" [x, y, "32"]
|
||||
schOp (Mul Bits32Type) [x, y] = op "b*" [x, y, "32"]
|
||||
schOp (Div Bits32Type) [x, y] = op "b/" [x, y, "32"]
|
||||
schOp (Add Bits64Type) [x, y] = op "b+" [x, y, "64"]
|
||||
schOp (Sub Bits64Type) [x, y] = op "b-" [x, y, "64"]
|
||||
schOp (Mul Bits64Type) [x, y] = op "b*" [x, y, "64"]
|
||||
schOp (Div Bits64Type) [x, y] = op "b/" [x, y, "64"]
|
||||
schOp (Add ty) [x, y] = op "+" [x, y]
|
||||
schOp (Sub ty) [x, y] = op "-" [x, y]
|
||||
schOp (Mul ty) [x, y] = op "*" [x, y]
|
||||
schOp (Div IntegerType) [x, y] = op "quotient" [x, y]
|
||||
schOp (Div ty) [x, y] = op "/" [x, y]
|
||||
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 IntType) [x, y] = op "blodwen-bits-shl-signed" [x, y, "63"]
|
||||
schOp (ShiftL Bits8Type) [x, y] = op "blodwen-bits-shl" [x, y, "8"]
|
||||
schOp (ShiftL Bits16Type) [x, y] = op "blodwen-bits-shl" [x, y, "16"]
|
||||
schOp (ShiftL Bits32Type) [x, y] = op "blodwen-bits-shl" [x, y, "32"]
|
||||
schOp (ShiftL Bits64Type) [x, y] = op "blodwen-bits-shl" [x, y, "64"]
|
||||
schOp (ShiftL ty) [x, y] = op "blodwen-shl" [x, y]
|
||||
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]
|
||||
@ -133,67 +155,25 @@ schOp DoubleSqrt [x] = op "flsqrt" [x]
|
||||
schOp DoubleFloor [x] = op "flfloor" [x]
|
||||
schOp DoubleCeiling [x] = op "flceiling" [x]
|
||||
|
||||
schOp (Cast IntType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast IntegerType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits8Type StringType) [x] = op "number->string" [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 DoubleType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast CharType StringType) [x] = op "string" [x]
|
||||
|
||||
schOp (Cast IntType IntegerType) [x] = x
|
||||
schOp (Cast Bits8Type IntegerType) [x] = x
|
||||
schOp (Cast Bits16Type IntegerType) [x] = x
|
||||
schOp (Cast Bits32Type IntegerType) [x] = x
|
||||
schOp (Cast Bits64Type IntegerType) [x] = 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 CharType IntegerType) [x] = op "char->integer" [x]
|
||||
schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]
|
||||
|
||||
schOp (Cast IntegerType IntType) [x] = x
|
||||
schOp (Cast Bits8Type IntType) [x] = x
|
||||
schOp (Cast Bits16Type IntType) [x] = x
|
||||
schOp (Cast Bits32Type IntType) [x] = x
|
||||
schOp (Cast Bits64Type IntType) [x] = x
|
||||
schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x]
|
||||
schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
|
||||
schOp (Cast CharType IntType) [x] = op "char->integer" [x]
|
||||
|
||||
schOp (Cast IntType Bits8Type) [x] = op "integer->bits8" [x]
|
||||
schOp (Cast IntType Bits16Type) [x] = op "integer->bits16" [x]
|
||||
schOp (Cast IntType Bits32Type) [x] = op "integer->bits32" [x]
|
||||
schOp (Cast IntType Bits64Type) [x] = op "integer->bits64" [x]
|
||||
|
||||
schOp (Cast IntegerType Bits8Type) [x] = op "integer->bits8" [x]
|
||||
schOp (Cast IntegerType Bits16Type) [x] = op "integer->bits16" [x]
|
||||
schOp (Cast IntegerType Bits32Type) [x] = op "integer->bits32" [x]
|
||||
schOp (Cast IntegerType Bits64Type) [x] = op "integer->bits64" [x]
|
||||
|
||||
schOp (Cast Bits8Type Bits16Type) [x] = x
|
||||
schOp (Cast Bits8Type Bits32Type) [x] = x
|
||||
schOp (Cast Bits8Type Bits64Type) [x] = x
|
||||
|
||||
schOp (Cast Bits16Type Bits8Type) [x] = op "bits16->bits8" [x]
|
||||
schOp (Cast Bits16Type Bits32Type) [x] = x
|
||||
schOp (Cast Bits16Type Bits64Type) [x] = x
|
||||
|
||||
schOp (Cast Bits32Type Bits8Type) [x] = op "bits32->bits8" [x]
|
||||
schOp (Cast Bits32Type Bits16Type) [x] = op "bits32->bits16" [x]
|
||||
schOp (Cast Bits32Type Bits64Type) [x] = x
|
||||
|
||||
schOp (Cast Bits64Type Bits8Type) [x] = op "bits64->bits8" [x]
|
||||
schOp (Cast Bits64Type Bits16Type) [x] = op "bits64->bits16" [x]
|
||||
schOp (Cast Bits64Type Bits32Type) [x] = op "bits64->bits32" [x]
|
||||
|
||||
|
||||
schOp (Cast 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 IntType DoubleType) [x] = op "exact->inexact" [x]
|
||||
schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]
|
||||
|
||||
schOp (Cast IntType CharType) [x] = op "cast-int-char" [x]
|
||||
|
||||
schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"
|
||||
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 BelieveMe [_,_,x] = x
|
||||
schOp Crash [_,msg] = "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))"
|
||||
|
@ -164,6 +164,36 @@ constTag DoubleType = 11
|
||||
constTag WorldType = 12
|
||||
constTag _ = 0
|
||||
|
||||
||| Precision of integral types.
|
||||
public export
|
||||
data Precision = P Int | Unlimited
|
||||
|
||||
export
|
||||
Eq Precision where
|
||||
(P m) == (P n) = m == n
|
||||
Unlimited == Unlimited = True
|
||||
_ == _ = False
|
||||
|
||||
export
|
||||
Ord Precision where
|
||||
compare (P m) (P n) = compare m n
|
||||
compare Unlimited Unlimited = EQ
|
||||
compare Unlimited _ = GT
|
||||
compare _ Unlimited = LT
|
||||
|
||||
public export
|
||||
data IntKind = Signed Precision | Unsigned Precision
|
||||
|
||||
public export
|
||||
intKind : Constant -> Maybe IntKind
|
||||
intKind IntegerType = Just $ Signed Unlimited
|
||||
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 _ = Nothing
|
||||
|
||||
-- All the internal operators, parameterised by their arity
|
||||
public export
|
||||
data PrimFn : Nat -> Type where
|
||||
|
@ -18,6 +18,9 @@
|
||||
(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))))
|
||||
|
@ -31,6 +31,9 @@
|
||||
`(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))))
|
||||
|
@ -15,6 +15,9 @@
|
||||
(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))))
|
||||
|
@ -9,7 +9,7 @@ large : (a: Type) -> a
|
||||
large Integer = 3518437212345678901234567890123
|
||||
-- int close to 2ˆ63
|
||||
-- we expect some operations will overflow
|
||||
large Int = 3518437212345678901234567890
|
||||
large Int = 9223372036854775800
|
||||
|
||||
small : (a: Type) -> a
|
||||
small Integer = 437
|
||||
|
@ -1,4 +1,4 @@
|
||||
1/1: Building Numbers (Numbers.idr)
|
||||
Main> [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]
|
||||
[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]
|
||||
[369, 9223372036854772792, 9223372036854775423, 24465177816590917, 91]
|
||||
Main> Bye for now!
|
||||
|
Loading…
Reference in New Issue
Block a user