This commit is contained in:
Ruslan Feizerakhmanov 2021-05-06 19:30:50 +03:00
commit d203597eb9
54 changed files with 3115 additions and 424 deletions

View File

@ -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

View File

@ -57,9 +57,9 @@ Ord UsePhase where
where
tag : UsePhase -> Int
tag Cases = 0
tag Lifted = 0
tag ANF = 0
tag VMCode = 0
tag Lifted = 1
tag ANF = 2
tag VMCode = 3
public export
record CompileData where
@ -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

View File

@ -31,13 +31,22 @@ numArgs defs (Ref _ _ n)
case definition gdef of
DCon _ arity Nothing => pure (EraseArgs arity (eraseArgs gdef))
DCon _ arity (Just (_, pos)) => pure (NewTypeBy arity pos)
PMDef _ args _ _ _ => pure (Arity (length args))
PMDef _ args _ _ _ => pure (EraseArgs (length args) (eraseArgs gdef))
ExternDef arity => pure (Arity arity)
ForeignDef arity _ => pure (Arity arity)
Builtin {arity} f => pure (Arity arity)
_ => pure (Arity 0)
numArgs _ tm = pure (Arity 0)
mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** SubVars ns' ns)
mkSub i _ [] = (_ ** SubRefl)
mkSub i [] ns = (_ ** SubRefl)
mkSub i (x :: xs) es
= let (ns' ** p) = mkSub (S i) xs es in
if i `elem` es
then (ns' ** DropCons p)
else (x :: ns' ** KeepCons p)
weakenVar : Var ns -> Var (a :: ns)
weakenVar (MkVar p) = (MkVar (Later p))
@ -98,23 +107,28 @@ applyNewType arity pos fn args
keepArg (CCon fc _ _ args) = keep 0 args
keepArg tm = CErased (getFC fn)
dropFrom : List Nat -> Nat -> List (CExp vs) -> List (CExp vs)
dropFrom epos i [] = []
dropFrom epos i (x :: xs)
= if i `elem` epos
then dropFrom epos (1 + i) xs
else x :: dropFrom epos (1 + i) xs
dropPos : List Nat -> CExp vs -> CExp vs
dropPos epos (CLam fc x sc) = CLam fc x (dropPos epos sc)
dropPos epos (CCon fc c a args) = CCon fc c a (drop 0 args)
where
drop : Nat -> List (CExp vs) -> List (CExp vs)
drop i [] = []
drop i (x :: xs)
= if i `elem` epos
then drop (1 + i) xs
else x :: drop (1 + i) xs
dropPos epos (CApp fc tm@(CApp _ _ _) args')
= CApp fc (dropPos epos tm) args'
dropPos epos (CApp fc f args) = CApp fc f (dropFrom epos 0 args)
dropPos epos (CCon fc c a args) = CCon fc c a (dropFrom epos 0 args)
dropPos epos tm = tm
eraseConArgs : {vars : _} ->
Nat -> List Nat -> CExp vars -> List (CExp vars) -> CExp vars
eraseConArgs arity epos fn args
= let fn' = expandToArity arity fn args in
dropPos epos fn' -- fn' might be lambdas, after eta expansion
if not (isNil epos)
then dropPos epos fn' -- fn' might be lambdas, after eta expansion
else fn'
mkDropSubst : Nat -> List Nat ->
(rest : List Name) ->
@ -638,13 +652,17 @@ getCFTypes args t
= pure (reverse args, !(nfToCFType (getLoc t) False t))
toCDef : {auto c : Ref Ctxt Defs} ->
Name -> ClosedTerm -> Def ->
Name -> ClosedTerm -> List Nat -> Def ->
Core CDef
toCDef n ty None
toCDef n ty _ None
= pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
toCDef n ty (PMDef _ args _ tree _)
= pure $ MkFun _ !(toCExpTree n tree)
toCDef n ty (ExternDef arity)
toCDef n ty erased (PMDef _ args _ tree _)
= do let (args' ** p) = mkSub 0 args erased
comptree <- toCExpTree n tree
if isNil erased
then pure $ MkFun args comptree
else pure $ MkFun args' (shrinkCExp p comptree)
toCDef n ty _ (ExternDef arity)
= let (ns ** args) = mkArgList 0 arity in
pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
where
@ -654,11 +672,11 @@ toCDef n ty (ExternDef arity)
getVars : ArgList k ns -> List (Var ns)
getVars NoArgs = []
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef n ty (ForeignDef arity cs)
toCDef n ty _ (ForeignDef arity cs)
= do defs <- get Ctxt
(atys, retty) <- getCFTypes [] !(nf defs [] ty)
pure $ MkForeign cs atys retty
toCDef n ty (Builtin {arity} op)
toCDef n ty _ (Builtin {arity} op)
= let (ns ** args) = mkArgList 0 arity in
pure $ MkFun _ (COp emptyFC op (map toArgExp (getVars args)))
where
@ -668,7 +686,7 @@ toCDef n ty (Builtin {arity} op)
getVars : ArgList k ns -> Vect k (Var ns)
getVars NoArgs = []
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef n _ (DCon tag arity pos)
toCDef n _ _ (DCon tag arity pos)
= do let nt = snd <$> pos
defs <- get Ctxt
args <- numArgs {vars = []} defs (Ref EmptyFC (DataCon tag arity) n)
@ -677,20 +695,20 @@ toCDef n _ (DCon tag arity pos)
EraseArgs ar erased => ar `minus` length erased
Arity ar => ar
pure $ MkCon (Just tag) arity' nt
toCDef n _ (TCon tag arity _ _ _ _ _ _)
toCDef n _ _ (TCon tag arity _ _ _ _ _ _)
= pure $ MkCon Nothing arity Nothing
-- We do want to be able to compile these, but also report an error at run time
-- (and, TODO: warn at compile time)
toCDef n ty (Hole _ _)
toCDef n ty _ (Hole _ _)
= pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++
show !(getFullName n))
toCDef n ty (Guess _ _ _)
toCDef n ty _ (Guess _ _ _)
= pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++
show !(getFullName n))
toCDef n ty (BySearch _ _ _)
toCDef n ty _ (BySearch _ _ _)
= pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++
show !(getFullName n))
toCDef n ty def
toCDef n ty _ def
= pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++
show (!(getFullName n), def))
@ -709,7 +727,7 @@ compileDef n
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
ce <- toCDef n (type gdef)
ce <- toCDef n (type gdef) (eraseArgs gdef)
!(toFullNames (definition gdef))
setCompiled n ce

View File

@ -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

View File

@ -150,7 +150,7 @@ mutual
-- boost by removing unnecessary lambdas that we'll keep the special case.
eval rec env stk (CRef fc n)
= case (n == NS primIONS (UN "io_bind"), stk) of
(True, _ :: _ :: act :: cont :: world :: stk) =>
(True, act :: cont :: world :: stk) =>
do xn <- genName "act"
sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])
pure $ unload stk $
@ -416,6 +416,43 @@ mergeLam (MkFun args def)
pure $ MkFun args' exp'
mergeLam d = pure d
mutual
addRefs : NameMap Bool -> CExp vars -> NameMap Bool
addRefs ds (CRef _ n) = insert n False ds
addRefs ds (CLam _ _ sc) = addRefs ds sc
addRefs ds (CLet _ _ _ val sc) = addRefs (addRefs ds val) sc
addRefs ds (CApp _ f args) = addRefsArgs (addRefs ds f) args
addRefs ds (CCon _ _ _ args) = addRefsArgs ds args
addRefs ds (COp _ _ args) = addRefsArgs ds (toList args)
addRefs ds (CExtPrim _ _ args) = addRefsArgs ds args
addRefs ds (CForce _ _ e) = addRefs ds e
addRefs ds (CDelay _ _ e) = addRefs ds e
addRefs ds (CConCase _ sc alts def)
= let ds' = maybe ds (addRefs ds) def in
addRefsConAlts (addRefs ds' sc) alts
addRefs ds (CConstCase _ sc alts def)
= let ds' = maybe ds (addRefs ds) def in
addRefsConstAlts (addRefs ds' sc) alts
addRefs ds tm = ds
addRefsArgs : NameMap Bool -> List (CExp vars) -> NameMap Bool
addRefsArgs ds [] = ds
addRefsArgs ds (a :: as) = addRefsArgs (addRefs ds a) as
addRefsConAlts : NameMap Bool -> List (CConAlt vars) -> NameMap Bool
addRefsConAlts ds [] = ds
addRefsConAlts ds (MkConAlt _ _ _ sc :: rest)
= addRefsConAlts (addRefs ds sc) rest
addRefsConstAlts : NameMap Bool -> List (CConstAlt vars) -> NameMap Bool
addRefsConstAlts ds [] = ds
addRefsConstAlts ds (MkConstAlt _ sc :: rest)
= addRefsConstAlts (addRefs ds sc) rest
getRefs : CDef -> NameMap Bool
getRefs (MkFun args exp) = addRefs empty exp
getRefs _ = empty
export
inlineDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
@ -425,6 +462,17 @@ inlineDef n
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(inline n cexpr)
-- Update the names a function refers to at runtime based on the transformation
-- results (saves generating code unnecessarily).
updateCallGraph : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
updateCallGraph n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
let refs = getRefs cexpr
ignore $ addDef n (record { refersToRuntimeM = Just refs } def)
export
fixArityDef : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
@ -462,6 +510,8 @@ compileAndInlineAll
traverse_ mergeLamDef cns
traverse_ caseLamDef cns
traverse_ fixArityDef cns
traverse_ updateCallGraph cns
where
nonErased : Name -> Core Bool
nonErased n

View File

@ -332,7 +332,6 @@ mutual
usedConstAlt : {default Nothing lazy : Maybe LazyReason} ->
Used vars -> LiftedConstAlt vars -> Used vars
usedConstAlt used (MkLConstAlt c sc) = usedVars used sc
usedVars used (LPrimVal _ _) = used
usedVars used (LErased _) = used
usedVars used (LCrash _ _) = used

View File

@ -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) ++ ")"

View File

@ -31,7 +31,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 48
ttcVersion = 49
export
checkTTCVersion : String -> Int -> Int -> Core ()

View File

@ -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

View File

@ -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)
]

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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')

