mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 00:31:57 +03:00
dbdf7dab3d
Following a fairly detailed discussion on slack, the feeling is generally that it's better to have a single interface. While precision is nice, it doesn't appear to buy us anything here. If that turns out to be wrong, or limiting somehow, we can revisit it later. Also: - it's easier for backend authors if the type of IO operations is slightly less restrictive. For example, if it's in HasIO, that limits alternative implementations, which might be awkward for some alternative back ends. - it's one less extra detail to learn. This is minor, but there needs to be a clear advantage if there's more detail to learn. - It is difficult to think of an underlying type that can't have a Monad instance (I have personally never encountered one - if they turns out to exist, again, we can revisit!)
99 lines
2.5 KiB
Idris
99 lines
2.5 KiB
Idris
module System.Directory
|
|
|
|
import public System.File
|
|
|
|
public export
|
|
DirPtr : Type
|
|
DirPtr = AnyPtr
|
|
|
|
support : String -> String
|
|
support fn = "C:" ++ fn ++ ", libidris2_support"
|
|
|
|
%foreign support "idris2_fileErrno"
|
|
prim_fileErrno : PrimIO Int
|
|
|
|
returnError : HasIO io => 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))
|
|
|
|
ok : HasIO io => 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 support "idris2_createDir"
|
|
prim_createDir : String -> PrimIO Int
|
|
|
|
%foreign support "idris2_openDir"
|
|
prim_openDir : String -> PrimIO DirPtr
|
|
|
|
%foreign support "idris2_closeDir"
|
|
prim_closeDir : DirPtr -> PrimIO ()
|
|
|
|
%foreign support "idris2_removeDir"
|
|
prim_removeDir : String -> PrimIO ()
|
|
|
|
%foreign support "idris2_nextDirEntry"
|
|
prim_dirEntry : DirPtr -> PrimIO (Ptr String)
|
|
|
|
export
|
|
data Directory : Type where
|
|
MkDir : DirPtr -> Directory
|
|
|
|
export
|
|
createDir : HasIO io => String -> io (Either FileError ())
|
|
createDir dir
|
|
= do res <- primIO (prim_createDir dir)
|
|
if res == 0
|
|
then ok ()
|
|
else returnError
|
|
|
|
export
|
|
changeDir : HasIO io => String -> io Bool
|
|
changeDir dir
|
|
= do ok <- primIO (prim_changeDir dir)
|
|
pure (ok == 0)
|
|
|
|
export
|
|
currentDir : HasIO io => io (Maybe String)
|
|
currentDir
|
|
= do res <- primIO prim_currentDir
|
|
if prim__nullPtr res /= 0
|
|
then pure Nothing
|
|
else pure (Just (prim__getString res))
|
|
|
|
export
|
|
openDir : HasIO io => String -> io (Either FileError Directory)
|
|
openDir d
|
|
= do res <- primIO (prim_openDir d)
|
|
if prim__nullAnyPtr res /= 0
|
|
then returnError
|
|
else ok (MkDir res)
|
|
|
|
export
|
|
closeDir : HasIO io => Directory -> io ()
|
|
closeDir (MkDir d) = primIO (prim_closeDir d)
|
|
|
|
export
|
|
removeDir : HasIO io => String -> io ()
|
|
removeDir dirName = primIO (prim_removeDir dirName)
|
|
|
|
export
|
|
dirEntry : HasIO io => Directory -> io (Either FileError String)
|
|
dirEntry (MkDir d)
|
|
= do res <- primIO (prim_dirEntry d)
|
|
if prim__nullPtr res /= 0
|
|
then returnError
|
|
else ok (prim__getString res)
|