on master help sign in
Report unbound variables in erasure.
commitbd58d80a4c7aefe25df072e89d7e6c08bb526e46 authorMatus Tejiscak <ziman@functor.sk> dateFri 31 Jan 2014, 11:04 (13 years ago) parent99d5a0a
1 file changed+6−2
src/Idris/Erasure.hs+6−2
src/Idris/Erasure.hs+6−2
@@ -145,7 +145,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
145145
146146 -- the variables that arose as function arguments only depend on (n, i)
147147 varMap = M.fromList [(v, S.singleton (fn, Arg i)) | (v,i) <- zip vars [0..]]
148− (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
148+ (vars, sc) = cases_runtime cdefs
149+ -- we use cases_runtime in order to have case-blocks
150+ -- resolved to top-level functions before our analysis
149151
150152 etaExpand :: [Name] -> Term -> Term
151153 etaExpand [] t = t
@@ -163,8 +165,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
163165 getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps
164166 getDepsAlt fn es vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
165167 getDepsAlt fn es vs var (ConstCase c sc) = getDepsSC fn es vs sc
166− getDepsAlt fn es vs var (SucCase n sc) = getDepsSC fn es vs sc -- deps for S can be hardcoded if needed
167168 getDepsAlt fn es vs var (DefaultCase sc) = getDepsSC fn es vs sc
169+ getDepsAlt fn es vs var (SucCase n sc)
170+ = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased
168171 getDepsAlt fn es vs var (ConCase n cnt ns sc)
169172 = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
170173 where
@@ -178,6 +181,7 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
178181 -- named variables introduce dependencies as described in `vs'
179182 getDepsTerm vs bs cd (P _ n _)
180183 | Just var <- M.lookup n vs = M.singleton cd var -- found among local variables
184+ | MN _ _ <- n = error $ "variable " ++ show n ++ " unbound in " ++ show cd
181185 | otherwise = M.singleton cd (S.singleton (n, Result)) -- assumed to be a global reference
182186
183187 -- dependencies of de bruijn variables are described in `bs'