View File

@ -80,12 +80,23 @@ renderHtml (STAnn ann rest) = do
pure $ "<!-- ann ignored START -->" ++ resthtml ++ "<!-- ann END -->"
renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs)
removeNewlinesFromDeclarations : SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
removeNewlinesFromDeclarations = go False
where
go : Bool -> SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
go False l@(STLine i) = l
go True l@(STLine i) = STEmpty
go ignoring (STConcat docs) = STConcat $ map (go ignoring) docs
go _ (STAnn Declarations rest) = STAnn Declarations $ go True rest
go _ (STAnn ann rest) = STAnn ann $ go False rest
go _ doc = doc
docDocToHtml : {auto c : Ref Ctxt Defs} ->
Doc IdrisDocAnn ->
Core String
docDocToHtml doc =
let dt = SimpleDocTree.fromStream $ layoutUnbounded doc in
renderHtml dt
renderHtml $ removeNewlinesFromDeclarations dt
htmlPreamble : String -> String -> String -> String
htmlPreamble title root class = "<!DOCTYPE html><html lang=\"en\"><head><meta charset=\"utf-8\">"

View File

@ -145,18 +145,21 @@ getDocsForName fc n
let root = nameRoot n in
if isOpName n then parens (pretty root) else pretty root
getDConDoc : Name -> Core (List (Doc IdrisDocAnn))
getDConDoc : Name -> Core (Doc IdrisDocAnn)
getDConDoc con
= do defs <- get Ctxt
Just def <- lookupCtxtExact con (gamma defs)
| Nothing => pure []
-- should never happen, since we know that the DCon exists:
| Nothing => pure Empty
syn <- get Syn
let [(n, str)] = lookupName con (docstrings syn)
| _ => pure []
ty <- resugar [] =<< normaliseHoles defs [] (type def)
pure $ pure $ vcat $
annotate (Decl con) (hsep [dCon (prettyName n), colon, prettyTerm ty])
:: reflowDoc str
let conWithTypeDoc = annotate (Decl con) (hsep [dCon (prettyName con), colon, prettyTerm ty])
let [(n, str)] = lookupName con (docstrings syn)
| _ => pure conWithTypeDoc
pure $ vcat
[ conWithTypeDoc
, annotate DocStringBody $ vcat $ reflowDoc str
]
getImplDoc : Name -> Core (List (Doc IdrisDocAnn))
getImplDoc n
@ -242,7 +245,7 @@ getDocsForName fc n
TCon _ _ _ _ _ _ cons _
=> do let tot = [showTotal n (totality d)]
cdocs <- traverse (getDConDoc <=< toFullNames) cons
let cdoc = case concat cdocs of
let cdoc = case cdocs of
[] => []
[doc] => [header "Constructor" <++> annotate Declarations doc]
docs => [vcat [header "Constructors"

View File

@ -655,6 +655,7 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts
optType (DumpVMCode f) = POpt
optType DebugElabCheck = POpt
optType (SetCG f) = POpt
optType (Directive d) = POpt
optType (BuildDir f) = POpt
optType (OutputDir f) = POpt
optType (ConsoleWidth n) = PIgnore
@ -682,6 +683,7 @@ errorMsg = unlines
, " --dumpvmcode <file>"
, " --debug-elab-check"
, " --codegen <cg>"
, " --directive <directive>"
, " --build-dir <dir>"
, " --output-dir <dir>"
]

View File

@ -9,6 +9,8 @@ import Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import Libraries.Utils.Term
import System
getPageWidth : {auto o : Ref ROpts REPLOpts} -> Core PageWidth
getPageWidth = do
consoleWidth <- getConsoleWidth
@ -25,11 +27,16 @@ render : {auto o : Ref ROpts REPLOpts} ->
Doc ann -> Core String
render stylerAnn doc = do
color <- getColor
isDumb <- (Just "dumb" ==) <$> coreLift (getEnv "TERM")
-- ^-- emacs sets the TERM variable to `dumb` and expects the compiler
-- to not emit any ANSI escape codes
pageWidth <- getPageWidth
let opts = MkLayoutOptions pageWidth
let layout = layoutPretty opts doc
pure $ renderString $
if color then reAnnotateS stylerAnn layout else unAnnotateS layout
if color && not isDumb
then reAnnotateS stylerAnn layout
else unAnnotateS layout
export
renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc ann -> Core String

View File

@ -232,4 +232,3 @@ equivTypes ty1 ty2 =
(\err => pure False)
when b $ logTerm "typesearch.equiv" 20 "Accepted: " ty1
pure b

View File

@ -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

View File

@ -13,6 +13,7 @@ import Core.Value
import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.Elab.ImplicitBind
import TTImp.Elab.Utils
import TTImp.TTImp
import TTImp.Utils
@ -205,6 +206,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
(maybe (Bind fc scrn (Pi fc caseRig Explicit scrty)
(weaken caseretty))
(const caseretty) splitOn)
(erasedargs, _) <- findErased casefnty
logEnv "elab.case" 10 "Case env" env
logTermNF "elab.case" 2 ("Case function type: " ++ show casen) [] casefnty
@ -215,8 +217,10 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
-- actually bound! This is rather hacky, but a lot less fiddly than
-- the alternative of fixing up the environment
when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty
cidx <- addDef casen (newDef fc casen (if isErased rigc then erased else top)
[] casefnty vis None)
cidx <- addDef casen (record { eraseArgs = erasedargs }
(newDef fc casen (if isErased rigc then erased else top)
[] casefnty vis None))
-- don't worry about totality of the case block; it'll be handled
-- by the totality of the parent function
setFlag fc (Resolved cidx) (SetTotal PartialOK)

View File

@ -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)

