git.iko.soy/Idris-dev
on master help sign in
Also print residual deps.
8c7af47Matus Tejiscak
src/IRTS/Compiler.hs+6−3
compare with master
unifiedsplit
@@ -52,10 +52,11 @@ compile codegen f tm
52 ctx <- tt_ctxt <$> getIState
52 ctx <- tt_ctxt <$> getIState
53 let depMap = buildDepMap ctx used
53 let depMap = buildDepMap ctx used
54 let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
54 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)
56
56
57− let (reachableNames', minUse) = minimalUsage depMap
57+ let (residDeps, (reachableNames', minUse)) = minimalUsage depMap
58 reachableNames = sUN "prim__subBigInt" : sUN "prim__addBigInt" : S.toList reachableNames'
58 reachableNames = sUN "prim__subBigInt" : sUN "prim__addBigInt" : S.toList reachableNames'
59+ iLOG $ "RESIDUAL DEPS:\n" ++ unlines (map printItem . M.toList $ residDeps)
59 iLOG $ "REACHABLE NAMES: " ++ show reachableNames
60 iLOG $ "REACHABLE NAMES: " ++ show reachableNames
60
61
61 let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
62 let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
@@ -274,7 +275,9 @@ instance ToIR (TT Name) where
274 _ -> [] -- TODO: is this correct?
275 _ -> [] -- TODO: is this correct?
275 if collapse
276 if collapse
276 then return LNothing
277 then return LNothing
278+ else do
279+ iLOG $ "ERASE:\n " ++ show tm ++ "\n ==>\n " ++ show (LApp False (LV (Glob n)) (mkUsed used 0 args'))
277− else return (LApp False (LV (Glob n))
280+ return (LApp False (LV (Glob n))
278 (mkUsed used 0 args'))
281 (mkUsed used 0 args'))
279 | (f, args) <- unApply tm
282 | (f, args) <- unApply tm
280 = do f' <- ir' env f
283 = do f' <- ir' env f
src/Idris/Erasure.hs+25−9
@@ -49,8 +49,8 @@ type Var = Set Node
49type Vars = Map Name Var
49type Vars = Map Name Var
50
50
51-- Find the minimal consistent usage by forward chaining.
51-- Find the minimal consistent usage by forward chaining.
52−minimalUsage :: Deps -> (Set Name, UseMap)
52+minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
53−minimalUsage = gather . forwardChain
53+minimalUsage = second gather . forwardChain
54 where
54 where
55 gather :: Set (Name, Arg) -> (Set Name, UseMap)
55 gather :: Set (Name, Arg) -> (Set Name, UseMap)
56 gather = foldr ins (S.empty, M.empty) . S.toList
56 gather = foldr ins (S.empty, M.empty) . S.toList
@@ -59,11 +59,11 @@ minimalUsage = gather . forwardChain
59 ins (n, Result) (ns, umap) = (S.insert n ns, umap)
59 ins (n, Result) (ns, umap) = (S.insert n ns, umap)
60 ins (n, Arg i ) (ns, umap) = (ns, M.insertWith IS.union n (IS.singleton i) umap)
60 ins (n, Arg i ) (ns, umap) = (ns, M.insertWith IS.union n (IS.singleton i) umap)
61
61
62−forwardChain :: Deps -> Set Node
62+forwardChain :: Deps -> (Deps, Set Node)
63forwardChain deps
63forwardChain deps
64 | Just trivials <- M.lookup S.empty deps
64 | Just trivials <- M.lookup S.empty deps
65− = trivials `S.union` forwardChain (remove trivials . M.delete S.empty $ deps)
65+ = (trivials `S.union`) `second` forwardChain (remove trivials . M.delete S.empty $ deps)
66− | otherwise = S.empty
66+ | otherwise = (deps, S.empty)
67 where
67 where
68 -- Remove the given nodes from the Deps entirely,
68 -- Remove the given nodes from the Deps entirely,
69 -- possibly creating new empty Conds.
69 -- possibly creating new empty Conds.
@@ -81,8 +81,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
81 where
81 where
82 -- mini-DSL for postulates
82 -- mini-DSL for postulates
83 (==>) ds rs = (S.fromList ds, S.fromList rs)
83 (==>) 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)
85 it n is = [(UN $ pack n, Arg i) | i <- is]
85 it n is = [(UN $ pack n, Arg i) | i <- is]
86+ mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
86
87
87 postulates =
88 postulates =
88 [ [] ==> concat
89 [ [] ==> concat
@@ -98,7 +99,12 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
98 , it "mkForeign" [1]
99 , it "mkForeign" [1]
99 , it "prim__toStrBigInt" [0]
100 , it "prim__toStrBigInt" [0]
100 , it "prim__addBigInt" [0,1]
101 , it "prim__addBigInt" [0,1]
102+ , it "prim__sextInt_BigInt" [0]
101 , it "prim__zextInt_BigInt" [0]
103 , 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]
102 ]
108 ]
103 ]
109 ]
104
110
@@ -180,9 +186,19 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
180
186
181 -- named variables introduce dependencies as described in `vs'
187 -- named variables introduce dependencies as described in `vs'
182 getDepsTerm vs bs cd (P _ n _)
188 getDepsTerm vs bs cd (P _ n _)
189+ -- local variables
183− | Just var <- M.lookup n vs = M.singleton cd var -- found among 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
184− | MN _ _ <- n = error $ "variable " ++ show n ++ " unbound in " ++ show cd
196+ = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
197+
185− | otherwise = M.singleton cd (S.singleton (n, Result)) -- assumed to be a global reference
198+ -- assumed to be a global reference
199+ | otherwise = M.singleton cd (S.singleton (n, Result))
200+ where
201+ specialMNs = words "{__Unit0}"
186
202
187 -- dependencies of de bruijn variables are described in `bs'
203 -- dependencies of de bruijn variables are described in `bs'
188 getDepsTerm vs bs cd (V i) = (bs !! i) cd
204 getDepsTerm vs bs cd (V i) = (bs !! i) cd