Skip to content

Commit

Permalink
Add directory management functions
Browse files Browse the repository at this point in the history
This uses the POSIX API, so I don't know if it'll work in Windows (I
assume not. Sorry.)
  • Loading branch information
edwinb committed Jan 5, 2018
1 parent d1fae54 commit 5eb8f83
Show file tree
Hide file tree
Showing 3 changed files with 104 additions and 0 deletions.
48 changes: 48 additions & 0 deletions libs/prelude/Prelude/File.idr
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,13 @@ import IO
data File : Type where
FHandle : (p : Ptr) -> File

||| A directory handle
data Directory : Type where
DHandle : (p : Ptr) -> Directory

-- Usage hints for erasure analysis
%used FHandle p
%used DHandle p

||| An error from a file operation
-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
Expand Down Expand Up @@ -280,3 +285,46 @@ writeFile fn contents = do
Right () <- fPutStr h contents | Left err => pure (Left err)
closeFile h
pure (Right ())


export
dirOpen : (d : String) -> IO (Either FileError Directory)
dirOpen d
= do dptr <- foreign FFI_C "idris_dirOpen" (String -> IO Ptr) d
if !(nullPtr dptr)
then do err <- getFileError
pure (Left err)
else pure (Right (DHandle dptr))

export
dirClose : Directory -> IO ()
dirClose (DHandle d) = foreign FFI_C "idris_dirClose" (Ptr -> IO ()) d

export
dirError : Directory -> IO Bool
dirError (DHandle d)
= do err <- foreign FFI_C "idris_dirError" (Ptr -> IO Int) d
pure (not (err == 0))

export
dirEntry : Directory -> IO (Either FileError String)
dirEntry (DHandle d)
= do fn <- foreign FFI_C "idris_nextDirEntry" (Ptr -> IO String) d
if !(dirError (DHandle d))
then pure (Left FileReadError)
else pure (Right fn)

export
createDir : String -> IO (Either FileError ())
createDir d
= do ok <- foreign FFI_C "idris_mkdir" (String -> IO Int) d
if (ok == 0)
then pure (Right ())
else do err <- getFileError
pure (Left err)

export
changeDir : String -> IO Bool
changeDir dir
= do ok <- foreign FFI_C "chdir" (String -> IO Int) dir
pure (ok == 0)
45 changes: 45 additions & 0 deletions rts/idris_stdfgn.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
#include <sys/stat.h>
#include <stdio.h>
#include <time.h>
#include <dirent.h>

#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
int win_fpoll(void* h);
Expand Down Expand Up @@ -59,6 +60,50 @@ int fileSize(void* h) {
}
}

typedef struct {
DIR* dirptr;
int error;
} DirInfo;

void* idris_dirOpen(char* dname) {
DIR *d = opendir(dname);
if (d == NULL) {
return NULL;
} else {
DirInfo* di = malloc(sizeof(DirInfo));
di->dirptr = d;

return (void*)di;
}
}

void idris_dirClose(void* h) {
DirInfo* di = (DirInfo*)h;

closedir(di->dirptr);
free(di);
}

char* idris_nextDirEntry(void* h) {
DirInfo* di = (DirInfo*)h;
struct dirent* de = readdir(di->dirptr);

if (de == NULL) {
di->error = -1;
return NULL;
} else {
return de->d_name;
}
}

int idris_mkdir(char* dname) {
return mkdir(dname, S_IRWXU | S_IRGRP | S_IROTH);
}

int idris_dirError(void *dptr) {
return ((DirInfo*)dptr)->error;
}

int idris_writeStr(void* h, char* str) {
FILE* f = (FILE*)h;
if (fputs(str, f) >= 0) {
Expand Down
11 changes: 11 additions & 0 deletions rts/idris_stdfgn.h
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,17 @@ int fileError(void* h);
// Returns a negative number if not a file (e.g. directory or device)
int fileSize(void* h);

void* idris_dirOpen(char* dname);
void idris_dirClose(void* h);
char* idris_nextDirEntry(void* h);

// Create a directory; return 0 on success or -1 on failure
int idris_mkdir(char* dname);

// Return 0 if ok, or -1 if there was an error with the given directory
// (like ferror)
int idris_dirError(void *dptr);

// return 0 on success
int idris_writeStr(void*h, char* str);
// construct a file error structure (see Prelude.File) from errno
Expand Down

0 comments on commit 5eb8f83

Please sign in to comment.