c69550a · Idris-dev · git.iko.soy

11import Idris.Core.Evaluate

12import Idris.Core.CaseTree

13

14+import Idris.Error

15+

14import Debug.Trace

16import Debug.Trace

15

17

16import Util.DynamicLinker

18import Util.DynamicLinker

113initState = do ist <- getIState

115initState = do ist <- getIState

114 return $ ExecState (idris_dynamic_libs ist)

116 return $ ExecState (idris_dynamic_libs ist)

115

117

116−type Exec = ErrorT String (StateT ExecState IO)

118+type Exec = ErrorT Err (StateT ExecState IO)

117

119

118−runExec :: Exec a -> ExecState -> IO (Either String a)

120+runExec :: Exec a -> ExecState -> IO (Either Err a)

119runExec ex st = fst <$> runStateT (runErrorT ex) st

121runExec ex st = fst <$> runStateT (runErrorT ex) st

120

122

121getExecState :: Exec ExecState

123getExecState :: Exec ExecState

124putExecState :: ExecState -> Exec ()

126putExecState :: ExecState -> Exec ()

125putExecState = lift . put

127putExecState = lift . put

126

128

127−execFail :: String -> Exec a

129+execFail :: Err -> Exec a

128execFail = throwError

130execFail = throwError

129

131

130execIO :: IO a -> Exec a

132execIO :: IO a -> Exec a

138 do res <- doExec [] ctxt tm

140 do res <- doExec [] ctxt tm

139 toTT res

141 toTT res

140 case res of

142 case res of

141− Left err -> fail err

143+ Left err -> ierror err

142 Right tm' -> return tm'

144 Right tm' -> return tm'

143

145

144ioWrap :: ExecVal -> ExecVal

146ioWrap :: ExecVal -> ExecVal

160 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

162 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

161 doExec env ctxt tm

163 doExec env ctxt tm

162 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

164 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

163− [] -> execFail $ "Could not find " ++ show n ++ " in definitions."

165+ [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."

164 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

166 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

165doExec env ctxt p@(P Bound n ty) =

167doExec env ctxt p@(P Bound n ty) =

166 case lookup n env of

168 case lookup n env of

167− Nothing -> execFail "not found"

169+ Nothing -> execFail . Msg $ "not found"

168 Just tm -> return tm

170 Just tm -> return tm

169doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

171doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

170doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

172doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

171doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

173doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

172− | otherwise = execFail "env too small"

174+ | otherwise = execFail . Msg $ "env too small"

173doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

175doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

174 doExec ((n, v'):env) ctxt body

176 doExec ((n, v'):env) ctxt body

175doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

177doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

216 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest

218 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest

217

219

218-- Special cases arising from not having access to the C RTS in the interpreter

220-- Special cases arising from not having access to the C RTS in the interpreter

219−execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

221+execApp env ctxt (EP _ fp _) (_:fn:str:_:rest)

220 | fp == mkfprim,

222 | fp == mkfprim,

221 Just (FFun "putStr" _ _) <- foreignFromTT fn

223 Just (FFun "putStr" _ _) <- foreignFromTT fn

224+ = case str of

222− = do execIO (putStr arg)

225+ EConstant (Str arg) -> do execIO (putStr arg)

223− execApp env ctxt ioUnit rest

226+ execApp env ctxt ioUnit rest

227+ _ -> execFail . Msg $

228+ "The argument to putStr should be a constant string, but it was " ++

229+ show str ++

230+ ". Are all cases covered?"

224−execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

231+execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)

225 | fp == mkfprim,

232 | fp == mkfprim,

226 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

233 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

234+ = case handle of

227− = do contents <- execIO $ hGetLine h

235+ EHandle h -> do contents <- execIO $ hGetLine h

228− execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest

236+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest

237+ _ -> execFail . Msg $

238+ "The argument to idris_readStr should be a handle, but it was " ++

239+ show handle ++

240+ ". Are all cases covered?"

229−execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

241+execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)

230 | fp == mkfprim,

242 | fp == mkfprim,

231 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

243 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

244+ = case (fileStr, modeStr) of

245+ (EConstant (Str f), EConstant (Str mode)) ->

232− = do f <- execIO $

246+ do f <- execIO $

233− catch (do let m = case mode of

247+ catch (do let m = case mode of

234− "r" -> Right ReadMode

248+ "r" -> Right ReadMode

235− "w" -> Right WriteMode

249+ "w" -> Right WriteMode

236− "a" -> Right AppendMode

250+ "a" -> Right AppendMode

237− "rw" -> Right ReadWriteMode

251+ "rw" -> Right ReadWriteMode

238− "wr" -> Right ReadWriteMode

252+ "wr" -> Right ReadWriteMode

239− "r+" -> Right ReadWriteMode

253+ "r+" -> Right ReadWriteMode

240− _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)

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

241− case fmap (openFile f) m of

255+ case fmap (openFile f) m of

242− Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)

256+ Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)

243− Left err -> return $ Left err)

257+ Left err -> return $ Left err)

