@@ -1,6 +1,6 @@
11{-|
22Module : Idris.Erasure
3−Description : Utilities to erase irrelevant stuff.
3+Description : Utilities to erase stuff not necessary for runtime.
44Copyright :
55License : BSD3
66Maintainer : The Idris Community.
@@ -145,10 +145,54 @@ performUsageAnalysis startNames = do
145145 fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]
146146 warn = logErasure 0
147147
148+type Constraint = (Cond, DepSet)
149+
148150-- | Find the minimal consistent usage by forward chaining.
151+--
152+-- We use a cleverer implementation that:
153+-- 1. First transforms Deps into a collection of numbered constraints
154+-- 2. For each node, we remember the numbers of constraints
155+-- that contain that node among their preconditions.
156+-- 3. When performing forward chaining, we perform unit propagation
157+-- only on the relevant constraints, not all constraints.
158+--
159+-- Typical numbers from the current version of Blodwen:
160+-- * 56 iterations until fixpoint
161+-- * out of 20k constraints total, 5-1000 are relevant per iteration
149162minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
150−minimalUsage = second gather . forwardChain
163+minimalUsage deps
164+ = fromNumbered *** gather
165+ $ forwardChain (index numbered) seedDeps seedDeps numbered
151166 where
167+ numbered = toNumbered deps
168+
169+ -- The initial solution. Consists of nodes that are
170+ -- reachable immediately, without any preconditions.
171+ seedDeps :: DepSet
172+ seedDeps = M.unionsWith S.union [ds | (cond, ds) <- IM.elems numbered, S.null cond]
173+
174+ toNumbered :: Deps -> IntMap Constraint
175+ toNumbered = IM.fromList . zip [0..] . M.toList
176+
177+ fromNumbered :: IntMap Constraint -> Deps
178+ fromNumbered = IM.foldr addConstraint M.empty
179+ where
180+ addConstraint (ns, vs) = M.insertWith (M.unionWith S.union) ns vs
181+
182+ -- Build an index that maps every node to the set of constraints
183+ -- where the node appears among the preconditions.
184+ index :: IntMap Constraint -> Map Node IntSet
185+ index = IM.foldrWithKey (
186+ -- for each clause (i. ns --> _ds)
187+ \i (ns, _ds) ix -> foldr (
188+ -- for each node `n` in `ns`
189+ \n ix' -> M.insertWith IS.union n (IS.singleton i) ix'
190+ ) ix (S.toList ns)
191+ ) M.empty
192+
193+ -- Convert a solution of constraints into:
194+ -- 1. the list of names used in the program
195+ -- 2. the list of arguments used, together with their reasons
152196 gather :: DepSet -> (Set Name, UseMap)
153197 gather = foldr ins (S.empty, M.empty) . M.toList
154198 where
@@ -156,17 +200,81 @@ minimalUsage = second gather . forwardChain
156200 ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
157201 ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
158202
159−forwardChain :: Deps -> (Deps, DepSet)
160−forwardChain deps
161− | Just trivials <- M.lookup S.empty deps
162− = (M.unionWith S.union trivials)
163− `second` forwardChain (remove trivials . M.delete S.empty $ deps)
164− | otherwise = (deps, M.empty)
203+-- | In each iteration, we find the set of nodes immediately reachable
204+-- from the current set of constraints, and then reduce the set of constraints
205+-- based on that knowledge.
206+--
207+-- In the implementation, this is phase-shifted. We first reduce the set
208+-- of constraints, given the newly reachable nodes from the previous iteration,
209+-- and then compute the set of currently reachable nodes.
210+-- Then we decide whether to iterate further.
211+forwardChain
212+ :: Map Node IntSet -- ^ node index
213+ -> DepSet -- ^ all reachable nodes found so far
214+ -> DepSet -- ^ nodes reached in the previous iteration
215+ -> IntMap Constraint -- ^ numbered constraints
216+ -> (IntMap Constraint, DepSet)
217+forwardChain index solution previouslyNew constrs
218+ -- no newly reachable nodes, fixed point has been reached
219+ | M.null currentlyNew
220+ = (constrs, solution)
221+
222+ -- some newly reachable nodes, iterate more
223+ | otherwise
224+ = forwardChain index
225+ (M.unionWith S.union solution currentlyNew)
226+ currentlyNew
227+ constrs'
165228 where
166− -- Remove the given nodes from the Deps entirely,
167− -- possibly creating new empty Conds.
168− remove :: DepSet -> Deps -> Deps
169− remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)
229+ -- which constraints could give new results,
230+ -- given that `previouslyNew` has been derived in the last iteration
231+ affectedIxs = IS.unions [
232+ M.findWithDefault IS.empty n index
233+ | n <- M.keys previouslyNew
234+ ]
235+
236+ -- traverse all (potentially) affected constraints, building:
237+ -- 1. a set of newly reached nodes
238+ -- 2. updated set of constraints where the previously
239+ -- reached nodes have been removed
240+ (currentlyNew, constrs')
241+ = IS.foldr
242+ (reduceConstraint $ M.keysSet previouslyNew)
243+ (M.empty, constrs)
244+ affectedIxs
245+
246+ -- Update the pair (newly reached nodes, numbered constraint set)
247+ -- by reducing the constraint with the given number.
248+ reduceConstraint
249+ :: Set Node -- ^ nodes reached in the previous iteration
250+ -> Int -- ^ constraint number
251+ -> (DepSet, IntMap (Cond, DepSet))
252+ -> (DepSet, IntMap (Cond, DepSet))
253+ reduceConstraint previouslyNew i (news, constrs)
254+ | Just (cond, deps) <- IM.lookup i constrs
255+ = case cond S.\\ previouslyNew of
256+ cond'
257+ -- This constraint's set of preconditions has shrunk
258+ -- to the empty set. We can add its RHS to the set of newly
259+ -- reached nodes, and remove the constraint altogether.
260+ | S.null cond'
261+ -> (M.unionWith S.union news deps, IM.delete i constrs)
262+
263+ -- This constraint's set of preconditions has shrunk
264+ -- so we need to overwrite the numbered slot
265+ -- with the updated constraint.
266+ | S.size cond' < S.size cond
267+ -> (news, IM.insert i (cond', deps) constrs)
268+
269+ -- This constraint's set of preconditions hasn't changed
270+ -- so we do not do anything about it.
271+ | otherwise
272+ -> (news, constrs)
273+
274+ -- Constraint number present in index but not found
275+ -- among the constraints. This happens more and more frequently
276+ -- as we delete constraints from the set.
277+ | otherwise = (news, constrs)
170278
171279-- | Build the dependency graph, starting the depth-first search from
172280-- a list of Names.