My profiling showed that the BinTree operations were responsible for about 60% of the CPU time when reading a large .gfo file. Replacing BinTree by Data.Map reduced this to about 6%, which meant about 50% reduction in total CPU time.

This commit is contained in:
bjorn
2008-11-26 15:44:22 +00:00
parent 260e13146e
commit 5dee98234e
8 changed files with 45 additions and 88 deletions

View File

@@ -38,10 +38,11 @@ shareModule opt (i,m) = case m of
(i,M.ModMod (M.replaceJudgements mo (mapTree (shareInfo opt) (M.jments mo))))
_ -> (i,m)
shareInfo opt (c, CncCat ty (Yes t) m) = (c,CncCat ty (Yes (shareOptim opt c t)) m)
shareInfo opt (c, CncFun kxs (Yes t) m) = (c,CncFun kxs (Yes (shareOptim opt c t)) m)
shareInfo opt (c, ResOper ty (Yes t)) = (c,ResOper ty (Yes (shareOptim opt c t)))
shareInfo _ i = i
shareInfo :: OptSpec -> (Ident, Info) -> Info
shareInfo opt (c, CncCat ty (Yes t) m) = CncCat ty (Yes (shareOptim opt c t)) m
shareInfo opt (c, CncFun kxs (Yes t) m) = CncFun kxs (Yes (shareOptim opt c t)) m
shareInfo opt (c, ResOper ty (Yes t)) = ResOper ty (Yes (shareOptim opt c t))
shareInfo _ (_,i) = i
-- the function putting together optimizations
shareOptim :: OptSpec -> Ident -> Term -> Term