View File

@ -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)))))

View File

@ -94,7 +94,7 @@ p {
}
.decls {
margin-top: 15px;
margin-top: 5px;
}
.decls > dt {
@ -111,7 +111,7 @@ p {
}
.decls > dd {
margin: 10px 0 10px 20px;
margin: 10px 0 20px 20px;
font-family: Arial, sans-serif;
font-size: 10pt;
}

View File

@ -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)

View File

@ -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)))))

View File

@ -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
View 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

View File

@ -0,0 +1,2 @@
1/1: Building Casts (Casts.idr)
Main> Main> Bye for now!

2
tests/chez/casts/input Normal file
View File

@ -0,0 +1,2 @@
:exec main
:q

3
tests/chez/casts/run Normal file
View File

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

View 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

View File

@ -0,0 +1,2 @@
1/1: Building IntOps (IntOps.idr)
Main> Main> Bye for now!

2
tests/chez/newints/input Normal file
View File

@ -0,0 +1,2 @@
:exec main
:q

3
tests/chez/newints/run Normal file
View File

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

View File

@ -2,35 +2,13 @@ Dumping case trees to Main.cases
prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
prim__lte_Integer = [{arg:N}, {arg:N}]: (<=Integer [!{arg:N}, !{arg:N}])
prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
Main.plus = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N})] Just (%let {e:N} (-Integer [!{arg:N}, 1]) (+Integer [1, (Main.plus [!{e:N}, !{arg:N}])])))
Main.main = [{ext:N}]: (Main.plus [(+Integer [1, 0]), (+Integer [1, (+Integer [1, 0])])])
Main.Z = Constructor tag Just 1 arity 0
Main.S = Constructor tag Just 0 arity 1
Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
Prelude.Basics.True = Constructor tag Just 0 arity 0
Prelude.Basics.False = Constructor tag Just 1 arity 0
Builtin.believe_me = [{arg:N}, {arg:N}, {ext:N}]: (believe_me [___, ___, !{ext:N}])
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [___, ___, !{arg:N}])), (%constcase 1 0)] Nothing)
Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [!{arg:N}])), (%constcase 1 0)] Nothing)
Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
Prelude.Types.Z = Constructor tag Just 0 arity 0
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
Prelude.Interfaces.pure = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, ___, !{arg:N}])
PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
PrimIO.case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [___, ___, ___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{arg:N}])])
PrimIO.unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeCreateWorld [___, (%lam w (PrimIO.case block in unsafePerformIO [___, !{arg:N}, ___, (!{arg:N} [!w])]))])
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}, {arg:N}]: !{arg:N}
PrimIO.unsafeCreateWorld = [{arg:N}, {arg:N}]: (!{arg:N} [%MkWorld])
PrimIO.io_pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
PrimIO.io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (PrimIO.case block in io_bind [___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{ext:N}])])
PrimIO.MkIORes = Constructor tag Just 0 arity 3 (newtype by 1)
PrimIO.MkIO = Constructor tag Just 0 arity 2 (newtype by 1)
Prelude.IO.pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
Prelude.IO.map = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (!{arg:N} [!{act:N}]))
Prelude.IO.Functor implementation at Prelude/IO.idr:L:C--L:C = [{ext:N}, {ext:N}, {ext:N}, {ext:N}, {ext:N}]: (Prelude.IO.map [___, ___, !{ext:N}, !{ext:N}, !{ext:N}])
Prelude.IO.Applicative implementation at Prelude/IO.idr:L:C--L:C = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam b (%lam a (%lam func (%lam {arg:N} (%lam {eta:N} (Prelude.IO.map [___, ___, !func, !{arg:N}, !{eta:N}])))))), (%lam a (%lam {arg:N} (%lam {eta:N} !{arg:N}))), (%lam b (%lam a (%lam {arg:N} (%lam {arg:N} (%lam {eta:N} (%let {act:N} (!{arg:N} [!{eta:N}]) (%let {act:N} (!{arg:N} [!{eta:N}]) (!{act:N} [!{act:N}]))))))))])
Prelude.IO.<*> = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (%let {act:N} (!{arg:N} [!{ext:N}]) (!{act:N} [!{act:N}])))
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}
PrimIO.unsafeCreateWorld = [{arg:N}]: (!{arg:N} [%MkWorld])

