@@ -30,145 +30,105 @@ import Data.IntMap (IntMap)
30-- UseMap maps names to the set of used (reachable) argument positions.
30-- UseMap maps names to the set of used (reachable) argument positions.
31type UseMap = Map Name IntSet
31type UseMap = Map Name IntSet
33−-- DepMap maps functions (only functions) to their Deps.
34−type DepMap = Map Name Deps
36type Node = (Name, Int)
33type Node = (Name, Int)
37−type FlatMap = Map Node (Set (Ctors, Cond))
34+type Deps = Map Cond (Set Node)
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))
44-- "Condition" is the conjunction
36-- "Condition" is the conjunction
45-- of elementary assumptions along the path from the root.
37-- of elementary assumptions along the path from the root.
46-- Elementary assumption (f, i) means that "function f uses the argument i".
38-- Elementary assumption (f, i) means that "function f uses the argument i".
47−type Cond = Set (Name, Int)
39+type Cond = Set Node
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)
53−-- Variables used in terms.
41+-- Every variable draws in certain dependencies.
54−type Var = Cond -> Deps
42+type Var = Set Node
55type Vars = Map Name Var
43type Vars = Map Name Var
57−-- Variables passing the pattern-matches before being used in terms.
58−type PatVar = Ctors -> Var
59−type PatVars = Map Name PatVar
61-- Find the minimal consistent usage by forward chaining.
45-- Find the minimal consistent usage by forward chaining.
62−minimalUsage :: DepMap -> UseMap
46+minimalUsage :: Deps -> UseMap
63−minimalUsage dmap = gather reachable
47+minimalUsage = gather . forwardChain
65− flatten :: DepMap -> FlatMap
66− flatten dmap = M.fromList $ concat [[((n,i), ccs) | (i, ccs) <- IM.toList deps] | (n, deps) <- M.toList dmap]
68 gather :: Ord a => Set (a, Int) -> Map a IntSet
49 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
50 gather = foldr (\(n,i) -> M.insertWith IS.union n (IS.singleton i)) M.empty . S.toList
71− reachable :: Set Node
72− reachable = forwardChain $ flatten dmap
52+forwardChain :: Deps -> Set Node
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)
77−forwardChain :: FlatMap -> Set Node
78−forwardChain dmap
53+forwardChain deps
79− | S.null trivials = S.empty
54+ | Just trivials <- M.lookup S.empty deps
80− | otherwise = trivials `S.union` forwardChain (remove trivials dmap)
55+ = trivials `S.union` forwardChain (remove trivials deps)
56+ | otherwise = S.empty
82− -- Remove the given nodes from the FlatMap entirely, including from Conds,
58+ -- Remove the given nodes from the Deps entirely,
83 -- possibly creating new empty Conds.
59 -- possibly creating new empty Conds.
84− remove :: Set Node -> FlatMap -> FlatMap
60+ remove :: Set Node -> Deps -> Deps
85− remove ns = M.mapMaybeWithKey rm
61+ remove ns = M.mapKeysWith S.union (S.\\ ns)
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
92− trivials = S.fromList . map fst . filter isTrivial . M.toList $ dmap
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
98− trivialConds :: Set (Ctors, Cond)
99− trivialConds = S.filter (S.null . snd) alts
101-- Build the dependency graph,
63-- Build the dependency graph,
102-- starting the depth-first search from a list of Names.
64-- starting the depth-first search from a list of Names.
103−buildDepMap :: Context -> [Name] -> DepMap
65+buildDepMap :: Context -> [Name] -> Deps
104−buildDepMap ctx ns = dfs M.empty ns
66+buildDepMap ctx ns = dfs S.empty M.empty ns
106 -- perform depth-first search
68 -- perform depth-first search
107 -- to discover all the names used in the program
69 -- to discover all the names used in the program
108 -- and call getDeps for every name
70 -- and call getDeps for every name
109− dfs :: DepMap -> [Name] -> DepMap
71+ dfs :: Set Name -> Deps -> [Name] -> Deps
110− dfs dmap [] = dmap
72+ dfs visited deps [] = deps
111− dfs dmap (n : ns)
73+ dfs visited deps (n : ns)
112− | n `M.member` dmap = dfs dmap ns
74+ | n `S.member` visited = dfs visited deps ns
113− | otherwise = dfs (M.insert n deps dmap) ns
75+ | otherwise = dfs (S.insert n visited) (M.unionWith S.union (getDeps n) deps) (next ++ ns)
115− next = [n | n <- S.toList depn, n `M.notMember` dmap]
77+ next = [n | n <- S.toList depn, n `S.notMember` visited]
116− depn = S.delete n (depNames deps)
78+ depn = S.delete n $ depNames deps
117 deps = getDeps n
79 deps = getDeps n
119 -- extract all names that a function depends on
81 -- extract all names that a function depends on
120 -- from the Deps of the function
82 -- from the Deps of the function
121 depNames :: Deps -> Set Name
83 depNames :: Deps -> Set Name
122− depNames = S.unions . map (S.unions . map f . S.toList) . IM.elems
84+ depNames = S.unions . map (S.map fst) . M.keys
124− f :: (Ctors, Cond) -> Set Name
125− f (ctors, cond) = S.map fst cond -- let's ignore ctors for now
127 -- get Deps for a Name
86 -- get Deps for a Name
128 getDeps :: Name -> Deps
87 getDeps :: Name -> Deps
129 getDeps n = case lookupDef n ctx of
88 getDeps n = case lookupDef n ctx of
130− [def] -> getDepsDef def
89+ [def] -> getDepsDef n def
131 [] -> error $ "erasure checker: unknown name: " ++ show n
90 [] -> error $ "erasure checker: unknown name: " ++ show n
132 _ -> error $ "erasure checker: ambiguous name: " ++ show n
91 _ -> error $ "erasure checker: ambiguous name: " ++ show n
134− getDepsDef :: Def -> Deps
93+ getDepsDef :: Name -> Def -> Deps
135− getDepsDef (Function ty t) = error "a function encountered" -- TODO
94+ getDepsDef n (Function ty t) = error "a function encountered" -- TODO
136− getDepsDef (TyDecl ty t) = IM.empty
95+ getDepsDef n (TyDecl ty t) = M.empty
137− getDepsDef (Operator ty n f) = IM.empty
96+ getDepsDef n (Operator ty n' f) = M.empty
138− getDepsDef (CaseOp ci ty tys def tot cdefs)
97+ getDepsDef n (CaseOp ci ty tys def tot cdefs)
139 = getDepsSC varMap sc
98 = getDepsSC varMap sc
141− pvar i cs cd = IM.singleton i (S.singleton (cs, cd))
100+ -- the variables that arose as function arguments only depend on (n, i)
142− varMap = M.fromList [(v, pvar i) | (v,i) <- zip vars [0..]]
101+ varMap = M.fromList [(v, S.singleton (n,i)) | (v,i) <- zip vars [0..]]
143 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
102 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
145− getDepsSC :: PatVars -> SC -> Deps
104+ getDepsSC :: Vars -> SC -> Deps
146− getDepsSC vs ImpossibleCase = IM.empty
105+ getDepsSC vs ImpossibleCase = M.empty
147− getDepsSC vs (UnmatchedCase msg) = IM.empty
106+ getDepsSC vs (UnmatchedCase msg) = M.empty
148 getDepsSC vs (ProjCase t alt) = error "ProjCase not supported"
107 getDepsSC vs (ProjCase t alt) = error "ProjCase not supported"
149− getDepsSC vs (STerm t) = getDepsTerm (M.map ($ S.empty) vs) [] S.empty t
108+ getDepsSC vs (STerm t) = getDepsTerm vs [] S.empty t
150− getDepsSC vs (Case n alts) = unionMap (getDepsAlt vs pvar) alts
109+ getDepsSC vs (Case n alts) = unionMap (getDepsAlt vs var) alts
152− pvar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
111+ var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
154− getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
113+ getDepsAlt :: Vars -> Var -> CaseAlt -> Deps
155− getDepsAlt vs pv (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
114+ getDepsAlt vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
156− getDepsAlt vs pv (ConstCase c sc) = getDepsSC vs sc
115+ getDepsAlt vs var (ConstCase c sc) = getDepsSC vs sc
157− getDepsAlt vs pv (SucCase n sc) = getDepsSC vs sc -- deps for S can be hardcoded if needed
116+ getDepsAlt vs var (SucCase n sc) = getDepsSC vs sc -- deps for S can be hardcoded if needed
158− getDepsAlt vs pv (DefaultCase sc) = getDepsSC vs sc
117+ getDepsAlt vs var (DefaultCase sc) = getDepsSC vs sc
159− getDepsAlt vs pv (ConCase n cnt ns sc)
118+ getDepsAlt vs var (ConCase n cnt ns sc)
160 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
119 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
121+ -- Here we insert dependencies that arose from pattern matching on a constructor.
162 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
122 -- 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..]]
165 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
125 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
166− getDepsTerm :: Vars -> [Var] -> Cond -> Term -> Deps
126+ getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
168 -- named variables introduce dependencies as described in `vs'
128 -- named variables introduce dependencies as described in `vs'
169 getDepsTerm vs bs cd (P _ n _)
129 getDepsTerm vs bs cd (P _ n _)
170− | Just var <- M.lookup n vs = var cd
130+ | Just var <- M.lookup n vs = M.singleton cd var -- this condition gives rise to these dependencies
171− | otherwise = IM.empty
131+ | otherwise = M.empty
173 -- dependencies of de bruijn variables are described in `bs'
133 -- dependencies of de bruijn variables are described in `bs'
174 getDepsTerm vs bs cd (V i) = (bs !! i) cd
134 getDepsTerm vs bs cd (V i) = (bs !! i) cd
@@ -176,15 +136,15 @@ buildDepMap ctx ns = dfs M.empty ns
176 getDepsTerm vs bs cd (Bind n bdr t)
136 getDepsTerm vs bs cd (Bind n bdr t)
177 -- here we just push IM.empty on the de bruijn stack
137 -- here we just push IM.empty on the de bruijn stack
178 -- the args will be marked as used at the usage site
138 -- the args will be marked as used at the usage site
179− | Lam ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
139+ | Lam ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t
180− | Pi ty <- bdr = getDepsTerm vs (const IM.empty : bs) cd t
140+ | Pi ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t
182 -- let-bound variables can get partially evaluated
142 -- let-bound variables can get partially evaluated
183 -- it is sufficient just to plug the Cond in when the bound names are used
143 -- 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
144+ | Let ty t <- bdr = getDepsTerm vs (var t : bs) cd t
185− | NLet ty v <- bdr = getDepsTerm (M.insert n (var v) vs) (var v : bs) cd t
145+ | NLet ty t <- bdr = getDepsTerm vs (var t : bs) cd t
187− var v cd = getDepsTerm vs bs cd v
147+ var t cd = getDepsTerm vs bs cd t
189 -- applications may add items to Cond
149 -- applications may add items to Cond
190 getDepsTerm vs bs cd app@(App _ _)
150 getDepsTerm vs bs cd app@(App _ _)
@@ -200,13 +160,13 @@ buildDepMap ctx ns = dfs M.empty ns
200 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
160 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
202 -- the easy cases
162 -- the easy cases
203− getDepsTerm vs bs cd (Constant _) = IM.empty
163+ getDepsTerm vs bs cd (Constant _) = M.empty
204− getDepsTerm vs bs cd Erased = IM.empty
164+ getDepsTerm vs bs cd (TType _) = M.empty
165+ getDepsTerm vs bs cd Erased = M.empty
205− getDepsTerm vs bs cd Impossible = IM.empty
166+ getDepsTerm vs bs cd Impossible = M.empty
206− getDepsTerm vs bs cd (TType _) = IM.empty
208 unions :: [Deps] -> Deps
168 unions :: [Deps] -> Deps
209− unions = IM.unionsWith S.union
169+ unions = M.unionsWith S.union
211 unionMap :: (a -> Deps) -> [a] -> Deps
171 unionMap :: (a -> Deps) -> [a] -> Deps
212 unionMap f = unions . map f
172 unionMap f = unions . map f