git.iko.soy/Idris-dev
on master help sign in
Compile io bind specially, to make sure effectful thunks are not memoised
commit6d01c6bc9f39dc6ea8004a260eb548850b3c6804 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 15 Dec 2011, 15:19 (15 years ago) parent11d4fee
3 files changed+24−7
compare with master
unifiedsplit
src/Idris/Compiler.hs+8−7 test/test004/expected+2 test/test004/test004.idr+14
src/Idris/Compiler.hs+8−7
@@ -63,12 +63,12 @@ instance ToEpic (TT Name) where
6363 return $ lazy_ arg'
6464 | (P _ (UN "believe_me") _, [_, _, arg]) <- unApply tm
6565 = 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+ | (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' @@ (effect_ v'))
7272 epic' env (P (DCon t a) n _) = return $ con_ t
7373 epic' env (P (TCon t a) n _) = return $ con_ t
7474 epic' env (P _ n _) = return $ ref (ename n)
@@ -94,7 +94,8 @@ doForeign (_ : fgn : args)
9494 rty = mkEty ret in
9595 do args' <- mapM epic args
9696 -- wrap it in a prim__IO
97− return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
97+ -- return $ con_ 0 @@ impossible @@
98+ return $ foreign_ rty fgnName (zip args' tys)
9899 | otherwise = fail "Badly formed foreign function call"
99100
100101getFTypes :: TT Name -> [E.Type]
test/test004/expected+2
@@ -3,3 +3,5 @@ Hello!
33World!
44
55---
6+Hello!
7+World!
test/test004/test004.idr+14
@@ -1,5 +1,10 @@
11module main;
22
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+
38readFile : String -> IO String;
49readFile fn = do { h <- fopen fn "r";
510 c <- readFile' h "";
@@ -16,6 +21,14 @@ readFile fn = do { h <- fopen fn "r";
1621 else (return contents); };
1722 }
1823
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+
1932main : IO ();
2033main = do { h <- fopen "testfile" "w";
2134 fwrite h "Hello!\nWorld!\n";
@@ -24,5 +37,6 @@ main = do { h <- fopen "testfile" "w";
2437 f <- readFile "testfile";
2538 putStrLn f;
2639 putStrLn "---";
40+ dumpFile "testfile";
2741 };
2842