8eb2087 · Idris-dev · git.iko.soy

lib/IO.idr+58−16

compare with master

unifiedsplit

@@ -2,24 +2,27 @@ import Prelude.List

2

3%access public

4

5−abstract data IO a = prim__IO a

5+abstract data PrimIO a = prim__IO a

6

7−abstract

7+abstract data World = TheWorld

8−io_bind : IO a -> (a -> IO b) -> IO b

9−io_bind (prim__IO v) k = k v

10

8

11−unsafePerformIO : IO a -> a

9+abstract WorldRes : Type -> Type

12−-- compiled as primitive

10+WorldRes x = x

11+

12+-- abstract data WorldRes a = MkWR a World

13+

14+abstract data IO a = MkIO (World -> PrimIO (WorldRes a))

13

15

14abstract

16abstract

15−io_return : a -> IO a

17+prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

16−io_return x = prim__IO x

18+prim_io_bind (prim__IO v) k = k v

17

19

18−-- This may seem pointless, but we can use it to force an

20+unsafePerformPrimIO : PrimIO a -> a

19−-- evaluation of main that Epic wouldn't otherwise do...

21+-- compiled as primitive

20

22

21−run__IO : IO () -> IO ()

23+abstract

22−run__IO v = io_bind v (\v' => io_return v')

24+prim_io_return : a -> PrimIO a

25+prim_io_return x = prim__IO x

23

26

24data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2

27data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2

25data FTy = FIntT IntTy

28data FTy = FIntT IntTy

@@ -89,7 +92,7 @@ interpFTy FUnit = ()

89interpFTy (FFunction a b) = interpFTy a -> interpFTy b

92interpFTy (FFunction a b) = interpFTy a -> interpFTy b

90

93

91ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

94ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

92−ForeignTy Nil rt = IO (interpFTy rt)

95+ForeignTy Nil rt = World -> PrimIO (interpFTy rt)

93ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt

96ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt

94

97

95

98

@@ -97,11 +100,50 @@ data Foreign : Type -> Type where

97 FFun : String -> (xs:List FTy) -> (t:FTy) ->

100 FFun : String -> (xs:List FTy) -> (t:FTy) ->

98 Foreign (ForeignTy xs t)

101 Foreign (ForeignTy xs t)

99

102

100−mkForeign : Foreign x -> x

103+mkForeignPrim : Foreign x -> x

101−mkLazyForeign : Foreign x -> x

104+mkLazyForeignPrim : Foreign x -> x

102-- mkForeign and mkLazyForeign compiled as primitives

105-- mkForeign and mkLazyForeign compiled as primitives

103

106

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+

104fork : |(thread:IO ()) -> IO Ptr

135fork : |(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))

106

148

107

149

lib/Prelude.idr+26−9

@@ -181,8 +181,11 @@ instance Show a => Show (Maybe a) where

181

182---- Functor instances

183

184+instance Functor PrimIO where

185+ map f io = prim_io_bind io (prim_io_return . f)

186+

184instance Functor IO where

187instance 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))

186

189

187instance Functor Maybe where

190instance Functor Maybe where

188 map f (Just x) = Just (f x)

191 map f (Just x) = Just (f x)

@@ -194,10 +197,16 @@ instance Functor (Either e) where

194

197

195---- Applicative instances

198---- Applicative instances

196

199

197−instance Applicative IO where

200+instance Applicative PrimIO where

198− pure = io_return

201+ pure = prim_io_return

199

202

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')))

201

210

202instance Applicative Maybe where

211instance Applicative Maybe where

203 pure = Just

212 pure = Just

@@ -237,7 +246,10 @@ instance Alternative List where

237

246

238---- Monad instances

247---- Monad instances

239

248

240−instance Monad IO where

249+instance Monad PrimIO where

250+ b >>= k = prim_io_bind b k

251+

252+instance Monad IO where

241 b >>= k = io_bind b k

253 b >>= k = io_bind b k

242

254

243instance Monad Maybe where

255instance Monad Maybe where

@@ -382,7 +394,7 @@ print x = putStrLn (show x)

382

394

383partial

395partial

384getLine : IO String

396getLine : IO String

385−getLine = return (prim__readString prim__stdin)

397+getLine = prim_fread prim__stdin

386

398

387partial

399partial

388putChar : Char -> IO ()

400putChar : Char -> IO ()

@@ -401,7 +413,8 @@ partial stdin : File

401stdin = FHandle prim__stdin

413stdin = FHandle prim__stdin

402

414

403do_fopen : String -> String -> IO Ptr

