cadffac · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'ziman-debruijn-names'

cadffacEdwin Brady12 years ago

src/Idris/ElabDecls.hs+2−1

compare with master

unifiedsplit

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

1195 force (normalisePats ctxt [] y))

1196 simple_lhs ctxt t = t

1197

1198− simple_rt ctxt (p, x, y) = (p, x, force (rt_simplify ctxt [] y))

1198+ simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

1199+ (rt_simplify ctxt [] y)))

1199

1200

1200 -- this is so pattern types are in the right form for erasure

1201 -- this is so pattern types are in the right form for erasure

1201 normalisePats ctxt env (Bind n (PVar t) sc)

1202 normalisePats ctxt env (Bind n (PVar t) sc)

src/Idris/Erasure.hs+18−10

@@ -294,7 +294,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

294 -- that the result of this function is used at all

295 = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

296 where

297−

298 addTagDep = case alts of

297 addTagDep = case alts of

299 [_] -> id -- single branch, tag not used

298 [_] -> id -- single branch, tag not used

300 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)

299 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)

@@ -329,11 +328,15 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

329 | otherwise = \j -> Nothing

328 | otherwise = \j -> Nothing

330

329

331 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

330 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

332− getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps

331+ getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps

333

332

334 -- named variables introduce dependencies as described in `vs'

333 -- named variables introduce dependencies as described in `vs'

335 getDepsTerm vs bs cd (P _ n _)

334 getDepsTerm vs bs cd (P _ n _)

335+ -- de bruijns (lambda-bound, let-bound vars)

336+ | Just deps <- lookup n bs

337+ = deps cd

338+

336− -- local variables

339+ -- ctor-bound/arg-bound variables

337 | Just var <- M.lookup n vs

340 | Just var <- M.lookup n vs

338 = M.singleton cd (viDeps var)

341 = M.singleton cd (viDeps var)

339

342

@@ -348,18 +351,18 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

348 specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"

351 specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"

349

352

350 -- dependencies of de bruijn variables are described in `bs'

353 -- dependencies of de bruijn variables are described in `bs'

351− getDepsTerm vs bs cd (V i) = (bs !! i) cd

354+ getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

352

355

353 getDepsTerm vs bs cd (Bind n bdr t)

356 getDepsTerm vs bs cd (Bind n bdr t)

354 -- here we just push IM.empty on the de bruijn stack

357 -- here we just push IM.empty on the de bruijn stack

355 -- the args will be marked as used at the usage site

358 -- the args will be marked as used at the usage site

356− | Lam ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

359+ | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

357− | Pi ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

360+ | Pi ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

358

361

359 -- let-bound variables can get partially evaluated

362 -- let-bound variables can get partially evaluated

360 -- it is sufficient just to plug the Cond in when the bound names are used

363 -- it is sufficient just to plug the Cond in when the bound names are used

361− | Let ty t <- bdr = getDepsTerm vs (var t : bs) cd t

364+ | Let ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

362− | NLet ty t <- bdr = getDepsTerm vs (var t : bs) cd t

365+ | NLet ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

363 where

366 where

364 var t cd = getDepsTerm vs bs cd t

367 var t cd = getDepsTerm vs bs cd t

365

368

@@ -386,6 +389,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

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

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

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

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

388 P _ n _

391 P _ n _

392+ -- debruijn-bound name

393+ | Just deps <- lookup n bs

394+ -> deps cd `union` unconditionalDeps args

395+

389 -- local name that refers to a method

396 -- local name that refers to a method

390 | Just var <- M.lookup n vs

397 | Just var <- M.lookup n vs

391 , Just meth <- viMethod var

398 , Just meth <- viMethod var

@@ -402,7 +409,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

402 -> conditionalDeps n args

409 -> conditionalDeps n args

403

410

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

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

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

412+ V i -> snd (bs !! i) cd `union` unconditionalDeps args

406

413

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

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

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

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

@@ -418,6 +425,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

418

425

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

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

420 where

427 where

428+ union = M.unionWith $ M.unionWith S.union

421 ins = M.insertWith (M.unionWith S.union) cd

429 ins = M.insertWith (M.unionWith S.union) cd

422

430

423 unconditionalDeps :: [Term] -> Deps

431 unconditionalDeps :: [Term] -> Deps

@@ -441,7 +449,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

441 , viMethod = Nothing

449 , viMethod = Nothing

442 }) | (v, i) <- zip args [0..]]

450 }) | (v, i) <- zip args [0..]]

443 deps i = M.singleton (metameth, Arg i) S.empty

451 deps i = M.singleton (metameth, Arg i) S.empty

444− bruijns = reverse [\cd -> M.singleton cd (deps i) | i <- [0 .. length args - 1]]

452+ bruijns = reverse [(n, \cd -> M.singleton cd (deps i)) | (i, n) <- zip [0..] args]

445 cond = S.singleton (metameth, Result)

453 cond = S.singleton (metameth, Result)

446 metameth = mkFieldName ctorName methNo

454 metameth = mkFieldName ctorName methNo

447 (args, body) = unfoldLams t

455 (args, body) = unfoldLams t