edwinb/Idris-dev — pull request #268 by david-christiansen (2013-04-04 09:12:24+00:00)
Title: Fix IO and normalisation

I've rewritten the executor completely. Previously, normalization would move IO actions around and potentially even copy or eliminate them. Thus,

module Main

main : IO ()
main = do l <- getLine
let ll = l ++ l
putStrLn ll

would normalize to ````mkForeign (FFun "putStr" (Prelude.List.:: FString (Prelude.List.Nil)) FUnit) (prim__concat (prim__concat (prim__readString prim__stdin) (prim__readString prim__stdin)) "\n") : IO ()````, which of course would read two different strings.

Now, evaluation order is strictly controlled, resulting in correct execution of the above. It has been added as a test case as well. The executor is still incomplete, but it's far better than it was.