238569e · Idris-dev · git.iko.soy

157

158 etaExpand :: [Name] -> Term -> Term

159 etaExpand [] t = t

160− etaExpand (n : ns) t = etaExpand ns (App t (P Bound n Erased))

160+ etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))

161

162 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps

163 getDepsSC fn es vs ImpossibleCase = M.empty

166 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)

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

169+ -- hence we add a new dependency whose only preconditions are that the result

170+ -- of this function is used at all

171+ = M.insertWith S.union (S.singleton (fn, Result)) casedVar -- add this dep to all deps

170− $ unionMap (getDepsAlt fn es vs casedVar) alts -- in the whole subtree

172+ $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

171 where

173 where

172 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)

174 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)

173

175

222 -- applications may add items to Cond

224 -- applications may add items to Cond

223 getDepsTerm vs bs cd app@(App _ _)

225 getDepsTerm vs bs cd app@(App _ _)

224 | (fun, args) <- unApply app = case fun of

226 | (fun, args) <- unApply app = case fun of

225− -- these depend on whether the referred thing uses the argument

227+ -- constructors

226− P Ref n _ -> node n args

228+ P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything

227− P (DCon _ _) n _ -> node n args

229+ P (DCon _ _) n _ -> node n args -- depends on whether (n,#) is used

228−

229− -- this does not

230− P (TCon _ _) n _ -> unconditionalDeps args

231

230

232 -- a bound variable might draw in additional dependencies,

231 -- a bound variable might draw in additional dependencies,

233 -- think: f x = x 0 <-- here, `x' _is_ used

232 -- think: f x = x 0 <-- here, `x' _is_ used

234− -- also, the arguments must be considered used

233+ P _ n _

235− -- since we don't know what's in the variable

234+ | Just var <- M.lookup n vs

236− P Bound n _ -> var n `ins` unconditionalDeps args

235+ -> var `ins` unconditionalDeps args

236+ | otherwise

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

237

238

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

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

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

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

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

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

250 where

251 where

251 ins = M.insertWith S.union cd

252 ins = M.insertWith S.union cd

252− var n = fromMaybe (error $ "non-existent bound variable: " ++ show n) (M.lookup n vs)

253 node n = ins (S.singleton (n, Result)) . unionMap (getDepsArgs n) . zip [0..]

254 getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t

255 unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args

256

257+ -- projections (= methods)

258+ getDepsTerm vs bs cd (Proj t i) | ("PROJ", t, S.toList cd) `traceShow` False = undefined

259+ getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t

260+

257 -- the easy cases

261 -- the easy cases

258− getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t

259 getDepsTerm vs bs cd (Constant _) = M.empty

262 getDepsTerm vs bs cd (Constant _) = M.empty

260 getDepsTerm vs bs cd (TType _) = M.empty

263 getDepsTerm vs bs cd (TType _) = M.empty

261 getDepsTerm vs bs cd Erased = M.empty

264 getDepsTerm vs bs cd Erased = M.empty