git.iko.soy/Idris-dev
on master help sign in
Compile io bind specially, to make sure effectful thunks are not memoised
6d01c6bEdwin Brady
src/Idris/Compiler.hs+8−7
compare with master
unifiedsplit
@@ -63,12 +63,12 @@ instance ToEpic (TT Name) where
63 return $ lazy_ arg'
63 return $ lazy_ arg'
64 | (P _ (UN "believe_me") _, [_, _, arg]) <- unApply tm
64 | (P _ (UN "believe_me") _, [_, _, arg]) <- unApply tm
65 = epic' env arg
65 = epic' env arg
66−-- | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm
66+ | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm
67−-- = epic' env v
67+ = epic' env v
68−-- | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
68+ | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
69−-- = do v' <- epic' env v
69+ = do v' <- epic' env v
70−-- k' <- epic' env k
70+ k' <- epic' env k
71−-- return (k' @@ v')
71+ return (k' @@ (effect_ v'))
72 epic' env (P (DCon t a) n _) = return $ con_ t
72 epic' env (P (DCon t a) n _) = return $ con_ t
73 epic' env (P (TCon t a) n _) = return $ con_ t
73 epic' env (P (TCon t a) n _) = return $ con_ t
74 epic' env (P _ n _) = return $ ref (ename n)
74 epic' env (P _ n _) = return $ ref (ename n)
@@ -94,7 +94,8 @@ doForeign (_ : fgn : args)
94 rty = mkEty ret in
94 rty = mkEty ret in
95 do args' <- mapM epic args
95 do args' <- mapM epic args
96 -- wrap it in a prim__IO
96 -- wrap it in a prim__IO
97+ -- return $ con_ 0 @@ impossible @@
97− return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
98+ return $ foreign_ rty fgnName (zip args' tys)
98 | otherwise = fail "Badly formed foreign function call"
99 | otherwise = fail "Badly formed foreign function call"
99
100
100getFTypes :: TT Name -> [E.Type]
101getFTypes :: TT Name -> [E.Type]
test/test004/expected+2
@@ -3,3 +3,5 @@ Hello!
3World!
3World!
4
4
5---
5---
6+Hello!
7+World!
test/test004/test004.idr+14
@@ -1,5 +1,10 @@
1module main;
1module main;
2
2
3+while : |(test : IO Bool) -> |(body : IO ()) -> IO ();
4+while t b = do { v <- t;
5+ if v then (do { b; while t b; }) else return (); };
6+
7+
3readFile : String -> IO String;
8readFile : String -> IO String;
4readFile fn = do { h <- fopen fn "r";
9readFile fn = do { h <- fopen fn "r";
5 c <- readFile' h "";
10 c <- readFile' h "";
@@ -16,6 +21,14 @@ readFile fn = do { h <- fopen fn "r";
16 else (return contents); };
21 else (return contents); };
17 }
22 }
18
23
24+dumpFile : String -> IO ();
25+dumpFile fn = do { h <- fopen fn "r";
26+ while (do { x <- feof h;
27+ return (not x); })
28+ (do { l <- fread h;
29+ putStr l; });
30+ fclose h; };
31+
19main : IO ();
32main : IO ();
20main = do { h <- fopen "testfile" "w";
33main = do { h <- fopen "testfile" "w";
21 fwrite h "Hello!\nWorld!\n";
34 fwrite h "Hello!\nWorld!\n";
@@ -24,5 +37,6 @@ main = do { h <- fopen "testfile" "w";
24 f <- readFile "testfile";
37 f <- readFile "testfile";
25 putStrLn f;
38 putStrLn f;
26 putStrLn "---";
39 putStrLn "---";
40+ dumpFile "testfile";
27 };
41 };
28
42