415do_fopen : String -> String -> IO Ptr

416+do_fopen f m

404−do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m

417+ = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m

405

418

406fopen : String -> String -> IO File

419fopen : String -> String -> IO File

407fopen f m = do h <- do_fopen f m

420fopen f m = do h <- do_fopen f m

@@ -426,7 +439,10 @@ closeFile (FHandle h) = do_fclose h

426

439

427partial

440partial

428do_fread : Ptr -> IO String

441do_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

430

446

431partial

447partial

432fread : File -> IO String

448fread : File -> IO String

@@ -434,7 +450,8 @@ fread (FHandle h) = do_fread h

434

450

435partial

451partial

436do_fwrite : Ptr -> String -> IO ()

452do_fwrite : Ptr -> String -> IO ()

453+do_fwrite h s

437−do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s

454+ = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s

438

455

439partial

456partial

440fwrite : File -> String -> IO ()

457fwrite : File -> String -> IO ()

papers/impl-paper/elaboration.tex+7−6

@@ -1181,7 +1181,8 @@ $\vV$ and $\vX$.

1181\MO{Let}\;(\vx\Hab\vX\defq\vV)\\

1182\MO{Focus}\;\vV\\

1183\ttinterp{\vv};\;

1184−\ttinterp{\ve}

1184+\ttinterp{\ve}\\

1185+\MO{Solve}

1185}

1186}

1187}

1187\subsubsection{Elaborating Applications}

1188\subsubsection{Elaborating Applications}

@@ -1659,11 +1660,11 @@ In general, \texttt{class} declarations are elaborated as follows:

1659\\

1660\\

1660\hg\hg

1661\hg\hg

1661\mq\;\RW{do}\;\AR{

1662\mq\;\RW{do}\;\AR{

1662−(\vec{\VV{meth}}\Hab\ttt)\gets\td\\

1663+%(\vec{\VV{meth}}\Hab\ttt)\gets\td\\

1663\MO{Elab}\;

1664\MO{Elab}\;

1664\AR{(\RW{data}\;\TC{C}\Hab(\ta\Hab\ttt)\to\Type\;\iwhere\\

1665\AR{(\RW{data}\;\TC{C}\Hab(\ta\Hab\ttt)\to\Type\;\iwhere\\

1665\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\;\ta)}\\

1666\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)\\

1667\vec{\MO{ElabParent}}\;\tc

1668\vec{\MO{ElabParent}}\;\tc

1668}

1669}

1669\medskip\\

1670\medskip\\

@@ -1756,13 +1757,13 @@ max x y = if (x > y) then x else y

1756

1757

1757If $\MO{Trivial}$ does not find a solution, $\MO{Instance}$ begins a global search,

1758If $\MO{Trivial}$ does not find a solution, $\MO{Instance}$ begins a global search,

1758applying every class instance, and attempting to resolve the instance's parameters

1759applying 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$:

1760

1761

1761\DM{

1762\DM{

1762−\MO{TryInstance}\;(\vI\;\ta)\;\mq\;\RW{do}\;

1763+\MO{TryInstance}\;(\FN{instanceC}\;\ta)\;\mq\;\RW{do}\;

1763\AR{

1764\AR{

1764\vec{\MO{Claim}}\;(\tx\Hab\ta)\\

1765\vec{\MO{Claim}}\;(\tx\Hab\ta)\\

1765−\ttinterp{\vI\;\tx}\\

1766+\ttinterp{\FN{instanceC};\tx}\\

1766\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}

1767\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}

1767}

1768}

1769}

rts/idris_rts.c+1

@@ -382,6 +382,7 @@ VAL idris_readStr(VM* vm, FILE* h) {

382 }

383

384 VAL str = MKSTR(vm, line_buf);

385+// printf("DBG: %s\n", line_buf);

385 free(line_buf);

386 free(line_buf);

386 return str;

387 return str;

387}

388}

rts/idris_stdfgn.h+2

@@ -8,6 +8,8 @@ void putStr(char* str);

8

9void* fileOpen(char* f, char* mode);

10void fileClose(void* h);

11+int fileEOF(void* h);

12+int fileError(void* h);

11void fputStr(void*h, char* str);

13void fputStr(void*h, char* str);

12

14

13int isNull(void* ptr);

15int isNull(void* ptr);

src/Core/Execute.hs+53−39

@@ -228,55 +228,69 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f

228

229execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

230execApp' 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 =

232 execApp' env ctxt v rest

233

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 =

235 do v'' <- tryForce v'

236 res <- execApp' env ctxt k [v''] >>= tryForce

