ce5e330 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add StringBuffer to Prelude.Strings

ce5e330Edwin Brady10 years ago

libs/prelude/Builtins.idr+1

compare with master

unifiedsplit

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

210export data CData : Type

211

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

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

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

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

214

215

215%extern prim__vm : prim__WorldType -> Ptr

216%extern prim__vm : prim__WorldType -> Ptr

libs/prelude/IO.idr+4

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

134prim_fread : Ptr -> IO' l String

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

136

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+

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

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

138prim_fwrite h s

142prim_fwrite h s

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

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

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

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

156do_fread : Ptr -> IO' l String

157do_fread h = prim_fread h

158

159+private

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

161+do_freadChars h len = prim_freadChars len h

162+

159export

163export

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

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

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

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

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

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

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

200fGetLine = fread

204fGetLine = fread

201

205

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+

202%deprecate fread "Use fGetLine instead"

215%deprecate fread "Use fGetLine instead"

203

216

204private

217private

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

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

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

252 pure (p > 0)

265 pure (p > 0)

253

266

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

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

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

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

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

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

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

270||| 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.

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

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

259export

274export

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

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

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

262 | Left err => pure (Left err)

277 | Left err => pure (Left err)

263 Right max <- fileSize h

278 Right max <- fileSize h

264 | Left err => pure (Left err)

279 | Left err => pure (Left err)

280+ sb <- newStringBuffer (max + 1)

265− c <- readFile' h max ""

281+ c <- readFile' h max sb

266 closeFile h

282 closeFile h

267 pure c

283 pure c

268 where

284 where

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

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

270 readFile' h max contents =

286 readFile' h max contents =

271 do x <- fEOF h

287 do x <- fEOF h

272 if not x && max > 0

288 if not x && max > 0

273− then do Right l <- fGetLine h

289+ then do Right l <- fGetChars h 1024000

274 | Left err => pure (Left err)

290 | Left err => pure (Left err)

291+ addToStringBuffer contents l

275 assert_total $

292 assert_total $

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

293+ readFile' h (max - 1024000) contents

294+ else do str <- getStringFromBuffer contents

277− else pure (Right contents)

295+ pure (Right str)

278

296

279||| Write a string to a file

297||| Write a string to a file

280export

298export

libs/prelude/Prelude/Strings.idr+33

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

36(++) : String -> String -> String

37(++) = prim__concat

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+

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

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

40|||

73|||

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

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

rts/idris_rts.c+21

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

239#endif

240 return ptr;

241 } 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+ }

242 idris_gc(vm);

247 idris_gc(vm);

243#ifdef HAS_PTHREAD

248#ifdef HAS_PTHREAD

244 if (lock) { // not message passing

249 if (lock) { // not message passing

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

595 return ret;

600 return ret;

596}

601}

597

602

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+

598void idris_crash(char* msg) {

619void idris_crash(char* msg) {

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

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

600 exit(1);

621 exit(1);

rts/idris_rts.h+3

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

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

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

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

375+// Read a line from a file

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

376VAL 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);

376

379

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

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

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

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

rts/idris_stdfgn.c+33

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

142void idris_forceGC(void* vm) {

143 idris_gc((VM*)vm);

144}

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);

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

21VAL idris_mkFileError(VM* vm);

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+

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

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

24int fpoll(void* h);

30int fpoll(void* h);

src/IRTS/CodegenC.hs+4

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

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

625 | rf == sUN "prim__readFile"

626 = 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 ++ "))"

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

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

628 | wf == sUN "prim__writeFile"

632 | wf == sUN "prim__writeFile"

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

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

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

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

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

30import Control.Monad.Trans.State.Strict

31import Data.Bits

32+import Data.IORef

32import qualified Data.Map as M

33import qualified Data.Map as M

33import Data.Maybe

34import Data.Maybe

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

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

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

70 | forall a. EPtr (Ptr a)

71 | forall a. EPtr (Ptr a)

71 | EThunk Context ExecEnv Term

72 | EThunk Context ExecEnv Term

72 | EHandle Handle

73 | 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

74instance Show ExecVal where

80instance Show ExecVal where

75 show (EP _ n _) = show n

81 show (EP _ n _) = show n

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

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

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

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

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

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

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

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

87toTT :: ExecVal -> Exec Term

94toTT :: ExecVal -> Exec Term

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

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

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

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

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

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

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

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

126toTT (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."

120

128

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

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

122unApplyV tm = ua [] tm

130unApplyV tm = ua [] tm

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

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

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

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

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

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

201 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

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

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

196 return $

204 return $

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

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

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

404 execIO $ hSetBuffering stdout NoBuffering

412 execIO $ hSetBuffering stdout NoBuffering

405 execApp env ctxt ioUnit (drop arity xs)

413 execApp env ctxt ioUnit (drop arity xs)

406

414

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+

407

446

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

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

409-- so just return 0.

448-- so just return 0.

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

438deNS n = n

477deNS n = n

439

478

440prf = sUN "prim__readFile"

479prf = sUN "prim__readFile"

480+prc = sUN "prim__readChars"

441pwf = sUN "prim__writeFile"

481pwf = sUN "prim__writeFile"

442prs = sUN "prim__readString"

482prs = sUN "prim__readString"

443pws = sUN "prim__writeString"

483pws = sUN "prim__writeString"

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

479 | fn == prf =

519 | fn == prf =

480 Just (do contents <- execIO $ hGetLine h

520 Just (do contents <- execIO $ hGetLine h

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

521 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)

482getOp fn (_ : arg : xs)

532getOp fn (_ : arg : xs)

483 | fn == prf =

533 | fn == prf =

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

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