ddece77 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Handle projections at least trivially.

commitddece776031465acc364e48e95a9da6fa2b96f8c authorMatus Tejiscak <ziman@functor.sk> dateWed 29 Jan 2014, 15:27 (13 years ago) parentd403d47

2 files changed+13−6

compare with master

unifiedsplit

src/Idris/ElabDecls.hs+2−2 src/Idris/Erasure.hs+11−4

src/Idris/ElabDecls.hs+2−2

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

10901090 let used = findUsedArgs sc' scargs'

10911091 -- let scg = buildSCG i sc scargs

10921092 -- 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

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

10951095 addToCG n cg

10961096 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

20882088 _ -> return ps'

20892089 getWParams (_ : ps) = getWParams ps

20902090

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

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

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

20932093

20942094 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

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

203203

204204 -- this does not

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

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

206206

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

208208 -- 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

210210

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

212212 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

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

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

217217

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

219222

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

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

221224 where

222225 ins = M.insertWith S.union cd

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

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

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

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

226230

227231 -- the easy cases

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

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

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

230235 getDepsTerm vs bs cd Erased = M.empty

231236 getDepsTerm vs bs cd Impossible = M.empty

232237

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

239+

233240 -- convert applications of lambdas to lets

234241 -- Note that this transformation preserves de bruijn numbering

235242 lamToLet :: [Term] -> Term -> Term