From ad9a2a187ff85f21a1485bb269ed498a539c3316 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 23 May 2020 22:19:10 +0100 Subject: [PATCH] Fix Char casting For the same behaviour as Idris 1, the primitive cast should return 0 if the integer is out of bounds. (We should probably drop the Cast implementation though, since ideally they won't be lossy in general, but that's an issue for another time...) All the tests pass in racket now, for me. --- INSTALL.md | 3 --- bootstrap-rkt.sh | 2 +- libs/base/System/File.idr | 4 ++-- src/Compiler/Scheme/Common.idr | 2 +- support/chez/support.ss | 6 ++++++ support/racket/support.rkt | 6 ++++++ 6 files changed, 16 insertions(+), 7 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index bd9240787..34f50fabc 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -14,9 +14,6 @@ On Windows, it has been reported that installing via `MSYS2` works By default, code generation is via Chez Scheme. You can use Racket instead, by setting the environment variable `IDRIS2_CG=racket` before running `make`. -[Note: a couple of tests are currently known to fail when installing via -Racket. This will be addressed soon!] - 1: Set the PREFIX ----------------- diff --git a/bootstrap-rkt.sh b/bootstrap-rkt.sh index 06b9700a5..0ddbe3640 100644 --- a/bootstrap-rkt.sh +++ b/bootstrap-rkt.sh @@ -27,4 +27,4 @@ make libs IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH} make install IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH} make clean IDRIS2_BOOT=${PREFIX}/bin/idris2 LD_LIBRARY_PATH=${DYLIB_PATH} make all IDRIS2_BOOT=${PREFIX}/bin/idris2 IDRIS2_CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} LD_LIBRARY_PATH=${DYLIB_PATH} -#make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib LD_LIBRARY_PATH=${DYLIB_PATH} +make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib LD_LIBRARY_PATH=${DYLIB_PATH} diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index 1972e4ce2..d8976e119 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -31,7 +31,7 @@ prim__readLine : FilePtr -> PrimIO (Ptr String) %foreign support "idris2_readChars" prim__readChars : Int -> FilePtr -> PrimIO (Ptr String) %foreign support "fgetc" -prim__readChar : FilePtr -> PrimIO Char +prim__readChar : FilePtr -> PrimIO Int %foreign support "idris2_writeLine" prim__writeLine : FilePtr -> String -> PrimIO Int %foreign support "idris2_eof" @@ -159,7 +159,7 @@ fGetChar (FHandle h) ferr <- primIO (prim_error h) if (ferr /= 0) then returnError - else ok c + else ok (cast c) export fPutStr : (h : File) -> String -> IO (Either FileError ()) diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index 9a91d750e..796f7478e 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -131,7 +131,7 @@ schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x] schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x] schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x] -schOp (Cast IntType CharType) [x] = op "integer->char" [x] +schOp (Cast IntType CharType) [x] = op "cast-int-char" [x] schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")" diff --git a/support/chez/support.ss b/support/chez/support.ss index 4a1bbd421..91f446d5f 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -33,6 +33,12 @@ (define cast-string-int (lambda (x) (floor (cast-num (string->number (destroy-prefix x)))))) +(define cast-int-char + (lambda (x) + (if (and (>= x 0) + (<= x #x10ffff)) + (integer->char x) + 0))) (define exact-floor (lambda (x) (inexact->exact (floor x)))) diff --git a/support/racket/support.rkt b/support/racket/support.rkt index 6d2e11ea7..880f1c601 100644 --- a/support/racket/support.rkt +++ b/support/racket/support.rkt @@ -33,6 +33,12 @@ (define cast-string-int (lambda (x) (floor (cast-num (string->number (destroy-prefix x)))))) +(define cast-int-char + (lambda (x) + (if (and (>= x 0) + (<= x #x10ffff)) + (integer->char x) + 0))) (define cast-string-double (lambda (x) (cast-num (string->number (destroy-prefix x)))))