git.iko.soy/Idris-dev
on master help sign in
Also print residual deps.
commit8c7af47c830fb9270745a0238158d0dd9e50c893 authorMatus Tejiscak <ziman@functor.sk> dateFri 31 Jan 2014, 20:10 (13 years ago) parentbd58d80
2 files changed+31−12
compare with master
unifiedsplit
src/IRTS/Compiler.hs+6−3 src/Idris/Erasure.hs+25−9
src/IRTS/Compiler.hs+6−3
@@ -52,10 +52,11 @@ compile codegen f tm
5252 ctx <- tt_ctxt <$> getIState
5353 let depMap = buildDepMap ctx used
5454 let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
55− iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
55+ -- iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
5656
57− let (reachableNames', minUse) = minimalUsage depMap
57+ let (residDeps, (reachableNames', minUse)) = minimalUsage depMap
5858 reachableNames = sUN "prim__subBigInt" : sUN "prim__addBigInt" : S.toList reachableNames'
59+ iLOG $ "RESIDUAL DEPS:\n" ++ unlines (map printItem . M.toList $ residDeps)
5960 iLOG $ "REACHABLE NAMES: " ++ show reachableNames
6061
6162 let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
@@ -274,7 +275,9 @@ instance ToIR (TT Name) where
274275 _ -> [] -- TODO: is this correct?
275276 if collapse
276277 then return LNothing
277− else return (LApp False (LV (Glob n))
278+ else do
279+ iLOG $ "ERASE:\n " ++ show tm ++ "\n ==>\n " ++ show (LApp False (LV (Glob n)) (mkUsed used 0 args'))
280+ return (LApp False (LV (Glob n))
278281 (mkUsed used 0 args'))
279282 | (f, args) <- unApply tm
280283 = do f' <- ir' env f
src/Idris/Erasure.hs+25−9
@@ -49,8 +49,8 @@ type Var = Set Node
4949type Vars = Map Name Var
5050
5151-- Find the minimal consistent usage by forward chaining.
52−minimalUsage :: Deps -> (Set Name, UseMap)
53−minimalUsage = gather . forwardChain
52+minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
53+minimalUsage = second gather . forwardChain
5454 where
5555 gather :: Set (Name, Arg) -> (Set Name, UseMap)
5656 gather = foldr ins (S.empty, M.empty) . S.toList
@@ -59,11 +59,11 @@ minimalUsage = gather . forwardChain
5959 ins (n, Result) (ns, umap) = (S.insert n ns, umap)
6060 ins (n, Arg i ) (ns, umap) = (ns, M.insertWith IS.union n (IS.singleton i) umap)
6161
62−forwardChain :: Deps -> Set Node
62+forwardChain :: Deps -> (Deps, Set Node)
6363forwardChain deps
6464 | Just trivials <- M.lookup S.empty deps
65− = trivials `S.union` forwardChain (remove trivials . M.delete S.empty $ deps)
66− | otherwise = S.empty
65+ = (trivials `S.union`) `second` forwardChain (remove trivials . M.delete S.empty $ deps)
66+ | otherwise = (deps, S.empty)
6767 where
6868 -- Remove the given nodes from the Deps entirely,
6969 -- possibly creating new empty Conds.
@@ -81,8 +81,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
8181 where
8282 -- mini-DSL for postulates
8383 (==>) ds rs = (S.fromList ds, S.fromList rs)
84− (.:) ms n = NS (UN $ pack n) (map pack ms)
84+ (.:) ms n = NS (UN $ pack n) (map pack $ reverse ms)
8585 it n is = [(UN $ pack n, Arg i) | i <- is]
86+ mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
8687
8788 postulates =
8889 [ [] ==> concat
@@ -98,7 +99,12 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
9899 , it "mkForeign" [1]
99100 , it "prim__toStrBigInt" [0]
100101 , it "prim__addBigInt" [0,1]
102+ , it "prim__sextInt_BigInt" [0]
101103 , it "prim__zextInt_BigInt" [0]
104+ , it "prim__eqString" [0,1]
105+ , it "prim__eqChar" [0,1]
106+ , it "prim__eqBigInt" [0,1]
107+ , mn "__MkPair" [0,1]
102108 ]
103109 ]
104110
@@ -180,9 +186,19 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
180186
181187 -- named variables introduce dependencies as described in `vs'
182188 getDepsTerm vs bs cd (P _ n _)
183− | Just var <- M.lookup n vs = M.singleton cd var -- found among local variables
184− | MN _ _ <- n = error $ "variable " ++ show n ++ " unbound in " ++ show cd
185− | otherwise = M.singleton cd (S.singleton (n, Result)) -- assumed to be a global reference
189+ -- local variables
190+ | Just var <- M.lookup n vs
191+ = M.singleton cd var
192+
193+ -- sanity check: machine-generated names shouldn't occur at top-level
194+ | MN _ _ <- n
195+ , show n `notElem` specialMNs
196+ = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
197+
198+ -- assumed to be a global reference
199+ | otherwise = M.singleton cd (S.singleton (n, Result))
200+ where
201+ specialMNs = words "{__Unit0}"
186202
187203 -- dependencies of de bruijn variables are described in `bs'
188204 getDepsTerm vs bs cd (V i) = (bs !! i) cd