git.iko.soy/Idris-dev
on master help sign in
Separate IO and PrimIO

PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325

commit8eb2087f1f2bb2f964e5654fe77479d303d59fcb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 2 Sep 2013, 14:58 (13 years ago) parent5ce8ee7
14 files changed+203−87
compare with master
unifiedsplit
lib/IO.idr+58−16 lib/Prelude.idr+26−9 papers/impl-paper/elaboration.tex+7−6 rts/idris_rts.c+1 rts/idris_stdfgn.h+2 src/Core/Execute.hs+53−39 src/IRTS/Compiler.hs+6−6 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/ElabDecls.hs+4−1 src/Idris/Parser.hs+16−1 src/Idris/Providers.hs+2−2 test/test004/expected+9 test/test004/test004.idr+14−5 test/test024/test024.idr+1−1
lib/IO.idr+58−16
@@ -2,24 +2,27 @@ import Prelude.List
22
33%access public
44
5−abstract data IO a = prim__IO a
5+abstract data PrimIO a = prim__IO a
66
7−abstract
8−io_bind : IO a -> (a -> IO b) -> IO b
9−io_bind (prim__IO v) k = k v
7+abstract data World = TheWorld
108
11−unsafePerformIO : IO a -> a
12−-- compiled as primitive
9+abstract WorldRes : Type -> Type
10+WorldRes x = x
11+
12+-- abstract data WorldRes a = MkWR a World
13+
14+abstract data IO a = MkIO (World -> PrimIO (WorldRes a))
1315
1416abstract
15−io_return : a -> IO a
16−io_return x = prim__IO x
17+prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
18+prim_io_bind (prim__IO v) k = k v
1719
18−-- This may seem pointless, but we can use it to force an
19−-- evaluation of main that Epic wouldn't otherwise do...
20+unsafePerformPrimIO : PrimIO a -> a
21+-- compiled as primitive
2022
21−run__IO : IO () -> IO ()
22−run__IO v = io_bind v (\v' => io_return v')
23+abstract
24+prim_io_return : a -> PrimIO a
25+prim_io_return x = prim__IO x
2326
2427data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
2528data FTy = FIntT IntTy
@@ -89,7 +92,7 @@ interpFTy FUnit = ()
8992interpFTy (FFunction a b) = interpFTy a -> interpFTy b
9093
9194ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
92−ForeignTy Nil rt = IO (interpFTy rt)
95+ForeignTy Nil rt = World -> PrimIO (interpFTy rt)
9396ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
9497
9598
@@ -97,11 +100,50 @@ data Foreign : Type -> Type where
97100 FFun : String -> (xs:List FTy) -> (t:FTy) ->
98101 Foreign (ForeignTy xs t)
99102
100−mkForeign : Foreign x -> x
101−mkLazyForeign : Foreign x -> x
103+mkForeignPrim : Foreign x -> x
104+mkLazyForeignPrim : Foreign x -> x
102105-- mkForeign and mkLazyForeign compiled as primitives
103106
107+abstract
108+io_bind : IO a -> (a -> IO b) -> IO b
109+io_bind (MkIO fn) k
110+ = MkIO (\w => prim_io_bind (fn w)
111+ (\ b => case k b of
112+ MkIO fkb => fkb w))
113+
114+abstract
115+io_return : a -> IO a
116+io_return x = MkIO (\w => prim_io_return x)
117+
118+liftPrimIO : (World -> PrimIO a) -> IO a
119+liftPrimIO f = MkIO (\w => prim_io_bind (f w)
120+ (\x => prim_io_return x))
121+
122+run__IO : IO () -> PrimIO ()
123+run__IO (MkIO f) = prim_io_bind (f TheWorld)
124+ (\ b => prim_io_return b)
125+
126+run__provider : IO a -> PrimIO a
127+run__provider (MkIO f) = prim_io_bind (f TheWorld)
128+ (\ b => prim_io_return b)
129+
130+-- io_bind v (\v' => io_return v')
131+
132+prim_fork : |(thread:PrimIO ()) -> PrimIO Ptr
133+prim_fork x = prim_io_return prim__vm -- compiled specially
134+
104135fork : |(thread:IO ()) -> IO Ptr
105−fork x = io_return prim__vm -- compiled specially
136+fork (MkIO f) = MkIO (\w => prim_io_bind
137+ (prim_fork (prim_io_bind (f w)
138+ (\ x => prim_io_return x)))
139+ (\x => prim_io_return x))
140+
141+partial
142+prim_fread : Ptr -> IO String
143+prim_fread h = MkIO (\w => prim_io_return (prim__readString h))
144+
145+unsafePerformIO : IO a -> a
146+unsafePerformIO (MkIO f) = unsafePerformPrimIO
147+ (prim_io_bind (f TheWorld) (\ b => prim_io_return b))
106148
107149
lib/Prelude.idr+26−9
@@ -181,8 +181,11 @@ instance Show a => Show (Maybe a) where
181181
182182---- Functor instances
183183
184+instance Functor PrimIO where
185+ map f io = prim_io_bind io (prim_io_return . f)
186+
184187instance Functor IO where
185− map f io = io_bind io (io_return . f)
188+ map f io = io_bind io (\b => io_return (f b))
186189
187190instance Functor Maybe where
188191 map f (Just x) = Just (f x)
@@ -194,10 +197,16 @@ instance Functor (Either e) where
194197
195198---- Applicative instances
196199
197−instance Applicative IO where
198− pure = io_return
200+instance Applicative PrimIO where
201+ pure = prim_io_return
199202
200− am <$> bm = io_bind am (\f => io_bind bm (io_return . f))
203+ am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
204+
205+instance Applicative IO where
206+ pure x = io_return x
207+ f <$> a = io_bind f (\f' =>
208+ io_bind a (\a' =>
209+ io_return (f' a')))
201210
202211instance Applicative Maybe where
203212 pure = Just
@@ -237,7 +246,10 @@ instance Alternative List where
237246
238247---- Monad instances
239248
240−instance Monad IO where
249+instance Monad PrimIO where
250+ b >>= k = prim_io_bind b k
251+
252+instance Monad IO where
241253 b >>= k = io_bind b k
242254
243255instance Monad Maybe where
@@ -382,7 +394,7 @@ print x = putStrLn (show x)
382394
383395partial
384396getLine : IO String
385−getLine = return (prim__readString prim__stdin)
397+getLine = prim_fread prim__stdin
386398
387399partial
388400putChar : Char -> IO ()
@@ -401,7 +413,8 @@ partial stdin : File
401413stdin = FHandle prim__stdin
402414
403415do_fopen : String -> String -> IO Ptr
404−do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
416+do_fopen f m
417+ = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
405418
406419fopen : String -> String -> IO File
407420fopen f m = do h <- do_fopen f m
@@ -426,7 +439,10 @@ closeFile (FHandle h) = do_fclose h
426439
427440partial
428441do_fread : Ptr -> IO String
429−do_fread h = return (prim__readString h)
442+do_fread h = prim_fread h
443+
444+-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
445+-- prim__vm h
430446
431447partial
432448fread : File -> IO String
@@ -434,7 +450,8 @@ fread (FHandle h) = do_fread h
434450
435451partial
436452do_fwrite : Ptr -> String -> IO ()
437−do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
453+do_fwrite h s
454+ = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
438455
439456partial
440457fwrite : File -> String -> IO ()
papers/impl-paper/elaboration.tex+7−6
@@ -1181,7 +1181,8 @@ $\vV$ and $\vX$.
11811181\MO{Let}\;(\vx\Hab\vX\defq\vV)\\
11821182\MO{Focus}\;\vV\\
11831183\ttinterp{\vv};\;
1184−\ttinterp{\ve}
1184+\ttinterp{\ve}\\
1185+\MO{Solve}
11851186}
11861187}
11871188\subsubsection{Elaborating Applications}
@@ -1659,11 +1660,11 @@ In general, \texttt{class} declarations are elaborated as follows:
16591660\\
16601661\hg\hg
16611662\mq\;\RW{do}\;\AR{
1662−(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
1663+%(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
16631664\MO{Elab}\;
16641665\AR{(\RW{data}\;\TC{C}\Hab(\ta\Hab\ttt)\to\Type\;\iwhere\\
16651666\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\;\ta)}\\
1666−\vec{\MO{ElabMeth}}\;(\vec{\VV{meth}}\Hab\ttt)\\
1667+\vec{\MO{ElabMeth}}\;\td\\ % (\vec{\VV{meth}}\Hab\ttt)\\
16671668\vec{\MO{ElabParent}}\;\tc
16681669}
16691670\medskip\\
@@ -1756,13 +1757,13 @@ max x y = if (x > y) then x else y
17561757
17571758If $\MO{Trivial}$ does not find a solution, $\MO{Instance}$ begins a global search,
17581759applying every class instance, and attempting to resolve the instance's parameters
1759−recursively. Given an instance $\vI$ with parameters $\ta$:
1760+recursively. Given an instance $\FN{instanceC}$ with parameters $\ta$:
17601761
17611762\DM{
1762−\MO{TryInstance}\;(\vI\;\ta)\;\mq\;\RW{do}\;
1763+\MO{TryInstance}\;(\FN{instanceC}\;\ta)\;\mq\;\RW{do}\;
17631764\AR{
17641765\vec{\MO{Claim}}\;(\tx\Hab\ta)\\
1765−\ttinterp{\vI\;\tx}\\
1766+\ttinterp{\FN{instanceC};\tx}\\
17661767\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}
17671768}
17681769}
rts/idris_rts.c+1
@@ -382,6 +382,7 @@ VAL idris_readStr(VM* vm, FILE* h) {
382382 }
383383
384384 VAL str = MKSTR(vm, line_buf);
385+// printf("DBG: %s\n", line_buf);
385386 free(line_buf);
386387 return str;
387388}
rts/idris_stdfgn.h+2
@@ -8,6 +8,8 @@ void putStr(char* str);
88
99void* fileOpen(char* f, char* mode);
1010void fileClose(void* h);
11+int fileEOF(void* h);
12+int fileError(void* h);
1113void fputStr(void*h, char* str);
1214
1315int isNull(void* ptr);
src/Core/Execute.hs+53−39
@@ -228,55 +228,69 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f
228228
229229execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
230230execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
231−execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
231+execApp' env ctxt (EP _ (UN "unsafePerformPrimIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
232232 execApp' env ctxt v rest
233233
234−execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
234+execApp' env ctxt (EP _ (UN "prim_io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
235235 do v'' <- tryForce v'
236236 res <- execApp' env ctxt k [v''] >>= tryForce
237237 execApp' env ctxt res rest
238−execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =
238+execApp' env ctxt con@(EP _ (UN "prim_io_return") _) args@(tp:v:rest) =
239239 do v' <- tryForce v
240240 execApp' env ctxt (mkEApp con [tp, v']) rest
241241
242242-- Special cases arising from not having access to the C RTS in the interpreter
243−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
244− | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
245− execApp' env ctxt ioUnit rest
246−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
247− | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
248− "r" -> return ReadMode
249− "w" -> return WriteMode
250− "a" -> return AppendMode
251− "rw" -> return ReadWriteMode
252− "wr" -> return ReadWriteMode
253− "r+" -> return ReadWriteMode
254− _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
255− h <- execIO $ openFile f m
256− execApp' env ctxt (ioWrap (EHandle h)) rest
257−
258−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
259− | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
260− let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
261− execApp' env ctxt res rest
262−
263−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
264− | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
265− execApp' env ctxt ioUnit rest
266−
267−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)
268− | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = ioWrap . EConstant . I $
269− if p == nullPtr then 1 else 0
270− in execApp' env ctxt res rest
271−
272−execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun f argTs retT) <- foreignFromTT fn
273− , length xs >= length argTs =
274− do res <- stepForeign (ty:fn:take (length argTs) xs)
243+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str arg):_:rest)
244+ | Just (FFun "putStr" _ _) <- foreignFromTT fn
245+ = do execIO (putStr arg)
246+ execApp' env ctxt ioUnit rest
247+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:_:EHandle h:_:rest)
248+ | Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
249+ = do contents <- execIO $ hGetLine h
250+ execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest
251+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
252+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn
253+ = do m <- case mode of
254+ "r" -> return ReadMode
255+ "w" -> return WriteMode
256+ "a" -> return AppendMode
257+ "rw" -> return ReadWriteMode
258+ "wr" -> return ReadWriteMode
259+ "r+" -> return ReadWriteMode
260+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
261+ h <- execIO $ openFile f m
262+ execApp' env ctxt (ioWrap (EHandle h)) (tail rest)
263+
264+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)
265+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn
266+ = do eofp <- execIO $ hIsEOF h
267+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
268+ execApp' env ctxt res (tail rest)
269+
270+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)
271+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn
272+ = do execIO $ hClose h
273+ execApp' env ctxt ioUnit (tail rest)
274+
275+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EPtr p):rest)
276+ | Just (FFun "isNull" _ _) <- foreignFromTT fn
277+ = let res = ioWrap . EConstant . I $
278+ if p == nullPtr then 1 else 0
279+ in execApp' env ctxt res (tail rest)
280+
281+-- Throw away the 'World' argument to the foreign function
282+
283+execApp' env ctxt f@(EP _ (UN "mkForeignPrim") _) args@(ty:fn:xs)
284+ | Just (FFun f argTs retT) <- foreignFromTT fn
285+ , length xs >= length argTs =
286+ do let (args', xs') = (take (length argTs) xs, -- foreign args
287+ drop (length argTs + 1) xs) -- rest
288+ res <- stepForeign (ty:fn:args')
275289 case res of
276290 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
277− "\" with args " ++ show (take (length argTs) xs)
278− Just r -> return (mkEApp r (drop (length argTs) xs))
279− | otherwise = return (mkEApp f args)
291+ "\" with args " ++ show args
292+ Just r -> return (mkEApp r xs')
293+ | otherwise = return (mkEApp f args)
280294
281295execApp' env ctxt c@(EP (DCon _ arity) n _) args =
282296 do args' <- mapM tryForce (take arity args)
@@ -502,7 +516,7 @@ stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
502516 Just f -> f args
503517 Nothing -> return Nothing
504518 return f'
505−stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
519+stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
506520
507521mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
508522mapMaybeM f [] = return []
src/IRTS/Compiler.hs+6−6
@@ -169,9 +169,9 @@ mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)
169169instance ToIR (TT Name) where
170170 ir tm = ir' [] tm where
171171 ir' env tm@(App f a)
172− | (P _ (UN "mkForeign") _, args) <- unApply tm
172+ | (P _ (UN "mkForeignPrim") _, args) <- unApply tm
173173 = doForeign env args
174− | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
174+ | (P _ (UN "unsafePerformPrimIO") _, [_, arg]) <- unApply tm
175175 = ir' env arg
176176 -- TMP HACK - until we get inlining.
177177 | (P _ (UN "replace") _, [_, _, _, _, _, arg]) <- unApply tm
@@ -184,17 +184,17 @@ instance ToIR (TT Name) where
184184 | (P _ (UN "par") _, [_, arg]) <- unApply tm
185185 = do arg' <- ir' env arg
186186 return $ LOp LPar [LLazyExp arg']
187− | (P _ (UN "fork") _, [arg]) <- unApply tm
187+ | (P _ (UN "prim_fork") _, [arg]) <- unApply tm
188188 = do arg' <- ir' env arg
189189 return $ LOp LFork [LLazyExp arg']
190190 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
191191 = do v' <- ir' env v
192192 return v'
193− | (P _ (UN "io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm
193+ | (P _ (UN "prim_io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm
194194 = do v' <- ir' env v
195195 sc' <- ir' (n:env) sc
196196 return (LLet n (LForce v') sc')
197− | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
197+ | (P _ (UN "prim_io_bind") _, [_,_,v,k]) <- unApply tm
198198 = do v' <- ir' env v
199199 k' <- ir' env k
200200 return (LApp False k' [LForce v'])
@@ -281,7 +281,7 @@ instance ToIR (TT Name) where
281281 case maybeTys of
282282 Nothing -> fail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
283283 Just tys -> do
284− args' <- mapM (ir' env) args
284+ args' <- mapM (ir' env) (init args)
285285 -- wrap it in a prim__IO
286286 -- return $ con_ 0 @@ impossible @@
287287 return $ -- LLazyExp $
src/Idris/AbsSyntaxTree.hs+4−1
@@ -138,7 +138,10 @@ data CGInfo = CGInfo { argsdef :: [Name],
138138deriving instance Binary CGInfo
139139!-}
140140
141−primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
141+primDefs = [UN "unsafePerformPrimIO",
142+ UN "mkLazyForeignPrim",
143+ UN "mkForeignPrim",
144+ UN "FalseElim"]
142145
143146-- information that needs writing for the current module's .ibc file
144147data IBCWrite = IBCFix FixDecl
src/Idris/ElabDecls.hs+4−1
@@ -306,7 +306,10 @@ elabProvider info syn fc n ty tm
306306 elabType info syn "" fc [] n ty
307307
308308 -- Execute the type provider and normalise the result
309− rhs <- execute e
309+ -- use 'run__provider' to convert to a primitive IO action
310+
311+ rhs <- execute (mkApp (P Ref (UN "run__provider") Erased)
312+ [Erased, e])
310313 let rhs' = normalise ctxt [] rhs
311314 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
312315
src/Idris/Parser.hs+16−1
@@ -927,7 +927,22 @@ pUnifyLog syn = do lchar '%'; reserved "unifyLog";
927927 tm <- pSimpleExpr syn
928928 return (PUnifyLog tm)
929929
930−pApp syn = do f <- pSimpleExpr syn
930+pApp syn = do f <- reserved "mkForeign"
931+ fc <- pfc
932+ fn <- pArg syn
933+ args <- many (do notEndApp; pArg syn)
934+ i <- getState
935+ -- mkForeign f args ==>
936+ -- liftPrimIO (\w => mkForeignPrim f args w)
937+ let ap = PApp fc (PRef fc (UN "liftPrimIO"))
938+ [pexp (PLam (MN 0 "w")
939+ Placeholder
940+ (PApp fc (PRef fc (UN "mkForeignPrim"))
941+ (fn : args ++
942+ [pexp (PRef fc (MN 0 "w"))])))]
943+ return (dslify i ap)
944+
945+ <|> do f <- pSimpleExpr syn
931946 fc <- pfc
932947 args <- many1 (do notEndApp
933948 pArg syn)
src/Idris/Providers.hs+2−2
@@ -15,12 +15,12 @@ providerTy fc tm = PApp fc (PRef fc $ UN "Provider") [PExp 0 False tm ""]
1515
1616-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.
1717getProvided :: TT Name -> Idris (TT Name)
18−getProvided tm | (P _ (UN "io_return") _, [tp, result]) <- unApply tm
18+getProvided tm | (P _ (UN "prim__IO") _, [tp, result]) <- unApply tm
1919 , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =
2020 case err of
2121 Constant (Str msg) -> ierror . ProviderError $ msg
2222 _ -> fail "Internal error in type provider, non-normalised error"
23− | (P _ (UN "io_return") _, [tp, result]) <- unApply tm
23+ | (P _ (UN "prim__IO") _, [tp, result]) <- unApply tm
2424 , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =
2525 return res
2626 | otherwise = fail $ "Internal type provider error: result was not " ++
test/test004/expected+9
@@ -1,7 +1,16 @@
11Reading testfile
22Hello!
33World!
4+...
5+3
6+4
7+Last line
48
59---
610Hello!
711World!
12+...
13+3
14+4
15+Last line
16+---
test/test004/test004.idr+14−5
@@ -1,21 +1,30 @@
11module Main
22
3+mwhile : |(test : IO Bool) -> |(body : IO ()) -> IO ()
4+mwhile t b = do v <- t
5+ case v of
6+ True => do b
7+ mwhile t b
8+ False => return ()
9+
310dumpFile : String -> IO ()
411dumpFile fn = do { h <- openFile fn Read
5− while (do { x <- feof h
6− return (not x) })
7− (do { l <- fread h
8− putStr l })
12+ mwhile (do { -- putStrLn "TEST"
13+ x <- feof h
14+ return (not x) })
15+ (do { l <- fread h
16+ putStr l })
917 closeFile h }
1018
1119main : IO ()
1220main = do { h <- openFile "testfile" Write
13− fwrite h "Hello!\nWorld!\n"
21+ fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
1422 closeFile h
1523 putStrLn "Reading testfile"
1624 f <- readFile "testfile"
1725 putStrLn f
1826 putStrLn "---"
1927 dumpFile "testfile"
28+ putStrLn "---"
2029 }
2130
test/test024/test024.idr+1−1
@@ -3,4 +3,4 @@ module Main
33main : IO ()
44main = do l <- getLine
55 let ll = l ++ l
6− putStrLn ll
6+ putStrLn ll