@@ -3,6 +3,7 @@
33module Idris.Erasure
44 ( findUnusedArgs
55 , buildDepMap
6+ , minimalUsage
67 ) where
78
89import Idris.AbsSyntax
@@ -12,6 +13,7 @@ import Idris.Core.Evaluate
1213
1314import Debug.Trace
1415
16+import Control.Arrow
1517import Control.Applicative
1618import Control.Monad.State
1719import Data.Maybe
@@ -30,7 +32,9 @@ type UseMap = Map Name IntSet
3032
3133-- DepMap maps functions (only functions) to their Deps.
3234type DepMap = Map Name Deps
33−type FlatMap = Map (Name, Int) (Set (Ctors, Cond))
35+
36+type Node = (Name, Int)
37+type FlatMap = Map Node (Set (Ctors, Cond))
3438
3539-- Deps of a function is a map from argument index
3640-- to all usages of the argument, including conditions
@@ -54,21 +58,45 @@ type Vars = Map Name Var
5458type PatVar = Ctors -> Var
5559type PatVars = Map Name PatVar
5660
57−{-
5861-- Find the minimal consistent usage by forward chaining.
5962minimalUsage :: DepMap -> UseMap
60−minimalUsage dmap =
63+minimalUsage dmap = gather reachable
6164 where
6265 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
6490
65− trivials :: DepMap
66− trivials = M.mapMaybeWithKey isTrivial dmap
91+ trivials :: Set Node
92+ trivials = S.fromList . map fst . filter isTrivial . M.toList $ dmap
6793
68− isTrivial :: Name -> (Deps, Set Name) -> Maybe (Deps, Set Name)
69− isTrivial n (deps, ns)
94+ -- A node is trivially reachable if it has at least one trivial (empty) Cond.
95+ isTrivial :: (Node, Set (Ctors, Cond)) -> Bool
96+ isTrivial (node, alts) = not . S.null $ trivialConds
7097 where
71−-}
98+ trivialConds :: Set (Ctors, Cond)
99+ trivialConds = S.filter (S.null . snd) alts
72100
73101-- Build the dependency graph,
74102-- starting the depth-first search from a list of Names.