cfb968c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Extend application analysis.

cfb968cMatus Tejiscak13 years ago

src/Idris/Erasure.hs+5

@@ -244,6 +244,9 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns

244 | otherwise

245 -> node n args -- depends on whether the referred thing uses its argument

246

247+ -- TODO: could we somehow infer how bound variables use their arguments?

248+ V i -> M.unionWith S.union ((bs !! i) cd) (unconditionalDeps args)

249+

247 -- we interpret applied lambdas as lets in order to reuse code here

250 -- we interpret applied lambdas as lets in order to reuse code here

248 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

251 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

249

252

@@ -261,6 +264,8 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns

261 Proj t i

264 Proj t i

262 -> error $ "cannot analyse projection !" ++ show i ++ " of " ++ show t

265 -> error $ "cannot analyse projection !" ++ show i ++ " of " ++ show t

263

266

267+ Erased -> M.empty

268+

264 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

269 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

265 where

270 where

266 ins = M.insertWith S.union cd

271 ins = M.insertWith S.union cd