237 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) =

239 do v' <- tryForce v

240 execApp' env ctxt (mkEApp con [tp, v']) rest

241

242-- 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)

243+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str arg):_:rest)

244− | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)

244+ | Just (FFun "putStr" _ _) <- foreignFromTT fn

245+ = do execIO (putStr arg)

245− execApp' env ctxt ioUnit rest

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

246−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

251+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

247− | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of

252+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn

253+ = do m <- case mode of

248− "r" -> return ReadMode

254+ "r" -> return ReadMode

249− "w" -> return WriteMode

255+ "w" -> return WriteMode

250− "a" -> return AppendMode

256+ "a" -> return AppendMode

251− "rw" -> return ReadWriteMode

257+ "rw" -> return ReadWriteMode

252− "wr" -> return ReadWriteMode

258+ "wr" -> return ReadWriteMode

253− "r+" -> return ReadWriteMode

259+ "r+" -> return ReadWriteMode

254− _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)

260+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)

255− h <- execIO $ openFile f m

261+ h <- execIO $ openFile f m

256− execApp' env ctxt (ioWrap (EHandle h)) rest

262+ execApp' env ctxt (ioWrap (EHandle h)) (tail rest)

257−

263+

258−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

264+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)

259− | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h

265+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn

266+ = do eofp <- execIO $ hIsEOF h

260− let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

267+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

261− execApp' env ctxt res rest

268+ execApp' env ctxt res (tail rest)

262−

269+

263−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

270+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)

264− | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h

271+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn

272+ = do execIO $ hClose h

265− execApp' env ctxt ioUnit rest

273+ execApp' env ctxt ioUnit (tail rest)

266−

274+

267−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)

275+execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EPtr p):rest)

268− | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = ioWrap . EConstant . I $

276+ | Just (FFun "isNull" _ _) <- foreignFromTT fn

277+ = let res = ioWrap . EConstant . I $

269− if p == nullPtr then 1 else 0

278+ if p == nullPtr then 1 else 0

270− in execApp' env ctxt res rest

279+ in execApp' env ctxt res (tail rest)

271−

280+

281+-- Throw away the 'World' argument to the foreign function

282+

283+execApp' env ctxt f@(EP _ (UN "mkForeignPrim") _) args@(ty:fn:xs)

272−execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun f argTs retT) <- foreignFromTT fn

284+ | Just (FFun f argTs retT) <- foreignFromTT fn

273− , length xs >= length argTs =

285+ , length xs >= length argTs =

286+ do let (args', xs') = (take (length argTs) xs, -- foreign args

287+ drop (length argTs + 1) xs) -- rest

274− do res <- stepForeign (ty:fn:take (length argTs) xs)

288+ res <- stepForeign (ty:fn:args')

275 case res of

289 case res of

276 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

290 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

277− "\" with args " ++ show (take (length argTs) xs)

291+ "\" with args " ++ show args

278− Just r -> return (mkEApp r (drop (length argTs) xs))

292+ Just r -> return (mkEApp r xs')

279− | otherwise = return (mkEApp f args)

293+ | otherwise = return (mkEApp f args)

280

294

281execApp' env ctxt c@(EP (DCon _ arity) n _) args =

295execApp' env ctxt c@(EP (DCon _ arity) n _) args =

282 do args' <- mapM tryForce (take arity args)

296 do args' <- mapM tryForce (take arity args)

@@ -502,7 +516,7 @@ stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn

502 Just f -> f args

516 Just f -> f args

503 Nothing -> return Nothing

517 Nothing -> return Nothing

504 return f'

518 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"

506

520

507mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]

521mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]

508mapMaybeM f [] = return []

522mapMaybeM f [] = return []

src/IRTS/Compiler.hs+6−6

@@ -169,9 +169,9 @@ mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)

169instance ToIR (TT Name) where

170 ir tm = ir' [] tm where

171 ir' env tm@(App f a)

172− | (P _ (UN "mkForeign") _, args) <- unApply tm

172+ | (P _ (UN "mkForeignPrim") _, args) <- unApply tm

173 = doForeign env args

174− | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm

174+ | (P _ (UN "unsafePerformPrimIO") _, [_, arg]) <- unApply tm

175 = ir' env arg

176 -- TMP HACK - until we get inlining.

177 | (P _ (UN "replace") _, [_, _, _, _, _, arg]) <- unApply tm

@@ -184,17 +184,17 @@ instance ToIR (TT Name) where

184 | (P _ (UN "par") _, [_, arg]) <- unApply tm

