git.iko.soy/Idris-dev
on master help sign in
Run erasure analysis even when not compiling.
commitdfb26635324316333b4d6d62dba35d7c66094d69 authorMatus Tejiscak <ziman@functor.sk> dateTue 11 Feb 2014, 15:37 (13 years ago) parent72b473d
3 files changed+45−32
compare with master
unifiedsplit
src/IRTS/Compiler.hs+1−25 src/Idris/Erasure.hs+39−6 src/Idris/REPL.hs+5−1
src/IRTS/Compiler.hs+1−25
@@ -46,24 +46,7 @@ import Paths_idris
4646compile :: Codegen -> FilePath -> Term -> Idris ()
4747compile codegen f tm
4848 = do checkMVs -- check for undefined metavariables
49− -- TODO: DEBUG-ONLY, remove
50− ctx <- tt_ctxt <$> getIState
51− ci <- idris_classes <$> getIState
52− let depMap = buildDepMap ci ctx (namesUsed $ STerm tm)
53− let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
54− -- iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
55−
56− let (residDeps, (reachableNames', minUse)) = minimalUsage depMap
57− reachableNames = sUN "prim__subBigInt" : sUN "prim__addBigInt" : S.toList reachableNames'
58− iLOG $ "RESIDUAL DEPS:\n" ++ unlines (map printItem . M.toList $ residDeps)
59− iLOG $ "REACHABLE NAMES:\n" ++ unlines (map show reachableNames)
60−
61− let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
62− iLOG $ "MINIMAL USAGE:\n" ++ fmtDepMap minUse
63−
64− mapM_ (uncurry storeUsage) (M.toList minUse)
65− -- END TODO
66−
49+ reachableNames <- performUsageAnalysis
6750 maindef <- irMain tm
6851 iLOG $ "MAIN: " ++ show maindef
6952 objs <- getObjectFiles codegen
@@ -120,13 +103,6 @@ compile codegen f tm
120103 ex <- doesFileExist f
121104 if ex then return f else return h
122105
123−storeUsage :: Name -> IntSet -> Idris ()
124−storeUsage n args = do
125− cg <- idris_callgraph <$> getIState
126− case lookupCtxt n cg of
127− [x] -> addToCG n x{ usedpos = IS.toList args }
128− _ -> addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors
129−
130106irMain :: TT Name -> Idris LDecl
131107irMain tm = do i <- ir tm
132108 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
src/Idris/Erasure.hs+39−6
@@ -1,9 +1,6 @@
11{-# LANGUAGE PatternGuards #-}
22
3−module Idris.Erasure
4− ( buildDepMap
5− , minimalUsage
6− ) where
3+module Idris.Erasure (performUsageAnalysis) where
74
85import Idris.AbsSyntax
96import Idris.Core.CaseTree
@@ -51,6 +48,42 @@ type Cond = Set Node
5148type Var = Set Node
5249type Vars = Map Name Var
5350
51+-- Perform usage analysis, write the relevant information in the internal
52+-- structures, returning the list of reachable names.
53+performUsageAnalysis :: Idris [Name]
54+performUsageAnalysis = do
55+ ctx <- tt_ctxt <$> getIState
56+ ci <- idris_classes <$> getIState
57+
58+ -- Build the dependency graph.
59+ let depMap = buildDepMap ci ctx (sNS (sUN "main") ["Main"])
60+
61+ -- Search for reachable nodes in the graph.
62+ let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
63+
64+ -- Print some debug info.
65+ logLvl 3 $ "Reachable names:\n" ++ unlines (map show . S.toList $ reachableNames)
66+ logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap minUse
67+ logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)
68+
69+ -- Store the usage info in the internal state.
70+ mapM_ storeUsage . M.toList $ minUse
71+
72+ return $ S.toList reachableNames
73+ where
74+ fmtItem :: (Cond, Set Node) -> String
75+ fmtItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
76+
77+ fmtUseMap :: UseMap -> String
78+ fmtUseMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
79+
80+ storeUsage :: (Name, IntSet) -> Idris ()
81+ storeUsage (n, args) = do
82+ cg <- idris_callgraph <$> getIState
83+ case lookupCtxt n cg of
84+ [x] -> addToCG n x{ usedpos = IS.toList args } -- functions
85+ _ -> addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors
86+
5487-- Find the minimal consistent usage by forward chaining.
5588minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
5689minimalUsage = second gather . forwardChain
@@ -75,8 +108,8 @@ forwardChain deps
75108
76109-- Build the dependency graph,
77110-- starting the depth-first search from a list of Names.
78−buildDepMap :: Ctxt ClassInfo -> Context -> [Name] -> Deps
79−buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
111+buildDepMap :: Ctxt ClassInfo -> Context -> Name -> Deps
112+buildDepMap ci ctx rootName = addPostulates $ dfs S.empty M.empty [rootName]
80113 where
81114 -- mark the result of Main.main as used with the empty assumption
82115 addPostulates :: Deps -> Deps
src/Idris/REPL.hs+5−1
@@ -1353,9 +1353,13 @@ idrisMain opts =
13531353
13541354 ok <- noErrors
13551355 when ok $ case output of
1356− [] -> return ()
1356+ -- just do the checks
1357+ [] -> performUsageAnalysis >> return ()
1358+
1359+ -- the compiler will run usage analysis itself
13571360 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
13581361 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1362+
13591363 case script of
13601364 Nothing -> return ()
13611365 Just expr -> execScript expr