git.iko.soy/Idris-dev
on master help sign in
Reinstate inlining of type class dictionaries
b6627beEdwin Brady
src/Core/Evaluate.hs+34−9
compare with master
unifiedsplit
@@ -22,6 +22,7 @@ import Core.CaseTree
22
22
23data EvalState = ES { limited :: [(Name, Int)],
23data EvalState = ES { limited :: [(Name, Int)],
24 nexthole :: Int }
24 nexthole :: Int }
25+ deriving Show
25
26
26type Eval a = State EvalState a
27type Eval a = State EvalState a
27
28
@@ -185,7 +186,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
185 -- normal evaluation should return false
186 -- normal evaluation should return false
186 blockSimplify (CaseInfo inl dict) n stk
187 blockSimplify (CaseInfo inl dict) n stk
187 | RunTT `elem` opts
188 | RunTT `elem` opts
188− = not inl || elem n stk
189+ = not (inl || dict) || elem n stk
189 | Simplify `elem` opts
190 | Simplify `elem` opts
190 = (not (inl || dict) || elem n stk)
191 = (not (inl || dict) || elem n stk)
191 || (n == UN "prim__syntactic_eq")
192 || (n == UN "prim__syntactic_eq")
@@ -260,7 +261,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
260 a' <- ev ntimes stk False env a
261 a' <- ev ntimes stk False env a
261 evApply ntimes stk top env [a'] f'
262 evApply ntimes stk top env [a'] f'
262 ev ntimes stk top env (Proj t i)
263 ev ntimes stk top env (Proj t i)
264+ = do -- evaluate dictionaries if it means the projection works
263− = do t' <- ev ntimes stk top env t
265+ t' <- ev ntimes stk top env t
266+-- tfull' <- reapply ntimes stk top env t' []
264 return (doProj t' (getValArgs t'))
267 return (doProj t' (getValArgs t'))
265 where doProj t' (VP (DCon _ _) _ _, args) | i < length args = args!!i
268 where doProj t' (VP (DCon _ _) _ _, args) | i < length args = args!!i
266 doProj t' _ = VProj t' i
269 doProj t' _ = VProj t' i
@@ -275,6 +278,22 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
275 evApply ntimes stk top env args f
278 evApply ntimes stk top env args f
276 = apply ntimes stk top env f args
279 = apply ntimes stk top env f args
277
280
281+ reapply ntimes stk top env f@(VP Ref n ty) args
282+ = let val = lookupDefAcc n atRepl ctxt in
283+ case val of
284+ [(CaseOp ci _ _ _ cd, acc)] ->
285+ let (ns, tree) = getCases cd in
286+ do c <- evCase ntimes n (n:stk) top env ns args tree
287+ case c of
288+ (Nothing, _) -> return $ unload env (VP Ref n ty) args
289+ (Just v, rest) -> evApply ntimes stk top env rest v
290+ _ -> case args of
291+ (a : as) -> return $ unload env f (a : as)
292+ [] -> return f
293+ reapply ntimes stk top env (VApp f a) args
294+ = reapply ntimes stk top env f (a : args)
295+ reapply ntimes stk top env v args = return v
296+
278 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
297 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
279 = do a' <- sc a
298 = do a' <- sc a
280 app <- apply ntimes stk top env a' as
299 app <- apply ntimes stk top env a' as
@@ -344,18 +363,24 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
344 etm' <- ev ntimes stk (not (conHeaded tm))
363 etm' <- ev ntimes stk (not (conHeaded tm))
345 (map snd amap ++ env) etm
364 (map snd amap ++ env) etm
346 return $ Just etm'
365 return $ Just etm'
366+ evTree ntimes stk top env amap (ProjCase t alts)
367+ = do t' <- ev ntimes stk top env t
368+ doCase ntimes stk top env amap t' alts
347 evTree ntimes stk top env amap (Case n alts)
369 evTree ntimes stk top env amap (Case n alts)
348 = case lookup n amap of
370 = case lookup n amap of
349− Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
371+ Just v -> doCase ntimes stk top env amap v alts
350− case c of
351− Just (altmap, sc) -> evTree ntimes stk top env altmap sc
352− _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
353− case c' of
354− Just (altmap, sc) -> evTree ntimes stk top env altmap sc
355− _ -> return Nothing
356 _ -> return Nothing
372 _ -> return Nothing
357 evTree ntimes stk top env amap ImpossibleCase = return Nothing
373 evTree ntimes stk top env amap ImpossibleCase = return Nothing
358
374
375+ doCase ntimes stk top env amap v alts =
376+ do c <- chooseAlt env v (getValArgs v) alts amap
377+ case c of
378+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc
379+ _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
380+ case c' of
381+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc
382+ _ -> return Nothing
383+
359 conHeaded tm@(App _ _)
384 conHeaded tm@(App _ _)
360 | (P (DCon _ _) _ _, args) <- unApply tm = True
385 | (P (DCon _ _) _ _, args) <- unApply tm = True
361 conHeaded t = False
386 conHeaded t = False