91 lines · 2.2 KB · Text
RawDownload
module System.Directory import public System.File public exportDirPtr : TypeDirPtr = AnyPtr support : String -> Stringsupport fn = "C:" ++ fn ++ ", libidris2_support" %foreign support "idris2_fileErrno"prim_fileErrno : PrimIO Int 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)) 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 support "idris2_createDir"prim_createDir : String -> PrimIO Int %foreign support "idris2_dirOpen"prim_openDir : String -> PrimIO DirPtr %foreign support "idris2_dirClose"prim_closeDir : DirPtr -> PrimIO () %foreign support "idris2_nextDirEntry"prim_dirEntry : DirPtr -> PrimIO (Ptr String) exportdata Directory : Type where     MkDir : DirPtr -> Directory exportcreateDir : String -> IO (Either FileError ())createDir dir    = do res <- primIO (prim_createDir dir)         if res == 0            then ok ()            else returnError exportchangeDir : String -> IO BoolchangeDir dir    = do ok <- primIO (prim_changeDir dir)         pure (ok == 0) exportcurrentDir : IO (Maybe String)currentDir    = do res <- primIO prim_currentDir         if prim__nullPtr res /= 0            then pure Nothing            else pure (Just (prim__getString res)) exportdirOpen : String -> IO (Either FileError Directory)dirOpen d    = do res <- primIO (prim_openDir d)         if prim__nullAnyPtr res /= 0            then returnError            else ok (MkDir res) exportdirClose : Directory -> IO ()dirClose (MkDir d) = primIO (prim_closeDir d) exportdirEntry : 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)

Keyboard shortcuts

General

Show keyboard shortcuts
?
Focus the current search
/

Issues and pull requests

Open filters
f

Issues, pull requests and Inbox

Select next item
j↓
Select previous item
k↑
Open selected item
Enter
Dismiss filters or clear selection
Esc

Repository code

Go to file
t