ce5e330 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add StringBuffer to Prelude.Strings

This allows building up a large string through a series of IO operations without reallocating every time. We can use this, for example, to implement readFile better. Also: added prim__readChars which reads a specific number of characters from a file (truncates if they aren't available), updated readFile to use the new primitives, and brought the Executor up to date with new primitives. Fixes #3602

commitce5e330fe7ca3ea5b8bd71b13fea6edbdeaf0fa7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 15 Mar 2017, 14:03 (10 years ago) parenteed3117

10 files changed+180−7

compare with master

unifiedsplit

libs/prelude/Builtins.idr+1 libs/prelude/IO.idr+4 libs/prelude/Prelude/File.idr+24−6 libs/prelude/Prelude/Strings.idr+33 rts/idris_rts.c+21 rts/idris_rts.h+3 rts/idris_stdfgn.c+33 rts/idris_stdfgn.h+6 src/IRTS/CodegenC.hs+4 src/Idris/Core/Execute.hs+51−1

libs/prelude/Builtins.idr+1

@@ -210,6 +210,7 @@ export data ManagedPtr : Type

210210export data CData : Type

211211

212212%extern prim__readFile : prim__WorldType -> Ptr -> String

213+%extern prim__readChars : prim__WorldType -> Int -> Ptr -> String

213214%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int

214215

215216%extern prim__vm : prim__WorldType -> Ptr

libs/prelude/IO.idr+4

@@ -134,6 +134,10 @@ prim_write s

134134prim_fread : Ptr -> IO' l String

135135prim_fread h = MkIO (\w => prim_io_pure (prim__readFile (world w) h))

136136

137+prim_freadChars : Int -> Ptr -> IO' l String

138+prim_freadChars len h

139+ = MkIO (\w => prim_io_pure (prim__readChars (world w) len h))

140+

137141prim_fwrite : Ptr -> String -> IO' l Int

138142prim_fwrite h s

139143 = MkIO (\w => prim_io_pure (prim__writeFile (world w) h s))

libs/prelude/Prelude/File.idr+24−6

@@ -156,6 +156,10 @@ private

156156do_fread : Ptr -> IO' l String

157157do_fread h = prim_fread h

158158

159+private

160+do_freadChars : Ptr -> Int -> IO' l String

161+do_freadChars h len = prim_freadChars len h

162+

159163export

160164fgetc : File -> IO (Either FileError Char)

161165fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)

@@ -199,6 +203,15 @@ export

199203fGetLine : (h : File) -> IO (Either FileError String)

200204fGetLine = fread

201205

206+||| Read up to a number of characters from a file

207+||| @h a file handle which must be open for reading

208+export

209+fGetChars : (h : File) -> (len : Int) -> IO (Either FileError String)

210+fGetChars (FHandle h) len = do str <- do_freadChars h len

211+ if !(ferror (FHandle h))

212+ then pure (Left FileReadError)

213+ else pure (Right str)

214+

202215%deprecate fread "Use fGetLine instead"

203216

204217private

@@ -251,10 +264,12 @@ fpoll : File -> IO Bool

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

252265 pure (p > 0)

253266

254−||| Read the contents of a file into a string

267+||| Read the contents of a text file into a string

255268||| This checks the size of the file before beginning to read, and only

256269||| reads that many bytes, to ensure that it remains a total function if

257270||| the file is appended to while being read.

271+||| This only works reliably with text files, since it relies on null-terminated

272+||| strings internally.

258273||| Returns an error if filepath is not a normal file.

259274export

260275readFile : (filepath : String) -> IO (Either FileError String)

@@ -262,19 +277,22 @@ readFile fn = do Right h <- openFile fn Read

262277 | Left err => pure (Left err)

263278 Right max <- fileSize h

264279 | Left err => pure (Left err)

265− c <- readFile' h max ""

280+ sb <- newStringBuffer (max + 1)

281+ c <- readFile' h max sb

266282 closeFile h

267283 pure c

268284 where