View File

@ -1,84 +1,32 @@
Dumping case trees to Main.cases
prim__add_Int = [{arg:N}, {arg:N}]: (+Int [!{arg:N}, !{arg:N}])
prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
prim__sub_Int = [{arg:N}, {arg:N}]: (-Int [!{arg:N}, !{arg:N}])
prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
prim__mul_Int = [{arg:N}, {arg:N}]: (*Int [!{arg:N}, !{arg:N}])
prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
prim__div_Int = [{arg:N}, {arg:N}]: (/Int [!{arg:N}, !{arg:N}])
prim__mod_Int = [{arg:N}, {arg:N}]: (%Int [!{arg:N}, !{arg:N}])
prim__lt_Int = [{arg:N}, {arg:N}]: (<Int [!{arg:N}, !{arg:N}])
prim__lte_Int = [{arg:N}, {arg:N}]: (<=Int [!{arg:N}, !{arg:N}])
prim__lte_Integer = [{arg:N}, {arg:N}]: (<=Integer [!{arg:N}, !{arg:N}])
prim__eq_Int = [{arg:N}, {arg:N}]: (==Int [!{arg:N}, !{arg:N}])
prim__gte_Int = [{arg:N}, {arg:N}]: (>=Int [!{arg:N}, !{arg:N}])
prim__gt_Int = [{arg:N}, {arg:N}]: (>Int [!{arg:N}, !{arg:N}])
prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
prim__crash = [{arg:N}, {arg:N}]: (crash [!{arg:N}, !{arg:N}])
prim__cast_IntegerInt = [{arg:N}]: (cast-Integer-Int [!{arg:N}])
Main.main = [{ext:N}]: (Prelude.Interfaces.sum [___, ___, (%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [___, ___, ___, !{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [___, (%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
Main.main = [{ext:N}]: (Prelude.Interfaces.sum [(%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [(%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
Prelude.Basics.not = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 0)] Nothing)
Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
Prelude.Basics.flip = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: ((!{arg:N} [!{arg:N}]) [!{arg:N}])
Prelude.Basics.True = Constructor tag Just 0 arity 0
Prelude.Basics.False = Constructor tag Just 1 arity 0
Prelude.Basics.Bool = Constructor tag Nothing arity 0
Prelude.Basics.&& = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%force Lazy !{arg:N})), (%constcase 1 1)] Nothing)
Builtin.snd = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
Builtin.idris_crash = [{arg:N}, {ext:N}]: (crash [___, !{ext:N}])
Builtin.fst = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
Builtin.believe_me = [{arg:N}, {arg:N}, {ext:N}]: (believe_me [___, ___, !{ext:N}])
Builtin.assert_total = [{arg:N}, {arg:N}]: !{arg:N}
Builtin.MkPair = Constructor tag Just 0 arity 2
Prelude.Types.case block in rangeFromThen = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])), (%constcase 1 (Prelude.Types.countFrom [___, !{arg:N}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))]))] Nothing)
Prelude.Types.case block in case block in case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.Nil Just 0 []))] Nothing)
Prelude.Types.case block in case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in case block in rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (Prelude.Basics.&& [(%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing), (%delay Lazy (%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing))])]))] Nothing)
Prelude.Types.case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)]))] Nothing)
Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam x (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [___, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
Prelude.Types.case block in takeBefore = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.Nil Just 0 [])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeBefore [___, !{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
Prelude.Types.case block in takeUntil = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeUntil [___, !{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [___, ___, !{arg:N}])), (%constcase 1 0)] Nothing)
Prelude.Types.rangeFrom = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]) [!{arg:N}]))] Nothing))])
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [___, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
Prelude.Types.rangeFromThen = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromThen [___, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
Prelude.Types.rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)])
Prelude.Types.null = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 1))] Nothing)
Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [___, ___, !{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [___, ___, !{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [___, ___, (%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [___, ___, ___, !{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing), !{ext:N}])
Prelude.Types.Range at Prelude/Types.idr:L:C--L:C = Constructor tag Just 0 arity 4
Prelude.Types.Range implementation at Prelude/Types.idr:L:C--L:C = [{arg:N}, {arg:N}]: (%con Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromTo [___, !{arg:N}, !{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}])))), (%lam {arg:N} (Prelude.Types.rangeFrom [___, !{arg:N}, !{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThen [___, !{arg:N}, !{arg:N}, !{arg:N}])))])
Prelude.Types.Foldable implementation at Prelude/Types.idr:L:C--L:C = []: (%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [___, ___, ___, !{i_con:N}, !funcM, !init, !input]))))))))])
Prelude.Types.takeUntil = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeUntil [___, !{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
Prelude.Types.takeBefore = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeBefore [___, !{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.Basics.flip = [{arg:N}, {arg:N}, {arg:N}]: ((!{arg:N} [!{arg:N}]) [!{arg:N}])
Builtin.snd = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
Builtin.idris_crash = [{ext:N}]: (crash [___, !{ext:N}])
Builtin.fst = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam x (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
Prelude.Types.case block in takeUntil = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeUntil [!{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [!{arg:N}])), (%constcase 1 0)] Nothing)
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
Prelude.Types.null = [{arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 1))] Nothing)
Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [!{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [!{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [(%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [!{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing), !{ext:N}])
Prelude.Types.takeUntil = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeUntil [!{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
Prelude.Types.countFrom = [{arg:N}, {arg:N}, {arg:N}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [___, (!{arg:N} [!{arg:N}]), !{arg:N}]))])
Prelude.Types.Z = Constructor tag Just 0 arity 0
Prelude.Types.Stream.Stream = Constructor tag Nothing arity 1
Prelude.Types.Nil = Constructor tag Just 0 arity 0
Prelude.Types.:: = Constructor tag Just 1 arity 2
Prelude.Types.Stream.:: = Constructor tag Just 0 arity 2
Prelude.Num.case block in mod = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (%Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in mod at Prelude/Num.idr:L:C--L:C"]))
Prelude.Num.case block in div = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (/Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in div at Prelude/Num.idr:L:C--L:C"]))
Prelude.Types.countFrom = [{arg:N}, {arg:N}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [(!{arg:N} [!{arg:N}]), !{arg:N}]))])
Prelude.Num.case block in mod = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (%Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash ["Unhandled input for Prelude.Num.case block in mod at Prelude/Num.idr:L:C--L:C"]))
Prelude.Num.case block in div = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (/Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash ["Unhandled input for Prelude.Num.case block in div at Prelude/Num.idr:L:C--L:C"]))
Prelude.Num.negate = [{arg:N}]: (-Int [0, !{arg:N}])
Prelude.Num.mod = [{arg:N}, {arg:N}]: (Prelude.Num.case block in mod [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])])])
Prelude.Num.fromInteger = [{ext:N}]: (cast-Integer-Int [!{ext:N}])
Prelude.Num.div = [{arg:N}, {arg:N}]: (Prelude.Num.case block in div [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])])])
Prelude.Num.Num at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
Prelude.Num.Constraint (Num ty) = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing)
Prelude.Num.Num implementation at Prelude/Num.idr:L:C--L:C = []: (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])
Prelude.Num.Neg implementation at Prelude/Num.idr:L:C--L:C = []: (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])
Prelude.Num.Integral implementation at Prelude/Num.idr:L:C--L:C = []: (%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))])
Prelude.Num.- = [{ext:N}, {ext:N}]: (-Int [!{ext:N}, !{ext:N}])
Prelude.Num.+ = [{ext:N}, {ext:N}]: (+Int [!{ext:N}, !{ext:N}])
Prelude.Num.* = [{ext:N}, {ext:N}]: (*Int [!{ext:N}, !{ext:N}])
Prelude.Num.fromInteger = [{arg:N}, {arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [!{ext:N}]))] Nothing)
Prelude.Num.- = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.Num.+ = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.EqOrd.case block in case block in compare = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 2)] Nothing)
Prelude.EqOrd.case block in compare = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 0), (%constcase 1 (Prelude.EqOrd.case block in case block in compare [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, !{arg:N}])]))] Nothing)
Prelude.EqOrd.case block in max = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N}), (%constcase 1 !{arg:N})] Nothing)
@ -86,47 +34,15 @@ Prelude.EqOrd.case block in min = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [
Prelude.EqOrd.min = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in min [!{arg:N}, !{arg:N}, (Prelude.EqOrd.< [!{arg:N}, !{arg:N}])])
Prelude.EqOrd.max = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in max [!{arg:N}, !{arg:N}, (Prelude.EqOrd.> [!{arg:N}, !{arg:N}])])
Prelude.EqOrd.compare = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in compare [!{arg:N}, !{arg:N}, (Prelude.EqOrd.< [!{arg:N}, !{arg:N}])])
Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C = Constructor tag Just 0 arity 8
Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C = Constructor tag Just 0 arity 2
Prelude.EqOrd.Constraint (Eq ty) = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] !{e:N})] Nothing)
Prelude.EqOrd.Ord implementation at Prelude/EqOrd.idr:L:C--L:C = []: (%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))])
Prelude.EqOrd.Eq implementation at Prelude/EqOrd.idr:L:C--L:C = []: (%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))])
Prelude.EqOrd.> = [{arg:N}, {arg:N}]: (%case (>Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.>= = [{arg:N}, {arg:N}]: (%case (>=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case (==Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.< = [{arg:N}, {arg:N}]: (%case (<Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.<= = [{arg:N}, {arg:N}]: (%case (<=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd./= = [{arg:N}, {arg:N}]: (Prelude.Basics.not [(Prelude.EqOrd.== [!{arg:N}, !{arg:N}])])
Prelude.EqOrd.LT = Constructor tag Just 0 arity 0
Prelude.EqOrd.GT = Constructor tag Just 2 arity 0
Prelude.EqOrd.EQ = Constructor tag Just 1 arity 0
Prelude.EqOrd.>= = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.EqOrd.> = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.EqOrd.== = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.EqOrd.<= = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.EqOrd.< = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 4
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
Prelude.Interfaces.Constraint (Applicative m) = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing)
Prelude.Interfaces.sum = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case (Builtin.fst [___, ___, !{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
Prelude.Interfaces.pure = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
Prelude.Interfaces.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
Prelude.Interfaces.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
Prelude.Interfaces.>>= = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]))] Nothing)
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, ___, !{arg:N}])
PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
PrimIO.case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [___, ___, ___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{arg:N}])])
PrimIO.unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeCreateWorld [___, (%lam w (PrimIO.case block in unsafePerformIO [___, !{arg:N}, ___, (!{arg:N} [!w])]))])
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}, {arg:N}]: !{arg:N}
PrimIO.unsafeCreateWorld = [{arg:N}, {arg:N}]: (!{arg:N} [%MkWorld])
PrimIO.io_pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
PrimIO.io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (PrimIO.case block in io_bind [___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{ext:N}])])
PrimIO.MkIORes = Constructor tag Just 0 arity 3 (newtype by 1)
PrimIO.MkIO = Constructor tag Just 0 arity 2 (newtype by 1)
Prelude.IO.pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
Prelude.IO.map = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (!{arg:N} [!{act:N}]))
Prelude.IO.Functor implementation at Prelude/IO.idr:L:C--L:C = [{ext:N}, {ext:N}, {ext:N}, {ext:N}, {ext:N}]: (Prelude.IO.map [___, ___, !{ext:N}, !{ext:N}, !{ext:N}])
Prelude.IO.Applicative implementation at Prelude/IO.idr:L:C--L:C = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam b (%lam a (%lam func (%lam {arg:N} (%lam {eta:N} (Prelude.IO.map [___, ___, !func, !{arg:N}, !{eta:N}])))))), (%lam a (%lam {arg:N} (%lam {eta:N} !{arg:N}))), (%lam b (%lam a (%lam {arg:N} (%lam {arg:N} (%lam {eta:N} (%let {act:N} (!{arg:N} [!{eta:N}]) (%let {act:N} (!{arg:N} [!{eta:N}]) (!{act:N} [!{act:N}]))))))))])
Prelude.IO.<*> = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (%let {act:N} (!{arg:N} [!{ext:N}]) (!{act:N} [!{act:N}])))
Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}
PrimIO.unsafeCreateWorld = [{arg:N}]: (!{arg:N} [%MkWorld])