185 = do arg' <- ir' env arg

186 return $ LOp LPar [LLazyExp arg']

187− | (P _ (UN "fork") _, [arg]) <- unApply tm

187+ | (P _ (UN "prim_fork") _, [arg]) <- unApply tm

188 = do arg' <- ir' env arg

189 return $ LOp LFork [LLazyExp arg']

190 | (P _ (UN "prim__IO") _, [v]) <- unApply tm

191 = do v' <- ir' env v

192 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

194 = do v' <- ir' env v

195 sc' <- ir' (n:env) sc

196 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

198 = do v' <- ir' env v

199 k' <- ir' env k

200 return (LApp False k' [LForce v'])

@@ -281,7 +281,7 @@ instance ToIR (TT Name) where

281 case maybeTys of

282 Nothing -> fail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

283 Just tys -> do

284− args' <- mapM (ir' env) args

284+ args' <- mapM (ir' env) (init args)

285 -- wrap it in a prim__IO

286 -- return $ con_ 0 @@ impossible @@

287 return $ -- LLazyExp $

src/Idris/AbsSyntaxTree.hs+4−1

@@ -138,7 +138,10 @@ data CGInfo = CGInfo { argsdef :: [Name],

138deriving instance Binary CGInfo

139!-}

140

141−primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]

141+primDefs = [UN "unsafePerformPrimIO",

142+ UN "mkLazyForeignPrim",

143+ UN "mkForeignPrim",

144+ UN "FalseElim"]

142

145

143-- information that needs writing for the current module's .ibc file

146-- information that needs writing for the current module's .ibc file

144data IBCWrite = IBCFix FixDecl

147data IBCWrite = IBCFix FixDecl

src/Idris/ElabDecls.hs+4−1

@@ -306,7 +306,10 @@ elabProvider info syn fc n ty tm

306 elabType info syn "" fc [] n ty

307

308 -- 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])

310 let rhs' = normalise ctxt [] rhs

313 let rhs' = normalise ctxt [] rhs

311 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

314 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

312

315

src/Idris/Parser.hs+16−1

@@ -927,7 +927,22 @@ pUnifyLog syn = do lchar '%'; reserved "unifyLog";

927 tm <- pSimpleExpr syn

928 return (PUnifyLog tm)

929

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+

930−pApp syn = do f <- pSimpleExpr syn

945+ <|> do f <- pSimpleExpr syn

931 fc <- pfc

946 fc <- pfc

932 args <- many1 (do notEndApp

947 args <- many1 (do notEndApp

933 pArg syn)

948 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 ""]

15

16-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

17getProvided :: 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

19 , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =

20 case err of

21 Constant (Str msg) -> ierror . ProviderError $ msg

22 _ -> 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

24 , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =

25 return res

26 | otherwise = fail $ "Internal type provider error: result was not " ++

test/test004/expected+9

@@ -1,7 +1,16 @@

1Reading testfile

2Hello!

3World!

4+...

5+3

6+4

7+Last line

4

8

5---

9---

6Hello!

10Hello!

7World!

11World!

12+...

13+3

14+4

15+Last line

16+---

test/test004/test004.idr+14−5

@@ -1,21 +1,30 @@

1module Main

2

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+

3dumpFile : String -> IO ()

10dumpFile : String -> IO ()

4dumpFile fn = do { h <- openFile fn Read

11dumpFile fn = do { h <- openFile fn Read

12+ mwhile (do { -- putStrLn "TEST"

5− while (do { x <- feof h

13+ x <- feof h

6− return (not x) })

14+ return (not x) })

7− (do { l <- fread h

15+ (do { l <- fread h

8− putStr l })

16+ putStr l })

9 closeFile h }

17 closeFile h }

10

18

11main : IO ()

19main : IO ()

12main = do { h <- openFile "testfile" Write

20main = do { h <- openFile "testfile" Write

13− fwrite h "Hello!\nWorld!\n"

21+ fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"

14 closeFile h

22 closeFile h

15 putStrLn "Reading testfile"

23 putStrLn "Reading testfile"

16 f <- readFile "testfile"

24 f <- readFile "testfile"

17 putStrLn f

25 putStrLn f

18 putStrLn "---"

26 putStrLn "---"

19 dumpFile "testfile"

27 dumpFile "testfile"

28+ putStrLn "---"

20 }

29 }

21

30

test/test024/test024.idr+1−1

@@ -3,4 +3,4 @@ module Main

3main : IO ()

4main = do l <- getLine

5 let ll = l ++ l

6− putStrLn ll

6+ putStrLn ll