11d4fee · Idris-dev · git.iko.soy

lib/io.idr+3−3

compare with master

unifiedsplit

@@ -6,13 +6,13 @@ io_bind : IO a -> (a -> IO b) -> IO b;

6io_bind (prim__IO v) k = k v;

7

8io_return : a -> IO a;

9−io_return = prim__IO;

9+io_return x = prim__IO x;

10

11-- This may seem pointless, but we can use it to force an

12-- evaluation of main that Epic wouldn't otherwise do...

13

14−run__IO : IO () -> IO ();

14+-- run__IO : IO () -> IO ();

15−run__IO (prim__IO v) = prim__IO v;

15+-- run__IO (prim__IO v) = prim__IO v;

16

17

lib/prelude.idr+39

@@ -141,3 +141,42 @@ print = putStrLn . show;

141readLine : IO String;

142readLine = mkForeign (FFun "readStr" Nil FString);

143

144+---- some basic file handling

145+

146+data File = FHandle Ptr;

147+

148+do_fopen : String -> String -> IO Ptr;

149+do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m;

150+

151+fopen : String -> String -> IO File;

152+fopen f m = do { h <- do_fopen f m;

153+ return (FHandle h); };

154+

155+do_fclose : Ptr -> IO ();

156+do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;

157+

158+fclose : File -> IO ();

159+fclose (FHandle h) = do_fclose h;

160+

161+do_fread : Ptr -> IO String;

162+do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;

163+

164+fread : File -> IO String;

165+fread (FHandle h) = do_fread h;

166+

167+do_fwrite : Ptr -> String -> IO ();

168+do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s;

169+

170+fwrite : File -> String -> IO ();

171+fwrite (FHandle h) s = do_fwrite h s;

172+

173+do_feof : Ptr -> IO Int;

174+do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h;

175+

176+feof : File -> IO Bool;

177+feof (FHandle h) = do { eof <- do_feof h;

178+ return (not (eof == 0)); };

179+

180+

181+

182+

src/Idris/AbsSyntax.hs+1−1

@@ -288,7 +288,7 @@ impl = Imp False Dynamic

288expl = Exp False Dynamic

289constraint = Constraint False Static

290

291−data FnOpt = Inlinable | Partial

291+data FnOpt = Inlinable | Partial | Abstract | Private

292 deriving (Show, Eq)

293

294type FnOpts = [FnOpt]

src/Idris/Compiler.hs+7−1

@@ -32,7 +32,7 @@ mkDecls = do i <- getIState

32ename x = name ("idris_" ++ show x)

33aname x = name ("a_" ++ show x)

34

35−epicMain = effect_ $ ref (ename (UN "run__IO")) @@

35+epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@

36 ref (ename (NS (UN "main") ["main"]))

37

38class ToEpic a where

@@ -63,6 +63,12 @@ instance ToEpic (TT Name) where

63 return $ lazy_ arg'

64 | (P _ (UN "believe_me") _, [_, _, arg]) <- unApply tm

65 = epic' env arg

66+-- | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm

67+-- = epic' env v

68+-- | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm

69+-- = do v' <- epic' env v

70+-- k' <- epic' env k

71+-- return (k' @@ v')

66 epic' env (P (DCon t a) n _) = return $ con_ t

72 epic' env (P (DCon t a) n _) = return $ con_ t

67 epic' env (P (TCon t a) n _) = return $ con_ t

73 epic' env (P (TCon t a) n _) = return $ con_ t

68 epic' env (P _ n _) = return $ ref (ename n)

74 epic' env (P _ n _) = return $ ref (ename n)

test/test004/expectednew file+5

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

1+Reading testfile

2+Hello!

3+World!

4+

5+---

test/test004/runnew file+4

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

1+#!/bin/bash

2+idris test004.idr -o test004

3+./test004

4+rm -f test004 test004.ibc testfile

test/test004/test004.idrnew file+28

@@ -0,0 +1,28 @@

1+module main;

2+

3+readFile : String -> IO String;

4+readFile fn = do { h <- fopen fn "r";

5+ c <- readFile' h "";

6+ fclose h;

7+ return c;

8+ }

9+ where {

10+ readFile' : File -> String -> IO String;

11+ readFile' h contents =

12+ do { x <- feof h;

13+ if (not x) then (do { l <- fread h;

14+ readFile' h (contents ++ l);

15+ })

16+ else (return contents); };

17+ }

18+

19+main : IO ();

20+main = do { h <- fopen "testfile" "w";

21+ fwrite h "Hello!\nWorld!\n";

22+ fclose h;

23+ putStrLn "Reading testfile";

24+ f <- readFile "testfile";

25+ putStrLn f;

26+ putStrLn "---";

27+ };

28+