@@ -12,6 +12,7 @@ import Idris.Core.TT
1212import Idris.Core.Evaluate
1313
1414import Debug.Trace
15+import System.IO.Unsafe
1516
1617import Control.Arrow
1718import Control.Applicative
@@ -67,6 +68,8 @@ forwardChain deps
6768
6869 | Just trivials <- M.lookup S.empty deps
6970 = trivials `S.union` forwardChain (remove trivials . M.delete S.empty $ deps)
71+
72+ | unsafePerformIO prn `seq` False = undefined
7073 | otherwise = S.empty
7174 where
7275 -- Remove the given nodes from the Deps entirely,
@@ -74,6 +77,11 @@ forwardChain deps
7477 remove :: Set Node -> Deps -> Deps
7578 remove ns = M.mapKeysWith S.union (S.\\ ns)
7679
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+
7785-- Build the dependency graph,
7886-- starting the depth-first search from a list of Names.
7987buildDepMap :: Context -> [Name] -> Deps
@@ -83,10 +91,23 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
8391 addPostulates :: Deps -> Deps
8492 addPostulates deps = foldr (\(ds, rs) -> M.insertWith S.union ds rs) deps postulates
8593 where
94+ -- mini-DSL for postulates
8695 (==>) ds rs = (S.fromList ds, S.fromList rs)
8796 (.:) ms n = NS (UN $ pack n) (map pack ms)
97+ name = UN . pack
98+
8899 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+ ]
90111 ]
91112
92113 -- perform depth-first search
@@ -179,12 +200,16 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
179200 P Ref n _ -> node n args
180201 P (DCon _ _) n _ -> node n args
181202
182− -- these do not
203+ -- this does not
183204 P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
184− P Bound 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
208+ P Bound n _ -> var n `ins` unionMap (getDepsTerm vs bs cd) args
185209 where
186− node n = M.insertWith S.union cd (S.singleton (n, Result))
187− . unionMap (getDepsArgs n) . zip [0..]
210+ ins = M.insertWith S.union cd
211+ var n = fromMaybe (error $ "non-existent bound variable: " ++ show n) (M.lookup n vs)
212+ node n = ins (S.singleton (n, Result)) . unionMap (getDepsArgs n) . zip [0..]
188213 getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t
189214
190215 -- the easy cases