on master help sign in
Making IO lazy means we need to force an evaluation for anything to happen at all...
commit22b2879815e548dc741b5dbc37dab35841233950 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Jan 2012, 20:55 (15 years ago) parent598160c
3 files changed+13−6
lib/io.idr+2−2 src/Idris/REPL.hs+10−3 test/test006/test006.idr+1−1
lib/io.idr+2−2
@@ -15,8 +15,8 @@ io_return x = prim__IO x
1515-- This may seem pointless, but we can use it to force an
1616-- evaluation of main that Epic wouldn't otherwise do...
1717
18−-- run__IO : IO () -> IO ()
19−-- run__IO (prim__IO v) = prim__IO v
18+run__IO : IO () -> IO ()
19+run__IO v = io_bind v (\v' => io_return v')
2020
2121data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
2222
src/Idris/REPL.hs+10−3
@@ -181,15 +181,22 @@ process TTShell = do ist <- get
181181 shst' <- lift $ runShell shst
182182 return ()
183183process Execute = do (m, _) <- elabVal toplevel False
184− (PRef (FC "main" 0) (NS (UN "main") ["main"]))
184+ (PApp fc
185+ (PRef fc (UN "run__IO"))
186+ [pexp $ PRef fc (NS (UN "main") ["main"])])
187+-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
185188 (tmpn, tmph) <- liftIO tempfile
186189 liftIO $ hClose tmph
187190 compile tmpn m
188191 liftIO $ system tmpn
189192 return ()
190−process (Compile f) = do (m, _) <- elabVal toplevel False
191− (PRef (FC "main" 0) (NS (UN "main") ["main"]))
193+ where fc = FC "main" 0
194+process (Compile f) = do (m, _) <- elabVal toplevel False
195+ (PApp fc
196+ (PRef fc (UN "run__IO"))
197+ [pexp $ PRef fc (NS (UN "main") ["main"])])
192198 compile f m
199+ where fc = FC "main" 0
193200process (LogLvl i) = setLogLevel i
194201process Metavars = do ist <- get
195202 let mvs = idris_metavars ist \\ primDefs
test/test006/test006.idr+1−1
@@ -18,7 +18,7 @@ natToBin k with (parity k)
1818 natToBin (S (j + j)) | odd = True :: natToBin j
1919
2020main : IO ()
21−main = print (natToBin 42)
21+main = do print (natToBin 42)
2222
2323---------- Proofs ----------
2424