18fbb2f · Idris-dev · git.iko.soy

81toTT (EType u) = return $ TType u

82toTT EErased = return Erased

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

84−toTT (EThunk i) = (force i) >>= toTT

84+toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT

85toTT (EHandle _) = return Erased

86

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

163ioUnit :: ExecVal

164ioUnit = ioWrap (EP Ref unitCon EErased)

165

166−type ExecEnv = [(Name, Binder ExecVal)]

166+type ExecEnv = [(Name, ExecVal)]

167

168doExec :: ExecEnv -> Context -> Term -> Exec ExecVal

169doExec env ctxt p@(P Ref n ty) =

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

180 case lookup n env of

181 Nothing -> execFail "not found"

182− Just (Let _ tm) -> return tm

182+ Just tm -> return tm

183− Just b -> execFail $ "Unknown binder " ++ show b

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

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

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

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

186−doExec env ctxt v@(V i) | i < length env = do let binder = env !! i

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

187− case binder of

188− (_, (Let t v)) -> return v

189− (_, (NLet t v)) -> return v

190− (n, b) -> doExec env ctxt (P Bound n Erased)

191 | otherwise = execFail "env too small"

186 | otherwise = execFail "env too small"

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

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

193− doExec ((n, Let EErased v'):env) ctxt body

188+ doExec ((n, v'):env) ctxt body

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

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

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

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

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

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

197− (\arg -> doExec ((n, Let EErased arg):env) ctxt body)

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

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

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

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

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

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

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

227 execApp' env ctxt v rest

222 execApp' env ctxt v rest

228

223

229execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =

224execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =

225+ do v'' <- tryForce v'

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

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

231 execApp' env ctxt res rest

227 execApp' env ctxt res rest

228+execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =

229+ do v' <- tryForce v

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

232

231

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

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

234execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)

233execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)

299 primResBool (s1 == s2)

298 primResBool (s1 == s2)

300 getOp (UN "prim__intToFloat") [EConstant (I i)] =

299 getOp (UN "prim__intToFloat") [EConstant (I i)] =

301 primRes Fl (fromRational (toRational i))

300 primRes Fl (fromRational (toRational i))

301+ getOp (UN "prim__intToStr") [EConstant (I i)] =

302+ primRes Str (show i)

302 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =

303 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =

303 primResBool (i1 < i2)

304 primResBool (i1 < i2)

304 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =

305 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =

352 if arity <= length args

353 if arity <= length args

353 then do let amap = zip ns args

354 then do let amap = zip ns args

354-- debugThunks

355-- debugThunks

356+-- trace ("Environment: " ++ show env) $ return ()

355-- trace ("Case exec in " ++ take 1000 (show amap) ++ "\nwith " ++ show sc++"\n") $ return ()

357-- trace ("Case exec in " ++ take 1000 (show amap) ++ "\nwith " ++ show sc++"\n") $ return ()

356 caseRes <- execCase' env ctxt amap sc

358 caseRes <- execCase' env ctxt amap sc

357 case caseRes of

359 case caseRes of

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

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

359 Nothing -> return Nothing

361 Nothing -> return Nothing

360 else return Nothing

362 else return Nothing

361

363

363execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)

365execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)

364execCase' env ctxt amap (UnmatchedCase _) = return Nothing

366execCase' env ctxt amap (UnmatchedCase _) = return Nothing

365execCase' env ctxt amap (STerm tm) =

367execCase' env ctxt amap (STerm tm) =

366− Just <$> doExec (map (\(n, v) -> (n, Let EErased v)) amap ++ env) ctxt tm

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

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

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

368 do tm' <- tryForce tm

370 do tm' <- tryForce tm

369 case chooseAlt tm' alts of

371 case chooseAlt tm' alts of