git.iko.soy/Idris-dev
on master help sign in
Also account for called references.
a92914bMatus Tejiscak
src/IRTS/Compiler.hs+2
compare with master
unifiedsplit
@@ -58,6 +58,8 @@ compile codegen f tm
58
58
59 let minUse = minimalUsage depMap
59 let minUse = minimalUsage depMap
60 iLOG $ "MINIMAL USAGE:\n" ++ unlines (map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) $ M.toList minUse)
60 iLOG $ "MINIMAL USAGE:\n" ++ unlines (map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) $ M.toList minUse)
61+
62+ iLOG $ "MAIN:\n" ++ show tm
61 -- END TODO
63 -- END TODO
62
64
63 maindef <- irMain tm
65 maindef <- irMain tm
src/Idris/Erasure.hs+30−5
@@ -12,6 +12,7 @@ import Idris.Core.TT
12import Idris.Core.Evaluate
12import Idris.Core.Evaluate
13
13
14import Debug.Trace
14import Debug.Trace
15+import System.IO.Unsafe
15
16
16import Control.Arrow
17import Control.Arrow
17import Control.Applicative
18import Control.Applicative
@@ -67,6 +68,8 @@ forwardChain deps
67
68
68 | Just trivials <- M.lookup S.empty deps
69 | Just trivials <- M.lookup S.empty deps
69 = trivials `S.union` forwardChain (remove trivials . M.delete S.empty $ deps)
70 = trivials `S.union` forwardChain (remove trivials . M.delete S.empty $ deps)
71+
72+ | unsafePerformIO prn `seq` False = undefined
70 | otherwise = S.empty
73 | otherwise = S.empty
71 where
74 where
72 -- Remove the given nodes from the Deps entirely,
75 -- Remove the given nodes from the Deps entirely,
@@ -74,6 +77,11 @@ forwardChain deps
74 remove :: Set Node -> Deps -> Deps
77 remove :: Set Node -> Deps -> Deps
75 remove ns = M.mapKeysWith S.union (S.\\ ns)
78 remove ns = M.mapKeysWith S.union (S.\\ ns)
76
79
80+ printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
81+ prn = do
82+ putStrLn $ "SINGLES:\n" ++ unlines (map show . filter ((==1) . S.size) $ M.keys deps)
83+ putStrLn $ "USAGE SUB-ANALYSIS:\n" ++ unlines (map printItem . M.toList $ deps)
84+
77-- Build the dependency graph,
85-- Build the dependency graph,
78-- starting the depth-first search from a list of Names.
86-- starting the depth-first search from a list of Names.
79buildDepMap :: Context -> [Name] -> Deps
87buildDepMap :: Context -> [Name] -> Deps
@@ -83,10 +91,23 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
83 addPostulates :: Deps -> Deps
91 addPostulates :: Deps -> Deps
84 addPostulates deps = foldr (\(ds, rs) -> M.insertWith S.union ds rs) deps postulates
92 addPostulates deps = foldr (\(ds, rs) -> M.insertWith S.union ds rs) deps postulates
85 where
93 where
94+ -- mini-DSL for postulates
86 (==>) ds rs = (S.fromList ds, S.fromList rs)
95 (==>) ds rs = (S.fromList ds, S.fromList rs)
87 (.:) ms n = NS (UN $ pack n) (map pack ms)
96 (.:) ms n = NS (UN $ pack n) (map pack ms)
97+ name = UN . pack
98+
88 postulates =
99 postulates =
89− [ [] ==> [(["Main"] .: "main", Result)]
100+ [ [] ==>
101+ [ (["Main"] .: "main", Result) -- These two, Main.main and run__IO, are always evaluated
102+ , (name "run__IO", Result) -- but evade analysis since they come from the seed term.
103+ , (name "prim__believe_me", Arg 2)
104+ , (name "prim__strCons", Arg 0)
105+ , (name "prim__strCons", Arg 1)
106+ , (name "prim__strHead", Arg 0)
107+ , (name "prim__strTail", Arg 0)
108+ , (name "mkForeignPrim", Arg 2)
109+-- , (name "MkIO", Arg 1)
110+ ]
90 ]
111 ]
91
112
92 -- perform depth-first search
113 -- perform depth-first search
@@ -179,12 +200,16 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
179 P Ref n _ -> node n args
200 P Ref n _ -> node n args
180 P (DCon _ _) n _ -> node n args
201 P (DCon _ _) n _ -> node n args
181
202
182− -- these do not
203+ -- this does not
183 P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
204 P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
205+
206+ -- a bound variable might draw in additional dependencies,
207+ -- think: f x = x 0 <-- here, `x' _is_ used
184− P Bound n _ -> unionMap (getDepsTerm vs bs cd) args
208+ P Bound n _ -> var n `ins` unionMap (getDepsTerm vs bs cd) args
185 where
209 where
186− node n = M.insertWith S.union cd (S.singleton (n, Result))
210+ ins = M.insertWith S.union cd
211+ var n = fromMaybe (error $ "non-existent bound variable: " ++ show n) (M.lookup n vs)
187− . unionMap (getDepsArgs n) . zip [0..]
212+ node n = ins (S.singleton (n, Result)) . unionMap (getDepsArgs n) . zip [0..]
188 getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t
213 getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t
189
214
190 -- the easy cases
215 -- the easy cases