@@ -3,7 +3,6 @@
33module Idris.Erasure
44 ( findUnusedArgs
55 , findUsed
6− , buildDepGraph
76 ) where
87
98import Idris.AbsSyntax
@@ -26,26 +25,42 @@ import Data.IntSet (IntSet)
2625import Data.Map (Map)
2726import Data.IntMap (IntMap)
2827
29−{- The whole idea of usage analysis is as follows:
30− -
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
34− -}
35−
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
39−
40−-- DepGraph maps a (Name, Arg) to (Name, Arg)'s that it depends upon.
41−type DepGraph = Map Name (Map Arg (Set (Name, Arg)))
42−
4328-- UseMap maps names to the set of used (reachable) argument positions.
4429type UseMap = Map Name IntSet
4530
46−-- PatvarMap maps pattern variable names to the corresponding (data-ctor-name, argpos).
47−type PatvarMap = Map Name (Name, Int)
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.
34+data Dep = Dep
35+ -- Effect
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.
39+
40+ -- Condition
41+ , depGuards :: Set (Name, Int) -- | All these arguments must be marked as used.
42+ }
43+ deriving (Eq, Ord, Show)
44+
45+-- DepMap maps function names to their sets of dependencies.
46+type DepMap = Map Name (Set Dep)
4847
48+findUsed :: Context -> Ctxt CGInfo -> [Name] -> UseMap
49+findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
50+ where
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
56+
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
62+
63+{-
4964buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
5065buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
5166 where
@@ -67,7 +82,7 @@ buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
6782 findDepsDef cg fn (Operator ty n f) = M.empty
6883 -- ^- non-pattern-matching definitions don't contribute to dependencies
6984
70− findDepsDef cg fn (CaseOp ci ty def tot cdefs)
85+ findDepsDef cg fn (CaseOp ci ty tys def tot cdefs)
7186 -- the fst component is the list of pattern variables, which we don't use
7287 = findDepsSC cg fn M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
7388
@@ -85,13 +100,18 @@ buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
85100 findDepsAlt cg fn vars (DefaultCase sc) = findDepsSC cg fn vars sc
86101 findDepsAlt cg fn vars (ConCase n cnt ns sc) = findDepsSC cg fn (ns `u` vars) sc
87102 where
103+ -- constructor name `n' is passed implicitly
88104 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
106+
107+ -- where do we introduce the dependency
108+ -- f x = x
109+ -- (f, Result) -> (f, 0) ?
90110
91111 findDepsTerm :: Ctxt CGInfo -> PatvarMap -> (Name, Arg) -> Term -> DepGraph
92112 findDepsTerm cg vars (tn,ta) (P _ n _) = tn ~> ta ~> case M.lookup n vars of
93− Just v -> S.singleton v -- an existing patvar
94− Nothing -> (n, Retval) -- must be the return value of something from the context
113+ Just vs -> vs -- an existing patvar
114+ Nothing -> S.singleton (n, Retval) -- must be the return value of something from the context
95115 findDepsTerm cg vars (tn,ta) (Bind n (Let t v) body) = union
96116 [ findDepsTerm cg vars (tn,ta) (instantiate v body)
97117 , findDepsTerm cg vars (tn,ta) t
@@ -166,6 +186,7 @@ findUsed ctx cg = unionMap $ findUsedDef cg . getDef ctx
166186 _ -> []
167187 in S.unions [findUsedTerm cg arg | (i,arg) <- zip [0..] args, i `notElem` unused]
168188 findUsedTerm cg _ = S.empty
189+-}
169190
170191findUnusedArgs :: [Name] -> Idris ()
171192findUnusedArgs names = do