ddece77 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Handle projections at least trivially.

ddece77Matus Tejiscak13 years ago

src/Idris/ElabDecls.hs+2−2

compare with master

unifiedsplit

@@ -1090,7 +1090,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

1090 let used = findUsedArgs sc' scargs'

1091 -- let scg = buildSCG i sc scargs

1092 -- add SCG later, when checking totality

1093− let cg = CGInfo scargs' calls [] used []

1093+ let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore

1094 logLvl 2 $ "Called names: " ++ show cg

1095 addToCG n cg

1096 addToCalledG n (nub (map fst calls)) -- plus names in type!

@@ -2088,7 +2088,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2088 _ -> return ps'

2089 getWParams (_ : ps) = getWParams ps

2090

2091− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2091+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2092 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2093

2094 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

src/Idris/Erasure.hs+11−4

@@ -202,11 +202,11 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns

202 P (DCon _ _) n _ -> node n args

203

204 -- this does not

205− P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args

205+ P (TCon _ _) n _ -> unconditionalDeps args

206

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

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

209− P Bound n _ -> var n `ins` unionMap (getDepsTerm vs bs cd) args

209+ P Bound n _ -> var n `ins` unconditionalDeps args

210

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

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

@@ -215,21 +215,28 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns

215 Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

216 Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

217

218− Proj t i -> error $ "cannot analyse applied projection: " ++ show t ++ " !! " ++ show i

218+ -- TODO: figure out what to do with methods

219+ -- the following code marks them as completely used

220+ Proj (P Ref inst _) i -> unconditionalDeps args -- named instances

221+ Proj _ i -> unconditionalDeps args -- dictionary reference in a variable

219

222

220− _ -> error $ "cannot analyse application of: " ++ show fun

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

221 where

224 where

222 ins = M.insertWith S.union cd

225 ins = M.insertWith S.union cd

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

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

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

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

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

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

229+ unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args

226

230

227 -- the easy cases

231 -- the easy cases

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

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

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

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

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

230 getDepsTerm vs bs cd Erased = M.empty

235 getDepsTerm vs bs cd Erased = M.empty

231 getDepsTerm vs bs cd Impossible = M.empty

236 getDepsTerm vs bs cd Impossible = M.empty

232

237

238+ getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t

239+

233 -- convert applications of lambdas to lets

240 -- convert applications of lambdas to lets

234 -- Note that this transformation preserves de bruijn numbering

241 -- Note that this transformation preserves de bruijn numbering

235 lamToLet :: [Term] -> Term -> Term

242 lamToLet :: [Term] -> Term -> Term