on master help sign in
Fix deps arising from case-splitting.
commit279d19204e7e1a341660b265eef5e0e1f82ce160 authorMatus Tejiscak <ziman@functor.sk> dateFri 31 Jan 2014, 20:30 (13 years ago) parent8c7af47
1 file changed+5−2
src/Idris/Erasure.hs+5−2
src/Idris/Erasure.hs+5−2
@@ -164,9 +164,12 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
164164 getDepsSC fn es vs (UnmatchedCase msg) = M.empty
165165 getDepsSC fn es vs (ProjCase t alt) = error "ProjCase not supported"
166166 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)
167− getDepsSC fn es vs (Case n alts) = unionMap (getDepsAlt fn es vs var) alts
167+ getDepsSC fn es vs (Case n alts)
168+ -- we case-split on this variable, which necessarily marks it as used
169+ = M.map (S.union casedVar) -- add the usage to all effects
170+ $ unionMap (getDepsAlt fn es vs casedVar) alts -- in the whole subtree
168171 where
169− var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
172+ casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
170173
171174 getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps
172175 getDepsAlt fn es vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?