mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Merge branch 'master' into fix-makefiles
This commit is contained in:
commit
8261b361e0
@ -13,6 +13,15 @@ Compiler updates:
|
||||
* 0-multiplicity constructor arguments are now properly erased, not just
|
||||
given a placeholder null value.
|
||||
|
||||
Language extensions:
|
||||
|
||||
* %transform directive, for declaring transformation rules on runtime
|
||||
expressions. Transformation rules are automatically added for top level
|
||||
implementations of interfaces.
|
||||
* A %spec flag on functions which allows arguments to be marked for partial
|
||||
evaluation, following the rules from "Scrapping Your Inefficient Engine"
|
||||
(ICFP 2010, Brady & Hammond)
|
||||
|
||||
Other improvements:
|
||||
|
||||
* Various performance improvements in the typechecker:
|
||||
|
@ -2,39 +2,54 @@ module System
|
||||
|
||||
import Data.So
|
||||
|
||||
support : String -> String
|
||||
support fn = "C:" ++ fn ++ ", libidris2_support"
|
||||
|
||||
%foreign support "idris2_sleep"
|
||||
prim_sleep : Int -> PrimIO ()
|
||||
%foreign support "idris2_usleep"
|
||||
prim_usleep : Int -> PrimIO ()
|
||||
|
||||
export
|
||||
sleep : Int -> IO ()
|
||||
sleep sec = schemeCall () "blodwen-sleep" [sec]
|
||||
sleep sec = primIO (prim_sleep sec)
|
||||
|
||||
export
|
||||
usleep : (x : Int) -> So (x >= 0) => IO ()
|
||||
usleep usec = schemeCall () "blodwen-usleep" [usec]
|
||||
usleep sec = primIO (prim_usleep sec)
|
||||
|
||||
-- This one is going to vary for different back ends. Probably needs a
|
||||
-- better convention. Will revisit...
|
||||
%foreign "scheme:blodwen-args"
|
||||
prim__getArgs : PrimIO (List String)
|
||||
|
||||
export
|
||||
getArgs : IO (List String)
|
||||
getArgs = schemeCall (List String) "blodwen-args" []
|
||||
getArgs = primIO prim__getArgs
|
||||
|
||||
%foreign "scheme:getenv"
|
||||
prim_getEnv : String -> PrimIO String
|
||||
|
||||
%foreign "scheme:blodwen-hasenv"
|
||||
prim_hasEnv : String -> PrimIO Int
|
||||
%foreign "C:getenv,libc"
|
||||
prim_getEnv : String -> PrimIO (Ptr String)
|
||||
|
||||
export
|
||||
getEnv : String -> IO (Maybe String)
|
||||
getEnv var
|
||||
= do ok <- primIO $ prim_hasEnv var
|
||||
if ok == 0
|
||||
= do env <- primIO $ prim_getEnv var
|
||||
if prim__nullPtr env /= 0
|
||||
then pure Nothing
|
||||
else map pure $ primIO (prim_getEnv var)
|
||||
else pure (Just (prim__getString env))
|
||||
|
||||
%foreign "scheme:blodwen-system"
|
||||
%foreign "C:system,libc"
|
||||
"scheme:blodwen-system"
|
||||
prim_system : String -> PrimIO Int
|
||||
|
||||
export
|
||||
system : String -> IO Int
|
||||
system cmd = primIO (prim_system cmd)
|
||||
|
||||
%foreign support "idris2_time"
|
||||
"scheme:blodwen-time"
|
||||
prim_time : PrimIO Int
|
||||
|
||||
export
|
||||
time : IO Integer
|
||||
time = schemeCall Integer "blodwen-time" []
|
||||
time = pure $ cast !(primIO prim_time)
|
||||
|
@ -3,37 +3,46 @@ module System.Directory
|
||||
import public System.File
|
||||
|
||||
public export
|
||||
data DirPtr : Type where
|
||||
DirPtr : Type
|
||||
DirPtr = AnyPtr
|
||||
|
||||
toFileError : Int -> FileError
|
||||
toFileError 1 = FileReadError
|
||||
toFileError 2 = FileWriteError
|
||||
toFileError 3 = FileNotFound
|
||||
toFileError 4 = PermissionDenied
|
||||
toFileError 5 = FileExists
|
||||
toFileError x = GenericFileError (x - 256)
|
||||
support : String -> String
|
||||
support fn = "C:" ++ fn ++ ", libidris2_support"
|
||||
|
||||
fpure : Either Int a -> IO (Either FileError a)
|
||||
fpure (Left err) = pure (Left (toFileError err))
|
||||
fpure (Right x) = pure (Right x)
|
||||
%foreign support "idris2_fileErrno"
|
||||
prim_fileErrno : PrimIO Int
|
||||
|
||||
%foreign "scheme:blodwen-current-directory"
|
||||
prim_currentDir : PrimIO String
|
||||
returnError : IO (Either FileError a)
|
||||
returnError
|
||||
= do err <- primIO prim_fileErrno
|
||||
case err of
|
||||
0 => pure $ Left FileReadError
|
||||
1 => pure $ Left FileWriteError
|
||||
2 => pure $ Left FileNotFound
|
||||
3 => pure $ Left PermissionDenied
|
||||
4 => pure $ Left FileExists
|
||||
_ => pure $ Left (GenericFileError (err-5))
|
||||
|
||||
%foreign "scheme:blodwen-change-directory"
|
||||
ok : a -> IO (Either FileError a)
|
||||
ok x = pure (Right x)
|
||||
|
||||
%foreign support "idris2_currentDirectory"
|
||||
prim_currentDir : PrimIO (Ptr String)
|
||||
|
||||
%foreign support "idris2_changeDir"
|
||||
prim_changeDir : String -> PrimIO Int
|
||||
|
||||
%foreign "scheme:blodwen-create-directory"
|
||||
prim_createDir : String -> PrimIO (Either Int ())
|
||||
%foreign support "idris2_createDir"
|
||||
prim_createDir : String -> PrimIO Int
|
||||
|
||||
%foreign "scheme:blodwen-open-directory"
|
||||
prim_openDir : String -> PrimIO (Either Int DirPtr)
|
||||
%foreign support "idris2_dirOpen"
|
||||
prim_openDir : String -> PrimIO DirPtr
|
||||
|
||||
%foreign "scheme:blodwen-close-directory"
|
||||
%foreign support "idris2_dirClose"
|
||||
prim_closeDir : DirPtr -> PrimIO ()
|
||||
|
||||
%foreign "scheme:blodwen-next-dir-entry"
|
||||
prim_dirEntry : DirPtr -> PrimIO (Either Int String)
|
||||
%foreign support "idris2_nextDirEntry"
|
||||
prim_dirEntry : DirPtr -> PrimIO (Ptr String)
|
||||
|
||||
export
|
||||
data Directory : Type where
|
||||
@ -42,8 +51,10 @@ data Directory : Type where
|
||||
export
|
||||
createDir : String -> IO (Either FileError ())
|
||||
createDir dir
|
||||
= do ok <- primIO (prim_createDir dir)
|
||||
fpure ok
|
||||
= do res <- primIO (prim_createDir dir)
|
||||
if res == 0
|
||||
then ok ()
|
||||
else returnError
|
||||
|
||||
export
|
||||
changeDir : String -> IO Bool
|
||||
@ -52,14 +63,20 @@ changeDir dir
|
||||
pure (ok /= 0)
|
||||
|
||||
export
|
||||
currentDir : IO String
|
||||
currentDir = primIO prim_currentDir
|
||||
currentDir : IO (Maybe String)
|
||||
currentDir
|
||||
= do res <- primIO prim_currentDir
|
||||
if prim__nullPtr res /= 0
|
||||
then pure Nothing
|
||||
else pure (Just (prim__getString res))
|
||||
|
||||
export
|
||||
dirOpen : String -> IO (Either FileError Directory)
|
||||
dirOpen d
|
||||
= do res <- primIO (prim_openDir d)
|
||||
fpure (map MkDir res)
|
||||
if prim__nullAnyPtr res /= 0
|
||||
then returnError
|
||||
else ok (MkDir res)
|
||||
|
||||
export
|
||||
dirClose : Directory -> IO ()
|
||||
@ -69,4 +86,6 @@ export
|
||||
dirEntry : Directory -> IO (Either FileError String)
|
||||
dirEntry (MkDir d)
|
||||
= do res <- primIO (prim_dirEntry d)
|
||||
fpure res
|
||||
if prim__nullPtr res /= 0
|
||||
then returnError
|
||||
else ok (prim__getString res)
|
||||
|
@ -7,21 +7,52 @@ public export
|
||||
data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend
|
||||
|
||||
public export
|
||||
data FilePtr : Type where
|
||||
FilePtr : Type
|
||||
FilePtr = AnyPtr
|
||||
|
||||
%extern prim__open : String -> String -> Int ->
|
||||
(1 x : %World) -> IORes (Either Int FilePtr)
|
||||
%extern prim__close : FilePtr -> (1 x : %World) -> IORes ()
|
||||
%extern prim__readLine : FilePtr -> (1 x : %World) -> IORes (Either Int String)
|
||||
%extern prim__writeLine : FilePtr -> String -> (1 x : %World) -> IORes (Either Int ())
|
||||
%extern prim__eof : FilePtr -> (1 x : %World) -> IORes Int
|
||||
support : String -> String
|
||||
support fn = "C:" ++ fn ++ ", libidris2_support"
|
||||
|
||||
%extern prim__fileModifiedTime : FilePtr -> (1 x : %World) ->
|
||||
IORes (Either Int Integer)
|
||||
%foreign support "idris2_openFile"
|
||||
prim__open : String -> String -> Int -> PrimIO FilePtr
|
||||
%foreign support "idris2_closeFile"
|
||||
prim__close : FilePtr -> PrimIO ()
|
||||
|
||||
%extern prim__stdin : FilePtr
|
||||
%extern prim__stdout : FilePtr
|
||||
%extern prim__stderr : FilePtr
|
||||
%foreign support "idris2_fileError"
|
||||
prim_error : FilePtr -> PrimIO Int
|
||||
|
||||
%foreign support "idris2_fileErrno"
|
||||
prim_fileErrno : PrimIO Int
|
||||
|
||||
%foreign support "idris2_readLine"
|
||||
prim__readLine : FilePtr -> PrimIO (Ptr String)
|
||||
%foreign support "idris2_readLine"
|
||||
prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
|
||||
%foreign support "idris2_writeLine"
|
||||
prim__writeLine : FilePtr -> String -> PrimIO Int
|
||||
%foreign support "idris2_eof"
|
||||
prim__eof : FilePtr -> PrimIO Int
|
||||
|
||||
%foreign support "idris2_fileRemove"
|
||||
prim__fileRemove : String -> PrimIO Int
|
||||
%foreign support "idris2_fileSize"
|
||||
prim__fileSize : FilePtr -> PrimIO Int
|
||||
%foreign support "idris2_fileSize"
|
||||
prim__fPoll : FilePtr -> PrimIO Int
|
||||
|
||||
%foreign support "idris2_fileAccessTime"
|
||||
prim__fileAccessTime : FilePtr -> PrimIO Int
|
||||
%foreign support "idris2_fileModifiedTime"
|
||||
prim__fileModifiedTime : FilePtr -> PrimIO Int
|
||||
%foreign support "idris2_fileStatusTime"
|
||||
prim__fileStatusTime : FilePtr -> PrimIO Int
|
||||
|
||||
%foreign support "idris2_stdin"
|
||||
prim__stdin : FilePtr
|
||||
%foreign support "idris2_stdout"
|
||||
prim__stdout : FilePtr
|
||||
%foreign support "idris2_stderr"
|
||||
prim__stderr : FilePtr
|
||||
|
||||
modeStr : Mode -> String
|
||||
modeStr Read = "r"
|
||||
@ -39,6 +70,17 @@ data FileError = GenericFileError Int -- errno
|
||||
| PermissionDenied
|
||||
| FileExists
|
||||
|
||||
returnError : IO (Either FileError a)
|
||||
returnError
|
||||
= do err <- primIO prim_fileErrno
|
||||
case err of
|
||||
0 => pure $ Left FileReadError
|
||||
1 => pure $ Left FileWriteError
|
||||
2 => pure $ Left FileNotFound
|
||||
3 => pure $ Left PermissionDenied
|
||||
4 => pure $ Left FileExists
|
||||
_ => pure $ Left (GenericFileError (err-5))
|
||||
|
||||
export
|
||||
Show FileError where
|
||||
show (GenericFileError errno) = "File error: " ++ show errno
|
||||
@ -48,29 +90,12 @@ Show FileError where
|
||||
show PermissionDenied = "Permission Denied"
|
||||
show FileExists = "File Exists"
|
||||
|
||||
toFileError : Int -> FileError
|
||||
toFileError 1 = FileReadError
|
||||
toFileError 2 = FileWriteError
|
||||
toFileError 3 = FileNotFound
|
||||
toFileError 4 = PermissionDenied
|
||||
toFileError 5 = FileExists
|
||||
toFileError x = GenericFileError (x - 256)
|
||||
|
||||
fpure : Either Int a -> IO (Either FileError a)
|
||||
fpure (Left err) = pure (Left (toFileError err))
|
||||
fpure (Right x) = pure (Right x)
|
||||
ok : a -> IO (Either FileError a)
|
||||
ok x = pure (Right x)
|
||||
|
||||
public export
|
||||
data FileT : Bool -> Type where
|
||||
FHandle : FilePtr -> FileT bin
|
||||
|
||||
public export
|
||||
File : Type
|
||||
File = FileT False
|
||||
|
||||
public export
|
||||
BinaryFile : Type
|
||||
BinaryFile = FileT True
|
||||
data File : Type where
|
||||
FHandle : FilePtr -> File
|
||||
|
||||
export
|
||||
stdin : File
|
||||
@ -88,29 +113,37 @@ export
|
||||
openFile : String -> Mode -> IO (Either FileError File)
|
||||
openFile f m
|
||||
= do res <- primIO (prim__open f (modeStr m) 0)
|
||||
fpure (map FHandle res)
|
||||
if prim__nullAnyPtr res /= 0
|
||||
then returnError
|
||||
else ok (FHandle res)
|
||||
|
||||
export
|
||||
openBinaryFile : String -> Mode -> IO (Either FileError BinaryFile)
|
||||
openBinaryFile f m
|
||||
= do res <- primIO (prim__open f (modeStr m) 1)
|
||||
fpure (map FHandle res)
|
||||
|
||||
export
|
||||
closeFile : FileT t -> IO ()
|
||||
closeFile : File -> IO ()
|
||||
closeFile (FHandle f) = primIO (prim__close f)
|
||||
|
||||
export
|
||||
fGetLine : (h : File) -> IO (Either FileError String)
|
||||
fGetLine (FHandle f)
|
||||
= do res <- primIO (prim__readLine f)
|
||||
fpure res
|
||||
if prim__nullPtr res /= 0
|
||||
then returnError
|
||||
else ok (prim__getString res)
|
||||
|
||||
export
|
||||
fGetChars : (h : File) -> Int -> IO (Either FileError String)
|
||||
fGetChars (FHandle f) max
|
||||
= do res <- primIO (prim__readChars max f)
|
||||
if prim__nullPtr res /= 0
|
||||
then returnError
|
||||
else ok (prim__getString res)
|
||||
|
||||
export
|
||||
fPutStr : (h : File) -> String -> IO (Either FileError ())
|
||||
fPutStr (FHandle f) str
|
||||
= do res <- primIO (prim__writeLine f str)
|
||||
fpure res
|
||||
if res == 0
|
||||
then returnError
|
||||
else ok ()
|
||||
|
||||
export
|
||||
fPutStrLn : (h : File) -> String -> IO (Either FileError ())
|
||||
@ -123,19 +156,59 @@ fEOF (FHandle f)
|
||||
pure (res /= 0)
|
||||
|
||||
export
|
||||
fileModifiedTime : (h : File) -> IO (Either FileError Integer)
|
||||
fileAccessTime : (h : File) -> IO (Either FileError Int)
|
||||
fileAccessTime (FHandle f)
|
||||
= do res <- primIO (prim__fileAccessTime f)
|
||||
if res > 0
|
||||
then ok res
|
||||
else returnError
|
||||
|
||||
export
|
||||
fileModifiedTime : (h : File) -> IO (Either FileError Int)
|
||||
fileModifiedTime (FHandle f)
|
||||
= do res <- primIO (prim__fileModifiedTime f)
|
||||
fpure res
|
||||
if res > 0
|
||||
then ok res
|
||||
else returnError
|
||||
|
||||
export
|
||||
fileStatusTime : (h : File) -> IO (Either FileError Int)
|
||||
fileStatusTime (FHandle f)
|
||||
= do res <- primIO (prim__fileStatusTime f)
|
||||
if res > 0
|
||||
then ok res
|
||||
else returnError
|
||||
|
||||
export
|
||||
fileRemove : String -> IO (Either FileError ())
|
||||
fileRemove fname
|
||||
= do res <- primIO (prim__fileRemove fname)
|
||||
if res == 0
|
||||
then ok ()
|
||||
else returnError
|
||||
|
||||
export
|
||||
fileSize : (h : File) -> IO (Either FileError Int)
|
||||
fileSize (FHandle f)
|
||||
= do res <- primIO (prim__fileSize f)
|
||||
if res >= 0
|
||||
then ok res
|
||||
else returnError
|
||||
|
||||
export
|
||||
fPoll : File -> IO Bool
|
||||
fPoll (FHandle f)
|
||||
= do p <- primIO (prim__fPoll f)
|
||||
pure (p > 0)
|
||||
|
||||
export
|
||||
readFile : String -> IO (Either FileError String)
|
||||
readFile file
|
||||
= do Right h <- openFile file Read
|
||||
| Left err => pure (Left err)
|
||||
| Left err => returnError
|
||||
Right content <- read [] h
|
||||
| Left err => do closeFile h
|
||||
pure (Left err)
|
||||
returnError
|
||||
closeFile h
|
||||
pure (Right (fastAppend content))
|
||||
where
|
||||
@ -146,8 +219,8 @@ readFile file
|
||||
then pure (Right (reverse acc))
|
||||
else
|
||||
do Right str <- fGetLine h
|
||||
| Left err => pure (Left err)
|
||||
read ((str ++ "\n") :: acc) h
|
||||
| Left err => returnError
|
||||
read (str :: acc) h
|
||||
|
||||
||| Write a string to a file
|
||||
export
|
||||
|
@ -123,6 +123,25 @@ export
|
||||
prim_fork : (1 prog : PrimIO ()) -> PrimIO ThreadID
|
||||
prim_fork act w = prim__schemeCall ThreadID "blodwen-thread" [act] w
|
||||
|
||||
%foreign "C:idris2_isNull, libidris2_support"
|
||||
export
|
||||
prim__nullAnyPtr : AnyPtr -> Int
|
||||
|
||||
prim__forgetPtr : Ptr t -> AnyPtr
|
||||
prim__forgetPtr = believe_me
|
||||
|
||||
export %inline
|
||||
prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function
|
||||
prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p)
|
||||
|
||||
%foreign "C:idris2_getString, libidris2_support"
|
||||
export
|
||||
prim__getString : Ptr String -> String
|
||||
|
||||
%foreign "C:idris2_readString, libidris2_support"
|
||||
export
|
||||
prim__getErrno : Int
|
||||
|
||||
unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a
|
||||
unsafeCreateWorld f = f %MkWorld
|
||||
|
||||
|
@ -534,7 +534,9 @@ nfToCFType _ s (NTCon fc n _ _ args)
|
||||
nfToCFType fc s t
|
||||
= do defs <- get Ctxt
|
||||
ty <- quote defs [] t
|
||||
throw (GenericMsg (getLoc t) ("Can't marshal type for foreign call " ++ show ty))
|
||||
throw (GenericMsg (getLoc t)
|
||||
("Can't marshal type for foreign call " ++
|
||||
show !(toFullNames ty)))
|
||||
|
||||
getCFTypes : {auto c : Ref Ctxt Defs} ->
|
||||
List CFType -> NF [] ->
|
||||
|
@ -161,12 +161,9 @@ schOp BelieveMe [_,_,x] = x
|
||||
public export
|
||||
data ExtPrim = CCall | SchemeCall
|
||||
| PutStr | GetStr | PutChar | GetChar
|
||||
| FileOpen | FileClose | FileReadLine | FileWriteLine
|
||||
| FileEOF | FileModifiedTime
|
||||
| NewIORef | ReadIORef | WriteIORef
|
||||
| NewArray | ArrayGet | ArraySet
|
||||
| GetField | SetField
|
||||
| Stdin | Stdout | Stderr
|
||||
| VoidElim
|
||||
| SysOS | SysCodegen
|
||||
| Unknown Name
|
||||
@ -179,12 +176,6 @@ Show ExtPrim where
|
||||
show GetStr = "GetStr"
|
||||
show PutChar = "PutChar"
|
||||
show GetChar = "GetChar"
|
||||
show FileOpen = "FileOpen"
|
||||
show FileClose = "FileClose"
|
||||
show FileReadLine = "FileReadLine"
|
||||
show FileWriteLine = "FileWriteLine"
|
||||
show FileEOF = "FileEOF"
|
||||
show FileModifiedTime = "FileModifiedTime"
|
||||
show NewIORef = "NewIORef"
|
||||
show ReadIORef = "ReadIORef"
|
||||
show WriteIORef = "WriteIORef"
|
||||
@ -193,9 +184,6 @@ Show ExtPrim where
|
||||
show ArraySet = "ArraySet"
|
||||
show GetField = "GetField"
|
||||
show SetField = "SetField"
|
||||
show Stdin = "Stdin"
|
||||
show Stdout = "Stdout"
|
||||
show Stderr = "Stderr"
|
||||
show VoidElim = "VoidElim"
|
||||
show SysOS = "SysOS"
|
||||
show SysCodegen = "SysCodegen"
|
||||
@ -210,12 +198,6 @@ toPrim pn@(NS _ n)
|
||||
(n == UN "prim__getStr", GetStr),
|
||||
(n == UN "prim__putChar", PutChar),
|
||||
(n == UN "prim__getChar", GetChar),
|
||||
(n == UN "prim__open", FileOpen),
|
||||
(n == UN "prim__close", FileClose),
|
||||
(n == UN "prim__readLine", FileReadLine),
|
||||
(n == UN "prim__writeLine", FileWriteLine),
|
||||
(n == UN "prim__eof", FileEOF),
|
||||
(n == UN "prim__fileModifiedTime", FileModifiedTime),
|
||||
(n == UN "prim__newIORef", NewIORef),
|
||||
(n == UN "prim__readIORef", ReadIORef),
|
||||
(n == UN "prim__writeIORef", WriteIORef),
|
||||
@ -224,9 +206,6 @@ toPrim pn@(NS _ n)
|
||||
(n == UN "prim__arraySet", ArraySet),
|
||||
(n == UN "prim__getField", GetField),
|
||||
(n == UN "prim__setField", SetField),
|
||||
(n == UN "prim__stdin", Stdin),
|
||||
(n == UN "prim__stdout", Stdout),
|
||||
(n == UN "prim__stderr", Stderr),
|
||||
(n == UN "void", VoidElim),
|
||||
(n == UN "prim__os", SysOS),
|
||||
(n == UN "prim__codegen", SysCodegen)
|
||||
@ -434,24 +413,6 @@ parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
|
||||
= pure $ "(begin (display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) ++ ")" -- code for MkUnit
|
||||
schExtCommon i GetChar [world]
|
||||
= pure $ mkWorld "(blodwen-get-char (current-input-port))"
|
||||
schExtCommon i FileOpen [file, mode, bin, world]
|
||||
= pure $ mkWorld $ fileOp $ "(blodwen-open "
|
||||
++ !(schExp i file) ++ " "
|
||||
++ !(schExp i mode) ++ " "
|
||||
++ !(schExp i bin) ++ ")"
|
||||
schExtCommon i FileClose [file, world]
|
||||
= pure $ "(blodwen-close-port " ++ !(schExp i file) ++ ") " ++ mkWorld (schConstructor 0 [])
|
||||
schExtCommon i FileReadLine [file, world]
|
||||
= pure $ mkWorld $ fileOp $ "(blodwen-get-line " ++ !(schExp i file) ++ ")"
|
||||
schExtCommon i FileWriteLine [file, str, world]
|
||||
= pure $ mkWorld $ fileOp $ "(blodwen-putstring "
|
||||
++ !(schExp i file) ++ " "
|
||||
++ !(schExp i str) ++ ")"
|
||||
schExtCommon i FileEOF [file, world]
|
||||
= pure $ mkWorld $ "(blodwen-eof " ++ !(schExp i file) ++ ")"
|
||||
schExtCommon i FileModifiedTime [file, world]
|
||||
= pure $ mkWorld $ fileOp $ "(blodwen-file-modified-time "
|
||||
++ !(schExp i file) ++ ")"
|
||||
schExtCommon i NewIORef [_, val, world]
|
||||
= pure $ mkWorld $ "(box " ++ !(schExp i val) ++ ")"
|
||||
schExtCommon i ReadIORef [_, ref, world]
|
||||
@ -476,9 +437,6 @@ parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
|
||||
= pure $ show os
|
||||
schExtCommon i (Unknown n) args
|
||||
= throw (InternalError ("Can't compile unknown external primitive " ++ show n))
|
||||
schExtCommon i Stdin [] = pure "(current-input-port)"
|
||||
schExtCommon i Stdout [] = pure "(current-output-port)"
|
||||
schExtCommon i Stderr [] = pure "(current-error-port)"
|
||||
schExtCommon i prim args
|
||||
= throw (InternalError ("Badly formed external primitive " ++ show prim
|
||||
++ " " ++ show args))
|
||||
|
82
support/c/getline.c
Normal file
82
support/c/getline.c
Normal file
@ -0,0 +1,82 @@
|
||||
/* $NetBSD: fgetln.c,v 1.9 2008/04/29 06:53:03 martin Exp $ */
|
||||
|
||||
/*-
|
||||
* Copyright (c) 2011 The NetBSD Foundation, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This code is derived from software contributed to The NetBSD Foundation
|
||||
* by Christos Zoulas.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions
|
||||
* are met:
|
||||
* 1. Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* 2. Redistributions in binary form must reproduce the above copyright
|
||||
* notice, this list of conditions and the following disclaimer in the
|
||||
* documentation and/or other materials provided with the distribution.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE NETBSD FOUNDATION, INC. AND CONTRIBUTORS
|
||||
* ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
|
||||
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
|
||||
* PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE FOUNDATION OR CONTRIBUTORS
|
||||
* BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
||||
* CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
||||
* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
||||
* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
||||
* CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
||||
* ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
||||
* POSSIBILITY OF SUCH DAMAGE.
|
||||
*/
|
||||
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
#include <unistd.h>
|
||||
#include <errno.h>
|
||||
#include <string.h>
|
||||
|
||||
ssize_t
|
||||
getdelim(char **buf, size_t *bufsiz, int delimiter, FILE *fp)
|
||||
{
|
||||
char *ptr, *eptr;
|
||||
|
||||
if (*buf == NULL || *bufsiz == 0) {
|
||||
*bufsiz = BUFSIZ;
|
||||
if ((*buf = malloc(*bufsiz)) == NULL)
|
||||
return -1;
|
||||
}
|
||||
|
||||
for (ptr = *buf, eptr = *buf + *bufsiz;;) {
|
||||
int c = fgetc(fp);
|
||||
if (c == -1) {
|
||||
if (feof(fp)) {
|
||||
*ptr = '\0';
|
||||
return ptr - *buf;
|
||||
} else {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
*ptr++ = c;
|
||||
if (c == delimiter) {
|
||||
*ptr = '\0';
|
||||
return ptr - *buf;
|
||||
}
|
||||
if (ptr + 2 >= eptr) {
|
||||
char *nbuf;
|
||||
size_t nbufsiz = *bufsiz * 2;
|
||||
ssize_t d = ptr - *buf;
|
||||
if ((nbuf = realloc(*buf, nbufsiz)) == NULL)
|
||||
return -1;
|
||||
*buf = nbuf;
|
||||
*bufsiz = nbufsiz;
|
||||
eptr = nbuf + nbufsiz;
|
||||
ptr = nbuf + d;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
ssize_t
|
||||
getline(char **buf, size_t *bufsiz, FILE *fp)
|
||||
{
|
||||
return getdelim(buf, bufsiz, '\n', fp);
|
||||
}
|
7
support/c/getline.h
Normal file
7
support/c/getline.h
Normal file
@ -0,0 +1,7 @@
|
||||
#ifndef GETLINE_H
|
||||
#define GETLINE_H
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
ssize_t getdelim(char **buf, size_t *bufsiz, int delimiter, FILE *fp);
|
||||
ssize_t getline(char **buf, size_t *bufsiz, FILE *fp);
|
||||
#endif // GETLINE_H
|
63
support/c/idris_directory.c
Normal file
63
support/c/idris_directory.c
Normal file
@ -0,0 +1,63 @@
|
||||
#include "idris_directory.h"
|
||||
|
||||
#include <sys/stat.h>
|
||||
#include <sys/types.h>
|
||||
#include <dirent.h>
|
||||
#include <stdlib.h>
|
||||
#include <unistd.h>
|
||||
|
||||
char* idris2_currentDirectory() {
|
||||
char cwd[1024]; // probably ought to deal with the unlikely event of this being too small
|
||||
return getcwd(cwd, sizeof(cwd)); // freed by RTS
|
||||
}
|
||||
|
||||
int idris2_changeDir(char* dir) {
|
||||
return chdir(dir);
|
||||
}
|
||||
|
||||
int idris2_createDir(char* dir) {
|
||||
#ifdef _WIN32
|
||||
return mkdir(dir);
|
||||
#else
|
||||
return mkdir(dir, S_IRWXU | S_IRGRP | S_IROTH);
|
||||
#endif
|
||||
}
|
||||
|
||||
typedef struct {
|
||||
DIR* dirptr;
|
||||
int error;
|
||||
} DirInfo;
|
||||
|
||||
void* idris2_dirOpen(char* dir) {
|
||||
DIR *d = opendir(dir);
|
||||
if (d == NULL) {
|
||||
return NULL;
|
||||
} else {
|
||||
DirInfo* di = malloc(sizeof(DirInfo));
|
||||
di->dirptr = d;
|
||||
di->error = 0;
|
||||
|
||||
return (void*)di;
|
||||
}
|
||||
}
|
||||
|
||||
void idris2_dirClose(void* d) {
|
||||
DirInfo* di = (DirInfo*)d;
|
||||
|
||||
closedir(di->dirptr);
|
||||
free(di);
|
||||
}
|
||||
|
||||
char* idris2_nextDirEntry(void* d) {
|
||||
DirInfo* di = (DirInfo*)d;
|
||||
struct dirent* de = readdir(di->dirptr);
|
||||
|
||||
if (de == NULL) {
|
||||
di->error = -1;
|
||||
return NULL;
|
||||
} else {
|
||||
return de->d_name;
|
||||
}
|
||||
}
|
||||
|
||||
|
11
support/c/idris_directory.h
Normal file
11
support/c/idris_directory.h
Normal file
@ -0,0 +1,11 @@
|
||||
#ifndef __IDRIS_DIRECTORY_H
|
||||
#define __IDRIS_DIRECTORY_H
|
||||
|
||||
char* idris2_currentDirectory();
|
||||
int idris2_changeDir(char* dir);
|
||||
int idris2_createDir(char* dir);
|
||||
void* idris2_dirOpen(char* dir);
|
||||
void idris2_dirClose(void* d);
|
||||
char* idris2_nextDirEntry(void* d);
|
||||
|
||||
#endif
|
162
support/c/idris_file.c
Normal file
162
support/c/idris_file.c
Normal file
@ -0,0 +1,162 @@
|
||||
#include "getline.h"
|
||||
#include "idris_file.h"
|
||||
|
||||
#include <fcntl.h>
|
||||
#include <errno.h>
|
||||
#include <sys/stat.h>
|
||||
#include <time.h>
|
||||
#include <dirent.h>
|
||||
#include <unistd.h>
|
||||
|
||||
#ifdef _WIN32
|
||||
#include "windows/win_utils.h"
|
||||
#else
|
||||
#include <sys/select.h>
|
||||
#endif
|
||||
|
||||
FILE* idris2_openFile(char* name, char* mode) {
|
||||
#ifdef _WIN32
|
||||
FILE *f = win32_u8fopen(name, mode);
|
||||
#else
|
||||
FILE *f = fopen(name, mode);
|
||||
#endif
|
||||
return (void *)f;
|
||||
}
|
||||
|
||||
void idris2_closeFile(FILE* f) {
|
||||
fclose(f);
|
||||
}
|
||||
|
||||
int idris2_fileError(FILE* f) {
|
||||
return ferror(f);
|
||||
}
|
||||
|
||||
int idris2_fileErrno() {
|
||||
switch(errno) {
|
||||
case ENOENT:
|
||||
return 2;
|
||||
case EACCES:
|
||||
return 3;
|
||||
default:
|
||||
return (errno + 5);
|
||||
}
|
||||
}
|
||||
|
||||
int idris2_fileRemove(const char *filename) {
|
||||
return remove(filename);
|
||||
}
|
||||
|
||||
int idris2_fileSize(FILE* f) {
|
||||
int fd = fileno(f);
|
||||
|
||||
struct stat buf;
|
||||
if (fstat(fd, &buf) == 0) {
|
||||
return (int)(buf.st_size);
|
||||
} else {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
|
||||
int idris2_fpoll(FILE* f)
|
||||
{
|
||||
#ifdef _WIN32
|
||||
return win_fpoll(f);
|
||||
#else
|
||||
fd_set x;
|
||||
struct timeval timeout;
|
||||
timeout.tv_sec = 1;
|
||||
timeout.tv_usec = 0;
|
||||
int fd = fileno(f);
|
||||
|
||||
FD_ZERO(&x);
|
||||
FD_SET(fd, &x);
|
||||
|
||||
int r = select(fd+1, &x, 0, 0, &timeout);
|
||||
return r;
|
||||
#endif
|
||||
}
|
||||
|
||||
|
||||
|
||||
char* idris2_readLine(FILE* f) {
|
||||
char *buffer = NULL;
|
||||
size_t n = 0;
|
||||
ssize_t len;
|
||||
len = getline(&buffer, &n, f);
|
||||
if (len < 0 && buffer != NULL) {
|
||||
buffer[0] = '\0'; // Copy Idris 1 behaviour - empty string if nothing read
|
||||
}
|
||||
return buffer; // freed by RTS if not NULL
|
||||
}
|
||||
|
||||
char* idris_readChars(int num, FILE* f) {
|
||||
char *buffer = malloc((num+1)*sizeof(char));
|
||||
size_t len;
|
||||
len = fread(buffer, sizeof(char), (size_t)num, f);
|
||||
buffer[len] = '\0';
|
||||
|
||||
if (len <= 0) {
|
||||
return NULL;
|
||||
} else {
|
||||
return buffer; // freed by RTS
|
||||
}
|
||||
}
|
||||
|
||||
int idris2_writeLine(FILE* f, char* str) {
|
||||
if (fputs(str, f) == EOF) {
|
||||
return 0;
|
||||
} else {
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
int idris2_eof(FILE* f) {
|
||||
return feof(f);
|
||||
}
|
||||
|
||||
int idris2_fileAccessTime(FILE* f) {
|
||||
int fd = fileno(f);
|
||||
|
||||
struct stat buf;
|
||||
if (fstat(fd, &buf) == 0) {
|
||||
return buf.st_atime;
|
||||
} else {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
|
||||
int idris2_fileModifiedTime(FILE* f) {
|
||||
int fd = fileno(f);
|
||||
|
||||
struct stat buf;
|
||||
if (fstat(fd, &buf) == 0) {
|
||||
return buf.st_mtime;
|
||||
} else {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
|
||||
int idris2_fileStatusTime(FILE* f) {
|
||||
int fd = fileno(f);
|
||||
|
||||
struct stat buf;
|
||||
if (fstat(fd, &buf) == 0) {
|
||||
return buf.st_ctime;
|
||||
} else {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
|
||||
FILE* idris2_stdin() {
|
||||
return stdin;
|
||||
}
|
||||
|
||||
FILE* idris2_stdout() {
|
||||
return stdout;
|
||||
}
|
||||
|
||||
FILE* idris2_stderr() {
|
||||
return stderr;
|
||||
}
|
||||
|
||||
|
34
support/c/idris_file.h
Normal file
34
support/c/idris_file.h
Normal file
@ -0,0 +1,34 @@
|
||||
#ifndef __IDRIS_FILE_H
|
||||
#define __IDRIS_FILE_H
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
FILE* idris2_openFile(char* name, char* mode);
|
||||
void idris2_closeFile(FILE* f);
|
||||
|
||||
int idris2_fileError(FILE* f);
|
||||
|
||||
// Turn errno into an integer understandable by System.File
|
||||
int idris2_fileErrno();
|
||||
|
||||
int idris2_fileRemove(const char *filename);
|
||||
int idris2_fileSize(FILE* h);
|
||||
|
||||
int idris2_fpoll(FILE* f);
|
||||
|
||||
// Treat as a Ptr String (might be NULL)
|
||||
char* idris2_readLine(FILE* f);
|
||||
char* idris_readChars(int num, FILE* f);
|
||||
|
||||
int idris2_writeLine(FILE* f, char* str);
|
||||
|
||||
int idris2_eof(FILE* f);
|
||||
int idris2_fileAccessTime(FILE* f);
|
||||
int idris2_fileModifiedTime(FILE* f);
|
||||
int idris2_fileStatusTime(FILE* f);
|
||||
|
||||
FILE* idris2_stdin();
|
||||
FILE* idris2_stdout();
|
||||
FILE* idris2_stderr();
|
||||
|
||||
#endif
|
@ -1,7 +1,36 @@
|
||||
#include "idris_support.h"
|
||||
#include <string.h>
|
||||
#include <errno.h>
|
||||
#include <time.h>
|
||||
|
||||
int idris2_isNull(void* ptr) {
|
||||
return (ptr == NULL);
|
||||
}
|
||||
|
||||
char* idris2_getString(void *p) {
|
||||
return (char*)p;
|
||||
}
|
||||
|
||||
int idris2_getErrno() {
|
||||
return errno;
|
||||
}
|
||||
|
||||
void idris2_sleep(int sec) {
|
||||
struct timespec t;
|
||||
t.tv_sec = sec;
|
||||
t.tv_nsec = 0;
|
||||
|
||||
nanosleep(&t, NULL);
|
||||
}
|
||||
|
||||
void idris2_usleep(int usec) {
|
||||
struct timespec t;
|
||||
t.tv_sec = usec / 1000000;
|
||||
t.tv_nsec = (usec % 1000000) * 1000;
|
||||
|
||||
nanosleep(&t, NULL);
|
||||
}
|
||||
|
||||
int idris2_time() {
|
||||
return time(NULL); // RTS needs to have 32 bit integers at least
|
||||
}
|
||||
|
@ -1,6 +1,15 @@
|
||||
#ifndef __IDRIS_SUPPORT_H
|
||||
#define __IDRIS_SUPPORT_H
|
||||
|
||||
// Return non-zero if the pointer is null
|
||||
int idris2_isNull(void*);
|
||||
// Convert a Ptr String intro a String, assuming the string has been checked
|
||||
// to be non-null
|
||||
char* idris2_getString(void *p);
|
||||
int idris2_getErrno();
|
||||
|
||||
void idris2_sleep(int sec);
|
||||
void idris2_usleep(int usec);
|
||||
int idris2_time();
|
||||
|
||||
#endif
|
||||
|
67
support/c/windows/win_utils.c
Normal file
67
support/c/windows/win_utils.c
Normal file
@ -0,0 +1,67 @@
|
||||
#include <io.h>
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
#include <windows.h>
|
||||
|
||||
|
||||
// THis file exists to avoid clashes between windows.h and idris_rts.h
|
||||
//
|
||||
|
||||
int win_fpoll(FILE *f)
|
||||
{
|
||||
HANDLE wh =(HANDLE) _get_osfhandle(_fileno(f));
|
||||
if (wh == INVALID_HANDLE_VALUE) {
|
||||
return -1;
|
||||
}
|
||||
DWORD ret = WaitForSingleObject(wh, 1000);
|
||||
// Imitate the return values of select()
|
||||
if (ret == WAIT_OBJECT_0)
|
||||
return 1;
|
||||
if (ret == WAIT_TIMEOUT)
|
||||
return 0;
|
||||
return -1;
|
||||
}
|
||||
|
||||
int widen_utf8(const char *filename_utf8, LPWSTR *filename_w)
|
||||
{
|
||||
int num_chars = MultiByteToWideChar(CP_UTF8, 0, filename_utf8, -1, 0, 0);
|
||||
int size = sizeof(WCHAR);
|
||||
*filename_w = (LPWSTR)malloc(size * num_chars);
|
||||
MultiByteToWideChar(CP_UTF8, 0, filename_utf8, -1, *filename_w, num_chars);
|
||||
return num_chars;
|
||||
}
|
||||
|
||||
FILE *win32_u8fopen(const char *path, const char *mode)
|
||||
{
|
||||
LPWSTR wpath, wmode;
|
||||
widen_utf8(path, &wpath);
|
||||
widen_utf8(mode, &wmode);
|
||||
FILE *f = _wfopen(wpath, wmode);
|
||||
free(wpath);
|
||||
free(wmode);
|
||||
return f;
|
||||
}
|
||||
|
||||
FILE *win32_u8popen(const char *path, const char *mode)
|
||||
{
|
||||
LPWSTR wpath, wmode;
|
||||
widen_utf8(path, &wpath);
|
||||
widen_utf8(mode, &wmode);
|
||||
FILE *f = _wpopen(wpath, wmode);
|
||||
free(wpath);
|
||||
free(wmode);
|
||||
return f;
|
||||
}
|
||||
|
||||
void win32_gettime(int64_t* sec, int64_t* nsec)
|
||||
{
|
||||
FILETIME ft;
|
||||
GetSystemTimePreciseAsFileTime(&ft);
|
||||
ULARGE_INTEGER t;
|
||||
t.HighPart = ft.dwHighDateTime;
|
||||
t.LowPart = ft.dwLowDateTime;
|
||||
|
||||
*nsec = (t.QuadPart % 10000000)*100;
|
||||
*sec = t.QuadPart / 10000000;
|
||||
*sec -= 11644473600; // LDAP epoch to Unix epoch
|
||||
}
|
9
support/c/windows/win_utils.h
Normal file
9
support/c/windows/win_utils.h
Normal file
@ -0,0 +1,9 @@
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
#pragma once
|
||||
|
||||
int win_fpoll(FILE *h);
|
||||
FILE *win32_u8fopen(const char *path, const char *mode);
|
||||
FILE *win32_u8popen(const char *path, const char *mode);
|
||||
void win32_gettime(int64_t* sec, int64_t* nsec);
|
@ -57,105 +57,6 @@
|
||||
(newline)
|
||||
(exit 1)))
|
||||
|
||||
;; Buffers
|
||||
|
||||
(define (blodwen-new-buffer size)
|
||||
(make-bytevector size 0))
|
||||
|
||||
(define (blodwen-buffer-size buf)
|
||||
(bytevector-length buf))
|
||||
|
||||
(define (blodwen-buffer-setbyte buf loc val)
|
||||
(bytevector-u8-set! buf loc val))
|
||||
|
||||
(define (blodwen-buffer-getbyte buf loc)
|
||||
(bytevector-u8-ref buf loc))
|
||||
|
||||
(define (blodwen-buffer-setint buf loc val)
|
||||
(bytevector-s32-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getint buf loc)
|
||||
(bytevector-s32-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setdouble buf loc val)
|
||||
(bytevector-ieee-double-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getdouble buf loc)
|
||||
(bytevector-ieee-double-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-stringbytelen str)
|
||||
(bytevector-length (string->utf8 str)))
|
||||
|
||||
(define (blodwen-buffer-setstring buf loc val)
|
||||
(let* [(strvec (string->utf8 val))
|
||||
(len (bytevector-length strvec))]
|
||||
(bytevector-copy! strvec 0 buf loc len)))
|
||||
|
||||
(define (blodwen-buffer-getstring buf loc len)
|
||||
(let [(newvec (make-bytevector len))]
|
||||
(bytevector-copy! buf loc newvec 0 len)
|
||||
(utf8->string newvec)))
|
||||
|
||||
(define (blodwen-buffer-copydata buf start len dest loc)
|
||||
(bytevector-copy! buf start dest loc len))
|
||||
|
||||
(define (blodwen-readbuffer-bytes h buf loc max)
|
||||
(guard (x (#t -1))
|
||||
(get-bytevector-n! h buf loc max)))
|
||||
|
||||
(define (blodwen-readbuffer h)
|
||||
(guard (x (#t (bytevector)))
|
||||
(get-bytevector-all h)))
|
||||
|
||||
(define (blodwen-writebuffer h buf loc max)
|
||||
(guard (x (#t -1))
|
||||
(put-bytevector h buf loc max)
|
||||
max))
|
||||
|
||||
;; Files: Much of the following adapted from idris-chez, thanks to Niklas
|
||||
;; Larsson
|
||||
|
||||
;; All the file operations are implemented as primitives which return
|
||||
;; Either Int x, where the Int is an error code:
|
||||
(define (blodwen-error-code x)
|
||||
(cond
|
||||
((i/o-read-error? x) 1)
|
||||
((i/o-write-error? x) 2)
|
||||
((i/o-file-does-not-exist-error? x) 3)
|
||||
((i/o-file-protection-error? x) 4)
|
||||
(else 255)))
|
||||
|
||||
;; If the file operation raises an error, catch it and return an appropriate
|
||||
;; error code
|
||||
(define (blodwen-file-op op)
|
||||
(guard
|
||||
(x ((i/o-error? x) (either-left (blodwen-error-code x))))
|
||||
(either-right (op))))
|
||||
|
||||
(define (blodwen-get-n n p)
|
||||
(if (port? p) (get-string-n p n) ""))
|
||||
|
||||
(define (blodwen-putstring p s)
|
||||
(if (port? p) (put-string p s) void)
|
||||
0)
|
||||
|
||||
(define (blodwen-open file mode bin)
|
||||
(define tc (if (= bin 1) #f (make-transcoder (utf-8-codec))))
|
||||
(define bm (buffer-mode line))
|
||||
(case mode
|
||||
(("r") (open-file-input-port file (file-options) bm tc))
|
||||
(("w") (open-file-output-port file (file-options no-fail) bm tc))
|
||||
(("wx") (open-file-output-port file (file-options) bm tc))
|
||||
(("a") (open-file-output-port file (file-options no-fail no-truncate) bm tc))
|
||||
(("r+") (open-file-input/output-port file (file-options no-create) bm tc))
|
||||
(("w+") (open-file-input/output-port file (file-options no-fail) bm tc))
|
||||
(("w+x") (open-file-input/output-port file (file-options) bm tc))
|
||||
(("a+") (open-file-input/output-port file (file-options no-fail no-truncate) bm tc))
|
||||
(else (raise (make-i/o-error)))))
|
||||
|
||||
(define (blodwen-close-port p)
|
||||
(when (port? p) (close-port p)))
|
||||
|
||||
(define (blodwen-get-line p)
|
||||
(if (port? p)
|
||||
(let ((str (get-line p)))
|
||||
@ -172,44 +73,6 @@
|
||||
chr))
|
||||
void))
|
||||
|
||||
(define (blodwen-file-modified-time p)
|
||||
(time-second (file-modification-time p)))
|
||||
|
||||
(define (blodwen-file-size p)
|
||||
(port-length p))
|
||||
|
||||
(define (blodwen-eof p)
|
||||
(if (port-eof? p)
|
||||
1
|
||||
0))
|
||||
|
||||
;; Directories
|
||||
|
||||
(define (blodwen-current-directory)
|
||||
(current-directory))
|
||||
|
||||
(define (blodwen-change-directory dir)
|
||||
(if (file-directory? dir)
|
||||
(begin (current-directory dir) 1)
|
||||
0))
|
||||
|
||||
(define (blodwen-create-directory dir)
|
||||
(blodwen-file-op (lambda () (mkdir dir) 0)))
|
||||
|
||||
; Scheme only gives a primitive for reading all the files in a directory,
|
||||
; so this is faking the C interface!
|
||||
(define (blodwen-open-directory dir)
|
||||
(blodwen-file-op (lambda () (box (directory-list dir)))))
|
||||
|
||||
(define (blodwen-close-directory dir) '()) ; no-op, it's not really open
|
||||
|
||||
(define (blodwen-next-dir-entry dir)
|
||||
(let [(dlist (unbox dir))]
|
||||
(if (null? dlist)
|
||||
(either-left 255)
|
||||
(begin (set-box! dir (cdr dlist))
|
||||
(either-right (car dlist))))))
|
||||
|
||||
;; Threads
|
||||
|
||||
(define blodwen-thread-data (make-thread-parameter #f))
|
||||
|
@ -69,101 +69,6 @@
|
||||
(newline)
|
||||
(exit 1)))
|
||||
|
||||
;; Buffers
|
||||
|
||||
(define blodwen-new-buffer make-u8vector)
|
||||
(define blodwen-buffer-size u8vector-length)
|
||||
|
||||
(define blodwen-buffer-setbyte ##u8vector-set!)
|
||||
(define blodwen-buffer-getbyte ##u8vector-ref)
|
||||
|
||||
(define blodwen-buffer-setint ##s32vector-set!)
|
||||
(define blodwen-buffer-getint ##s32vector-ref)
|
||||
|
||||
(define blodwen-buffer-setdouble ##f64vector-set!)
|
||||
(define blodwen-buffer-getdouble ##f64vector-ref)
|
||||
|
||||
(define (blodwen-stringbytelen str)
|
||||
(u8vector-length (string->utf8 str)))
|
||||
|
||||
(define (blodwen-buffer-setstring buf loc val)
|
||||
(let* ((strvec (string->utf8 val))
|
||||
(len (u8vector-length strvec)))
|
||||
(u8vector-copy! buf loc strvec 0 len)))
|
||||
|
||||
(define (blodwen-buffer-getstring buf loc len)
|
||||
(let ((newvec (make-u8vector len)))
|
||||
(u8vector-copy! newvec 0 buf loc (fx+ loc len))
|
||||
(utf8->string newvec)))
|
||||
|
||||
(define (blodwen-buffer-copydata buf start len dest loc)
|
||||
(u8vector-copy! dest loc buf start (fx+ start len)))
|
||||
|
||||
(define (blodwen-readbuffer-bytes h buf loc max)
|
||||
(with-exception-catcher
|
||||
(lambda (e) -1)
|
||||
(lambda () (read-subu8vector buf loc (fx+ loc max) h))))
|
||||
|
||||
(define (blodwen-readbuffer h)
|
||||
(with-exception-catcher
|
||||
(lambda (e) #u8())
|
||||
(lambda () (list->u8vector (read-all h read-u8)))))
|
||||
|
||||
(define (blodwen-writebuffer h buf loc max)
|
||||
(with-exception-catcher
|
||||
(lambda (e) -1)
|
||||
(lambda () (write-subu8vector buf loc (fx+ loc max) h) max)))
|
||||
|
||||
;; Files
|
||||
|
||||
;; Only used in this file for errno extraction
|
||||
(define-macro (errno-magic)
|
||||
(fx- 0 (fxnot (fx- (fxarithmetic-shift 1 29) 1)) (fxarithmetic-shift 320 16)))
|
||||
|
||||
;; If the file operation raises an error, catch it and return an appropriate
|
||||
;; error code
|
||||
(define (blodwen-file-op op)
|
||||
;; All the file operations are implemented as primitives which return
|
||||
;; Either Int x, where the Int is an error code:
|
||||
(define (blodwen-error-code x)
|
||||
(either-left
|
||||
;; TODO Equivalent of i/o-read-error? and i/o-write-error?
|
||||
;; TODO Uncomment the lines below on the next release (> 4.9.3) of Gambit
|
||||
(cond ((no-such-file-or-directory-exception? x) 3)
|
||||
; ((permission-denied-exception? x) 4)
|
||||
; ((file-exists-exception? x) 5)
|
||||
(else (fx+ (os-exception-code x) (errno-magic) 256)))))
|
||||
(with-exception-catcher
|
||||
blodwen-error-code
|
||||
(lambda () (either-right (op)))))
|
||||
|
||||
#|
|
||||
(define (blodwen-get-n n p)
|
||||
(if (input-port? p) (read-string n p) ""))
|
||||
|#
|
||||
|
||||
(define (blodwen-putstring p s)
|
||||
(if (output-port? p) (write-string s p))
|
||||
0)
|
||||
|
||||
(define (blodwen-open file mode bin)
|
||||
(define settings
|
||||
(if (fx= bin 1)
|
||||
`(path: ,file buffering: line)
|
||||
`(path: ,file buffering: line char-encoding: UTF-8)))
|
||||
(cond
|
||||
((string=? mode "r") (open-input-file settings))
|
||||
((string=? mode "w") (open-output-file settings))
|
||||
((string=? mode "wx") (open-output-file `(,@settings create: #t)))
|
||||
((string=? mode "a") (open-output-file `(,@settings append: #t)))
|
||||
((string=? mode "r+") (open-file settings))
|
||||
((string=? mode "w+") (open-file `(,@settings create: maybe truncate: #t)))
|
||||
((string=? mode "w+x") (open-file `(,@settings create: #t truncate: #t)))
|
||||
((string=? mode "a+") (open-file `(,@settings create: maybe append: #t)))))
|
||||
|
||||
(define (blodwen-close-port p)
|
||||
(if (port? p) (close-port p)))
|
||||
|
||||
(define (blodwen-get-line p)
|
||||
(if (input-port? p)
|
||||
(let ((str (read-line p)))
|
||||
@ -176,40 +81,6 @@
|
||||
(if (eof-object? chr) #\null chr))
|
||||
#\null))
|
||||
|
||||
(define (blodwen-file-modified-time p) ; XXX
|
||||
(exact-floor (time->seconds (file-last-modification-time (##port-name p)))))
|
||||
|
||||
#|
|
||||
(define (blodwen-file-size p) ; XXX
|
||||
(file-size (##port-name p)))
|
||||
|#
|
||||
|
||||
(define (blodwen-eof p)
|
||||
(if (eof-object? (peek-char p)) 1 0))
|
||||
|
||||
;; Directories
|
||||
|
||||
(define blodwen-current-directory current-directory)
|
||||
|
||||
(define (blodwen-change-directory dir)
|
||||
(with-exception-catcher
|
||||
(lambda (e) 0)
|
||||
(lambda () (current-directory dir) 1)))
|
||||
|
||||
(define (blodwen-create-directory dir)
|
||||
(blodwen-file-op (lambda () (create-directory dir) 0)))
|
||||
|
||||
(define (blodwen-open-directory dir)
|
||||
(blodwen-file-op (lambda () (open-directory dir))))
|
||||
|
||||
(define blodwen-close-directory close-input-port)
|
||||
|
||||
(define (blodwen-next-dir-entry dir)
|
||||
(let ((e (read dir)))
|
||||
(if (eof-object? e)
|
||||
(either-left 255)
|
||||
(either-right e))))
|
||||
|
||||
;; Threads
|
||||
|
||||
(define (blodwen-thread p)
|
||||
|
@ -54,111 +54,6 @@
|
||||
(newline)
|
||||
(exit 1)))
|
||||
|
||||
;; Buffers
|
||||
|
||||
(define (blodwen-new-buffer size)
|
||||
(make-bytevector size 0))
|
||||
|
||||
(define (blodwen-buffer-size buf)
|
||||
(bytevector-length buf))
|
||||
|
||||
(define (blodwen-buffer-setbyte buf loc val)
|
||||
(bytevector-u8-set! buf loc val))
|
||||
|
||||
(define (blodwen-buffer-getbyte buf loc)
|
||||
(bytevector-u8-ref buf loc))
|
||||
|
||||
(define (blodwen-buffer-setint buf loc val)
|
||||
(bytevector-s32-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getint buf loc)
|
||||
(bytevector-s32-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-setdouble buf loc val)
|
||||
(bytevector-ieee-double-set! buf loc val (native-endianness)))
|
||||
|
||||
(define (blodwen-buffer-getdouble buf loc)
|
||||
(bytevector-ieee-double-ref buf loc (native-endianness)))
|
||||
|
||||
(define (blodwen-stringbytelen str)
|
||||
(bytevector-length (string->utf8 str)))
|
||||
|
||||
(define (blodwen-buffer-setstring buf loc val)
|
||||
(let* [(strvec (string->utf8 val))
|
||||
(len (bytevector-length strvec))]
|
||||
(bytevector-copy! strvec 0 buf loc len)))
|
||||
|
||||
(define (blodwen-buffer-getstring buf loc len)
|
||||
(let [(newvec (make-bytevector len))]
|
||||
(bytevector-copy! buf loc newvec 0 len)
|
||||
(utf8->string newvec)))
|
||||
|
||||
(define (blodwen-buffer-copydata buf start len dest loc)
|
||||
(bytevector-copy! buf start dest loc len))
|
||||
|
||||
(define (blodwen-readbuffer-bytes h buf loc max)
|
||||
(with-handlers
|
||||
([(lambda (x) #t) (lambda (exn) -1)])
|
||||
(get-bytevector-n! h buf loc max)))
|
||||
|
||||
(define (blodwen-readbuffer h)
|
||||
(with-handlers
|
||||
([(lambda (x) #t) (lambda (exn) (make-bytevector 0))])
|
||||
(get-bytevector-all h)))
|
||||
|
||||
(define (blodwen-writebuffer h buf loc max)
|
||||
(with-handlers
|
||||
([(lambda (x) #t) (lambda (exn) -1)])
|
||||
(put-bytevector h buf loc max)))
|
||||
|
||||
;; Files : Much of the following adapted from idris-chez, thanks to Niklas
|
||||
;; Larsson
|
||||
|
||||
;; All the file operations are implemented as primitives which return
|
||||
;; Either Int x, where the Int is an error code
|
||||
(define (blodwen-error-code x)
|
||||
(cond
|
||||
((eq? x (lookup-errno 'ENOENT)) 3)
|
||||
((eq? x (lookup-errno 'EACCES)) 4)
|
||||
((eq? x (lookup-errno 'EEXIST)) 5)
|
||||
(else (+ x 256))))
|
||||
|
||||
;; If the file operation raises an error, catch it and return an appropriate
|
||||
;; error code
|
||||
(define (blodwen-file-op op)
|
||||
(with-handlers
|
||||
([exn:fail:filesystem:errno?
|
||||
(lambda (exn) (either-left (blodwen-error-code
|
||||
(car (exn:fail:filesystem:errno-errno exn)))))]
|
||||
[exn:fail:filesystem?
|
||||
(lambda (exn) (either-left 255))]
|
||||
)
|
||||
(either-right (op))))
|
||||
|
||||
(define (blodwen-putstring p s)
|
||||
(if (port? p) (write-string s p) void)
|
||||
0)
|
||||
|
||||
(define (blodwen-open file mode bin)
|
||||
(define tc (if (= bin 1) #f (make-transcoder (utf-8-codec))))
|
||||
(define bm (buffer-mode line))
|
||||
(case mode
|
||||
(("r") (open-file-input-port file (file-options) bm tc))
|
||||
(("w") (open-file-output-port file (file-options no-fail) bm tc))
|
||||
(("wx") (open-file-output-port file (file-options) bm tc))
|
||||
(("a") (open-file-output-port file (file-options no-fail no-truncate) bm tc))
|
||||
(("r+") (open-file-input/output-port file (file-options no-create) bm tc))
|
||||
(("w+") (open-file-input/output-port file (file-options no-fail) bm tc))
|
||||
(("w+x") (open-file-input/output-port file (file-options) bm tc))
|
||||
(("a+") (open-file-input/output-port file (file-options no-fail no-truncate) bm tc))
|
||||
(else (raise (make-i/o-error)))))
|
||||
|
||||
|
||||
(define (blodwen-close-port p)
|
||||
(cond
|
||||
((input-port? p) (close-input-port p))
|
||||
((output-port? p) (close-output-port p))))
|
||||
|
||||
(define (blodwen-get-line p)
|
||||
(if (port? p)
|
||||
(let ((str (read-line p)))
|
||||
@ -175,38 +70,6 @@
|
||||
chr))
|
||||
void))
|
||||
|
||||
(define (blodwen-eof p)
|
||||
(if (eof-object? (peek-char p))
|
||||
1
|
||||
0))
|
||||
|
||||
;; Directories
|
||||
|
||||
(define (blodwen-current-directory)
|
||||
(path->string (current-directory)))
|
||||
|
||||
(define (blodwen-change-directory dir)
|
||||
(if (directory-exists? dir)
|
||||
(begin (current-directory dir) 1)
|
||||
0))
|
||||
|
||||
(define (blodwen-create-directory dir)
|
||||
(blodwen-file-op (lambda () (make-directory dir))))
|
||||
|
||||
; Scheme only gives a primitive for reading all the files in a directory,
|
||||
; so this is faking the C interface!
|
||||
(define (blodwen-open-directory dir)
|
||||
(blodwen-file-op (lambda () (box (directory-list dir)))))
|
||||
|
||||
(define (blodwen-close-directory dir) '()) ; no-op, it's not really open
|
||||
|
||||
(define (blodwen-next-dir-entry dir)
|
||||
(let [(dlist (unbox dir))]
|
||||
(if (null? dlist)
|
||||
(either-left 255)
|
||||
(begin (set-box! dir (cdr dlist))
|
||||
(either-right (path->string (car dlist)))))))
|
||||
|
||||
;; Threads
|
||||
|
||||
(define blodwen-thread-data (make-thread-cell #f))
|
||||
|
@ -98,7 +98,7 @@ chezTests : List String
|
||||
chezTests
|
||||
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
|
||||
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
||||
"chez013", "chez014", "chez015", "chez016", "chez017",
|
||||
"chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
|
||||
"reg001"]
|
||||
|
||||
ideModeTests : List String
|
||||
|
14
tests/chez/chez018/File.idr
Normal file
14
tests/chez/chez018/File.idr
Normal file
@ -0,0 +1,14 @@
|
||||
import System.File
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do Right ok <- readFile "test.txt"
|
||||
| Left err => printLn err
|
||||
putStr ok
|
||||
writeFile "testout.txt" "abc\ndef\n"
|
||||
Right ok <- readFile "testout.txt"
|
||||
| Left err => printLn err
|
||||
putStr ok
|
||||
Right ok <- readFile "notfound"
|
||||
| Left err => printLn err
|
||||
putStr ok
|
6
tests/chez/chez018/expected
Normal file
6
tests/chez/chez018/expected
Normal file
@ -0,0 +1,6 @@
|
||||
test test
|
||||
unfinished lineabc
|
||||
def
|
||||
File Not Found
|
||||
1/1: Building File (File.idr)
|
||||
Main> Main> Bye for now!
|
2
tests/chez/chez018/input
Normal file
2
tests/chez/chez018/input
Normal file
@ -0,0 +1,2 @@
|
||||
:exec main
|
||||
:q
|
3
tests/chez/chez018/run
Executable file
3
tests/chez/chez018/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --no-banner File.idr < input
|
||||
|
||||
rm -rf build testout.txt
|
2
tests/chez/chez018/test.txt
Normal file
2
tests/chez/chez018/test.txt
Normal file
@ -0,0 +1,2 @@
|
||||
test test
|
||||
unfinished line
|
Loading…
Reference in New Issue
Block a user