269− readFile' : File -> Int -> String -> IO (Either FileError String)

285+ readFile' : File -> Int -> StringBuffer -> IO (Either FileError String)

270286 readFile' h max contents =

271287 do x <- fEOF h

272288 if not x && max > 0

273− then do Right l <- fGetLine h

289+ then do Right l <- fGetChars h 1024000

274290 | Left err => pure (Left err)

291+ addToStringBuffer contents l

275292 assert_total $

276− readFile' h (max - cast (length l)) (contents ++ l)

277− else pure (Right contents)

293+ readFile' h (max - 1024000) contents

294+ else do str <- getStringFromBuffer contents

295+ pure (Right str)

278296

279297||| Write a string to a file

280298export

libs/prelude/Prelude/Strings.idr+33

@@ -36,6 +36,39 @@ foldl1 f (x::xs) = foldl f x xs

3636(++) : String -> String -> String

3737(++) = prim__concat

3838

39+||| A preallocated buffer for building a String. This allows a function (in IO)

40+||| to allocate enough space for a stirng which will be build from smaller

41+||| pieces without having to allocate at every step.

42+||| To build a string using a `StringBuffer`, see `newStringBuffer`,

43+||| `addToStringBuffer` and `getStringFromBuffer`.

44+export

45+data StringBuffer = MkString Ptr

46+

47+||| Create a buffer for a string with maximum length len

48+export

49+newStringBuffer : (len : Int) -> IO StringBuffer

50+newStringBuffer len = do ptr <- foreign FFI_C "idris_makeStringBuffer"

51+ (Int -> IO Ptr) len

52+ pure (MkString ptr)

53+

54+||| Append a string to the end of a string buffer

55+export

56+addToStringBuffer : StringBuffer -> String -> IO ()

57+addToStringBuffer (MkString ptr) str =

58+ foreign FFI_C "idris_addToString" (Ptr -> String -> IO ())

59+ ptr str

60+

61+||| Get the string from a string buffer. The buffer is invalid after

62+||| this.

63+export

64+getStringFromBuffer : StringBuffer -> IO String

65+getStringFromBuffer (MkString ptr) =

66+ do vm <- getMyVM

67+ MkRaw str <- foreign FFI_C "idris_getString"

68+ (Ptr -> Ptr -> IO (Raw String))

69+ vm ptr

70+ pure str

71+

3972||| Returns the first character in the specified string.

4073|||

4174||| Doesn't work for empty strings.

rts/idris_rts.c+21

