25c1352 · Idris-dev · git.iko.soy

47

48data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

49

50−data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

51− , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

52− , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

53− , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

50+newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

54− }

51+ }

55

52

56data ExecVal = EP NameType Name ExecVal

53data ExecVal = EP NameType Name ExecVal

57 | EV Int

54 | EV Int

61 | EErased

58 | EErased

62 | EConstant Const

59 | EConstant Const

63 | forall a. EPtr (Ptr a)

60 | forall a. EPtr (Ptr a)

64− | EThunk Int

61+ | EThunk ExecEnv Term

65 | EHandle Handle

62 | EHandle Handle

66

63

67instance Show ExecVal where

64instance Show ExecVal where

73 show EErased = "[__]"

70 show EErased = "[__]"

74 show (EConstant c) = show c

71 show (EConstant c) = show c

75 show (EPtr p) = "<<ptr " ++ show p ++ ">>"

72 show (EPtr p) = "<<ptr " ++ show p ++ ">>"

76− show (EThunk i) = "<<thunk " ++ show i ++ ">>"

73+ show (EThunk env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"

77 show (EHandle h) = "<<handle " ++ show h ++ ">>"

74 show (EHandle h) = "<<handle " ++ show h ++ ">>"

78

75

79toTT :: ExecVal -> Exec Term

76toTT :: ExecVal -> Exec Term

97toTT (EType u) = return $ TType u

94toTT (EType u) = return $ TType u

98toTT EErased = return Erased

95toTT EErased = return Erased

99toTT (EConstant c) = return (Constant c)

96toTT (EConstant c) = return (Constant c)

100−toTT (EThunk i) = return (P (DCon 0 0) (sMN i "THUNK") Erased) --(force i) >>= toTT

97+toTT (EThunk env tm) = return tm

101toTT (EHandle _) = return Erased

98toTT (EHandle _) = return Erased

102

99

103unApplyV :: ExecVal -> (ExecVal, [ExecVal])

100unApplyV :: ExecVal -> (ExecVal, [ExecVal])

111

108

112initState :: Idris ExecState

109initState :: Idris ExecState

113initState = do ist <- getIState

110initState = do ist <- getIState

114− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

111+ return $ ExecState (idris_dynamic_libs ist)

115

112

116type Exec = ErrorT String (StateT ExecState IO)

113type Exec = ErrorT String (StateT ExecState IO)

117

114

130execIO :: IO a -> Exec a

127execIO :: IO a -> Exec a

131execIO = lift . lift

128execIO = lift . lift

132

129

133−delay :: ExecEnv -> Context -> Term -> Exec ExecVal

134−delay env ctxt tm =

135− do st <- getExecState

136− let i = exec_next_thunk st

137− putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

138− , exec_next_thunk = exec_next_thunk st + 1

139− }

140− return $ EThunk i

141−

142−force :: Int -> Exec ExecVal

143−force i = do st <- getExecState

144− case M.lookup i (exec_thunks st) of

145− Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

146− case tm' of

147− EThunk i ->

148− do res <- force i

149− update res i

150− return res

151− _ -> do update tm' i

152− return tm'

153− Just (Forced tm) -> return tm

154− Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

155− where update :: ExecVal -> Int -> Exec ()

156− update tm i = do est <- getExecState

157− putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

158−

159−tryForce :: ExecVal -> Exec ExecVal

160−tryForce (EThunk i) = force i

161−tryForce tm = return tm

162−

163−debugThunks :: Exec ()

164−debugThunks = do st <- getExecState

165− execIO $ putStrLn (take 4000 (show (exec_thunks st)))

166

130

167execute :: Term -> Idris Term

131execute :: Term -> Idris Term

168execute tm = do est <- initState

132execute tm = do est <- initState

169 ctxt <- getContext

133 ctxt <- getContext

170− res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm

134+ res <- lift . lift . flip runExec est $

135+ do res <- doExec [] ctxt tm

171− toTT res

136+ toTT res

172 case res of

137 case res of

173 Left err -> fail err

138 Left err -> fail err

174 Right tm' -> return tm'

139 Right tm' -> return tm'

208doExec env ctxt tm@(Bind n b body) = return $

173doExec env ctxt tm@(Bind n b body) = return $

209 EBind n (fmap (\_->EErased) b)

174 EBind n (fmap (\_->EErased) b)

210 (\arg -> doExec ((n, arg):env) ctxt body)

175 (\arg -> doExec ((n, arg):env) ctxt body)

211−doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

176+doExec env ctxt a@(App _ _) =

177+ do let (f, args) = unApply a

178+ f' <- doExec env ctxt f

179+ args' <- case f' of

180+ (EP _ d _) | d == delay ->

181+ case args of

182+ [t,a,tm] -> do t' <- doExec env ctxt t

183+ a' <- doExec env ctxt a

184+ return [t', a', EThunk env tm]

185+ _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate

186+ fun' -> do mapM (doExec env ctxt) args

187+ execApp env ctxt f' args'

212doExec env ctxt (Constant c) = return (EConstant c)

