idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-29 14:44:03 +03:00
Code Issues Projects Releases Wiki Activity

Fix Char casting

Browse Source 
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.
This commit is contained in:
Edwin Brady 2020-05-23 22:19:10 +01:00
parent cff5fc2625
commit ad9a2a187f
6 changed files with 16 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
INSTALL.md
View File

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

2
bootstrap-rkt.sh
View File

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

4
libs/base/System/File.idr
View File

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

2
src/Compiler/Scheme/Common.idr
View File

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

6
support/chez/support.ss
View File

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

6
support/racket/support.rkt
View File

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