git.iko.soy/Idris-dev
on master help sign in
Run erasure analysis even when not compiling.
dfb2663Matus Tejiscak
src/IRTS/Compiler.hs+1−25
compare with master
unifiedsplit
@@ -46,24 +46,7 @@ import Paths_idris
46compile :: Codegen -> FilePath -> Term -> Idris ()
46compile :: Codegen -> FilePath -> Term -> Idris ()
47compile codegen f tm
47compile codegen f tm
48 = do checkMVs -- check for undefined metavariables
48 = do checkMVs -- check for undefined metavariables
49− -- TODO: DEBUG-ONLY, remove
49+ reachableNames <- performUsageAnalysis
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−
67 maindef <- irMain tm
50 maindef <- irMain tm
68 iLOG $ "MAIN: " ++ show maindef
51 iLOG $ "MAIN: " ++ show maindef
69 objs <- getObjectFiles codegen
52 objs <- getObjectFiles codegen
@@ -120,13 +103,6 @@ compile codegen f tm
120 ex <- doesFileExist f
103 ex <- doesFileExist f
121 if ex then return f else return h
104 if ex then return f else return h
122
105
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−
130irMain :: TT Name -> Idris LDecl
106irMain :: TT Name -> Idris LDecl
131irMain tm = do i <- ir tm
107irMain tm = do i <- ir tm
132 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
108 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
src/Idris/Erasure.hs+39−6
@@ -1,9 +1,6 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2
2
3−module Idris.Erasure
3+module Idris.Erasure (performUsageAnalysis) where
4− ( buildDepMap
5− , minimalUsage
6− ) where
7
4
8import Idris.AbsSyntax
5import Idris.AbsSyntax
9import Idris.Core.CaseTree
6import Idris.Core.CaseTree
@@ -51,6 +48,42 @@ type Cond = Set Node
51type Var = Set Node
48type Var = Set Node
52type Vars = Map Name Var
49type Vars = Map Name Var
53
50
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+
54-- Find the minimal consistent usage by forward chaining.
87-- Find the minimal consistent usage by forward chaining.
55minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
88minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
56minimalUsage = second gather . forwardChain
89minimalUsage = second gather . forwardChain
@@ -75,8 +108,8 @@ forwardChain deps
75
108
76-- Build the dependency graph,
109-- Build the dependency graph,
77-- starting the depth-first search from a list of Names.
110-- starting the depth-first search from a list of Names.
78−buildDepMap :: Ctxt ClassInfo -> Context -> [Name] -> Deps
111+buildDepMap :: Ctxt ClassInfo -> Context -> Name -> Deps
79−buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
112+buildDepMap ci ctx rootName = addPostulates $ dfs S.empty M.empty [rootName]
80 where
113 where
81 -- mark the result of Main.main as used with the empty assumption
114 -- mark the result of Main.main as used with the empty assumption
82 addPostulates :: Deps -> Deps
115 addPostulates :: Deps -> Deps
src/Idris/REPL.hs+5−1
@@ -1353,9 +1353,13 @@ idrisMain opts =
1353
1353
1354 ok <- noErrors
1354 ok <- noErrors
1355 when ok $ case output of
1355 when ok $ case output of
1356− [] -> return ()
1356+ -- just do the checks
1357+ [] -> performUsageAnalysis >> return ()
1358+
1359+ -- the compiler will run usage analysis itself
1357 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1360 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1358 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1361 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1362+
1359 case script of
1363 case script of
1360 Nothing -> return ()
1364 Nothing -> return ()
1361 Just expr -> execScript expr
1365 Just expr -> execScript expr