@@ -30,145 +30,105 @@ import Data.IntMap (IntMap)
3030-- UseMap maps names to the set of used (reachable) argument positions.
3131type UseMap = Map Name IntSet
3232
33−-- DepMap maps functions (only functions) to their Deps.
34−type DepMap = Map Name Deps
35−
3633type Node = (Name, Int)
37−type FlatMap = Map Node (Set (Ctors, Cond))
38−
39−-- Deps of a function is a map from argument index
40−-- to all usages of the argument, including conditions
41−-- and which constructor fields the particular usage touched.
42−type Deps = IntMap (Set (Ctors, Cond))
34+type Deps = Map Cond (Set Node)
4335
4436-- "Condition" is the conjunction
4537-- of elementary assumptions along the path from the root.
4638-- Elementary assumption (f, i) means that "function f uses the argument i".
47−type Cond = Set (Name, Int)
48−
49−-- "Ctors" is the set of pairs (ctor_name, arg_no) saying
50−-- which constructor fields have been accessed to obtain the variable.
51−type Ctors = Set (Name, Int)
39+type Cond = Set Node
5240
53−-- Variables used in terms.
54−type Var = Cond -> Deps
41+-- Every variable draws in certain dependencies.
42+type Var = Set Node
5543type Vars = Map Name Var
5644
57−-- Variables passing the pattern-matches before being used in terms.
58−type PatVar = Ctors -> Var
59−type PatVars = Map Name PatVar
60−
6145-- Find the minimal consistent usage by forward chaining.
62−minimalUsage :: DepMap -> UseMap
63−minimalUsage dmap = gather reachable
46+minimalUsage :: Deps -> UseMap
47+minimalUsage = gather . forwardChain
6448 where
65− flatten :: DepMap -> FlatMap
66− flatten dmap = M.fromList $ concat [[((n,i), ccs) | (i, ccs) <- IM.toList deps] | (n, deps) <- M.toList dmap]
67−
6849 gather :: Ord a => Set (a, Int) -> Map a IntSet
6950 gather = foldr (\(n,i) -> M.insertWith IS.union n (IS.singleton i)) M.empty . S.toList
7051
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)
52+forwardChain :: Deps -> Set Node
53+forwardChain deps
54+ | Just trivials <- M.lookup S.empty deps
55+ = trivials `S.union` forwardChain (remove trivials deps)
56+ | otherwise = S.empty
8157 where
82− -- Remove the given nodes from the FlatMap entirely, including from Conds,
58+ -- Remove the given nodes from the Deps entirely,
8359 -- 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
90−
91− trivials :: Set Node
92− trivials = S.fromList . map fst . filter isTrivial . M.toList $ dmap
93−
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
97− where
98− trivialConds :: Set (Ctors, Cond)
99− trivialConds = S.filter (S.null . snd) alts
60+ remove :: Set Node -> Deps -> Deps
61+ remove ns = M.mapKeysWith S.union (S.\\ ns)
10062
10163-- Build the dependency graph,
10264-- starting the depth-first search from a list of Names.
103−buildDepMap :: Context -> [Name] -> DepMap
104−buildDepMap ctx ns = dfs M.empty ns
65+buildDepMap :: Context -> [Name] -> Deps
66+buildDepMap ctx ns = dfs S.empty M.empty ns
10567 where
10668 -- perform depth-first search
10769 -- to discover all the names used in the program
10870 -- and call getDeps for every name
109− dfs :: DepMap -> [Name] -> DepMap
110− dfs dmap [] = dmap
111− dfs dmap (n : ns)
112− | n `M.member` dmap = dfs dmap ns
113− | otherwise = dfs (M.insert n deps dmap) ns
71+ dfs :: Set Name -> Deps -> [Name] -> Deps
72+ dfs visited deps [] = deps
73+ dfs visited deps (n : ns)
74+ | n `S.member` visited = dfs visited deps ns
75+ | otherwise = dfs (S.insert n visited) (M.unionWith S.union (getDeps n) deps) (next ++ ns)
11476 where
115− next = [n | n <- S.toList depn, n `M.notMember` dmap]
116− depn = S.delete n (depNames deps)
77+ next = [n | n <- S.toList depn, n `S.notMember` visited]
78+ depn = S.delete n $ depNames deps
11779 deps = getDeps n
11880
11981 -- extract all names that a function depends on
12082 -- from the Deps of the function
12183 depNames :: Deps -> Set Name
122− depNames = S.unions . map (S.unions . map f . S.toList) . IM.elems
123− where
124− f :: (Ctors, Cond) -> Set Name
125− f (ctors, cond) = S.map fst cond -- let's ignore ctors for now
84+ depNames = S.unions . map (S.map fst) . M.keys
12685
12786 -- get Deps for a Name
12887 getDeps :: Name -> Deps
12988 getDeps n = case lookupDef n ctx of
130− [def] -> getDepsDef def
89+ [def] -> getDepsDef n def
13190 [] -> error $ "erasure checker: unknown name: " ++ show n
13291 _ -> error $ "erasure checker: ambiguous name: " ++ show n
13392
134− getDepsDef :: Def -> Deps
135− getDepsDef (Function ty t) = error "a function encountered" -- TODO
136− getDepsDef (TyDecl ty t) = IM.empty
137− getDepsDef (Operator ty n f) = IM.empty
138− getDepsDef (CaseOp ci ty tys def tot cdefs)
93+ getDepsDef :: Name -> Def -> Deps
94+ getDepsDef n (Function ty t) = error "a function encountered" -- TODO
95+ getDepsDef n (TyDecl ty t) = M.empty
96+ getDepsDef n (Operator ty n' f) = M.empty
97+ getDepsDef n (CaseOp ci ty tys def tot cdefs)
13998 = getDepsSC varMap sc
14099 where
141− pvar i cs cd = IM.singleton i (S.singleton (cs, cd))
142− varMap = M.fromList [(v, pvar i) | (v,i) <- zip vars [0..]]
100+ -- the variables that arose as function arguments only depend on (n, i)
101+ varMap = M.fromList [(v, S.singleton (n,i)) | (v,i) <- zip vars [0..]]
143102 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
144103
145− getDepsSC :: PatVars -> SC -> Deps
146− getDepsSC vs ImpossibleCase = IM.empty
147− getDepsSC vs (UnmatchedCase msg) = IM.empty
104+ getDepsSC :: Vars -> SC -> Deps
105+ getDepsSC vs ImpossibleCase = M.empty
106+ getDepsSC vs (UnmatchedCase msg) = M.empty
148107 getDepsSC vs (ProjCase t alt) = error "ProjCase not supported"
149− getDepsSC vs (STerm t) = getDepsTerm (M.map ($ S.empty) vs) [] S.empty t
150− getDepsSC vs (Case n alts) = unionMap (getDepsAlt vs pvar) alts
108+ getDepsSC vs (STerm t) = getDepsTerm vs [] S.empty t
109+ getDepsSC vs (Case n alts) = unionMap (getDepsAlt vs var) alts
151110 where
152− pvar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
153−
154− getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
155− getDepsAlt vs pv (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
156− getDepsAlt vs pv (ConstCase c sc) = getDepsSC vs sc
157− getDepsAlt vs pv (SucCase n sc) = getDepsSC vs sc -- deps for S can be hardcoded if needed
158− getDepsAlt vs pv (DefaultCase sc) = getDepsSC vs sc
159− getDepsAlt vs pv (ConCase n cnt ns sc)
111+ var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
112+
113+ getDepsAlt :: Vars -> Var -> CaseAlt -> Deps
114+ getDepsAlt vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
115+ getDepsAlt vs var (ConstCase c sc) = getDepsSC vs sc
116+ getDepsAlt vs var (SucCase n sc) = getDepsSC vs sc -- deps for S can be hardcoded if needed
117+ getDepsAlt vs var (DefaultCase sc) = getDepsSC vs sc
118+ getDepsAlt vs var (ConCase n cnt ns sc)
160119 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
161120 where
121+ -- Here we insert dependencies that arose from pattern matching on a constructor.
162122 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
163− vs' = M.fromList [(v, pv . S.insert (n,j)) | (v,j) <- zip ns [0..]]
123+ vs' = M.fromList [(v, S.insert (n,j) var) | (v,j) <- zip ns [0..]]
164124
165125 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
166− getDepsTerm :: Vars -> [Var] -> Cond -> Term -> Deps
126+ getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
167127
168128 -- named variables introduce dependencies as described in `vs'
169129 getDepsTerm vs bs cd (P _ n _)
170− | Just var <- M.lookup n vs = var cd
171− | otherwise = IM.empty
130+ | Just var <- M.lookup n vs = M.singleton cd var -- this condition gives rise to these dependencies
131+ | otherwise = M.empty
172132
173133 -- dependencies of de bruijn variables are described in `bs'
174134 getDepsTerm vs bs cd (V i) = (bs !! i) cd
@@ -176,15 +136,15 @@ buildDepMap ctx ns = dfs M.empty ns
176136 getDepsTerm vs bs cd (Bind n bdr t)
177137 -- here we just push IM.empty on the de bruijn stack
178138 -- the args will be marked as used at the usage site
179− | Lam ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
180− | Pi ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
139+ | Lam ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t
140+ | Pi ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t
181141
182142 -- let-bound variables can get partially evaluated
183143 -- it is sufficient just to plug the Cond in when the bound names are used
184− | Let ty v <- bdr = getDepsTerm (M.insert n (var v) vs) (var v : bs) cd t
185− | NLet ty v <- bdr = getDepsTerm (M.insert n (var v) vs) (var v : bs) cd t
144+ | Let ty t <- bdr = getDepsTerm vs (var t : bs) cd t
145+ | NLet ty t <- bdr = getDepsTerm vs (var t : bs) cd t
186146 where
187− var v cd = getDepsTerm vs bs cd v
147+ var t cd = getDepsTerm vs bs cd t
188148
189149 -- applications may add items to Cond
190150 getDepsTerm vs bs cd app@(App _ _)
@@ -200,13 +160,13 @@ buildDepMap ctx ns = dfs M.empty ns
200160 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
201161
202162 -- the easy cases
203− getDepsTerm vs bs cd (Constant _) = IM.empty
204− getDepsTerm vs bs cd Erased = IM.empty
205− getDepsTerm vs bs cd Impossible = IM.empty
206− getDepsTerm vs bs cd (TType _) = IM.empty
163+ getDepsTerm vs bs cd (Constant _) = M.empty
164+ getDepsTerm vs bs cd (TType _) = M.empty
165+ getDepsTerm vs bs cd Erased = M.empty
166+ getDepsTerm vs bs cd Impossible = M.empty
207167
208168 unions :: [Deps] -> Deps
209− unions = IM.unionsWith S.union
169+ unions = M.unionsWith S.union
210170
211171 unionMap :: (a -> Deps) -> [a] -> Deps
212172 unionMap f = unions . map f