188doExec env ctxt (Constant c) = return (EConstant c)

213doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

189doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

214 doExec env ctxt ((x:xs) !! i)

190 doExec env ctxt ((x:xs) !! i)

216doExec env ctxt Impossible = fail "Tried to execute an impossible case"

192doExec env ctxt Impossible = fail "Tried to execute an impossible case"

217doExec env ctxt (TType u) = return (EType u)

193doExec env ctxt (TType u) = return (EType u)

218

194

219−execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

195+

220−execApp env ctxt (f, args) = do newF <- doExec env ctxt f

221− laziness <- (++ repeat False) <$> (getLaziness newF)

222− newArgs <- mapM argExec (zip args laziness)

223− res <- execApp' env ctxt newF newArgs

224− return res

225− where getLaziness (EP _ l _) | l == sUN "lazy" = return [False, True]

226− getLaziness (EP _ n _) = do est <- getExecState

227− let argInfo = exec_implicits est

228− case lookupCtxtName n argInfo of

229− [] -> return (repeat False)

230− [ps] -> return $ map lazyarg (snd ps)

231− many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

232− getLaziness _ = return (repeat False) -- ok due to zip above

233− argExec :: (Term, Bool) -> Exec ExecVal

234− argExec (tm, False) = doExec env ctxt tm

235− argExec (tm, True) = delay env ctxt tm

236−

237−

238−execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

196+execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

239−execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

197+execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls

198+execApp env ctxt (EP _ f _) (t:a:delayed:rest)

199+ | f == force

200+ , (_, [_, _, EThunk tmEnv tm]) <- unApplyV delayed =

201+ do tm' <- doExec tmEnv ctxt tm

202+ execApp env ctxt tm' rest

240−execApp' env ctxt (EP _ fp _) (ty:action:rest)

203+execApp env ctxt (EP _ fp _) (ty:action:rest)

241 | fp == upio,

204 | fp == upio,

242 (prim__IO, [_, v]) <- unApplyV action

205 (prim__IO, [_, v]) <- unApplyV action

243− = execApp' env ctxt v rest

206+ = execApp env ctxt v rest

244

207

245−execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)

208+execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)

246 | fp == piobind,

209 | fp == piobind,

