on master help sign in
Connect erasure with analysis.
b1bef1cMatus Tejiscak
src/IRTS/Compiler.hs+10
@@ -28,6 +28,7 @@ import Idris.Core.CaseTree
28import Control.Applicative
28import Control.Applicative
29import Control.Monad.State
29import Control.Monad.State
30import Data.List
30import Data.List
31+import Data.IntSet (IntSet)
31import qualified Data.IntMap as IM
32import qualified Data.IntMap as IM
32import qualified Data.IntSet as IS
33import qualified Data.IntSet as IS
33import qualified Data.Map as M
34import qualified Data.Map as M
@@ -60,6 +61,8 @@ compile codegen f tm
60 let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
61 let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
61 let minUse = minimalUsage depMap
62 let minUse = minimalUsage depMap
62 iLOG $ "MINIMAL USAGE:\n" ++ fmtDepMap minUse
63 iLOG $ "MINIMAL USAGE:\n" ++ fmtDepMap minUse
64+
65+ mapM_ (uncurry storeUsage) (M.toList minUse)
63 -- END TODO
66 -- END TODO
64
67
65 maindef <- irMain tm
68 maindef <- irMain tm
@@ -116,6 +119,13 @@ compile codegen f tm
116 ex <- doesFileExist f
119 ex <- doesFileExist f
117 if ex then return f else return h
120 if ex then return f else return h
118
121
122+storeUsage :: Name -> IntSet -> Idris ()
123+storeUsage n args = do
124+ cg <- idris_callgraph <$> getIState
125+ case lookupCtxt n cg of
126+ [x] -> addToCG n x{ usedpos = IS.toList args }
127+ _ -> return ()
128+
119irMain :: TT Name -> Idris LDecl
129irMain :: TT Name -> Idris LDecl
120irMain tm = do i <- ir tm
130irMain tm = do i <- ir tm
121 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
131 return $ LFun [] (sMN 0 "runMain") [] (LForce i)