@@ -239,6 +239,11 @@ void* allocate(size_t size, int outerlock) {

239239#endif

240240 return ptr;

241241 } else {

242+ // If we're trying to allocate something bigger than the heap,

243+ // grow the heap here so that the new heap is big enough.

244+ if (size > vm->heap.size) {

245+ vm->heap.size += size;

246+ }

242247 idris_gc(vm);

243248#ifdef HAS_PTHREAD

244249 if (lock) { // not message passing

@@ -595,6 +600,22 @@ VAL idris_readStr(VM* vm, FILE* h) {

595600 return ret;

596601}

597602

603+VAL idris_readChars(VM* vm, int num, FILE* h) {

604+ VAL ret;

605+ char *buffer = malloc((num+1)*sizeof(char));

606+ size_t len;

607+ len = fread(buffer, sizeof(char), (size_t)num, h);

608+ buffer[len] = '\0';

609+

610+ if (len <= 0) {

611+ ret = MKSTR(vm, "");

612+ } else {

613+ ret = MKSTR(vm, buffer);

614+ }

615+ free(buffer);

616+ return ret;

617+}

618+

598619void idris_crash(char* msg) {

599620 fprintf(stderr, "%s\n", msg);

600621 exit(1);

rts/idris_rts.h+3

@@ -372,7 +372,10 @@ VAL idris_concat(VM* vm, VAL l, VAL r);

372372VAL idris_strlt(VM* vm, VAL l, VAL r);

373373VAL idris_streq(VM* vm, VAL l, VAL r);

374374VAL idris_strlen(VM* vm, VAL l);

375+// Read a line from a file

375376VAL idris_readStr(VM* vm, FILE* h);

377+// Read up to 'num' characters from a file

378+VAL idris_readChars(VM* vm, int num, FILE* h);

376379

377380VAL idris_strHead(VM* vm, VAL str);

378381VAL idris_strTail(VM* vm, VAL str);

rts/idris_stdfgn.c+33

@@ -142,3 +142,36 @@ VAL idris_mkFileError(VM* vm) {

142142void idris_forceGC(void* vm) {

143143 idris_gc((VM*)vm);

144144}

145+

146+typedef struct {

147+ char* string;

148+ int len;

149+} StrBuffer;

150+

151+void* idris_makeStringBuffer(int len) {

152+ StrBuffer* sb = malloc(sizeof(StrBuffer));

153+ if (sb != NULL) {

154+ sb->string = malloc(len);

155+ sb->string[0] = '\0';

156+ sb->len = 0;

157+ }

158+ return sb;

159+}

160+

161+void idris_addToString(void* buffer, char* str) {

162+ StrBuffer* sb = (StrBuffer*)buffer;

163+ int len = strlen(str);

164+

165+ memcpy(sb->string + sb->len, str, len+1);

166+ sb->len += len;

167+}

168+

169+VAL idris_getString(VM* vm, void* buffer) {

170+ StrBuffer* sb = (StrBuffer*)buffer;

171+

172+ VAL str = MKSTR(vm, sb->string);

173+ free(sb->string);

174+ free(sb);

175+ return str;

176+}

177+

rts/idris_stdfgn.h+6

@@ -20,6 +20,12 @@ int idris_writeStr(void*h, char* str);

2020// construct a file error structure (see Prelude.File) from errno

2121VAL idris_mkFileError(VM* vm);

2222

23+// Some machinery for building a large string without reallocating

24+// Create a string with space for 'len' bytes

25+void* idris_makeStringBuffer(int len);

26+void idris_addToString(void* buffer, char* str);

27+VAL idris_getString(VM* vm, void* buffer);

28+

2329void* do_popen(const char* cmd, const char* mode);

2430int fpoll(void* h);

2531

src/IRTS/CodegenC.hs+4

@@ -624,6 +624,10 @@ doOp v LNoOp args = v ++ creg (last args)

624624doOp v (LExternal rf) [_,x]

625625 | rf == sUN "prim__readFile"

626626 = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

627+doOp v (LExternal rf) [_,len,x]

628+ | rf == sUN "prim__readChars"

629+ = v ++ "idris_readChars(vm, GETINT(" ++ creg len ++

630+ "), GETPTR(" ++ creg x ++ "))"

627631doOp v (LExternal wf) [_,x,s]

628632 | wf == sUN "prim__writeFile"

629633 = v ++ "MKINT((i_int)(idris_writeStr(GETPTR(" ++ creg x

src/Idris/Core/Execute.hs+51−1

@@ -29,6 +29,7 @@ import Control.Monad.Trans

2929import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)

3030import Control.Monad.Trans.State.Strict

3131import Data.Bits

32+import Data.IORef

3233import qualified Data.Map as M

3334import Data.Maybe

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

@@ -70,6 +71,11 @@ data ExecVal = EP NameType Name ExecVal

7071 | forall a. EPtr (Ptr a)

7172 | EThunk Context ExecEnv Term

7273 | EHandle Handle

74+ | EStringBuf (IORef String)

75+

76+mkRaw :: ExecVal -> ExecVal

77+mkRaw arg = EApp (EApp (EP (DCon 0 1 False) (sNS (sUN "MkRaw") ["FFI_C"]) EErased)

78+ EErased) arg

7379

7480instance Show ExecVal where

7581 show (EP _ n _) = show n

@@ -83,6 +89,7 @@ instance Show ExecVal where

8389 show (EPtr p) = "<<ptr " ++ show p ++ ">>"

8490 show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"

8591 show (EHandle h) = "<<handle " ++ show h ++ ">>"

92+ show (EStringBuf h) = "<<string buffer>>"

8693

8794toTT :: ExecVal -> Exec Term

8895toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

@@ -117,6 +124,7 @@ toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

117124 return (n, RigW, Let Erased v')

118125toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."

119126toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."

127+toTT (EStringBuf ptr) = execFail $ Msg "Can't convert string buffers back to TT after execution."

120128

121129unApplyV :: ExecVal -> (ExecVal, [ExecVal])

122130unApplyV tm = ua [] tm

@@ -191,7 +199,7 @@ doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

191199 | otherwise = execFail . Msg $ "env too small"

192200doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

193201 doExec ((n, v'):env) ctxt body

194−doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

202+doExec env ctxt (Bind n (NLet t v) body) = undefined

195203doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)

196204 return $

197205 EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)

@@ -404,6 +412,37 @@ execForeign env ctxt arity ty fn xs onfail

404412 execIO $ hSetBuffering stdout NoBuffering

405413 execApp env ctxt ioUnit (drop arity xs)

406414

415+ -- Just use a Haskell String in an IORef for a string buffer

416+ | Just (FFun "idris_makeStringBuffer" [(_, len)] _) <- foreignFromTT arity ty fn xs

417+ = case len of

418+ EConstant (I _) -> do buf <- execIO $ newIORef ""

419+ let res = ioWrap (EStringBuf buf)

420+ execApp env ctxt res (drop arity xs)

421+

422+ _ -> execFail . Msg $

423+ "The argument to idris_makeStringBuffer should be an Int, but it was " ++

424+ show len ++

425+ ". Are all cases covered?"

426+ | Just (FFun "idris_addToString" [(_, strBuf), (_, str)] _) <- foreignFromTT arity ty fn xs

427+ = case (strBuf, str) of

428+ (EStringBuf ref, EConstant (Str add)) ->

429+ do execIO $ modifyIORef ref (++add)

430+ execApp env ctxt ioUnit (drop arity xs)

431+ _ -> execFail . Msg $

432+ "The arguments to idris_addToString should be a StringBuffer and a String, but were " ++

433+ show strBuf ++ " and " ++ show str ++

434+ ". Are all cases covered?"

435+ | Just (FFun "idris_getString" [_, (_, str)] _) <- foreignFromTT arity ty fn xs

436+ = case str of

437+ EStringBuf ref -> do str <- execIO $ readIORef ref

438+ let res = ioWrap (mkRaw (EConstant (Str str)))

439+ execApp env ctxt res (drop arity xs)

440+ _ -> execFail . Msg $

441+ "The argument to idris_getString should be a StringBuffer, but it was " ++

442+ show str ++

443+ ". Are all cases covered?"

444+

445+

407446

408447-- Right now, there's no way to send command-line arguments to the executor,

409448-- so just return 0.

@@ -438,6 +477,7 @@ deNS (NS n _) = n

438477deNS n = n

439478

440479prf = sUN "prim__readFile"

480+prc = sUN "prim__readChars"

441481pwf = sUN "prim__writeFile"

442482prs = sUN "prim__readString"

443483pws = sUN "prim__writeString"

@@ -479,6 +519,16 @@ getOp fn (_ : EHandle h : xs)

479519 | fn == prf =

480520 Just (do contents <- execIO $ hGetLine h

481521 return (EConstant (Str (contents ++ "\n"))), xs)

522+getOp fn (_ : EConstant (I len) : EHandle h : xs)

523+ | fn == prc =

524+ Just (do contents <- execIO $ hGetChars h len

525+ return (EConstant (Str contents)), xs)

526+ where hGetChars h 0 = return ""

527+ hGetChars h i = do eof <- hIsEOF h

528+ if eof then return "" else do

529+ c <- hGetChar h

530+ rest <- hGetChars h (i - 1)

531+ return (c : rest)

482532getOp fn (_ : arg : xs)

483533 | fn == prf =

484534 Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)