on master help sign in
Some cleanup in Erasure.hs.
commit62044f7fe4d06a328d1f83083a50aae15cab2873 authorMatus Tejiscak <ziman@functor.sk> dateTue 11 Feb 2014, 09:22 (13 years ago) parente20cc53
1 file changed+3−3
src/Idris/Erasure.hs+3−3
src/Idris/Erasure.hs+3−3
@@ -146,7 +146,7 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
146146 getDepsDef :: Name -> Def -> Deps
147147 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
148148 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?
150150 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
151151 = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
152152 where
@@ -207,13 +207,13 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
207207
208208 -- sanity check: machine-generated names shouldn't occur at top-level
209209 | MN _ _ <- n
210− , show n `notElem` specialMNs
210+ , n `notElem` specialMNs
211211 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
212212
213213 -- assumed to be a global reference
214214 | otherwise = M.singleton cd (S.singleton (n, Result))
215215 where
216− specialMNs = words "{__Unit0} {__False0} {__True0}"
216+ specialMNs = [sMN 0 "__Unit", sMN 0 "__True", sMN 0 "__False"]
217217
218218 -- dependencies of de bruijn variables are described in `bs'
219219 getDepsTerm vs bs cd (V i) = (bs !! i) cd