View File

@ -13,6 +13,16 @@ export
hello : Int -> Int
hello x = x*2
public export
data WrappedInt : Type where
MkWrappedInt : Int -> WrappedInt
public export
record SimpleRec where
constructor MkSimpleRec
a : Int
b : String
namespace NS
namespace NestedNS

View File

@ -1,9 +1,22 @@
1/1: Building Doc (Doc.idr)
Doc> hello : Int -> Int
Doc> MkSimpleRec : Int -> String -> SimpleRec
MkWrappedInt : Int -> WrappedInt
SimpleRec : Type
WrappedInt : Type
a : SimpleRec -> Int
b : SimpleRec -> String
hello : Int -> Int
Hello!
world : Nat -> Nat
World!
Doc> Doc.NS.NestedNS.Foo : Type
A type of Foo
Doc> Doc.WrappedInt : Type
Totality: total
Constructor: MkWrappedInt : Int -> WrappedInt
Doc> Doc.SimpleRec : Type
Totality: total
Constructor: MkSimpleRec : Int -> String -> SimpleRec
Doc> Bye for now!

View File

@ -1,3 +1,5 @@
:browse Doc
:doc Foo
:doc WrappedInt
:doc SimpleRec
:q

View File

@ -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

View File

@ -11,6 +11,7 @@ Overridable options are:
--dumpvmcode <file>
--debug-elab-check
--codegen <cg>
--directive <directive>
--build-dir <dir>
--output-dir <dir>

690
tests/node/casts/Casts.idr Normal file
View 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

View File

@ -0,0 +1,2 @@
1/1: Building Casts (Casts.idr)
Main> Main> Bye for now!

2
tests/node/casts/input Normal file
View File

@ -0,0 +1,2 @@
:exec main
:q

3
tests/node/casts/run Normal file
View File

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

View 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

View File

@ -0,0 +1,2 @@
1/1: Building IntOps (IntOps.idr)
Main> Main> Bye for now!

2
tests/node/newints/input Normal file
View File

@ -0,0 +1,2 @@
:exec main
:q

3
tests/node/newints/run Normal file
View File

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

View File

@ -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!

View File

@ -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:

View File

@ -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!

View File

@ -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!