git.iko.soy/Idris-dev
on master help sign in
HNF in unification to speed things up
e5706d3Edwin Brady
src/Core/CaseTree.hs+1−1
compare with master
unifiedsplit
@@ -79,7 +79,7 @@ instance TermSize CaseAlt where
79small :: Name -> [Name] -> SC -> Bool
79small :: Name -> [Name] -> SC -> Bool
80small n args t = let as = findAllUsedArgs t args in
80small n args t = let as = findAllUsedArgs t args in
81 length as == length (nub as) &&
81 length as == length (nub as) &&
82− termsize n t < 20
82+ termsize n t < 20
83
83
84namesUsed :: SC -> [Name]
84namesUsed :: SC -> [Name]
85namesUsed sc = nub $ nu' [] sc where
85namesUsed sc = nub $ nu' [] sc where
src/Core/Evaluate.hs+1−1
@@ -224,7 +224,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
224 do let val = lookupDefAcc Nothing n atRepl ctxt
224 do let val = lookupDefAcc Nothing n atRepl ctxt
225 case val of
225 case val of
226 [(CaseOp inl inr _ _ _ ns tree _ _, acc)]
226 [(CaseOp inl inr _ _ _ ns tree _ _, acc)]
227− | acc == Public || simpl -> -- unoptimised version
227+ | acc == Public -> -- unoptimised version
228 if canSimplify inl inr n stk
228 if canSimplify inl inr n stk
229 then return $ unload env (VP Ref n ty) args
229 then return $ unload env (VP Ref n ty) args
230 else do c <- evCase ntimes (n:stk) top env ns args tree
230 else do c <- evCase ntimes (n:stk) top env ns args tree
src/Core/Unify.hs+1−1
@@ -163,7 +163,7 @@ unify ctxt env topx topy injtc holes =
163 unArgs uf argsx argsy
163 unArgs uf argsx argsy
164 else unifyTmpFail appx appy
164 else unifyTmpFail appx appy
165 where hnormalise [] _ _ t = t
165 where hnormalise [] _ _ t = t
166− hnormalise ns ctxt env t = normalise ctxt env t
166+ hnormalise ns ctxt env t = hnf ctxt env t
167 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
167 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
168 | x /= y = unifyFail appx appy
168 | x /= y = unifyFail appx appy
169 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
169 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)