247 (prim__IO, [_, v']) <- unApplyV v =

210 (prim__IO, [_, v']) <- unApplyV v =

248− do v'' <- tryForce v'

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

211+ do res <- execApp env ctxt k [v']

250− execApp' env ctxt res rest

212+ execApp env ctxt res rest

251−execApp' env ctxt con@(EP _ fp _) args@(tp:v:rest)

213+execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)

252− | fp == pioret =

253− do v' <- tryForce v

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

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

255

215

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

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

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

217+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

258 | fp == mkfprim,

218 | fp == mkfprim,

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

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

260 = do execIO (putStr arg)

220 = do execIO (putStr arg)

261− execApp' env ctxt ioUnit rest

221+ execApp env ctxt ioUnit rest

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

222+execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

263 | fp == mkfprim,

223 | fp == mkfprim,

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

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

265 = do contents <- execIO $ hGetLine h

225 = do contents <- execIO $ hGetLine h

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

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

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

227+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

268 | fp == mkfprim,

228 | fp == mkfprim,

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

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

270 = do f <- execIO $

230 = do f <- execIO $

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

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

284 case f of

244 case f of

285 Left err -> execFail err

245 Left err -> execFail err

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

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

287

247

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

248+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

289 | fp == mkfprim,

249 | fp == mkfprim,

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

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

291 = do eofp <- execIO $ hIsEOF h

251 = do eofp <- execIO $ hIsEOF h

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

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

293− execApp' env ctxt res (tail rest)

253+ execApp env ctxt res (tail rest)

294

254

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

255+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

296 | fp == mkfprim,

256 | fp == mkfprim,

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

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

298 = do execIO $ hClose h

258 = do execIO $ hClose h

299− execApp' env ctxt ioUnit (tail rest)

259+ execApp env ctxt ioUnit (tail rest)

300

260

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

261+execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

302 | fp == mkfprim,

262 | fp == mkfprim,

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

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

304 = let res = ioWrap . EConstant . I $

264 = let res = ioWrap . EConstant . I $

305 if p == nullPtr then 1 else 0

265 if p == nullPtr then 1 else 0

306− in execApp' env ctxt res (tail rest)

266+ in execApp env ctxt res (tail rest)

307

267

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

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

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

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

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

270+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

311 | fp == mkfprim,

271 | fp == mkfprim,

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

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

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

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

314− in execApp' env ctxt res (tail rest)

274+ in execApp env ctxt res (tail rest)

315

275

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

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

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

277+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

318 | fp == mkfprim,

278 | fp == mkfprim,

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

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

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

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

321− in execApp' env ctxt res (tail rest)

281+ in execApp env ctxt res (tail rest)

322

282

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

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

324-- so just return 0.

284-- so just return 0.

325−execApp' env ctxt (EP _ fp _) (_:fn:rest)

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

326 | fp == mkfprim,

286 | fp == mkfprim,

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

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

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

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

329− in execApp' env ctxt res (tail rest)

289+ in execApp env ctxt res (tail rest)

330-- Throw away the 'World' argument to the foreign function

290-- Throw away the 'World' argument to the foreign function

331

291

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

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

333 = case foreignFromTT fn of

293 = case foreignFromTT fn of

334 Just (FFun f argTs retT) | length xs >= length argTs ->

294 Just (FFun f argTs retT) | length xs >= length argTs ->

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

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

341 Just r -> return (mkEApp r xs')

301 Just r -> return (mkEApp r xs')

342 Nothing -> return (mkEApp f args)

302 Nothing -> return (mkEApp f args)

343

303

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

304+execApp env ctxt c@(EP (DCon _ arity) n _) args =

345− do args' <- mapM tryForce (take arity args)

305+ do let args' = take arity args

346 let restArgs = drop arity args

306 let restArgs = drop arity args

347− execApp' env ctxt (mkEApp c args') restArgs

307+ execApp env ctxt (mkEApp c args') restArgs

348

308

349−execApp' env ctxt c@(EP (TCon _ arity) n _) args =

309+execApp env ctxt c@(EP (TCon _ arity) n _) args =

350− do args' <- mapM tryForce (take arity args)

310+ do let args' = take arity args

351 let restArgs = drop arity args

311 let restArgs = drop arity args

352− execApp' env ctxt (mkEApp c args') restArgs

312+ execApp env ctxt (mkEApp c args') restArgs

353

313

354−execApp' env ctxt f@(EP _ n _) args =

314+execApp env ctxt f@(EP _ n _) args =

355 do let val = lookupDef n ctxt

315 do let val = lookupDef n ctxt

356 case val of

316 case val of

357 [Function _ tm] -> fail "should already have been eval'd"

317 [Function _ tm] -> fail "should already have been eval'd"

358 [TyDecl nt ty] -> return $ mkEApp f args

318 [TyDecl nt ty] -> return $ mkEApp f args

359 [Operator tp arity op] ->

319 [Operator tp arity op] ->

360 if length args >= arity

320 if length args >= arity

361− then do args' <- mapM tryForce $ take arity args

321+ then let args' = take arity args in

362− case getOp n args' of

322+ case getOp n args' of

363− Just res -> do r <- res

323+ Just res -> do r <- res

364− execApp' env ctxt r (drop arity args)

324+ execApp env ctxt r (drop arity args)

365− Nothing -> return (mkEApp f args)

325+ Nothing -> return (mkEApp f args)

366 else return (mkEApp f args)

326 else return (mkEApp f args)

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

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

368 do rhs <- doExec env ctxt tm

328 do rhs <- doExec env ctxt tm

369− execApp' env ctxt rhs args

329+ execApp env ctxt rhs args

370 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

330 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

371 do res <- execCase env ctxt ns sc args

331 do res <- execCase env ctxt ns sc args

372 return $ fromMaybe (mkEApp f args) res

332 return $ fromMaybe (mkEApp f args) res

373 thing -> return $ mkEApp f args

333 thing -> return $ mkEApp f args

374−execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

334+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

375− let (f', as) = unApplyV ret

335+ let (f', as) = unApplyV ret

376− execApp' env ctxt f' (as ++ args)

336+ execApp env ctxt f' (as ++ args)

377−execApp' env ctxt (EThunk i) args = do f <- force i

378− execApp' env ctxt f args

379−execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

337+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)

380−execApp' env ctxt f args = return (mkEApp f args)

338+execApp env ctxt f args = return (mkEApp f args)

381

339

382prs = sUN "prim__readString"

340prs = sUN "prim__readString"

383pbm = sUN "prim__believe_me"

341pbm = sUN "prim__believe_me"

386pioret = sUN "prim_io_return"

344pioret = sUN "prim_io_return"

387piobind = sUN "prim_io_bind"

345piobind = sUN "prim_io_bind"

388upio = sUN "unsafePerformPrimIO"

346upio = sUN "unsafePerformPrimIO"

347+delay = sUN "Delay"

348+force = sUN "Force"

389

349

390-- | Look up primitive operations in the global table and transform them into ExecVal functions

350-- | Look up primitive operations in the global table and transform them into ExecVal functions

391getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

351getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

426-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

386-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

427 caseRes <- execCase' env ctxt amap sc

387 caseRes <- execCase' env ctxt amap sc

428 case caseRes of

388 case caseRes of

429− Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

389+ Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

430 Nothing -> return Nothing

390 Nothing -> return Nothing

431 else return Nothing

391 else return Nothing

432

392

436execCase' env ctxt amap (STerm tm) =

396execCase' env ctxt amap (STerm tm) =

437 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

397 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

438execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

398execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

439− do tm' <- tryForce tm

440− case chooseAlt tm' alts of

399+ case chooseAlt tm alts of

441 Just (newCase, newBindings) ->

400 Just (newCase, newBindings) ->

442 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

401 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

443 execCase' env ctxt amap' newCase

402 execCase' env ctxt amap' newCase