idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 15:07:37 +03:00
Code Issues Projects Releases Wiki Activity

Run tests chez029 and node022 via code generator

Browse Source
This commit is contained in:
Christian Rasmussen 2020-10-16 17:52:15 +02:00 committed by G. Allais
parent f79b86ae41
commit 66fe57f340
8 changed files with 68 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Compiler/ES/ES.idr
View File

@ -258,6 +258,7 @@ jsOp DoubleATan [x] = pure $ "Math.atan(" ++ x ++ ")"
jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")"
jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")"
jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")"
jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast CharType IntType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
@ -270,6 +271,16 @@ jsOp (Cast IntegerType IntType) [x] = boundedInt 63 x
jsOp (Cast IntType IntegerType) [x] = pure x
jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"
jsOp (Cast Bits8Type IntType) [x] = pure x
jsOp (Cast Bits16Type IntType) [x] = pure x
jsOp (Cast Bits32Type IntType) [x] = pure x
jsOp (Cast Bits64Type IntType) [x] = pure x
jsOp (Cast Bits8Type IntegerType) [x] = pure x
jsOp (Cast Bits16Type IntegerType) [x] = pure x
jsOp (Cast Bits32Type IntegerType) [x] = pure x
jsOp (Cast Bits64Type IntegerType) [x] = pure x
jsOp (Cast IntType Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast IntType Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast IntType Bits32Type) [x] = boundedUInt 32 x

18
tests/chez/chez029/BitCasts.idr
View File

@ -1,6 +1,6 @@
-- Tests to check that casting between integer types works as expected
--
-- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
-- The tests in `idris2/basic043`, `chez/chez029` and `node/node022` are the
-- same and should all have the same output.
--
@ -93,3 +93,19 @@ negativeNumberCast = [
show $ cast {to = Bits32} (-19),
show $ cast {to = Bits64} (-19)
]
--
-- Run via code generator
--
main : IO ()
main = do
printLn bits8WideningNoEffect
printLn bits16WideningNoEffect
printLn bits32WideningNoEffect
printLn narrowFromInteger
printLn narrowFromInt
printLn narrowFromBits64
printLn narrowFromBits32
printLn narrowFromBits16
printLn negativeNumberCast

20
tests/chez/chez029/expected
View File

@ -1,11 +1,11 @@
["123", "123", "123", "123", "123"]
["1234", "1234", "1234", "1234"]
["1234567", "1234567", "1234567"]
["134", "134", "134", "134"]
["134", "134", "134", "134"]
["134", "134", "134"]
["134", "134"]
["134"]
["237", "65517", "4294967277", "18446744073709551597"]
1/1: Building BitCasts (BitCasts.idr)
Main> ["123", "123", "123", "123", "123"]
Main> ["1234", "1234", "1234", "1234"]
Main> ["1234567", "1234567", "1234567"]
Main> ["134", "134", "134", "134"]
Main> ["134", "134", "134", "134"]
Main> ["134", "134", "134"]
Main> ["134", "134"]
Main> ["134"]
Main> ["237", "65517", "4294967277", "18446744073709551597"]
Main> Bye for now!
Main> Main> Bye for now!

10
tests/chez/chez029/input
View File

@ -1,10 +1,2 @@
bits8WideningNoEffect
bits16WideningNoEffect
bits32WideningNoEffect
narrowFromInteger
narrowFromInt
narrowFromBits64
narrowFromBits32
narrowFromBits16
negativeNumberCast
:exec main
:q

2
tests/idris2/basic043/BitCasts.idr
View File

@ -1,6 +1,6 @@
-- Tests to check that casting between integer types works as expected
--
-- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
-- The tests in `idris2/basic043`, `chez/chez029` and `node/node022` are the
-- same and should all have the same output.
--

18
tests/node/node022/BitCasts.idr
View File

@ -1,6 +1,6 @@
-- Tests to check that casting between integer types works as expected
--
-- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
-- The tests in `idris2/basic043`, `chez/chez029` and `node/node022` are the
-- same and should all have the same output.
--
@ -93,3 +93,19 @@ negativeNumberCast = [
show $ cast {to = Bits32} (-19),
show $ cast {to = Bits64} (-19)
]
--
-- Run via code generator
--
main : IO ()
main = do
printLn bits8WideningNoEffect
printLn bits16WideningNoEffect
printLn bits32WideningNoEffect
printLn narrowFromInteger
printLn narrowFromInt
printLn narrowFromBits64
printLn narrowFromBits32
printLn narrowFromBits16
printLn negativeNumberCast

20
tests/node/node022/expected
View File

@ -1,11 +1,11 @@
["123", "123", "123", "123", "123"]
["1234", "1234", "1234", "1234"]
["1234567", "1234567", "1234567"]
["134", "134", "134", "134"]
["134", "134", "134", "134"]
["134", "134", "134"]
["134", "134"]
["134"]
["237", "65517", "4294967277", "18446744073709551597"]
1/1: Building BitCasts (BitCasts.idr)
Main> ["123", "123", "123", "123", "123"]
Main> ["1234", "1234", "1234", "1234"]
Main> ["1234567", "1234567", "1234567"]
Main> ["134", "134", "134", "134"]
Main> ["134", "134", "134", "134"]
Main> ["134", "134", "134"]
Main> ["134", "134"]
Main> ["134"]
Main> ["237", "65517", "4294967277", "18446744073709551597"]
Main> Bye for now!
Main> Main> Bye for now!

10
tests/node/node022/input
View File

@ -1,10 +1,2 @@
bits8WideningNoEffect
bits16WideningNoEffect
bits32WideningNoEffect
narrowFromInteger
narrowFromInt
narrowFromBits64
narrowFromBits32
narrowFromBits16
negativeNumberCast
:exec main
:q