on master help sign in
Add comments, add version number to CHANGELOG.
0fcab91Matus Tejiscak
CHANGELOG.md+1−1
@@ -1,4 +1,4 @@
1−# New in ...
1+# New in 1.1.1
2
2
3+ Erasure analysis is now faster thanks to a bit smarter constraint solving.
3+ Erasure analysis is now faster thanks to a bit smarter constraint solving.
4
4
src/Idris/Erasure.hs+42−13
@@ -158,7 +158,7 @@ type Constraint = (Cond, DepSet)
158--
158--
159-- Typical numbers from the current version of Blodwen:
159-- Typical numbers from the current version of Blodwen:
160-- * 56 iterations until fixpoint
160-- * 56 iterations until fixpoint
161−-- * out of 20k constraints total, 5-200 are relevant per iteration
161+-- * out of 20k constraints total, 5-1000 are relevant per iteration
162minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
162minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
163minimalUsage deps
163minimalUsage deps
164 = fromNumbered *** gather
164 = fromNumbered *** gather
@@ -166,6 +166,8 @@ minimalUsage deps
166 where
166 where
167 numbered = toNumbered deps
167 numbered = toNumbered deps
168
168
169+ -- The initial solution. Consists of nodes that are
170+ -- reachable immediately, without any preconditions.
169 seedDeps :: DepSet
171 seedDeps :: DepSet
170 seedDeps = M.unionsWith S.union [ds | (cond, ds) <- IM.elems numbered, S.null cond]
172 seedDeps = M.unionsWith S.union [ds | (cond, ds) <- IM.elems numbered, S.null cond]
171
173
@@ -177,6 +179,8 @@ minimalUsage deps
177 where
179 where
178 addConstraint (ns, vs) = M.insertWith (M.unionWith S.union) ns vs
180 addConstraint (ns, vs) = M.insertWith (M.unionWith S.union) ns vs
179
181
182+ -- Build an index that maps every node to the set of constraints
183+ -- where the node appears among the preconditions.
180 index :: IntMap Constraint -> Map Node IntSet
184 index :: IntMap Constraint -> Map Node IntSet
181 index = IM.foldrWithKey (
185 index = IM.foldrWithKey (
182 -- for each clause (i. ns --> _ds)
186 -- for each clause (i. ns --> _ds)
@@ -186,6 +190,9 @@ minimalUsage deps
186 ) ix (S.toList ns)
190 ) ix (S.toList ns)
187 ) M.empty
191 ) M.empty
188
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
189 gather :: DepSet -> (Set Name, UseMap)
196 gather :: DepSet -> (Set Name, UseMap)
190 gather = foldr ins (S.empty, M.empty) . M.toList
197 gather = foldr ins (S.empty, M.empty) . M.toList
191 where
198 where
@@ -193,16 +200,25 @@ minimalUsage deps
193 ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
200 ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
194 ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
201 ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
195
202
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.
196forwardChain
210forwardChain
197− :: Map Node IntSet
211+ :: Map Node IntSet -- ^ node index
198− -> DepSet
212+ -> DepSet -- ^ all reachable nodes found so far
199− -> DepSet
213+ -> DepSet -- ^ nodes reached in the previous iteration
200− -> IntMap Constraint
214+ -> IntMap Constraint -- ^ numbered constraints
201 -> (IntMap Constraint, DepSet)
215 -> (IntMap Constraint, DepSet)
202forwardChain index solution previouslyNew constrs
216forwardChain index solution previouslyNew constrs
217+ -- no newly reachable nodes, fixed point has been reached
203 | M.null currentlyNew
218 | M.null currentlyNew
204 = (constrs, solution)
219 = (constrs, solution)
205
220
221+ -- some newly reachable nodes, iterate more
206 | otherwise
222 | otherwise
207 = forwardChain index
223 = forwardChain index
208 (M.unionWith S.union solution currentlyNew)
224 (M.unionWith S.union solution currentlyNew)
@@ -226,25 +242,38 @@ forwardChain index solution previouslyNew constrs
226 (M.empty, constrs)
242 (M.empty, constrs)
227 affectedIxs
243 affectedIxs
228
244
245+ -- Update the pair (newly reached nodes, numbered constraint set)
246+ -- by reducing the constraint with the given number.
229 reduceConstraint
247 reduceConstraint
230− :: Set Node
248+ :: Set Node -- ^ nodes reached in the previous iteration
231− -> Int
249+ -> Int -- ^ constraint number
232 -> (DepSet, IntMap (Cond, DepSet))
250 -> (DepSet, IntMap (Cond, DepSet))
233 -> (DepSet, IntMap (Cond, DepSet))
251 -> (DepSet, IntMap (Cond, DepSet))
234− reduceConstraint previouslyNew i (news, clauses)
252+ reduceConstraint previouslyNew i (news, constrs)
235− | Just (cond, deps) <- IM.lookup i clauses
253+ | Just (cond, deps) <- IM.lookup i constrs
236 = case cond S.\\ previouslyNew of
254 = case cond S.\\ previouslyNew of
237 cond'
255 cond'
256+ -- This constraint's set of preconditions has shrunk
257+ -- to the empty set. We can add its RHS to the set of newly
258+ -- reached nodes, and remove the constraint altogether.
238 | S.null cond'
259 | S.null cond'
239− -> (M.unionWith S.union news deps, IM.delete i clauses)
260+ -> (M.unionWith S.union news deps, IM.delete i constrs)
240
261
262+ -- This constraint's set of preconditions has shrunk
263+ -- so we need to overwrite the numbered slot
264+ -- with the updated constraint.
241 | S.size cond' < S.size cond
265 | S.size cond' < S.size cond
242− -> (news, IM.insert i (cond', deps) clauses)
266+ -> (news, IM.insert i (cond', deps) constrs)
243
267
268+ -- This constraint's set of preconditions hasn't changed
269+ -- so we do not do anything about it.
244 | otherwise
270 | otherwise
245− -> (news, clauses)
271+ -> (news, constrs)
246
272
273+ -- Constraint number present in index but not found
274+ -- among the constraints. This happens more and more frequently
275+ -- as we delete constraints from the set.
247− | otherwise = (news, clauses)
276+ | otherwise = (news, constrs)
248
277
249-- | Build the dependency graph, starting the depth-first search from
278-- | Build the dependency graph, starting the depth-first search from
250-- a list of Names.
279-- a list of Names.