git.iko.soy/Idris-dev
on master help sign in
Add directory management functions

This uses the POSIX API, so I don't know if it'll work in Windows (I assume not. Sorry.)

commit5eb8f8393f068fb04aaf02d0a8617d16f5092d93 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 5 Jan 2018, 18:30 (9 years ago) parentd1fae54
3 files changed+104
compare with master
unifiedsplit
libs/prelude/Prelude/File.idr+48 rts/idris_stdfgn.c+45 rts/idris_stdfgn.h+11
libs/prelude/Prelude/File.idr+48
@@ -21,8 +21,13 @@ import IO
2121data File : Type where
2222 FHandle : (p : Ptr) -> File
2323
24+||| A directory handle
25+data Directory : Type where
26+ DHandle : (p : Ptr) -> Directory
27+
2428-- Usage hints for erasure analysis
2529%used FHandle p
30+%used DHandle p
2631
2732||| An error from a file operation
2833-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
@@ -280,3 +285,46 @@ writeFile fn contents = do
280285 Right () <- fPutStr h contents | Left err => pure (Left err)
281286 closeFile h
282287 pure (Right ())
288+
289+
290+export
291+dirOpen : (d : String) -> IO (Either FileError Directory)
292+dirOpen d
293+ = do dptr <- foreign FFI_C "idris_dirOpen" (String -> IO Ptr) d
294+ if !(nullPtr dptr)
295+ then do err <- getFileError
296+ pure (Left err)
297+ else pure (Right (DHandle dptr))
298+
299+export
300+dirClose : Directory -> IO ()
301+dirClose (DHandle d) = foreign FFI_C "idris_dirClose" (Ptr -> IO ()) d
302+
303+export
304+dirError : Directory -> IO Bool
305+dirError (DHandle d)
306+ = do err <- foreign FFI_C "idris_dirError" (Ptr -> IO Int) d
307+ pure (not (err == 0))
308+
309+export
310+dirEntry : Directory -> IO (Either FileError String)
311+dirEntry (DHandle d)
312+ = do fn <- foreign FFI_C "idris_nextDirEntry" (Ptr -> IO String) d
313+ if !(dirError (DHandle d))
314+ then pure (Left FileReadError)
315+ else pure (Right fn)
316+
317+export
318+createDir : String -> IO (Either FileError ())
319+createDir d
320+ = do ok <- foreign FFI_C "idris_mkdir" (String -> IO Int) d
321+ if (ok == 0)
322+ then pure (Right ())
323+ else do err <- getFileError
324+ pure (Left err)
325+
326+export
327+changeDir : String -> IO Bool
328+changeDir dir
329+ = do ok <- foreign FFI_C "chdir" (String -> IO Int) dir
330+ pure (ok == 0)
rts/idris_stdfgn.c+45
@@ -8,6 +8,7 @@
88#include <sys/stat.h>
99#include <stdio.h>
1010#include <time.h>
11+#include <dirent.h>
1112
1213#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
1314int win_fpoll(void* h);
@@ -59,6 +60,50 @@ int fileSize(void* h) {
5960 }
6061}
6162
63+typedef struct {
64+ DIR* dirptr;
65+ int error;
66+} DirInfo;
67+
68+void* idris_dirOpen(char* dname) {
69+ DIR *d = opendir(dname);
70+ if (d == NULL) {
71+ return NULL;
72+ } else {
73+ DirInfo* di = malloc(sizeof(DirInfo));
74+ di->dirptr = d;
75+
76+ return (void*)di;
77+ }
78+}
79+
80+void idris_dirClose(void* h) {
81+ DirInfo* di = (DirInfo*)h;
82+
83+ closedir(di->dirptr);
84+ free(di);
85+}
86+
87+char* idris_nextDirEntry(void* h) {
88+ DirInfo* di = (DirInfo*)h;
89+ struct dirent* de = readdir(di->dirptr);
90+
91+ if (de == NULL) {
92+ di->error = -1;
93+ return NULL;
94+ } else {
95+ return de->d_name;
96+ }
97+}
98+
99+int idris_mkdir(char* dname) {
100+ return mkdir(dname, S_IRWXU | S_IRGRP | S_IROTH);
101+}
102+
103+int idris_dirError(void *dptr) {
104+ return ((DirInfo*)dptr)->error;
105+}
106+
62107int idris_writeStr(void* h, char* str) {
63108 FILE* f = (FILE*)h;
64109 if (fputs(str, f) >= 0) {
rts/idris_stdfgn.h+11
@@ -15,6 +15,17 @@ int fileError(void* h);
1515// Returns a negative number if not a file (e.g. directory or device)
1616int fileSize(void* h);
1717
18+void* idris_dirOpen(char* dname);
19+void idris_dirClose(void* h);
20+char* idris_nextDirEntry(void* h);
21+
22+// Create a directory; return 0 on success or -1 on failure
23+int idris_mkdir(char* dname);
24+
25+// Return 0 if ok, or -1 if there was an error with the given directory
26+// (like ferror)
27+int idris_dirError(void *dptr);
28+
1829// return 0 on success
1930int idris_writeStr(void*h, char* str);
2031// construct a file error structure (see Prelude.File) from errno