@@ -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,47 @@ 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-200 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+ seedDeps :: DepSet
170+ seedDeps = M.unionsWith S.union [ds | (cond, ds) <- IM.elems numbered, S.null cond]
171+
172+ toNumbered :: Deps -> IntMap Constraint
173+ toNumbered = IM.fromList . zip [0..] . M.toList
174+
175+ fromNumbered :: IntMap Constraint -> Deps
176+ fromNumbered = IM.foldr addConstraint M.empty
177+ where
178+ addConstraint (ns, vs) = M.insertWith (M.unionWith S.union) ns vs
179+
180+ index :: IntMap Constraint -> Map Node IntSet
181+ index = IM.foldrWithKey (
182+ -- for each clause (i. ns --> _ds)
183+ \i (ns, _ds) ix -> foldr (
184+ -- for each node `n` in `ns`
185+ \n ix' -> M.insertWith IS.union n (IS.singleton i) ix'
186+ ) ix (S.toList ns)
187+ ) M.empty
188+
152189 gather :: DepSet -> (Set Name, UseMap)
153190 gather = foldr ins (S.empty, M.empty) . M.toList
154191 where
@@ -156,17 +193,58 @@ minimalUsage = second gather . forwardChain
156193 ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
157194 ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
158195
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)
196+forwardChain
197+ :: Map Node IntSet
198+ -> DepSet
199+ -> DepSet
200+ -> IntMap Constraint
201+ -> (IntMap Constraint, DepSet)
202+forwardChain index solution previouslyNew constrs
203+ | M.null currentlyNew
204+ = (constrs, solution)
205+
206+ | otherwise
207+ = forwardChain index
208+ (M.unionWith S.union solution currentlyNew)
209+ currentlyNew
210+ constrs'
165211 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)
212+ -- which constraints could give new results,
213+ -- given that `previouslyNew` has been derived in the last iteration
214+ affectedIxs = IS.unions [
215+ M.findWithDefault IS.empty n index
216+ | n <- M.keys previouslyNew
217+ ]
218+
219+ -- traverse all (potentially) affected constraints, building:
220+ -- 1. a set of newly reached nodes
221+ -- 2. updated set of constraints where the previously
222+ -- reached nodes have been removed
223+ (currentlyNew, constrs')
224+ = IS.foldr
225+ (reduceConstraint $ M.keysSet previouslyNew)
226+ (M.empty, constrs)
227+ affectedIxs
228+
229+ reduceConstraint
230+ :: Set Node
231+ -> Int
232+ -> (DepSet, IntMap (Cond, DepSet))
233+ -> (DepSet, IntMap (Cond, DepSet))
234+ reduceConstraint previouslyNew i (news, clauses)
235+ | Just (cond, deps) <- IM.lookup i clauses
236+ = case cond S.\\ previouslyNew of
237+ cond'
238+ | S.null cond'
239+ -> (M.unionWith S.union news deps, IM.delete i clauses)
240+
241+ | S.size cond' < S.size cond
242+ -> (news, IM.insert i (cond', deps) clauses)
243+
244+ | otherwise
245+ -> (news, clauses)
246+
247+ | otherwise = (news, clauses)
170248
171249-- | Build the dependency graph, starting the depth-first search from
172250-- a list of Names.