git.iko.soy/Idris-dev
on master help sign in
getDepsTerm covers all cases.
0a71ea2Matus Tejiscak
src/Idris/Erasure.hs+8−4
compare with master
unifiedsplit
@@ -84,9 +84,9 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
84
84
85 getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
85 getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
86 getDepsAlt vs pv (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
86 getDepsAlt vs pv (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
87− getDepsAlt vs pv (ConstCase c sc) = IM.empty
87+ getDepsAlt vs pv (ConstCase c sc) = getDepsSC vs sc
88− getDepsAlt vs pv (SucCase n sc) = error "a SucCase encountered"
88+ getDepsAlt vs pv (SucCase n sc) = getDepsSC vs sc -- deps for S can be hardcoded if needed
89− getDepsAlt vs pv (DefaultCase sc) = error $ "a DefaultCase encountered: " ++ show (DefaultCase sc)
89+ getDepsAlt vs pv (DefaultCase sc) = getDepsSC vs sc
90 getDepsAlt vs pv (ConCase n cnt ns sc)
90 getDepsAlt vs pv (ConCase n cnt ns sc)
91 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
91 = getDepsSC (vs' `M.union` vs) sc -- left-biased union
92 where
92 where
@@ -130,7 +130,11 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
130 where
130 where
131 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
131 called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
132
132
133− getDepsTerm _ _ _ t = error $ "getDepsTerm: unrecognised term: " ++ show t
133+ -- the easy cases
134+ getDepsTerm vs bs cd (Constant _) = IM.empty
135+ getDepsTerm vs bs cd Erased = IM.empty
136+ getDepsTerm vs bs cd Impossible = IM.empty
137+ getDepsTerm vs bs cd (TType _) = IM.empty
134
138
135{-
139{-
136data TT n = P NameType n (TT n) -- ^ named references
140data TT n = P NameType n (TT n) -- ^ named references