c7a05af · Idris-dev · git.iko.soy

libs/prelude/Prelude/File.idr+11

compare with master

unifiedsplit

@@ -289,6 +289,17 @@ fEOF : File -> IO Bool

289fEOF (FHandle h) = do eof <- do_feof h

290 pure (not (eof == 0))

291

292+private

293+do_fremove : String -> IO Int

294+do_fremove s = foreign FFI_C "fileRemove" (String -> IO Int) s

295+

296+||| Remove a file

297+||| @s the file name

298+export

299+fRemove : (s : String) -> IO Bool

300+fRemove s = do res <- do_fremove s

301+ pure (res == 0)

302+

292export

303export

293fpoll : File -> IO Bool

304fpoll : File -> IO Bool

294fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

305fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

rts/idris_stdfgn.c+4

@@ -46,6 +46,10 @@ int fileError(void* h) {

46 return ferror(f);

47}

48

49+int fileRemove(const char *filename) {

50+ return remove(filename);

51+}

52+

49int fileSize(void* h) {

53int fileSize(void* h) {

50 FILE* f = (FILE*)h;

54 FILE* f = (FILE*)h;

51 int fd = fileno(f);

55 int fd = fileno(f);

rts/idris_stdfgn.h+1

@@ -12,6 +12,7 @@ void* fileOpen(char* f, char* mode);

12void fileClose(void* h);

13int fileEOF(void* h);

14int fileError(void* h);

15+int fileRemove(const char* fname);

15// Returns a negative number if not a file (e.g. directory or device)

16// Returns a negative number if not a file (e.g. directory or device)

16int fileSize(void* h);

17int fileSize(void* h);

17

18

src/Idris/Core/Execute.hs+12

@@ -30,6 +30,7 @@ import Data.Maybe

30import Data.Time.Clock.POSIX (getPOSIXTime)

31import Data.Traversable (forM)

32import Debug.Trace

33+import System.Directory

33import System.IO

34import System.IO

34import System.IO.Error

35import System.IO.Error

35import System.IO.Unsafe

36import System.IO.Unsafe

@@ -387,6 +388,17 @@ execForeign env ctxt arity ty fn xs onfail

387 "The argument to fileError should be a file handle, but it was " ++

388 "The argument to fileError should be a file handle, but it was " ++

388 show handle ++

389 show handle ++

389 ". Are all cases covered?"

390 ". Are all cases covered?"

391+ | Just (FFun "fileRemove" [(_,fileStr)] _) <- foreignFromTT arity ty fn xs

392+ = case fileStr of

393+ EConstant (Str f) -> do res <- execIO $ catch (do removeFile f

394+ return $ ioWrap $ EConstant $ I 0)

395+ (\e -> do writeIORef fileError $ mapError e

396+ return $ ioWrap $ EConstant $ I (-1))

397+ execApp env ctxt res (drop arity xs)

398+ _ -> execFail . Msg $

399+ "The argument to fileRemove should be a constant string, but it was " ++

400+ show fileStr ++

401+ ". Are all cases covered?"

390 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs

402 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs

391 = case handle of

403 = case handle of

392 EHandle h -> do execIO $ hClose h

404 EHandle h -> do execIO $ hClose h

test/TestData.hs+1

@@ -141,6 +141,7 @@ testFamiliesData = [

141 , ( 10, NODE_CG )

142 , ( 11, NODE_CG )

143 , ( 12, NODE_CG )

144+ , ( 13, C_CG )

144 ]),

145 ]),

145 ("folding", "Folding",

146 ("folding", "Folding",

146 [ ( 1, ANY )]),

147 [ ( 1, ANY )]),

test/ffi013/expectednew file+4

@@ -0,0 +1,4 @@

1+success

2+confirmed

3+success

4+confirmed

test/ffi013/ffi013.idrnew file+5

@@ -0,0 +1,5 @@

1+module Main

2+

3+main : IO ()

4+main = do b <- fRemove "remove.me"

5+ putStrLn $ if b then "success" else "failure"

test/ffi013/runnew file+17

@@ -0,0 +1,17 @@

1+#!/usr/bin/env bash

2+echo "test" > remove.me

3+${IDRIS:-idris} $@ --quiet --port none ffi013.idr -o ffi013

4+./ffi013

5+if [ -f "remove.me" ]; then

6+ echo "still exists"

7+else

8+ echo "confirmed"

9+fi

10+echo "test2" > remove.me

11+${IDRIS:-idris} $@ --quiet --port none --nocolour ffi013.idr --exec main

12+if [ -f "remove.me" ]; then

13+ echo "still exists"

14+else

15+ echo "confirmed"

16+fi

17+rm -f ffi013 remove.me *.ibc