2405b0b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

add fRemove FFI call

commit2405b0b42518cbbb582b018326415806e38140b3 authorAlex Gryzlov <skyrodent@gmail.com> dateWed 10 Jul 2019, 13:21 (7 years ago) parent26fa6c3

6 files changed+36

compare with master

unifiedsplit

libs/prelude/Prelude/File.idr+11 rts/idris_stdfgn.c+4 rts/idris_stdfgn.h+1 src/Idris/Core/Execute.hs+10 test/ffi013/ffi013.idr+5 test/ffi013/run+5

libs/prelude/Prelude/File.idr+11

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

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

290290 pure (not (eof == 0))

291291

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+

292303export

293304fpoll : File -> IO Bool

294305fpoll (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) {

4646 return ferror(f);

4747}

4848

49+int fileRemove(const char *filename) {

50+ return remove(filename);

51+}

52+

4953int fileSize(void* h) {

5054 FILE* f = (FILE*)h;

5155 int fd = fileno(f);

rts/idris_stdfgn.h+1

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

1212void fileClose(void* h);

1313int fileEOF(void* h);

1414int fileError(void* h);

15+int fileRemove(const char* fname);

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

1617int fileSize(void* h);

1718

src/Idris/Core/Execute.hs+10

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

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

3131import Data.Traversable (forM)

3232import Debug.Trace

33+import System.Directory

3334import System.IO

3435import System.IO.Error

3536import System.IO.Unsafe

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

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

388389 show handle ++

389390 ". Are all cases covered?"

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

392+ = case fileStr of

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

394+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

395+ execApp env ctxt res (drop arity xs)

396+ _ -> execFail . Msg $

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

398+ show handle ++

399+ ". Are all cases covered?"

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

391401 = case handle of

392402 EHandle h -> do execIO $ hClose h

test/ffi013/ffi013.idrnew file+5

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

1+module Main

3+main : IO ()

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

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

test/ffi013/runnew file+5

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

1+#!/usr/bin/env bash

2+echo "test" > remove.me

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

4+./ffi013

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