@@ -29,7 +29,7 @@ import Data.Text (pack)
2929import qualified Data.Text as T
3030
3131-- UseMap maps names to the set of used (reachable) argument positions.
32−type UseMap = Map Name IntSet
32+type UseMap = Map Name (IntMap (Set Reason))
3333
3434data Arg = Arg !Int | Result deriving (Eq, Ord)
3535
@@ -38,7 +38,11 @@ instance Show Arg where
3838 show Result = "*"
3939
4040type Node = (Name, Arg)
41−type Deps = Map Cond (Set Node)
41+type Deps = Map Cond DepSet
42+type Reason = (Name, Int) -- function name, argument index
43+
44+-- Nodes along with sets of reasons for every one.
45+type DepSet = Map Node (Set Reason)
4246
4347-- "Condition" is the conjunction
4448-- of elementary assumptions along the path from the root.
@@ -46,7 +50,7 @@ type Deps = Map Cond (Set Node)
4650type Cond = Set Node
4751
4852-- Every variable draws in certain dependencies.
49−type Var = Set Node
53+type Var = DepSet
5054type Vars = Map Name Var
5155
5256-- Perform usage analysis, write the relevant information in the internal
@@ -85,49 +89,55 @@ performUsageAnalysis = do
8589 mainName = sNS (sUN "main") ["Main"]
8690 indent = (" " ++)
8791
88− fmtItem :: (Cond, Set Node) -> String
89− fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (S.toList deps)
92+ fmtItem :: (Cond, DepSet) -> String
93+ fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (M.toList deps)
9094
91− fmtUseMap :: [(Name, IntSet)] -> String
92− fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ show (IS.toList is))
95+ fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
96+ fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ show (IM.toList is))
9397
94− storeUsage :: Ctxt CGInfo -> (Name, IntSet) -> Idris ()
98+ storeUsage :: Ctxt CGInfo -> (Name, IntMap (Set Reason)) -> Idris ()
9599 storeUsage cg (n, args)
96100 | [x] <- lookupCtxt n cg
97− = addToCG n x{ usedpos = IS.toList args } -- functions
101+ = addToCG n x{ usedpos = flat } -- functions
98102
99103 | otherwise
100− = addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors
104+ = addToCG n (CGInfo [] [] [] [] flat) -- data ctors
105+ where
106+ flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]
101107
102− checkAccessibility :: Ctxt OptInfo -> (Name, IntSet) -> Idris ()
108+ checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
103109 checkAccessibility opt (n, reachable)
104110 | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt
105− , eargs@(_:_) <- [show n | (i,n) <- inaccessible, i `IS.member` reachable]
106− = ifail $ show n ++ ": inaccessible arguments reachable: " ++ intercalate ", " eargs
111+ , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]
112+ = ifail $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs
107113
108114 | otherwise = return ()
115+ where
116+ fmt n [] = show n ++ " (no more information available)"
117+ fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]
109118
110119-- Find the minimal consistent usage by forward chaining.
111120minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
112121minimalUsage = second gather . forwardChain
113122 where
114− gather :: Set (Name, Arg) -> (Set Name, UseMap)
115− gather = foldr ins (S.empty, M.empty) . S.toList
123+ gather :: DepSet -> (Set Name, UseMap)
124+ gather = foldr ins (S.empty, M.empty) . M.toList
116125 where
117− ins :: Node -> (Set Name, UseMap) -> (Set Name, UseMap)
118− ins (n, Result) (ns, umap) = (S.insert n ns, umap)
119− ins (n, Arg i ) (ns, umap) = (ns, M.insertWith IS.union n (IS.singleton i) umap)
126+ ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
127+ ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
128+ ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
120129
121−forwardChain :: Deps -> (Deps, Set Node)
130+forwardChain :: Deps -> (Deps, DepSet)
122131forwardChain deps
123132 | Just trivials <- M.lookup S.empty deps
124− = (trivials `S.union`) `second` forwardChain (remove trivials . M.delete S.empty $ deps)
125− | otherwise = (deps, S.empty)
133+ = (M.unionWith S.union trivials)
134+ `second` forwardChain (remove trivials . M.delete S.empty $ deps)
135+ | otherwise = (deps, M.empty)
126136 where
127137 -- Remove the given nodes from the Deps entirely,
128138 -- possibly creating new empty Conds.
129− remove :: Set Node -> Deps -> Deps
130− remove ns = M.mapKeysWith S.union (S.\\ ns)
139+ remove :: DepSet -> Deps -> Deps
140+ remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)
131141
132142-- Build the dependency graph,
133143-- starting the depth-first search from a list of Names.
@@ -136,10 +146,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
136146 where
137147 -- mark the result of Main.main as used with the empty assumption
138148 addPostulates :: Deps -> Deps
139− addPostulates deps = foldr (\(ds, rs) -> M.insertWith S.union ds rs) deps postulates
149+ addPostulates deps = foldr (\(ds, rs) -> M.insertWith (M.unionWith S.union) ds rs) deps postulates
140150 where
141151 -- mini-DSL for postulates
142− (==>) ds rs = (S.fromList ds, S.fromList rs)
152+ (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])
143153 it n is = [(sUN n, Arg i) | i <- is]
144154 mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
145155
@@ -178,7 +188,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
178188 dfs visited deps [] = deps
179189 dfs visited deps (n : ns)
180190 | n `S.member` visited = dfs visited deps ns
181− | otherwise = dfs (S.insert n visited) (M.unionWith S.union deps' deps) (next ++ ns)
191+ | otherwise = dfs (S.insert n visited) (M.unionWith (M.unionWith S.union) deps' deps) (next ++ ns)
182192 where
183193 next = [n | n <- S.toList depn, n `S.notMember` visited]
184194 depn = S.delete n $ allNames deps'
@@ -189,7 +199,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
189199 allNames :: Deps -> Set Name
190200 allNames = S.unions . map names . M.toList
191201 where
192− names (cs, ns) = S.map fst cs `S.union` S.map fst ns
202+ names (cs, ns) = S.map fst cs `S.union` S.map fst (M.keysSet ns)
193203
194204 -- get Deps for a Name
195205 getDeps :: Name -> Deps
@@ -203,17 +213,19 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
203213 getDepsDef fn (TyDecl ty t) = M.empty
204214 getDepsDef fn (Operator ty n' f) = M.empty -- TODO: what's this?
205215 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
206− = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
216+ = getDepsSC fn etaVars (etaMap `union` varMap) sc
207217 where
218+ union = M.unionWith (M.unionWith S.union)
219+
208220 -- we must eta-expand the definition with fresh variables
209221 -- to capture these dependencies as well
210222 etaIdx = [length vars .. length tys - 1]
211223 etaVars = [eta i | i <- etaIdx]
212− etaMap = M.fromList [(eta i, S.singleton (fn, Arg i)) | i <- etaIdx]
224+ etaMap = M.fromList [(eta i, M.singleton (fn, Arg i) S.empty) | i <- etaIdx]
213225 eta i = MN i (pack "eta")
214226
215227 -- the variables that arose as function arguments only depend on (n, i)
216− varMap = M.fromList [(v, S.singleton (fn, Arg i)) | (v,i) <- zip vars [0..]]
228+ varMap = M.fromList [(v, M.singleton (fn, Arg i) S.empty) | (v,i) <- zip vars [0..]]
217229 (vars, sc) = cases_runtime cdefs
218230 -- we use cases_runtime in order to have case-blocks
219231 -- resolved to top-level functions before our analysis
@@ -234,9 +246,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
234246 -- that the result of this function is used at all
235247 = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree
236248 where
249+
237250 addTagDep = case alts of
238251 [_] -> id -- single branch, tag not used
239− _ -> M.insertWith S.union (S.singleton (fn, Result)) casedVar -- more case branches
252+ _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) casedVar
240253 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
241254
242255 getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps
@@ -246,11 +259,16 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
246259 getDepsAlt fn es vs var (SucCase n sc)
247260 = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased
248261 getDepsAlt fn es vs var (ConCase n cnt ns sc)
249− = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
262+ = getDepsSC fn es (vs' `union` vs) sc -- left-biased union
250263 where
264+ union = M.unionWith (M.unionWith S.union)
265+
251266 -- Here we insert dependencies that arose from pattern matching on a constructor.
252267 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
253− vs' = M.fromList [(v, S.insert (n, Arg j) var) | (v,j) <- zip ns [0..]]
268+ vs' = M.fromList [(v, M.insertWith S.union (n, Arg j) (S.singleton (fn, varIdx)) var) | (v,j) <- zip ns [0..]]
269+
270+ -- hack: get the index of the variable from its content
271+ varIdx = head [i | (n, Arg i) <- M.keys var, n == fn]
254272
255273 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
256274 getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
@@ -267,7 +285,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
267285 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
268286
269287 -- assumed to be a global reference
270− | otherwise = M.singleton cd (S.singleton (n, Result))
288+ | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)
271289 where
272290 specialMNs = [sMN 0 "__Unit", sMN 0 "__True", sMN 0 "__False"]
273291
@@ -312,7 +330,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
312330 -> node n args -- depends on whether the referred thing uses its argument
313331
314332 -- TODO: could we somehow infer how bound variables use their arguments?
315− V i -> M.unionWith S.union ((bs !! i) cd) (unconditionalDeps args)
333+ V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)
316334
317335 -- we interpret applied lambdas as lets in order to reuse code here
318336 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
@@ -325,7 +343,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
325343 -- the following code marks them as completely used
326344 Proj (P Ref n@(SN (InstanceN className parms)) _) i
327345 | [CI ctorName ms ds dscs ps is] <- lookupCtxt className ci
328− -> S.fromList [(ctorName, Arg i), (n, Result)]
346+ -> M.fromList [((ctorName, Arg i), S.empty), ((n, Result), S.empty)]
329347 `ins` unconditionalDeps args
330348
331349 Proj t i
@@ -335,11 +353,11 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
335353
336354 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args
337355 where
338− ins = M.insertWith S.union cd
356+ ins = M.insertWith (M.unionWith S.union) cd
339357 unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args
340358
341359 node :: Name -> [Term] -> Deps
342− node n = ins (S.singleton (n, Result)) . unionMap (getDepsArgs n) . zip indices
360+ node n = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices
343361 where
344362 indices = map Just [0 .. getArity n - 1] ++ repeat Nothing
345363 getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional
@@ -373,7 +391,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
373391 lamToLet [] t = t
374392
375393 unions :: [Deps] -> Deps
376− unions = M.unionsWith S.union
394+ unions = M.unionsWith (M.unionWith S.union)
377395
378396 unionMap :: (a -> Deps) -> [a] -> Deps
379− unionMap f = unions . map f
397+ unionMap f = M.unionsWith (M.unionWith S.union) . map f