@@ -3,7 +3,6 @@
3module Idris.Erasure
3module Idris.Erasure
4 ( findUnusedArgs
4 ( findUnusedArgs
9import Idris.AbsSyntax
8import Idris.AbsSyntax
@@ -26,26 +25,42 @@ import Data.IntSet (IntSet)
26import Data.Map (Map)
25import Data.Map (Map)
27import Data.IntMap (IntMap)
26import Data.IntMap (IntMap)
29−{- The whole idea of usage analysis is as follows:
31− - 1. traverse all definitions and build a DepGraph
32− - 2. perform search of DepGraph from (main, Result)
33− - 3. record all reachable nodes into UseMap
36−-- An Arg, for the purposes of usage analysis, is either an argument
37−-- of a function or the return value of the function.
38−data Arg = Arg Int | Retval
40−-- DepGraph maps a (Name, Arg) to (Name, Arg)'s that it depends upon.
41−type DepGraph = Map Name (Map Arg (Set (Name, Arg)))
43-- UseMap maps names to the set of used (reachable) argument positions.
28-- UseMap maps names to the set of used (reachable) argument positions.
44type UseMap = Map Name IntSet
29type UseMap = Map Name IntSet
46−-- PatvarMap maps pattern variable names to the corresponding (data-ctor-name, argpos).
31+-- A dependency, potential edge in the dep graph.
32+-- Every dependency belongs to a certain Idris function.
33+-- For the effect to take place, the condition must be true.
36+ { depArg :: Int -- | This argument of the function should be marked as used.
37+ , depCtors :: Set (Name, Int) -- | These ctor fields should be marked as used.
38+ , depTags :: Set Name -- | Tags of these ADTs should be marked as used.
41+ , depGuards :: Set (Name, Int) -- | All these arguments must be marked as used.
43+ deriving (Eq, Ord, Show)
45+-- DepMap maps function names to their sets of dependencies.
47−type PatvarMap = Map Name (Name, Int)
46+type DepMap = Map Name (Set Dep)
48+findUsed :: Context -> Ctxt CGInfo -> [Name] -> UseMap
49+findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
51+ getDeps :: Name -> Set Dep
52+ getDeps n = case lookupDef n ctx of
53+ [def] -> getDepsDef def
54+ [] -> error $ "erasure checker: unknown name: " ++ show n
55+ _ -> error $ "erasure checker: ambiguous name: " ++ show n
57+ getDepsDef :: Def -> Set Dep
58+ getDepsDef (Function ty t) = S.empty
59+ getDepsDef (TyDecl ty t) = S.empty
60+ getDepsDef (Operator ty n f) = S.empty
61+ getDepsDef (CaseOp ci ty tys def tot cdefs) = S.empty
49buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
64buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
50buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
65buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
@@ -67,7 +82,7 @@ buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
67 findDepsDef cg fn (Operator ty n f) = M.empty
82 findDepsDef cg fn (Operator ty n f) = M.empty
68 -- ^- non-pattern-matching definitions don't contribute to dependencies
83 -- ^- non-pattern-matching definitions don't contribute to dependencies
70− findDepsDef cg fn (CaseOp ci ty def tot cdefs)
85+ findDepsDef cg fn (CaseOp ci ty tys def tot cdefs)
71 -- the fst component is the list of pattern variables, which we don't use
86 -- the fst component is the list of pattern variables, which we don't use
72 = findDepsSC cg fn M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
87 = findDepsSC cg fn M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
@@ -85,13 +100,18 @@ buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
85 findDepsAlt cg fn vars (DefaultCase sc) = findDepsSC cg fn vars sc
100 findDepsAlt cg fn vars (DefaultCase sc) = findDepsSC cg fn vars sc
86 findDepsAlt cg fn vars (ConCase n cnt ns sc) = findDepsSC cg fn (ns `u` vars) sc
101 findDepsAlt cg fn vars (ConCase n cnt ns sc) = findDepsSC cg fn (ns `u` vars) sc
103+ -- constructor name `n' is passed implicitly
88 u :: [Name] -> PatvarMap -> PatvarMap
104 u :: [Name] -> PatvarMap -> PatvarMap
89− vs `u` pmap = M.fromList [(var, (n, i)) | (i, var) <- zip [0..] vs] `M.union` pmap
105+ vs `u` pmap = M.fromList [(var, S.singleton (n, i)) | (i, var) <- zip [0..] vs] `M.union` pmap
107+ -- where do we introduce the dependency
109+ -- (f, Result) -> (f, 0) ?
91 findDepsTerm :: Ctxt CGInfo -> PatvarMap -> (Name, Arg) -> Term -> DepGraph
111 findDepsTerm :: Ctxt CGInfo -> PatvarMap -> (Name, Arg) -> Term -> DepGraph
92 findDepsTerm cg vars (tn,ta) (P _ n _) = tn ~> ta ~> case M.lookup n vars of
112 findDepsTerm cg vars (tn,ta) (P _ n _) = tn ~> ta ~> case M.lookup n vars of
93− Just v -> S.singleton v -- an existing patvar
113+ Just vs -> vs -- an existing patvar
94− Nothing -> (n, Retval) -- must be the return value of something from the context
114+ Nothing -> S.singleton (n, Retval) -- must be the return value of something from the context
95 findDepsTerm cg vars (tn,ta) (Bind n (Let t v) body) = union
115 findDepsTerm cg vars (tn,ta) (Bind n (Let t v) body) = union
96 [ findDepsTerm cg vars (tn,ta) (instantiate v body)
116 [ findDepsTerm cg vars (tn,ta) (instantiate v body)
97 , findDepsTerm cg vars (tn,ta) t
117 , findDepsTerm cg vars (tn,ta) t
@@ -166,6 +186,7 @@ findUsed ctx cg = unionMap $ findUsedDef cg . getDef ctx
167 in S.unions [findUsedTerm cg arg | (i,arg) <- zip [0..] args, i `notElem` unused]
187 in S.unions [findUsedTerm cg arg | (i,arg) <- zip [0..] args, i `notElem` unused]
168 findUsedTerm cg _ = S.empty
188 findUsedTerm cg _ = S.empty
170findUnusedArgs :: [Name] -> Idris ()
191findUnusedArgs :: [Name] -> Idris ()
171findUnusedArgs names = do
192findUnusedArgs names = do