git.iko.soy/Idris-dev
on master help sign in
Add basic conversion to unused-map.
commitf0d787687a96c400a3cdf0b532d81c1ed467d287 authorMatus Tejiscak <ziman@functor.sk> dateMon 27 Jan 2014, 13:46 (13 years ago) parentdd7a2b2
2 files changed+24−3
compare with master
unifiedsplit
src/IRTS/Compiler.hs+8−3 src/Idris/Erasure.hs+16
src/IRTS/Compiler.hs+8−3
@@ -25,6 +25,7 @@ import Idris.Core.TT
2525import Idris.Core.Evaluate
2626import Idris.Core.CaseTree
2727
28+import Control.Applicative
2829import Control.Monad.State
2930import Data.List
3031import qualified Data.IntMap as IM
@@ -51,13 +52,17 @@ compile codegen f tm
5152 -- TODO: traverse all names correctly
5253
5354 -- TODO: DEBUG-ONLY, remove
54− ist <- getIState
55− let depMap = buildDepMap (tt_ctxt ist) used
55+ ctx <- tt_ctxt <$> getIState
56+ let depMap = buildDepMap ctx used
5657 let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
5758 iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
5859
60+ let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
5961 let minUse = minimalUsage depMap
60− iLOG $ "MINIMAL USAGE:\n" ++ unlines (map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) $ M.toList minUse)
62+ iLOG $ "MINIMAL USAGE:\n" ++ fmtDepMap minUse
63+
64+ let unusedMap = usedToUnused ctx minUse
65+ iLOG $ "UNUSED:\n" ++ fmtDepMap unusedMap
6166 -- END TODO
6267
6368 maindef <- irMain tm
src/Idris/Erasure.hs+16
@@ -4,6 +4,7 @@ module Idris.Erasure
44 ( findUnusedArgs
55 , buildDepMap
66 , minimalUsage
7+ , usedToUnused
78 ) where
89
910import Idris.AbsSyntax
@@ -49,6 +50,21 @@ type Cond = Set Node
4950type Var = Set Node
5051type Vars = Map Name Var
5152
53+-- Change the map of used args to a map of unused args.
54+usedToUnused :: Context -> UseMap -> UseMap
55+usedToUnused ctx = M.mapWithKey invert
56+ where
57+ invert :: Name -> IntSet -> IntSet
58+ invert n used = IS.fromList [0 .. arity n - 1] IS.\\ used
59+
60+ arity :: Name -> Int
61+ arity n = case lookupDef n ctx of
62+ [TyDecl (DCon tag n) t] -> n
63+ [CaseOp ci ty tys def tot cdefs] -> length tys
64+ [def] -> error $ "unsupported definition of " ++ show n ++ ": " ++ show def
65+ [] -> error $ "unknown name in conversion to unused: " ++ show n
66+ _ -> error $ "ambiguous name in conversion to unused: " ++ show n
67+
5268-- Find the minimal consistent usage by forward chaining.
5369minimalUsage :: Deps -> UseMap
5470minimalUsage = gather . forwardChain