@@ -146,7 +146,7 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
146 getDepsDef :: Name -> Def -> Deps
146 getDepsDef :: Name -> Def -> Deps
147 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
147 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
148 getDepsDef fn (TyDecl ty t) = M.empty
148 getDepsDef fn (TyDecl ty t) = M.empty
149− getDepsDef fn (Operator ty n' f) = M.empty
149+ getDepsDef fn (Operator ty n' f) = M.empty -- TODO: what's this?
150 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
150 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
151 = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
151 = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
@@ -207,13 +207,13 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
208 -- sanity check: machine-generated names shouldn't occur at top-level
208 -- sanity check: machine-generated names shouldn't occur at top-level
209 | MN _ _ <- n
209 | MN _ _ <- n
210− , show n `notElem` specialMNs
210+ , n `notElem` specialMNs
211 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
211 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
213 -- assumed to be a global reference
213 -- assumed to be a global reference
214 | otherwise = M.singleton cd (S.singleton (n, Result))
214 | otherwise = M.singleton cd (S.singleton (n, Result))
216− specialMNs = words "{__Unit0} {__False0} {__True0}"
216+ specialMNs = [sMN 0 "__Unit", sMN 0 "__True", sMN 0 "__False"]
218 -- dependencies of de bruijn variables are described in `bs'
218 -- dependencies of de bruijn variables are described in `bs'
219 getDepsTerm vs bs cd (V i) = (bs !! i) cd
219 getDepsTerm vs bs cd (V i) = (bs !! i) cd