mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-01 16:12:26 +03:00
Edwin Brady
GitHub
commit
7944da4121
12
CHANGELOG.md
12
CHANGELOG.md
@ -1,3 +1,15 @@
|
||||
Changes since Idris 2 v0.2.0
|
||||
----------------------------
|
||||
|
||||
Language changes:
|
||||
|
||||
* `Bits8`, `Bits16`, `Bits32` and `Bits64` primitive types added, with:
|
||||
+ `Num`, `Eq`, `Ord` and `Show` implementations.
|
||||
+ Casts from `Integer`, for literals
|
||||
+ Casts to `Int` (except `Bits64` which might not fit), `Integer` and `String`
|
||||
+ Passed to C FFI as `unsigned`
|
||||
+ Primitives added in `Data.Buffer`
|
||||
|
||||
Changes since Idris 2 v0.1.0
|
||||
----------------------------
|
||||
|
||||
|
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
@ -32,6 +32,8 @@ freeBuffer buf = pure ()
|
||||
|
||||
%foreign "scheme:blodwen-buffer-setbyte"
|
||||
prim__setByte : Buffer -> Int -> Int -> PrimIO ()
|
||||
%foreign "scheme:blodwen-buffer-setbyte"
|
||||
prim__setBits8 : Buffer -> Int -> Bits8 -> PrimIO ()
|
||||
|
||||
-- Assumes val is in the range 0-255
|
||||
export
|
||||
@ -39,14 +41,74 @@ setByte : Buffer -> (loc : Int) -> (val : Int) -> IO ()
|
||||
setByte buf loc val
|
||||
= primIO (prim__setByte buf loc val)
|
||||
|
||||
export
|
||||
setBits8 : Buffer -> (loc : Int) -> (val : Bits8) -> IO ()
|
||||
setBits8 buf loc val
|
||||
= primIO (prim__setBits8 buf loc val)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-getbyte"
|
||||
prim__getByte : Buffer -> Int -> PrimIO Int
|
||||
%foreign "scheme:blodwen-buffer-getbyte"
|
||||
prim__getBits8 : Buffer -> Int -> PrimIO Bits8
|
||||
|
||||
export
|
||||
getByte : Buffer -> (loc : Int) -> IO Int
|
||||
getByte buf loc
|
||||
= primIO (prim__getByte buf loc)
|
||||
|
||||
export
|
||||
getBits8 : Buffer -> (loc : Int) -> IO Bits8
|
||||
getBits8 buf loc
|
||||
= primIO (prim__getBits8 buf loc)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-setbits16"
|
||||
prim__setBits16 : Buffer -> Int -> Bits16 -> PrimIO ()
|
||||
|
||||
export
|
||||
setBits16 : Buffer -> (loc : Int) -> (val : Bits16) -> IO ()
|
||||
setBits16 buf loc val
|
||||
= primIO (prim__setBits16 buf loc val)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-getbits16"
|
||||
prim__getBits16 : Buffer -> Int -> PrimIO Bits16
|
||||
|
||||
export
|
||||
getBits16 : Buffer -> (loc : Int) -> IO Bits16
|
||||
getBits16 buf loc
|
||||
= primIO (prim__getBits16 buf loc)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-setbits32"
|
||||
prim__setBits32 : Buffer -> Int -> Bits32 -> PrimIO ()
|
||||
|
||||
export
|
||||
setBits32 : Buffer -> (loc : Int) -> (val : Bits32) -> IO ()
|
||||
setBits32 buf loc val
|
||||
= primIO (prim__setBits32 buf loc val)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-getbits32"
|
||||
prim__getBits32 : Buffer -> Int -> PrimIO Bits32
|
||||
|
||||
export
|
||||
getBits32 : Buffer -> (loc : Int) -> IO Bits32
|
||||
getBits32 buf loc
|
||||
= primIO (prim__getBits32 buf loc)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-setbits64"
|
||||
prim__setBits64 : Buffer -> Int -> Bits64 -> PrimIO ()
|
||||
|
||||
export
|
||||
setBits64 : Buffer -> (loc : Int) -> (val : Bits64) -> IO ()
|
||||
setBits64 buf loc val
|
||||
= primIO (prim__setBits64 buf loc val)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-getbits64"
|
||||
prim__getBits64 : Buffer -> Int -> PrimIO Bits64
|
||||
|
||||
export
|
||||
getBits64 : Buffer -> (loc : Int) -> IO Bits64
|
||||
getBits64 buf loc
|
||||
= primIO (prim__getBits64 buf loc)
|
||||
|
||||
%foreign "scheme:blodwen-buffer-setint32"
|
||||
prim__setInt32 : Buffer -> Int -> Int -> PrimIO ()
|
||||
|
||||
|
||||
@ -213,6 +213,22 @@ public export
|
||||
Eq Integer where
|
||||
x == y = intToBool (prim__eq_Integer x y)
|
||||
|
||||
public export
|
||||
Eq Bits8 where
|
||||
x == y = intToBool (prim__eq_Bits8 x y)
|
||||
|
||||
public export
|
||||
Eq Bits16 where
|
||||
x == y = intToBool (prim__eq_Bits16 x y)
|
||||
|
||||
public export
|
||||
Eq Bits32 where
|
||||
x == y = intToBool (prim__eq_Bits32 x y)
|
||||
|
||||
public export
|
||||
Eq Bits64 where
|
||||
x == y = intToBool (prim__eq_Bits64 x y)
|
||||
|
||||
public export
|
||||
Eq Double where
|
||||
x == y = intToBool (prim__eq_Double x y)
|
||||
@ -291,6 +307,42 @@ Ord Integer where
|
||||
(>) x y = intToBool (prim__gt_Integer x y)
|
||||
(>=) x y = intToBool (prim__gte_Integer x y)
|
||||
|
||||
public export
|
||||
Ord Bits8 where
|
||||
compare x y = if x < y then LT else if x == y then EQ else GT
|
||||
|
||||
(<) x y = intToBool (prim__lt_Bits8 x y)
|
||||
(<=) x y = intToBool (prim__lte_Bits8 x y)
|
||||
(>) x y = intToBool (prim__gt_Bits8 x y)
|
||||
(>=) x y = intToBool (prim__gte_Bits8 x y)
|
||||
|
||||
public export
|
||||
Ord Bits16 where
|
||||
compare x y = if x < y then LT else if x == y then EQ else GT
|
||||
|
||||
(<) x y = intToBool (prim__lt_Bits16 x y)
|
||||
(<=) x y = intToBool (prim__lte_Bits16 x y)
|
||||
(>) x y = intToBool (prim__gt_Bits16 x y)
|
||||
(>=) x y = intToBool (prim__gte_Bits16 x y)
|
||||
|
||||
public export
|
||||
Ord Bits32 where
|
||||
compare x y = if x < y then LT else if x == y then EQ else GT
|
||||
|
||||
(<) x y = intToBool (prim__lt_Bits32 x y)
|
||||
(<=) x y = intToBool (prim__lte_Bits32 x y)
|
||||
(>) x y = intToBool (prim__gt_Bits32 x y)
|
||||
(>=) x y = intToBool (prim__gte_Bits32 x y)
|
||||
|
||||
public export
|
||||
Ord Bits64 where
|
||||
compare x y = if x < y then LT else if x == y then EQ else GT
|
||||
|
||||
(<) x y = intToBool (prim__lt_Bits64 x y)
|
||||
(<=) x y = intToBool (prim__lte_Bits64 x y)
|
||||
(>) x y = intToBool (prim__gt_Bits64 x y)
|
||||
(>=) x y = intToBool (prim__gte_Bits64 x y)
|
||||
|
||||
public export
|
||||
Ord Double where
|
||||
compare x y = if x < y then LT else if x == y then EQ else GT
|
||||
@ -434,6 +486,42 @@ Integral Int where
|
||||
= case y == 0 of
|
||||
False => prim__mod_Int x y
|
||||
|
||||
-- Bits8
|
||||
|
||||
%inline
|
||||
public export
|
||||
Num Bits8 where
|
||||
(+) = prim__add_Bits8
|
||||
(*) = prim__mul_Bits8
|
||||
fromInteger = prim__cast_IntegerBits8
|
||||
|
||||
-- Bits16
|
||||
|
||||
%inline
|
||||
public export
|
||||
Num Bits16 where
|
||||
(+) = prim__add_Bits16
|
||||
(*) = prim__mul_Bits16
|
||||
fromInteger = prim__cast_IntegerBits16
|
||||
|
||||
-- Bits32
|
||||
|
||||
%inline
|
||||
public export
|
||||
Num Bits32 where
|
||||
(+) = prim__add_Bits32
|
||||
(*) = prim__mul_Bits32
|
||||
fromInteger = prim__cast_IntegerBits32
|
||||
|
||||
-- Bits64
|
||||
|
||||
%inline
|
||||
public export
|
||||
Num Bits64 where
|
||||
(+) = prim__add_Bits64
|
||||
(*) = prim__mul_Bits64
|
||||
fromInteger = prim__cast_IntegerBits64
|
||||
|
||||
-- Double
|
||||
|
||||
public export
|
||||
@ -1346,6 +1434,22 @@ export
|
||||
Show Integer where
|
||||
showPrec = primNumShow prim__cast_IntegerString
|
||||
|
||||
export
|
||||
Show Bits8 where
|
||||
showPrec = primNumShow prim__cast_Bits8String
|
||||
|
||||
export
|
||||
Show Bits16 where
|
||||
showPrec = primNumShow prim__cast_Bits16String
|
||||
|
||||
export
|
||||
Show Bits32 where
|
||||
showPrec = primNumShow prim__cast_Bits32String
|
||||
|
||||
export
|
||||
Show Bits64 where
|
||||
showPrec = primNumShow prim__cast_Bits64String
|
||||
|
||||
export
|
||||
Show Double where
|
||||
showPrec = primNumShow prim__cast_DoubleString
|
||||
|
||||
@ -501,6 +501,10 @@ getNArgs defs n args = pure $ User n args
|
||||
nfToCFType : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> (inStruct : Bool) -> NF [] -> Core CFType
|
||||
nfToCFType _ _ (NPrimVal _ IntType) = pure CFInt
|
||||
nfToCFType _ _ (NPrimVal _ Bits8Type) = pure CFUnsigned
|
||||
nfToCFType _ _ (NPrimVal _ Bits16Type) = pure CFUnsigned
|
||||
nfToCFType _ _ (NPrimVal _ Bits32Type) = pure CFUnsigned
|
||||
nfToCFType _ _ (NPrimVal _ Bits64Type) = pure CFUnsigned
|
||||
nfToCFType _ False (NPrimVal _ StringType) = pure CFString
|
||||
nfToCFType fc True (NPrimVal _ StringType)
|
||||
= throw (GenericMsg fc "String not allowed in a foreign struct")
|
||||
|
||||
@ -166,6 +166,7 @@ data Structs : Type where
|
||||
cftySpec : FC -> CFType -> Core String
|
||||
cftySpec fc CFUnit = pure "void"
|
||||
cftySpec fc CFInt = pure "int"
|
||||
cftySpec fc CFUnsigned = pure "unsigned"
|
||||
cftySpec fc CFString = pure "string"
|
||||
cftySpec fc CFDouble = pure "double"
|
||||
cftySpec fc CFChar = pure "char"
|
||||
|
||||
@ -63,6 +63,22 @@ schOp (Add IntType) [x, y] = op "b+" [x, y, "63"]
|
||||
schOp (Sub IntType) [x, y] = op "b-" [x, y, "63"]
|
||||
schOp (Mul IntType) [x, y] = op "b*" [x, y, "63"]
|
||||
schOp (Div IntType) [x, y] = op "b/" [x, y, "63"]
|
||||
schOp (Add Bits8Type) [x, y] = op "b+" [x, y, "8"]
|
||||
schOp (Sub Bits8Type) [x, y] = op "b-" [x, y, "8"]
|
||||
schOp (Mul Bits8Type) [x, y] = op "b*" [x, y, "8"]
|
||||
schOp (Div Bits8Type) [x, y] = op "b/" [x, y, "8"]
|
||||
schOp (Add Bits16Type) [x, y] = op "b+" [x, y, "16"]
|
||||
schOp (Sub Bits16Type) [x, y] = op "b-" [x, y, "16"]
|
||||
schOp (Mul Bits16Type) [x, y] = op "b*" [x, y, "16"]
|
||||
schOp (Div Bits16Type) [x, y] = op "b/" [x, y, "16"]
|
||||
schOp (Add Bits32Type) [x, y] = op "b+" [x, y, "32"]
|
||||
schOp (Sub Bits32Type) [x, y] = op "b-" [x, y, "32"]
|
||||
schOp (Mul Bits32Type) [x, y] = op "b*" [x, y, "32"]
|
||||
schOp (Div Bits32Type) [x, y] = op "b/" [x, y, "32"]
|
||||
schOp (Add Bits64Type) [x, y] = op "b+" [x, y, "64"]
|
||||
schOp (Sub Bits64Type) [x, y] = op "b-" [x, y, "64"]
|
||||
schOp (Mul Bits64Type) [x, y] = op "b*" [x, y, "64"]
|
||||
schOp (Div Bits64Type) [x, y] = op "b/" [x, y, "64"]
|
||||
schOp (Add ty) [x, y] = op "+" [x, y]
|
||||
schOp (Sub ty) [x, y] = op "-" [x, y]
|
||||
schOp (Mul ty) [x, y] = op "*" [x, y]
|
||||
@ -70,6 +86,11 @@ schOp (Div IntegerType) [x, y] = op "quotient" [x, y]
|
||||
schOp (Div ty) [x, y] = op "/" [x, y]
|
||||
schOp (Mod ty) [x, y] = op "remainder" [x, y]
|
||||
schOp (Neg ty) [x] = op "-" [x]
|
||||
schOp (ShiftL IntType) [x, y] = op "blodwen-bits-shl" [x, y, "63"]
|
||||
schOp (ShiftL Bits8Type) [x, y] = op "blodwen-bits-shl" [x, y, "8"]
|
||||
schOp (ShiftL Bits16Type) [x, y] = op "blodwen-bits-shl" [x, y, "16"]
|
||||
schOp (ShiftL Bits32Type) [x, y] = op "blodwen-bits-shl" [x, y, "32"]
|
||||
schOp (ShiftL Bits64Type) [x, y] = op "blodwen-bits-shl" [x, y, "64"]
|
||||
schOp (ShiftL ty) [x, y] = op "blodwen-shl" [x, y]
|
||||
schOp (ShiftR ty) [x, y] = op "blodwen-shr" [x, y]
|
||||
schOp (BAnd ty) [x, y] = op "blodwen-and" [x, y]
|
||||
@ -114,19 +135,35 @@ schOp DoubleCeiling [x] = op "ceiling" [x]
|
||||
|
||||
schOp (Cast IntType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast IntegerType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits8Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits16Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits32Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast Bits64Type StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast DoubleType StringType) [x] = op "number->string" [x]
|
||||
schOp (Cast CharType StringType) [x] = op "string" [x]
|
||||
|
||||
schOp (Cast IntType IntegerType) [x] = x
|
||||
schOp (Cast Bits8Type IntegerType) [x] = x
|
||||
schOp (Cast Bits16Type IntegerType) [x] = x
|
||||
schOp (Cast Bits32Type IntegerType) [x] = x
|
||||
schOp (Cast Bits64Type IntegerType) [x] = x
|
||||
schOp (Cast DoubleType IntegerType) [x] = op "exact-floor" [x]
|
||||
schOp (Cast CharType IntegerType) [x] = op "char->integer" [x]
|
||||
schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]
|
||||
|
||||
schOp (Cast IntegerType IntType) [x] = x
|
||||
schOp (Cast Bits8Type IntType) [x] = x
|
||||
schOp (Cast Bits16Type IntType) [x] = x
|
||||
schOp (Cast Bits32Type IntType) [x] = x
|
||||
schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x]
|
||||
schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
|
||||
schOp (Cast CharType IntType) [x] = op "char->integer" [x]
|
||||
|
||||
schOp (Cast IntegerType Bits8Type) [x] = op "integer->bits8" [x]
|
||||
schOp (Cast IntegerType Bits16Type) [x] = op "integer->bits16" [x]
|
||||
schOp (Cast IntegerType Bits32Type) [x] = op "integer->bits32" [x]
|
||||
schOp (Cast IntegerType Bits64Type) [x] = op "integer->bits64" [x]
|
||||
|
||||
schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x]
|
||||
schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x]
|
||||
schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]
|
||||
@ -192,6 +229,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 _ (BI x) = show x
|
||||
schConstant _ (B8 x) = show x
|
||||
schConstant _ (B16 x) = show x
|
||||
schConstant _ (B32 x) = show x
|
||||
schConstant _ (B64 x) = show x
|
||||
schConstant schString (Str x) = schString x
|
||||
schConstant _ (Ch x)
|
||||
= if (the Int (cast x) >= 32 && the Int (cast x) < 127)
|
||||
@ -201,6 +242,10 @@ schConstant _ (Db x) = show x
|
||||
schConstant _ WorldVal = "#f"
|
||||
schConstant _ IntType = "#t"
|
||||
schConstant _ IntegerType = "#t"
|
||||
schConstant _ Bits8Type = "#t"
|
||||
schConstant _ Bits16Type = "#t"
|
||||
schConstant _ Bits32Type = "#t"
|
||||
schConstant _ Bits64Type = "#t"
|
||||
schConstant _ StringType = "#t"
|
||||
schConstant _ CharType = "#t"
|
||||
schConstant _ DoubleType = "#t"
|
||||
|
||||
@ -126,6 +126,7 @@ data Structs : Type where
|
||||
cftySpec : FC -> CFType -> Core String
|
||||
cftySpec fc CFUnit = pure "void"
|
||||
cftySpec fc CFInt = pure "int"
|
||||
cftySpec fc CFUnsigned = pure "unsigned-int"
|
||||
cftySpec fc CFString = pure "UTF-8-string"
|
||||
cftySpec fc CFDouble = pure "double"
|
||||
cftySpec fc CFChar = pure "char"
|
||||
|
||||
@ -108,6 +108,7 @@ data Done : Type where
|
||||
cftySpec : FC -> CFType -> Core String
|
||||
cftySpec fc CFUnit = pure "_void"
|
||||
cftySpec fc CFInt = pure "_int"
|
||||
cftySpec fc CFUnsigned = pure "_uint"
|
||||
cftySpec fc CFString = pure "_string/utf-8"
|
||||
cftySpec fc CFDouble = pure "_double"
|
||||
cftySpec fc CFChar = pure "_int8"
|
||||
|
||||
@ -30,7 +30,7 @@ import Data.Buffer
|
||||
-- TTC files can only be compatible if the version number is the same
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 31
|
||||
ttcVersion = 32
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
|
||||
@ -111,6 +111,7 @@ public export
|
||||
data CFType : Type where
|
||||
CFUnit : CFType
|
||||
CFInt : CFType
|
||||
CFUnsigned : CFType
|
||||
CFString : CFType
|
||||
CFDouble : CFType
|
||||
CFChar : CFType
|
||||
@ -290,6 +291,7 @@ export
|
||||
Show CFType where
|
||||
show CFUnit = "Unit"
|
||||
show CFInt = "Int"
|
||||
show CFUnsigned = "Bits_n"
|
||||
show CFString = "String"
|
||||
show CFDouble = "Double"
|
||||
show CFChar = "Char"
|
||||
|
||||
@ -103,6 +103,10 @@ mutual
|
||||
chkConstant : FC -> Constant -> Term vars
|
||||
chkConstant fc (I x) = PrimVal fc IntType
|
||||
chkConstant fc (BI x) = PrimVal fc IntegerType
|
||||
chkConstant fc (B8 x) = PrimVal fc Bits8Type
|
||||
chkConstant fc (B16 x) = PrimVal fc Bits16Type
|
||||
chkConstant fc (B32 x) = PrimVal fc Bits32Type
|
||||
chkConstant fc (B64 x) = PrimVal fc Bits64Type
|
||||
chkConstant fc (Str x) = PrimVal fc StringType
|
||||
chkConstant fc (Ch x) = PrimVal fc CharType
|
||||
chkConstant fc (Db x) = PrimVal fc DoubleType
|
||||
|
||||
@ -33,12 +33,20 @@ unaryOp _ _ = Nothing
|
||||
castString : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castString [NPrimVal fc (I 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)))
|
||||
castString [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString [NPrimVal fc (Ch i)] = Just (NPrimVal fc (Str (stripQuotes (show i))))
|
||||
castString [NPrimVal fc (Db i)] = Just (NPrimVal fc (Str (show i)))
|
||||
castString _ = Nothing
|
||||
|
||||
castInteger : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castInteger [NPrimVal fc (I i)] = Just (NPrimVal fc (BI (cast 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)))
|
||||
castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI i))
|
||||
castInteger [NPrimVal fc (Ch i)] = Just (NPrimVal fc (BI (cast (cast {to=Int} i))))
|
||||
castInteger [NPrimVal fc (Db i)] = Just (NPrimVal fc (BI (cast i)))
|
||||
castInteger [NPrimVal fc (Str i)] = Just (NPrimVal fc (BI (cast i)))
|
||||
@ -46,11 +54,46 @@ castInteger _ = Nothing
|
||||
|
||||
castInt : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (fromInteger i)))
|
||||
castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I i))
|
||||
castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I i))
|
||||
castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I i))
|
||||
castInt [NPrimVal fc (Db i)] = Just (NPrimVal fc (I (cast i)))
|
||||
castInt [NPrimVal fc (Ch i)] = Just (NPrimVal fc (I (cast i)))
|
||||
castInt [NPrimVal fc (Str i)] = Just (NPrimVal fc (I (cast i)))
|
||||
castInt _ = Nothing
|
||||
|
||||
castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castBits8 [NPrimVal fc (BI i)]
|
||||
= let max = prim__shl_Int 1 8 in
|
||||
if i > 0 -- oops, we don't have `rem` yet!
|
||||
then Just (NPrimVal fc (B8 (fromInteger i `mod` max)))
|
||||
else Just (NPrimVal fc (B8 (max + fromInteger i `mod` max)))
|
||||
castBits8 _ = Nothing
|
||||
|
||||
castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castBits16 [NPrimVal fc (BI i)]
|
||||
= let max = prim__shl_Int 1 16 in
|
||||
if i > 0 -- oops, we don't have `rem` yet!
|
||||
then Just (NPrimVal fc (B16 (fromInteger i `mod` max)))
|
||||
else Just (NPrimVal fc (B16 (max + fromInteger i `mod` max)))
|
||||
castBits16 _ = Nothing
|
||||
|
||||
castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castBits32 [NPrimVal fc (BI i)]
|
||||
= let max = prim__shl_Int 1 32 in
|
||||
if i > 0 -- oops, we don't have `rem` yet!
|
||||
then Just (NPrimVal fc (B32 (fromInteger i `mod` max)))
|
||||
else Just (NPrimVal fc (B32 (max + fromInteger i `mod` max)))
|
||||
castBits32 _ = Nothing
|
||||
|
||||
castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castBits64 [NPrimVal fc (BI i)]
|
||||
= let max = prim__shl_Integer 1 64 in
|
||||
if i > 0 -- oops, we don't have `rem` yet!
|
||||
then Just (NPrimVal fc (B64 (i `mod` max)))
|
||||
else Just (NPrimVal fc (B64 (max + i `mod` max)))
|
||||
castBits64 _ = Nothing
|
||||
|
||||
castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castDouble [NPrimVal fc (I i)] = Just (NPrimVal fc (Db (cast i)))
|
||||
castDouble [NPrimVal fc (BI i)] = Just (NPrimVal fc (Db (cast i)))
|
||||
@ -107,6 +150,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 (B8 x) (B8 y) = pure $ B8 $ (x + y)
|
||||
add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` (prim__shl_Int 1 16)
|
||||
add (B32 x) (B32 y) = pure $ B32 $ (x + y) `mod` (prim__shl_Int 1 32)
|
||||
add (B64 x) (B64 y) = pure $ B64 $ (x + y) `mod` (prim__shl_Integer 1 64)
|
||||
add (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x + cast y))
|
||||
add (Db x) (Db y) = pure $ Db (x + y)
|
||||
add _ _ = Nothing
|
||||
@ -120,6 +167,10 @@ sub _ _ = Nothing
|
||||
|
||||
mul : Constant -> Constant -> Maybe Constant
|
||||
mul (BI x) (BI y) = pure $ BI (x * y)
|
||||
mul (B8 x) (B8 y) = pure $ B8 $ (x * y) `mod` (prim__shl_Int 1 8)
|
||||
mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` (prim__shl_Int 1 16)
|
||||
mul (B32 x) (B32 y) = pure $ B32 $ (x * y) `mod` (prim__shl_Int 1 32)
|
||||
mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` (prim__shl_Integer 1 64)
|
||||
mul (I x) (I y) = pure $ I (x * y)
|
||||
mul (Db x) (Db y) = pure $ Db (x * y)
|
||||
mul _ _ = Nothing
|
||||
@ -142,25 +193,44 @@ mod _ _ = Nothing
|
||||
shiftl : Constant -> Constant -> Maybe Constant
|
||||
shiftl (I x) (I y) = pure $ I (shiftL x y)
|
||||
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` (prim__shl_Int 1 8)
|
||||
shiftl (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 16)
|
||||
shiftl (B32 x) (B32 y) = pure $ B32 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 32)
|
||||
shiftl (B64 x) (B64 y) = pure $ B64 $ (prim__shl_Integer x y) `mod` (prim__shl_Integer 1 64)
|
||||
shiftl _ _ = Nothing
|
||||
|
||||
shiftr : Constant -> Constant -> Maybe Constant
|
||||
shiftr (I x) (I y) = pure $ I (shiftR x y)
|
||||
shiftr (BI x) (BI y) = pure $ BI (prim__shr_Integer x y)
|
||||
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)
|
||||
shiftr (B64 x) (B64 y) = pure $ B64 $ (prim__shr_Integer x y)
|
||||
shiftr _ _ = Nothing
|
||||
|
||||
band : Constant -> Constant -> Maybe Constant
|
||||
band (I x) (I y) = pure $ I (prim__and_Int 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)
|
||||
band (B32 x) (B32 y) = pure $ B32 (prim__and_Int x y)
|
||||
band (B64 x) (B64 y) = pure $ B64 (prim__and_Integer x y)
|
||||
band _ _ = Nothing
|
||||
|
||||
bor : Constant -> Constant -> Maybe Constant
|
||||
bor (I x) (I y) = pure $ I (prim__or_Int 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)
|
||||
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
|
||||
|
||||
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)
|
||||
bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Int x y)
|
||||
bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Int x y)
|
||||
bxor _ _ = Nothing
|
||||
|
||||
neg : Constant -> Maybe Constant
|
||||
@ -176,6 +246,10 @@ toInt False = I 0
|
||||
lt : Constant -> Constant -> Maybe Constant
|
||||
lt (I x) (I 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)
|
||||
lt (B32 x) (B32 y) = pure $ toInt (x < y)
|
||||
lt (B64 x) (B64 y) = pure $ toInt (x < y)
|
||||
lt (Str x) (Str y) = pure $ toInt (x < y)
|
||||
lt (Ch x) (Ch y) = pure $ toInt (x < y)
|
||||
lt (Db x) (Db y) = pure $ toInt (x < y)
|
||||
@ -184,6 +258,10 @@ lt _ _ = Nothing
|
||||
lte : Constant -> Constant -> Maybe Constant
|
||||
lte (I x) (I 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)
|
||||
lte (B32 x) (B32 y) = pure $ toInt (x <= y)
|
||||
lte (B64 x) (B64 y) = pure $ toInt (x <= y)
|
||||
lte (Str x) (Str y) = pure $ toInt (x <= y)
|
||||
lte (Ch x) (Ch y) = pure $ toInt (x <= y)
|
||||
lte (Db x) (Db y) = pure $ toInt (x <= y)
|
||||
@ -192,6 +270,10 @@ lte _ _ = Nothing
|
||||
eq : Constant -> Constant -> Maybe Constant
|
||||
eq (I x) (I 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)
|
||||
eq (B32 x) (B32 y) = pure $ toInt (x == y)
|
||||
eq (B64 x) (B64 y) = pure $ toInt (x == y)
|
||||
eq (Str x) (Str y) = pure $ toInt (x == y)
|
||||
eq (Ch x) (Ch y) = pure $ toInt (x == y)
|
||||
eq (Db x) (Db y) = pure $ toInt (x == y)
|
||||
@ -200,6 +282,10 @@ eq _ _ = Nothing
|
||||
gte : Constant -> Constant -> Maybe Constant
|
||||
gte (I x) (I 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)
|
||||
gte (B32 x) (B32 y) = pure $ toInt (x >= y)
|
||||
gte (B64 x) (B64 y) = pure $ toInt (x >= y)
|
||||
gte (Str x) (Str y) = pure $ toInt (x >= y)
|
||||
gte (Ch x) (Ch y) = pure $ toInt (x >= y)
|
||||
gte (Db x) (Db y) = pure $ toInt (x >= y)
|
||||
@ -208,6 +294,10 @@ gte _ _ = Nothing
|
||||
gt : Constant -> Constant -> Maybe Constant
|
||||
gt (I x) (I 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)
|
||||
gt (B32 x) (B32 y) = pure $ toInt (x > y)
|
||||
gt (B64 x) (B64 y) = pure $ toInt (x > y)
|
||||
gt (Str x) (Str y) = pure $ toInt (x > y)
|
||||
gt (Ch x) (Ch y) = pure $ toInt (x > y)
|
||||
gt (Db x) (Db y) = pure $ toInt (x > y)
|
||||
@ -297,6 +387,10 @@ crashTy
|
||||
castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castTo IntType = castInt
|
||||
castTo IntegerType = castInteger
|
||||
castTo Bits8Type = castBits8
|
||||
castTo Bits16Type = castBits16
|
||||
castTo Bits32Type = castBits32
|
||||
castTo Bits64Type = castBits64
|
||||
castTo StringType = castString
|
||||
castTo CharType = castChar
|
||||
castTo DoubleType = castDouble
|
||||
@ -397,24 +491,24 @@ opName Crash = prim $ "crash"
|
||||
export
|
||||
allPrimitives : List Prim
|
||||
allPrimitives =
|
||||
map (\t => MkPrim (Add t) (arithTy t) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
|
||||
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, DoubleType] ++
|
||||
map (\t => MkPrim (Div t) (arithTy t) notCovering) [IntType, IntegerType, DoubleType] ++
|
||||
map (\t => MkPrim (Mod t) (arithTy t) notCovering) [IntType, IntegerType] ++
|
||||
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] ++
|
||||
map (\t => MkPrim (ShiftR t) (arithTy t) isTotal) [IntType, IntegerType] ++
|
||||
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 (BAnd t) (arithTy t) isTotal) [IntType, IntegerType] ++
|
||||
map (\t => MkPrim (BOr t) (arithTy t) isTotal) [IntType, IntegerType] ++
|
||||
map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType] ++
|
||||
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, Bits8Type, Bits16Type, Bits32Type] ++
|
||||
|
||||
map (\t => MkPrim (LT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
|
||||
map (\t => MkPrim (LTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
|
||||
map (\t => MkPrim (EQ t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
|
||||
map (\t => MkPrim (GTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
|
||||
map (\t => MkPrim (GT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
|
||||
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] ++
|
||||
|
||||
[MkPrim StrLength (predTy StringType IntType) isTotal,
|
||||
MkPrim StrHead (predTy StringType CharType) notCovering,
|
||||
@ -439,8 +533,13 @@ allPrimitives =
|
||||
MkPrim DoubleFloor doubleTy isTotal,
|
||||
MkPrim DoubleCeiling doubleTy isTotal] ++
|
||||
|
||||
map (\t => MkPrim (Cast t StringType) (predTy t StringType) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Cast t IntegerType) (predTy t IntegerType) isTotal) [StringType, IntType, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Cast t StringType) (predTy t StringType) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Cast t IntegerType) (predTy t IntegerType) isTotal) [StringType, IntType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, Bits8Type, Bits16Type, Bits32Type, CharType, DoubleType] ++
|
||||
map (\t => MkPrim (Cast t 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 CharType) (predTy t CharType) isTotal) [StringType, IntType] ++
|
||||
|
||||
map (\t => MkPrim (Cast t Bits8Type) (predTy t Bits8Type) isTotal) [IntegerType] ++
|
||||
map (\t => MkPrim (Cast t Bits16Type) (predTy t Bits16Type) isTotal) [IntegerType] ++
|
||||
map (\t => MkPrim (Cast t Bits32Type) (predTy t Bits32Type) isTotal) [IntegerType] ++
|
||||
map (\t => MkPrim (Cast t Bits64Type) (predTy t Bits64Type) isTotal) [IntegerType]
|
||||
|
||||
@ -285,6 +285,18 @@ Reify Constant where
|
||||
(NS _ (UN "BI"), [x])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (BI x')
|
||||
(NS _ (UN "B8"), [x])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (B8 x')
|
||||
(NS _ (UN "B16"), [x])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (B16 x')
|
||||
(NS _ (UN "B32"), [x])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (B32 x')
|
||||
(NS _ (UN "B64"), [x])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (B64 x')
|
||||
(NS _ (UN "Str"), [x])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (Str x')
|
||||
@ -300,6 +312,14 @@ Reify Constant where
|
||||
=> pure IntType
|
||||
(NS _ (UN "IntegerType"), [])
|
||||
=> pure IntegerType
|
||||
(NS _ (UN "Bits8Type"), [])
|
||||
=> pure Bits8Type
|
||||
(NS _ (UN "Bits16Type"), [])
|
||||
=> pure Bits16Type
|
||||
(NS _ (UN "Bits32Type"), [])
|
||||
=> pure Bits32Type
|
||||
(NS _ (UN "Bits64Type"), [])
|
||||
=> pure Bits64Type
|
||||
(NS _ (UN "StringType"), [])
|
||||
=> pure StringType
|
||||
(NS _ (UN "CharType"), [])
|
||||
@ -319,6 +339,18 @@ Reflect Constant where
|
||||
reflect fc defs env (BI x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflectiontt "BI") [x']
|
||||
reflect fc defs env (B8 x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflectiontt "B8") [x']
|
||||
reflect fc defs env (B16 x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflectiontt "B16") [x']
|
||||
reflect fc defs env (B32 x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflectiontt "B32") [x']
|
||||
reflect fc defs env (B64 x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflectiontt "B64") [x']
|
||||
reflect fc defs env (Str x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflectiontt "Str") [x']
|
||||
@ -334,6 +366,14 @@ Reflect Constant where
|
||||
= getCon fc defs (reflectiontt "IntType")
|
||||
reflect fc defs env IntegerType
|
||||
= getCon fc defs (reflectiontt "IntegerType")
|
||||
reflect fc defs env Bits8Type
|
||||
= getCon fc defs (reflectiontt "Bits8Type")
|
||||
reflect fc defs env Bits16Type
|
||||
= getCon fc defs (reflectiontt "Bits16Type")
|
||||
reflect fc defs env Bits32Type
|
||||
= getCon fc defs (reflectiontt "Bits32Type")
|
||||
reflect fc defs env Bits64Type
|
||||
= getCon fc defs (reflectiontt "Bits64Type")
|
||||
reflect fc defs env StringType
|
||||
= getCon fc defs (reflectiontt "StringType")
|
||||
reflect fc defs env CharType
|
||||
|
||||
@ -24,6 +24,11 @@ public export
|
||||
data Constant
|
||||
= I Int
|
||||
| BI Integer
|
||||
| B8 Int -- For now, since we don't have Bits types. We need to
|
||||
-- make sure the Integer remains in range
|
||||
| B16 Int
|
||||
| B32 Int
|
||||
| B64 Integer
|
||||
| Str String
|
||||
| Ch Char
|
||||
| Db Double
|
||||
@ -31,6 +36,10 @@ data Constant
|
||||
|
||||
| IntType
|
||||
| IntegerType
|
||||
| Bits8Type
|
||||
| Bits16Type
|
||||
| Bits32Type
|
||||
| Bits64Type
|
||||
| StringType
|
||||
| CharType
|
||||
| DoubleType
|
||||
@ -64,12 +73,20 @@ export
|
||||
Show Constant where
|
||||
show (I x) = show x
|
||||
show (BI x) = show x
|
||||
show (B8 x) = show x
|
||||
show (B16 x) = show x
|
||||
show (B32 x) = show x
|
||||
show (B64 x) = show x
|
||||
show (Str x) = show x
|
||||
show (Ch x) = show x
|
||||
show (Db x) = show x
|
||||
show WorldVal = "%MkWorld"
|
||||
show IntType = "Int"
|
||||
show IntegerType = "Integer"
|
||||
show Bits8Type = "Bits8"
|
||||
show Bits16Type = "Bits16"
|
||||
show Bits32Type = "Bits32"
|
||||
show Bits64Type = "Bits64"
|
||||
show StringType = "String"
|
||||
show CharType = "Char"
|
||||
show DoubleType = "Double"
|
||||
@ -79,12 +96,20 @@ export
|
||||
Eq Constant where
|
||||
(I x) == (I y) = x == y
|
||||
(BI x) == (BI y) = x == y
|
||||
(B8 x) == (B8 y) = x == y
|
||||
(B16 x) == (B16 y) = x == y
|
||||
(B32 x) == (B32 y) = x == y
|
||||
(B64 x) == (B64 y) = x == y
|
||||
(Str x) == (Str y) = x == y
|
||||
(Ch x) == (Ch y) = x == y
|
||||
(Db x) == (Db y) = x == y
|
||||
WorldVal == WorldVal = True
|
||||
IntType == IntType = True
|
||||
IntegerType == IntegerType = True
|
||||
Bits8Type == Bits8Type = True
|
||||
Bits16Type == Bits16Type = True
|
||||
Bits32Type == Bits32Type = True
|
||||
Bits64Type == Bits64Type = True
|
||||
StringType == StringType = True
|
||||
CharType == CharType = True
|
||||
DoubleType == DoubleType = True
|
||||
@ -97,10 +122,14 @@ constTag : Constant -> Int
|
||||
-- 1 = ->, 2 = Type
|
||||
constTag IntType = 3
|
||||
constTag IntegerType = 4
|
||||
constTag StringType = 5
|
||||
constTag CharType = 6
|
||||
constTag DoubleType = 7
|
||||
constTag WorldType = 8
|
||||
constTag Bits8Type = 5
|
||||
constTag Bits16Type = 6
|
||||
constTag Bits32Type = 7
|
||||
constTag Bits64Type = 8
|
||||
constTag StringType = 9
|
||||
constTag CharType = 10
|
||||
constTag DoubleType = 11
|
||||
constTag WorldType = 12
|
||||
constTag _ = 0
|
||||
|
||||
-- All the internal operators, parameterised by their arity
|
||||
|
||||
@ -107,32 +107,48 @@ export
|
||||
TTC Constant where
|
||||
toBuf b (I x) = do tag 0; toBuf b x
|
||||
toBuf b (BI x) = do tag 1; toBuf b x
|
||||
toBuf b (Str x) = do tag 2; toBuf b x
|
||||
toBuf b (Ch x) = do tag 3; toBuf b x
|
||||
toBuf b (Db x) = do tag 4; toBuf b x
|
||||
toBuf b (B8 x) = do tag 2; toBuf b x
|
||||
toBuf b (B16 x) = do tag 3; toBuf b x
|
||||
toBuf b (B32 x) = do tag 4; toBuf b x
|
||||
toBuf b (B64 x) = do tag 5; toBuf b x
|
||||
toBuf b (Str x) = do tag 6; toBuf b x
|
||||
toBuf b (Ch x) = do tag 7; toBuf b x
|
||||
toBuf b (Db x) = do tag 8; toBuf b x
|
||||
|
||||
toBuf b WorldVal = tag 5
|
||||
toBuf b IntType = tag 6
|
||||
toBuf b IntegerType = tag 7
|
||||
toBuf b StringType = tag 8
|
||||
toBuf b CharType = tag 9
|
||||
toBuf b DoubleType = tag 10
|
||||
toBuf b WorldType = tag 11
|
||||
toBuf b WorldVal = tag 9
|
||||
toBuf b IntType = tag 10
|
||||
toBuf b IntegerType = tag 11
|
||||
toBuf b Bits8Type = tag 12
|
||||
toBuf b Bits16Type = tag 13
|
||||
toBuf b Bits32Type = tag 14
|
||||
toBuf b Bits64Type = tag 15
|
||||
toBuf b StringType = tag 16
|
||||
toBuf b CharType = tag 17
|
||||
toBuf b DoubleType = tag 18
|
||||
toBuf b WorldType = tag 19
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
0 => do x <- fromBuf b; pure (I x)
|
||||
1 => do x <- fromBuf b; pure (BI x)
|
||||
2 => do x <- fromBuf b; pure (Str x)
|
||||
3 => do x <- fromBuf b; pure (Ch x)
|
||||
4 => do x <- fromBuf b; pure (Db x)
|
||||
5 => pure WorldVal
|
||||
6 => pure IntType
|
||||
7 => pure IntegerType
|
||||
8 => pure StringType
|
||||
9 => pure CharType
|
||||
10 => pure DoubleType
|
||||
11 => pure WorldType
|
||||
2 => do x <- fromBuf b; pure (B8 x)
|
||||
3 => do x <- fromBuf b; pure (B16 x)
|
||||
4 => do x <- fromBuf b; pure (B32 x)
|
||||
5 => do x <- fromBuf b; pure (B64 x)
|
||||
6 => do x <- fromBuf b; pure (Str x)
|
||||
7 => do x <- fromBuf b; pure (Ch x)
|
||||
8 => do x <- fromBuf b; pure (Db x)
|
||||
9 => pure WorldVal
|
||||
10 => pure IntType
|
||||
11 => pure IntegerType
|
||||
12 => pure Bits8Type
|
||||
13 => pure Bits16Type
|
||||
14 => pure Bits32Type
|
||||
15 => pure Bits64Type
|
||||
16 => pure StringType
|
||||
17 => pure CharType
|
||||
18 => pure DoubleType
|
||||
19 => pure WorldType
|
||||
_ => corrupt "Constant"
|
||||
|
||||
export
|
||||
@ -662,29 +678,31 @@ export
|
||||
TTC CFType where
|
||||
toBuf b CFUnit = tag 0
|
||||
toBuf b CFInt = tag 1
|
||||
toBuf b CFString = tag 2
|
||||
toBuf b CFDouble = tag 3
|
||||
toBuf b CFChar = tag 4
|
||||
toBuf b CFPtr = tag 5
|
||||
toBuf b CFWorld = tag 6
|
||||
toBuf b (CFFun s t) = do tag 7; toBuf b s; toBuf b t
|
||||
toBuf b (CFIORes t) = do tag 8; toBuf b t
|
||||
toBuf b (CFStruct n a) = do tag 9; toBuf b n; toBuf b a
|
||||
toBuf b (CFUser n a) = do tag 10; toBuf b n; toBuf b a
|
||||
toBuf b CFUnsigned = tag 2
|
||||
toBuf b CFString = tag 3
|
||||
toBuf b CFDouble = tag 4
|
||||
toBuf b CFChar = tag 5
|
||||
toBuf b CFPtr = tag 6
|
||||
toBuf b CFWorld = tag 7
|
||||
toBuf b (CFFun s t) = do tag 8; toBuf b s; toBuf b t
|
||||
toBuf b (CFIORes t) = do tag 9; toBuf b t
|
||||
toBuf b (CFStruct n a) = do tag 10; toBuf b n; toBuf b a
|
||||
toBuf b (CFUser n a) = do tag 11; toBuf b n; toBuf b a
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
0 => pure CFUnit
|
||||
1 => pure CFInt
|
||||
2 => pure CFString
|
||||
3 => pure CFDouble
|
||||
4 => pure CFChar
|
||||
5 => pure CFPtr
|
||||
6 => pure CFWorld
|
||||
7 => do s <- fromBuf b; t <- fromBuf b; pure (CFFun s t)
|
||||
8 => do t <- fromBuf b; pure (CFIORes t)
|
||||
9 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
|
||||
10 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
|
||||
2 => pure CFUnsigned
|
||||
3 => pure CFString
|
||||
4 => pure CFDouble
|
||||
5 => pure CFChar
|
||||
6 => pure CFPtr
|
||||
7 => pure CFWorld
|
||||
8 => do s <- fromBuf b; t <- fromBuf b; pure (CFFun s t)
|
||||
9 => do t <- fromBuf b; pure (CFIORes t)
|
||||
10 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
|
||||
11 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
|
||||
_ => corrupt "CFType"
|
||||
|
||||
export
|
||||
|
||||
@ -167,16 +167,17 @@ perror (BadUnboundImplicit _ env n ty)
|
||||
= pure $ "Can't bind name " ++ nameRoot n ++ " with type " ++ !(pshow env ty)
|
||||
++ " here. Try binding explicitly."
|
||||
perror (CantSolveGoal _ env g)
|
||||
= let (_ ** (env', g')) = dropPis env g in
|
||||
= let (_ ** (env', g')) = dropEnv env g in
|
||||
pure $ "Can't find an implementation for " ++ !(pshow env' g')
|
||||
where
|
||||
-- For display, we don't want to see the full top level type; just the
|
||||
-- return type
|
||||
dropPis : {vars : _} ->
|
||||
dropEnv : {vars : _} ->
|
||||
Env Term vars -> Term vars ->
|
||||
(ns ** (Env Term ns, Term ns))
|
||||
dropPis env (Bind _ n b@(Pi _ _ _) sc) = dropPis (b :: env) sc
|
||||
dropPis env tm = (_ ** (env, tm))
|
||||
dropEnv env (Bind _ n b@(Pi _ _ _) sc) = dropEnv (b :: env) sc
|
||||
dropEnv env (Bind _ n b@(Let _ _ _) sc) = dropEnv (b :: env) sc
|
||||
dropEnv env tm = (_ ** (env, tm))
|
||||
|
||||
perror (DeterminingArg _ n i env g)
|
||||
= pure $ "Can't find an implementation for " ++ !(pshow env g) ++ "\n" ++
|
||||
|
||||
@ -44,6 +44,10 @@ constant
|
||||
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
|
||||
_ => Nothing)
|
||||
|
||||
@ -160,8 +164,8 @@ holeName
|
||||
|
||||
reservedNames : List String
|
||||
reservedNames
|
||||
= ["Type", "Int", "Integer", "String", "Char", "Double",
|
||||
"Lazy", "Inf", "Force", "Delay"]
|
||||
= ["Type", "Int", "Integer", "Bits8", "Bits16", "Bits32", "Bits64",
|
||||
"String", "Char", "Double", "Lazy", "Inf", "Force", "Delay"]
|
||||
|
||||
export
|
||||
name : Rule Name
|
||||
|
||||
@ -8,6 +8,10 @@ export
|
||||
checkPrim : FC -> Constant -> (Term vars, Term vars)
|
||||
checkPrim fc (I i) = (PrimVal fc (I i), PrimVal fc IntType)
|
||||
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)
|
||||
checkPrim fc (B32 i) = (PrimVal fc (B32 i), PrimVal fc Bits32Type)
|
||||
checkPrim fc (B64 i) = (PrimVal fc (B64 i), PrimVal fc Bits64Type)
|
||||
checkPrim fc (Str s) = (PrimVal fc (Str s), PrimVal fc StringType)
|
||||
checkPrim fc (Ch c) = (PrimVal fc (Ch c), PrimVal fc CharType)
|
||||
checkPrim fc (Db d) = (PrimVal fc (Db d), PrimVal fc DoubleType)
|
||||
@ -15,6 +19,10 @@ checkPrim fc WorldVal = (PrimVal fc WorldVal, PrimVal fc WorldType)
|
||||
|
||||
checkPrim fc IntType = (PrimVal fc IntType, 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)
|
||||
checkPrim fc Bits32Type = (PrimVal fc Bits32Type, TType fc)
|
||||
checkPrim fc Bits64Type = (PrimVal fc Bits64Type, TType fc)
|
||||
checkPrim fc StringType = (PrimVal fc StringType, TType fc)
|
||||
checkPrim fc CharType = (PrimVal fc CharType, TType fc)
|
||||
checkPrim fc DoubleType = (PrimVal fc DoubleType, TType fc)
|
||||
|
||||
@ -10,11 +10,17 @@
|
||||
((0) '())
|
||||
((1) (cons (vector-ref desc 2)
|
||||
(blodwen-read-args (vector-ref desc 3)))))))
|
||||
(define b+ (lambda (x y bits) (remainder (+ x y) (expt 2 bits))))
|
||||
(define b- (lambda (x y bits) (remainder (- x y) (expt 2 bits))))
|
||||
(define b* (lambda (x y bits) (remainder (* x y) (expt 2 bits))))
|
||||
(define b/ (lambda (x y bits) (remainder (exact-floor (/ x y)) (expt 2 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 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))))
|
||||
(define integer->bits64 (lambda (x) (modulo x (expt 2 64))))
|
||||
|
||||
(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)))
|
||||
@ -102,11 +108,23 @@
|
||||
(define (blodwen-buffer-getbyte buf loc)
|
||||
(bytevector-u8-ref buf loc))
|
||||
|
||||
(define (blodwen-buffer-setint buf loc val)
|
||||
(bytevector-s64-set! buf loc val (native-endianness)))
|
||||
(define (blodwen-buffer-setbits16 buf loc val)
|
||||
(bytevector-u16-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getint buf loc)
|
||||
(bytevector-s64-ref buf loc (native-endianness)))
|
||||
(define (blodwen-buffer-getbits16 buf loc)
|
||||
(bytevector-u16-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setbits32 buf loc val)
|
||||
(bytevector-u32-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getbits32 buf loc)
|
||||
(bytevector-u32-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setbits64 buf loc val)
|
||||
(bytevector-u64-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getbits64 buf loc)
|
||||
(bytevector-u64-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setint32 buf loc val)
|
||||
(bytevector-s32-set! buf loc val (native-endianness)))
|
||||
@ -114,6 +132,12 @@
|
||||
(define (blodwen-buffer-getint32 buf loc)
|
||||
(bytevector-s32-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setint buf loc val)
|
||||
(bytevector-s64-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getint buf loc)
|
||||
(bytevector-s64-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setdouble buf loc val)
|
||||
(bytevector-ieee-double-set! buf loc val (native-endianness)))
|
||||
|
||||
|
||||
@ -31,9 +31,17 @@
|
||||
`(remainder (floor (/ ,x ,y)) ,(arithmetic-shift 1 bits))
|
||||
`(remainder (floor (/ ,x ,y)) (arithmetic-shift 1 ,bits))))
|
||||
|
||||
(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))))
|
||||
(define integer->bits64 (lambda (x) (modulo x (expt 2 64))))
|
||||
|
||||
(define-macro (blodwen-and . args) `(bitwise-and ,@args))
|
||||
(define-macro (blodwen-or . args) `(bitwise-ior ,@args))
|
||||
(define-macro (blodwen-xor . args) `(bitwise-xor ,@args))
|
||||
(define-macro (blodwen-bits-shl x y bits)
|
||||
`(remainder (arithmetic-shift ,x ,y)
|
||||
(arithmetic-shitt 1 ,bits)))
|
||||
(define-macro (blodwen-shl x y) `(arithmetic-shift ,x ,y))
|
||||
(define-macro (blodwen-shr x y) `(arithmetic-shift ,x (- ,y)))
|
||||
|
||||
|
||||
@ -10,11 +10,17 @@
|
||||
((0) '())
|
||||
((1) (cons (vector-ref desc 2)
|
||||
(blodwen-read-args (vector-ref desc 3)))))))
|
||||
(define b+ (lambda (x y bits) (remainder (+ x y) (expt 2 bits))))
|
||||
(define b- (lambda (x y bits) (remainder (- x y) (expt 2 bits))))
|
||||
(define b* (lambda (x y bits) (remainder (* x y) (expt 2 bits))))
|
||||
(define b/ (lambda (x y bits) (remainder (exact-floor (/ x y)) (expt 2 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 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))))
|
||||
(define integer->bits64 (lambda (x) (modulo x (expt 2 64))))
|
||||
|
||||
(define blodwen-bits-shl (lambda (x y bits) (remainder (arithmetic-shift x y) (arithmetic-shift 1 bits))))
|
||||
(define blodwen-shl (lambda (x y) (arithmetic-shift x y)))
|
||||
(define blodwen-shr (lambda (x y) (arithmetic-shift x (- y))))
|
||||
(define blodwen-and (lambda (x y) (bitwise-and x y)))
|
||||
@ -97,11 +103,23 @@
|
||||
(define (blodwen-buffer-getbyte buf loc)
|
||||
(bytevector-u8-ref buf loc))
|
||||
|
||||
(define (blodwen-buffer-setint buf loc val)
|
||||
(bytevector-s64-set! buf loc val (native-endianness)))
|
||||
(define (blodwen-buffer-setbits16 buf loc val)
|
||||
(bytevector-u16-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getint buf loc)
|
||||
(bytevector-s64-ref buf loc (native-endianness)))
|
||||
(define (blodwen-buffer-getbits16 buf loc)
|
||||
(bytevector-u16-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setbits32 buf loc val)
|
||||
(bytevector-u32-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getbits32 buf loc)
|
||||
(bytevector-u32-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setbits64 buf loc val)
|
||||
(bytevector-u64-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getbits64 buf loc)
|
||||
(bytevector-u64-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setint32 buf loc val)
|
||||
(bytevector-s32-set! buf loc val (native-endianness)))
|
||||
@ -109,6 +127,12 @@
|
||||
(define (blodwen-buffer-getint32 buf loc)
|
||||
(bytevector-s32-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setint buf loc val)
|
||||
(bytevector-s64-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getint buf loc)
|
||||
(bytevector-s64-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setdouble buf loc val)
|
||||
(bytevector-ieee-double-set! buf loc val (native-endianness)))
|
||||
|
||||
|
||||
@ -110,7 +110,7 @@ chezTests
|
||||
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
|
||||
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
||||
"chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
|
||||
"chez019", "chez020",
|
||||
"chez019", "chez020", "chez021",
|
||||
"reg001"]
|
||||
|
||||
ideModeTests : List String
|
||||
|
||||
@ -24,6 +24,10 @@ main
|
||||
val <- getString buf 26 6
|
||||
printLn val
|
||||
|
||||
setBits16 buf 32 65535
|
||||
val <- getBits16 buf 32
|
||||
printLn val
|
||||
|
||||
ds <- bufferData buf
|
||||
printLn ds
|
||||
|
||||
|
||||
@ -3,7 +3,8 @@
|
||||
94.42
|
||||
"Hello"
|
||||
"there!"
|
||||
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
|
||||
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
|
||||
65535
|
||||
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
|
||||
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
|
||||
1/1: Building Buffer (Buffer.idr)
|
||||
Main> Main> Bye for now!
|
||||
|
||||
43
tests/chez/chez021/Bits.idr
Normal file
43
tests/chez/chez021/Bits.idr
Normal file
@ -0,0 +1,43 @@
|
||||
t1 : Bits8
|
||||
t1 = 2
|
||||
|
||||
t2 : Bits8
|
||||
t2 = 255
|
||||
|
||||
t3 : Bits8
|
||||
t3 = 100
|
||||
|
||||
tests8 : List String
|
||||
tests8 = map show [t1 + t2,
|
||||
t1 * t3,
|
||||
the Bits8 (fromInteger (-8)),
|
||||
the Bits8 257,
|
||||
the Bits8 (fromInteger (-1)),
|
||||
prim__shl_Bits8 t3 1,
|
||||
prim__shl_Bits8 t2 1]
|
||||
|
||||
testsCmp : List String
|
||||
testsCmp = map show [t1 < t2, t3 < (t2 + t1)]
|
||||
|
||||
testsMax : List String
|
||||
testsMax = [show (the Bits8 (fromInteger (-1))),
|
||||
show (the Bits16 (fromInteger (-1))),
|
||||
show (the Bits32 (fromInteger (-1))),
|
||||
show (the Bits64 (fromInteger (-1)))]
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do printLn (t1 + t2)
|
||||
printLn (t1 * t3)
|
||||
printLn (t1 < t2)
|
||||
printLn (prim__shl_Bits8 t3 1)
|
||||
printLn (prim__shl_Bits8 t2 1)
|
||||
printLn (t3 < (t2 + t1))
|
||||
printLn (the Bits8 (fromInteger (-8)))
|
||||
printLn (the Bits8 257)
|
||||
printLn (the Bits64 1234567890)
|
||||
printLn (the Bits8 (fromInteger (-1)))
|
||||
printLn (the Bits16 (fromInteger (-1)))
|
||||
printLn (the Bits32 (fromInteger (-1)))
|
||||
printLn (the Bits64 (fromInteger (-1)))
|
||||
|
||||
18
tests/chez/chez021/expected
Normal file
18
tests/chez/chez021/expected
Normal file
@ -0,0 +1,18 @@
|
||||
1
|
||||
200
|
||||
True
|
||||
200
|
||||
254
|
||||
False
|
||||
248
|
||||
1
|
||||
1234567890
|
||||
255
|
||||
65535
|
||||
4294967295
|
||||
18446744073709551615
|
||||
1/1: Building Bits (Bits.idr)
|
||||
Main> ["257", "200", "248", "1", "255", "200", "254"]
|
||||
Main> ["True", "True"]
|
||||
Main> ["255", "65535", "4294967295", "18446744073709551615"]
|
||||
Main> Main> Bye for now!
|
||||
5
tests/chez/chez021/input
Normal file
5
tests/chez/chez021/input
Normal file
@ -0,0 +1,5 @@
|
||||
tests8
|
||||
testsCmp
|
||||
testsMax
|
||||
:exec main
|
||||
:q
|
||||
3
tests/chez/chez021/run
Normal file
3
tests/chez/chez021/run
Normal file
@ -0,0 +1,3 @@
|
||||
$1 --no-banner Bits.idr < input
|
||||
|
||||
rm -rf build
|
||||
@ -8,7 +8,7 @@
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
|
||||
@ -8,7 +8,7 @@
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
1/1: Building wcov (wcov.idr)
|
||||
Main> Main.tfoo is total
|
||||
Main> Main.wfoo is total
|
||||
Main> Main.wbar is not covering due to call to function Main.with block in 1210
|
||||
Main> Main.wbar is not covering due to call to function Main.with block in 1368
|
||||
Main> Main.wbar1 is total
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
1/1: Building casetot (casetot.idr)
|
||||
casetot.idr:12:1--13:1:main is not covering:
|
||||
Calls non covering function Main.case block in 1921(290)
|
||||
Calls non covering function Main.case block in 2079(290)
|
||||
|
||||
@ -2,5 +2,5 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
|
||||
Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved120 ?Main.{a:62}_[]), ($resolved100 ?Main.{a:62}_[])]
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved190 ?Main.{a:62}_[]), ($resolved170 ?Main.{a:62}_[])]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,10 +2,10 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved116 {b:27}[1] {a:26}[0] $resolved98 ($resolved107 {a:26}[0]) ($resolved107 {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} => ($resolved186 {b:27}[1] {a:26}[0] $resolved168 ($resolved177 {a:26}[0]) ($resolved177 {b:27}[1])) is not a valid impossible pattern because it typechecks
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Vect3.yaff:25:1--26:1:Not a valid impossible pattern:
|
||||
Vect3.yaff:25:9--25:11:When unifying: $resolved97 and ($resolved105 ?Main.{n:21}_[] ?Main.{b:19}_[])
|
||||
Vect3.yaff:25:9--25:11:Type mismatch: $resolved97 and ($resolved105 ?Main.{n:21}_[] ?Main.{b:19}_[])
|
||||
Vect3.yaff:25:9--25:11:When unifying: $resolved167 and ($resolved175 ?Main.{n:21}_[] ?Main.{b:19}_[])
|
||||
Vect3.yaff:25:9--25:11:Type mismatch: $resolved167 and ($resolved175 ?Main.{n:21}_[] ?Main.{b:19}_[])
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,6 +2,6 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.lookup: All cases covered
|
||||
Yaffle> Main.lookup':
|
||||
($resolved147 [__] [__] ($resolved113 [__]) {_:62})
|
||||
($resolved217 [__] [__] ($resolved183 [__]) {_:62})
|
||||
Yaffle> Main.lookup'': Calls non covering function Main.lookup'
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -3,13 +3,13 @@ Written TTC
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
|
||||
Dot2.yaff:15:28--15:30:Pattern variable {P:n:102} unifies with ?{P:m:102}_[]
|
||||
Dot2.yaff:15:28--15:30:Pattern variable {P:n:172} unifies with ?{P:m:172}_[]
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
|
||||
Dot3.yaff:18:10--18:15:Can't match on ($resolved94 ?{P:x:107}_[] ?{P:x:107}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved94 ?Main.{_:13}_[] ?Main.{_:14}_[])
|
||||
Dot3.yaff:18:10--18:15:Can't match on ($resolved164 ?{P:x:177}_[] ?{P:x:177}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved164 ?Main.{_:13}_[] ?Main.{_:14}_[])
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot4.yaff:17:1--19:1:When elaborating left hand side of Main.addBaz4:
|
||||
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:109}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
|
||||
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:179}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Processing as TTImp
|
||||
Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
|
||||
Eta.yaff:16:10--17:1:When unifying: ($resolved99 ?Main.{b:18}_[] ?Main.{b:18}_[] \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved109 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved109 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and ($resolved99 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved108)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved108)) $resolved109 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved109 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
|
||||
Eta.yaff:16:10--17:1:When unifying: ($resolved169 ?Main.{b:18}_[] ?Main.{b:18}_[] \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved179 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved179 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and ($resolved169 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved178)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved178)) $resolved179 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved179 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
|
||||
Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
|
||||
Yaffle> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user