244− (\e -> let _ = ( e::SomeException)

258+ (\e -> let _ = ( e::SomeException)

245− in return $ Right (ioWrap (EPtr nullPtr), tail rest))

259+ in return $ Right (ioWrap (EPtr nullPtr), tail rest))

246− case f of

260+ case f of

247− Left err -> execFail err

261+ Left err -> execFail . Msg $ err

248− Right (res, rest) -> execApp env ctxt res rest

262+ Right (res, rest) -> execApp env ctxt res rest

249−

263+ _ -> execFail . Msg $

264+ "The arguments to fileOpen should be constant strings, but they were " ++

265+ show fileStr ++ " and " ++ show modeStr ++

266+ ". Are all cases covered?"

267+

250−execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

268+execApp env ctxt (EP _ fp _) (_:fn:handle:rest)

251 | fp == mkfprim,

269 | fp == mkfprim,

252 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

270 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

271+ = case handle of

253− = do eofp <- execIO $ hIsEOF h

272+ EHandle h -> do eofp <- execIO $ hIsEOF h

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

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

255− execApp env ctxt res (tail rest)

274+ execApp env ctxt res (tail rest)

256−

275+ _ -> execFail . Msg $

276+ "The argument to fileEOF should be a file handle, but it was " ++

277+ show handle ++

278+ ". Are all cases covered?"

279+

257−execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

280+execApp env ctxt (EP _ fp _) (_:fn:handle:rest)

258 | fp == mkfprim,

281 | fp == mkfprim,

259 Just (FFun "fileClose" _ _) <- foreignFromTT fn

282 Just (FFun "fileClose" _ _) <- foreignFromTT fn

283+ = case handle of

260− = do execIO $ hClose h

284+ EHandle h -> do execIO $ hClose h

261− execApp env ctxt ioUnit (tail rest)

285+ execApp env ctxt ioUnit (tail rest)

262−

286+ _ -> execFail . Msg $

263−execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

287+ "The argument to fileClose should be a file handle, but it was " ++

264− | fp == mkfprim,

288+ show handle ++

265− Just (FFun "isNull" _ _) <- foreignFromTT fn

289+ ". Are all cases covered?"

266− = let res = ioWrap . EConstant . I $

290+

267− if p == nullPtr then 1 else 0

268− in execApp env ctxt res (tail rest)

269−

270−-- Handles will be checked as null pointers sometimes - but if we got a

271−-- real Handle, then it's valid, so just return 1.

272−execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

291+execApp env ctxt (EP _ fp _) (_:fn:ptr:rest)

273 | fp == mkfprim,

292 | fp == mkfprim,

274 Just (FFun "isNull" _ _) <- foreignFromTT fn

293 Just (FFun "isNull" _ _) <- foreignFromTT fn

294+ = case ptr of

295+ EPtr p -> let res = ioWrap . EConstant . I $

296+ if p == nullPtr then 1 else 0

297+ in execApp env ctxt res (tail rest)

298+ -- Handles will be checked as null pointers sometimes - but if we got a

299+ -- real Handle, then it's valid, so just return 1.

300+ EHandle h -> let res = ioWrap . EConstant . I $ 0

301+ in execApp env ctxt res (tail rest)

302+ -- A foreign-returned char* has to be tested for NULL sometimes

275− = let res = ioWrap . EConstant . I $ 0

303+ EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0

276− in execApp env ctxt res (tail rest)

304+ in execApp env ctxt res (tail rest)

305+ _ -> execFail . Msg $

306+ "The argument to isNull should be a pointer or file handle or string, but it was " ++

307+ show ptr ++

308+ ". Are all cases covered?"

277

309

278−-- A foreign-returned char* has to be tested for NULL sometimes

279−execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

280− | fp == mkfprim,

281− Just (FFun "isNull" _ _) <- foreignFromTT fn

282− = let res = ioWrap . EConstant . I $ 0

283− in execApp env ctxt res (tail rest)

284

310

285-- Right now, there's no way to send command-line arguments to the executor,

311-- Right now, there's no way to send command-line arguments to the executor,

286-- so just return 0.

312-- so just return 0.

289 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

315 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

290 = let res = ioWrap . EConstant . I $ 0

316 = let res = ioWrap . EConstant . I $ 0

291 in execApp env ctxt res (tail rest)

317 in execApp env ctxt res (tail rest)

292−-- Throw away the 'World' argument to the foreign function

293

318

294execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

319execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

295 = case foreignFromTT fn of

320 = case foreignFromTT fn of