git.iko.soy/Idris-dev
on master help sign in
Forward chaining search implemented.
da67875Matus Tejiscak
src/IRTS/Compiler.hs+4
compare with master
unifiedsplit
@@ -28,6 +28,7 @@ import Idris.Core.CaseTree
28import Control.Monad.State
28import Control.Monad.State
29import Data.List
29import Data.List
30import qualified Data.IntMap as IM
30import qualified Data.IntMap as IM
31+import qualified Data.IntSet as IS
31import qualified Data.Map as M
32import qualified Data.Map as M
32import qualified Data.Set as S
33import qualified Data.Set as S
33import System.Process
34import System.Process
@@ -56,6 +57,9 @@ compile codegen f tm
56 let printDep (i, conds) = unlines . map (" "++) $ (show i : map printCond (S.toList conds))
57 let printDep (i, conds) = unlines . map (" "++) $ (show i : map printCond (S.toList conds))
57 let printItem (fn, deps) = unlines (show fn : map printDep (IM.toList deps))
58 let printItem (fn, deps) = unlines (show fn : map printDep (IM.toList deps))
58 iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
59 iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
60+
61+ let minUse = minimalUsage depMap
62+ iLOG $ "MINIMAL USAGE:\n" ++ unlines (map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) $ M.toList minUse)
59 -- END TODO
63 -- END TODO
60
64
61 maindef <- irMain tm
65 maindef <- irMain tm
src/Idris/Erasure.hs+37−9
@@ -3,6 +3,7 @@
3module Idris.Erasure
3module Idris.Erasure
4 ( findUnusedArgs
4 ( findUnusedArgs
5 , buildDepMap
5 , buildDepMap
6+ , minimalUsage
6 ) where
7 ) where
7
8
8import Idris.AbsSyntax
9import Idris.AbsSyntax
@@ -12,6 +13,7 @@ import Idris.Core.Evaluate
12
13
13import Debug.Trace
14import Debug.Trace
14
15
16+import Control.Arrow
15import Control.Applicative
17import Control.Applicative
16import Control.Monad.State
18import Control.Monad.State
17import Data.Maybe
19import Data.Maybe
@@ -30,7 +32,9 @@ type UseMap = Map Name IntSet
30
32
31-- DepMap maps functions (only functions) to their Deps.
33-- DepMap maps functions (only functions) to their Deps.
32type DepMap = Map Name Deps
34type DepMap = Map Name Deps
35+
36+type Node = (Name, Int)
33−type FlatMap = Map (Name, Int) (Set (Ctors, Cond))
37+type FlatMap = Map Node (Set (Ctors, Cond))
34
38
35-- Deps of a function is a map from argument index
39-- Deps of a function is a map from argument index
36-- to all usages of the argument, including conditions
40-- to all usages of the argument, including conditions
@@ -54,21 +58,45 @@ type Vars = Map Name Var
54type PatVar = Ctors -> Var
58type PatVar = Ctors -> Var
55type PatVars = Map Name PatVar
59type PatVars = Map Name PatVar
56
60
57−{-
58-- Find the minimal consistent usage by forward chaining.
61-- Find the minimal consistent usage by forward chaining.
59minimalUsage :: DepMap -> UseMap
62minimalUsage :: DepMap -> UseMap
60−minimalUsage dmap =
63+minimalUsage dmap = gather reachable
61 where
64 where
62 flatten :: DepMap -> FlatMap
65 flatten :: DepMap -> FlatMap
63− flatten
66+ flatten dmap = M.fromList $ concat [[((n,i), ccs) | (i, ccs) <- IM.toList deps] | (n, deps) <- M.toList dmap]
67+
68+ gather :: Ord a => Set (a, Int) -> Map a IntSet
69+ gather = foldr (\(n,i) -> M.insertWith IS.union n (IS.singleton i)) M.empty . S.toList
70+
71+ reachable :: Set Node
72+ reachable = forwardChain $ flatten dmap
73+
74+ -- TODO: final pass to find out the constructors
75+ -- (cannot be done on the fly because new reasons can be discovered after the rule has been triggered)
76+
77+forwardChain :: FlatMap -> Set Node
78+forwardChain dmap
79+ | S.null trivials = S.empty
80+ | otherwise = trivials `S.union` forwardChain (remove trivials dmap)
81+ where
82+ -- Remove the given nodes from the FlatMap entirely, including from Conds,
83+ -- possibly creating new empty Conds.
84+ remove :: Set Node -> FlatMap -> FlatMap
85+ remove ns = M.mapMaybeWithKey rm
86+ where
87+ rm :: Node -> Set (Ctors, Cond) -> Maybe (Set (Ctors, Cond))
88+ rm n ccs | n `S.member` ns = Nothing
89+ rm n ccs = Just $ S.map (second (S.\\ ns)) ccs
64
90
65− trivials :: DepMap
91+ trivials :: Set Node
66− trivials = M.mapMaybeWithKey isTrivial dmap
92+ trivials = S.fromList . map fst . filter isTrivial . M.toList $ dmap
67
93
68− isTrivial :: Name -> (Deps, Set Name) -> Maybe (Deps, Set Name)
94+ -- A node is trivially reachable if it has at least one trivial (empty) Cond.
69− isTrivial n (deps, ns)
95+ isTrivial :: (Node, Set (Ctors, Cond)) -> Bool
96+ isTrivial (node, alts) = not . S.null $ trivialConds
70 where
97 where
71−-}
98+ trivialConds :: Set (Ctors, Cond)
99+ trivialConds = S.filter (S.null . snd) alts
72
100
73-- Build the dependency graph,
101-- Build the dependency graph,
74-- starting the depth-first search from a list of Names.
102-- starting the depth-first search from a list of Names.