b1ce3cb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Implement a form of pattern unification

b1ce3cbEdwin Brady11 years ago

CHANGELOG+1−1

compare with master

unifiedsplit

@@ -4,7 +4,7 @@ New in 0.9.20:

4Language updates

5----------------

7−[None so far]

7+* Improved unification by implementing a pattern unification rule

9Library updates

10---------------

idris.cabal+3

@@ -365,6 +365,9 @@ Extra-source-files:

365 test/basic013/run

366 test/basic013/*.idr

367 test/basic013/expected

368+ test/basic014/run

369+ test/basic014/*.idr

370+ test/basic014/expected

368

371

369 test/bignum001/run

372 test/bignum001/run

370 test/bignum001/*.idr

373 test/bignum001/*.idr

libs/base/Control/Category.idr+3−1

@@ -10,7 +10,9 @@ class Category (cat : Type -> Type -> Type) where

11instance Category Morphism where

12 id = Mor id

13+ -- disambiguation needed below, because unification can now get further

14+ -- here with Category.(.) and it's only type class resolution that fails!

13− (Mor f) . (Mor g) = Mor (f . g)

15+ (Mor f) . (Mor g) = with Basics (Mor (f . g))

15instance Monad m => Category (Kleislimorphism m) where

17instance Monad m => Category (Kleislimorphism m) where

16 id = Kleisli (return . id)

18 id = Kleisli (return . id)

src/Idris/Core/ProofState.hs+2−2

@@ -154,7 +154,7 @@ instance Pretty ProofState OutputAnnotation where

154holeName i = sMN i "hole"

155

156qshow :: Fails -> String

157−qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)

157+qshow fs = show (map (\ (x, y, hs, env, _, _, t) -> (t, map fst env, x, y, hs)) fs)

158

159match_unify' :: Context -> Env ->

160 (TT Name, Maybe Provenance) ->

@@ -218,7 +218,7 @@ unify' ctxt env (topx, xfrom) (topy, yfrom) =

218 ("Trying " ++ show (topx, topy) ++

219 "\nNormalised " ++ show (normalise ctxt env topx,

220 normalise ctxt env topy) ++

221− " in " ++ show env ++

221+ " in\n" ++ show env ++

222 "\nHoles: " ++ show (holes ps)

223 ++ "\nInjective: " ++ show (injective ps)

224 ++ "\n") $

src/Idris/Core/Unify.hs+130−77

@@ -8,6 +8,7 @@ import Idris.Core.Evaluate

9import Control.Monad

10import Control.Monad.State.Strict

11+import Data.Maybe

11import Data.List

12import Data.List

12import Debug.Trace

13import Debug.Trace

@@ -321,7 +322,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

321 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

322 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

322 StateT UInfo

323 StateT UInfo

323 TC [(Name, TT Name)]

324 TC [(Name, TT Name)]

324− un = un'

325+ un = un' env

325-- un fn names x y

326-- un fn names x y

326-- = let (xf, _) = unApply x

327-- = let (xf, _) = unApply x

327-- (yf, _) = unApply y in

328-- (yf, _) = unApply y in

@@ -329,23 +330,23 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

329-- uplus (un' fn names x y)

330-- uplus (un' fn names x y)

330-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

331-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

331

332

332− un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

333+ un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

333 StateT UInfo

334 StateT UInfo

334 TC [(Name, TT Name)]

335 TC [(Name, TT Name)]

335− un' fn names x y | x == y = return [] -- shortcut

336+ un' env fn names x y | x == y = return [] -- shortcut

336− un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)

337+ un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)

337 | x /= y = unifyFail topx topy

338 | x /= y = unifyFail topx topy

338− un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)

339+ un' env fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)

339 | x /= y = unifyFail topx topy

340 | x /= y = unifyFail topx topy

340− un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)

341+ un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)

341 = unifyFail topx topy

342 = unifyFail topx topy

342− un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)

343+ un' env fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)

343 = unifyFail topx topy

344 = unifyFail topx topy

344− un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)

345+ un' env fn names topx@(Constant _) topy@(P (TCon _ _) y _)

345 = unifyFail topx topy

346 = unifyFail topx topy

346− un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)

347+ un' env fn names topx@(P (TCon _ _) x _) topy@(Constant _)

347 = unifyFail topx topy

348 = unifyFail topx topy

348− un' fn bnames tx@(P _ x _) ty@(P _ y _)

349+ un' env fn bnames tx@(P _ x _) ty@(P _ y _)

349 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []

350 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []

350 | injective tx && not (holeIn env y || y `elem` holes)

351 | injective tx && not (holeIn env y || y `elem` holes)

351 = unifyTmpFail tx ty

352 = unifyTmpFail tx ty

@@ -360,7 +361,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

360 where envPos i n ((n',_):env) | n == n' = i

361 where envPos i n ((n',_):env) | n == n' = i

361 envPos i n (_:env) = envPos (i+1) n env

362 envPos i n (_:env) = envPos (i+1) n env

362 envPos _ _ _ = 100000

363 envPos _ _ _ = 100000

363− un' fn bnames xtm@(P _ x _) tm

364+ un' env fn bnames xtm@(P _ x _) tm

364 | pureTerm tm, holeIn env x || x `elem` holes

365 | pureTerm tm, holeIn env x || x `elem` holes

365 = do UI s f <- get

366 = do UI s f <- get

366 -- injectivity check

367 -- injectivity check

@@ -374,7 +375,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

374 | pureTerm tm, not (injective xtm) && injective tm

375 | pureTerm tm, not (injective xtm) && injective tm

375 = do checkCycle bnames (x, tm)

376 = do checkCycle bnames (x, tm)

376 unifyTmpFail xtm tm

377 unifyTmpFail xtm tm

377− un' fn bnames tm ytm@(P _ y _)

378+ un' env fn bnames tm ytm@(P _ y _)

378 | pureTerm tm, holeIn env y || y `elem` holes

379 | pureTerm tm, holeIn env y || y `elem` holes

379 = do UI s f <- get

380 = do UI s f <- get

380 -- injectivity check

381 -- injectivity check

@@ -388,62 +389,118 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

388 | pureTerm tm, not (injective ytm) && injective tm

389 | pureTerm tm, not (injective ytm) && injective tm

389 = do checkCycle bnames (y, tm)

390 = do checkCycle bnames (y, tm)

390 unifyTmpFail tm ytm

391 unifyTmpFail tm ytm

391− un' fn bnames (V i) (P _ x _)

392+ un' env fn bnames (V i) (P _ x _)

392 | length bnames > i,

393 | length bnames > i,

393 fst ((map fst bnames)!!i) == x ||

394 fst ((map fst bnames)!!i) == x ||

394 snd ((map fst bnames)!!i) == x = do sc 1; return []

395 snd ((map fst bnames)!!i) == x = do sc 1; return []

395− un' fn bnames (P _ x _) (V i)

396+ un' env fn bnames (P _ x _) (V i)

396 | length bnames > i,

397 | length bnames > i,

397 fst ((map fst bnames)!!i) == x ||

398 fst ((map fst bnames)!!i) == x ||

398 snd ((map fst bnames)!!i) == x = do sc 1; return []

399 snd ((map fst bnames)!!i) == x = do sc 1; return []

399

400

400− un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

401+ un' env fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

401− un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy

402+ un' env fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy

402−

403+

404+-- Pattern unification rule

405+ un' env fn bnames tm app@(App _ _ _)

406+ | (P _ mv _, args) <- unApply app,

407+ holeIn env mv || mv `elem` holes,

408+ all rigid args,

409+ containsOnly (mapMaybe getname args) (mapMaybe getV args) tm

410+ -- && TODO: tm does not refer to any variables other than those

411+ -- in 'args'

412+ = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $

413+ checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))

414+ where rigid (V i) = True

415+ rigid (P _ t _) = not (holeIn env t || t `elem` holes)

416+ rigid _ = False

417+

418+ getV (V i) = Just i

419+ getV _ = Nothing

420+

421+ getname (P _ n _) = Just n

422+ getname _ = Nothing

423+

424+ containsOnly args vs (V i) = i `elem` vs

425+ containsOnly args vs (P Bound n ty)

426+ = n `elem` args && containsOnly args vs ty

427+ containsOnly args vs (P _ n ty)

428+ = not (holeIn env n || n `elem` holes)

429+ && containsOnly args vs ty

430+ containsOnly args vs (App _ f a)

431+ = containsOnly args vs f && containsOnly args vs a

432+ containsOnly args vs (Bind _ b sc)

433+ = containsOnly args vs (binderTy b) &&

434+ containsOnly args (0 : map (+1) vs) sc

435+ containsOnly args vs _ = True

436+

437+ bindLams [] tm = tm

438+ bindLams (a : as) tm = bindLam a (bindLams as tm)

439+

440+ bindLam (V i) tm = Bind (fst (env !! i))

441+ (Lam (binderTy (snd (env !! i))))

442+ tm

443+ bindLam (P _ n ty) tm = Bind n (Lam ty) tm

444+ bindLam _ tm = error "Can't happen [non rigid bindLam]"

445+

446+ substEnv [] tm = tm

447+ substEnv ((n, t) : env) tm

448+ = substEnv env (substV (P Bound n (binderTy t)) tm)

449+

450+ -- remove any unnecessary lambdas (helps with type class

451+ -- resolution later).

452+ eta ks (Bind n (Lam ty) sc) = eta ((n, ty) : ks) sc

453+ eta ks t = rebind ks t

454+

455+ rebind ((n, ty) : ks) (App _ f (P _ n' _))

456+ | n == n' = eta ks f

457+ rebind ((n, ty) : ks) t = rebind ks (Bind n (Lam ty) t)

458+ rebind _ t = t

459+

403− un' fn bnames appx@(App _ _ _) appy@(App _ _ _)

460+ un' env fn bnames appx@(App _ _ _) appy@(App _ _ _)

404− = unApp fn bnames appx appy

461+ = unApp env fn bnames appx appy

405-- = uplus (unApp fn bnames appx appy)

462-- = uplus (unApp fn bnames appx appy)

406-- (unifyTmpFail appx appy) -- take the whole lot

463-- (unifyTmpFail appx appy) -- take the whole lot

407

464

408− un' fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))

465+ un' env fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))

409− | n == n' = un' False bnames x y

466+ | n == n' = un' env False bnames x y

410− un' fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y

467+ un' env fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y

411− | n == n' = un' False bnames x y

468+ | n == n' = un' env False bnames x y

412− un' fn bnames x (Bind n (Lam t) (App _ y (V 0)))

469+ un' env fn bnames x (Bind n (Lam t) (App _ y (V 0)))

413− = un' False bnames x y

470+ = un' env False bnames x y

414− un' fn bnames (Bind n (Lam t) (App _ x (V 0))) y

471+ un' env fn bnames (Bind n (Lam t) (App _ x (V 0))) y

415− = un' False bnames x y

472+ = un' env False bnames x y

416−-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

473+-- un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

417−-- = un' False ((x,y):bnames) sx sy

474+-- = un' env False ((x,y):bnames) sx sy

418−-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

475+-- un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

419−-- = un' False ((x,y):bnames) sx sy

476+-- = un' env False ((x,y):bnames) sx sy

420

477

421 -- f D unifies with t -> D. This is dubious, but it helps with type

478 -- f D unifies with t -> D. This is dubious, but it helps with type

422 -- class resolution for type classes over functions.

479 -- class resolution for type classes over functions.

423

480

424− un' fn bnames (App _ f x) (Bind n (Pi i t k) y)

481+ un' env fn bnames (App _ f x) (Bind n (Pi i t k) y)

425 | noOccurrence n y && injectiveApp f

482 | noOccurrence n y && injectiveApp f

426− = do ux <- un' False bnames x y

483+ = do ux <- un' env False bnames x y

427− uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

484+ uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

428 (Bind n (Pi i t k) (V 1)))

485 (Bind n (Pi i t k) (V 1)))

429− combine bnames ux uf

486+ combine env bnames ux uf

430

487

431− un' fn bnames (Bind n (Pi i t k) y) (App _ f x)

488+ un' env fn bnames (Bind n (Pi i t k) y) (App _ f x)

432 | noOccurrence n y && injectiveApp f

489 | noOccurrence n y && injectiveApp f

433− = do ux <- un' False bnames y x

490+ = do ux <- un' env False bnames y x

434− uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

491+ uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

435 (Bind n (Pi i t k) (V 1))) f

492 (Bind n (Pi i t k) (V 1))) f

436− combine bnames ux uf

493+ combine env bnames ux uf

437

494

438− un' fn bnames (Bind x bx sx) (Bind y by sy)

495+ un' env fn bnames (Bind x bx sx) (Bind y by sy)

439 | sameBinder bx by

496 | sameBinder bx by

440− = do h1 <- uB bnames bx by

497+ = do h1 <- uB env bnames bx by

441− h2 <- un' False (((x,y),binderTy bx):bnames) sx sy

498+ h2 <- un' ((x, bx) : env) False (((x,y),binderTy bx):bnames) sx sy

442− combine bnames h1 h2

499+ combine env bnames h1 h2

443 where sameBinder (Lam _) (Lam _) = True

500 where sameBinder (Lam _) (Lam _) = True

444 sameBinder (Pi i _ _) (Pi i' _ _) = True

501 sameBinder (Pi i _ _) (Pi i' _ _) = True

445 sameBinder _ _ = False -- never unify holes/guesses/etc

502 sameBinder _ _ = False -- never unify holes/guesses/etc

446− un' fn bnames x y

503+ un' env fn bnames x y

447 | OK True <- convEq' ctxt holes x y = do sc 1; return []

504 | OK True <- convEq' ctxt holes x y = do sc 1; return []

448 | isUniverse x && isUniverse y = do sc 1; return []

505 | isUniverse x && isUniverse y = do sc 1; return []

449 | otherwise = do UI s f <- get

506 | otherwise = do UI s f <- get

@@ -455,11 +512,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

455 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

512 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

456 return [] -- lift $ tfail err

513 return [] -- lift $ tfail err

457

514

458− unApp fn bnames appx@(App _ fx ax) appy@(App _ fy ay)

515+ unApp env fn bnames appx@(App _ fx ax) appy@(App _ fy ay)

459 -- shortcut for the common case where we just want to check the

516 -- shortcut for the common case where we just want to check the

460 -- arguments are correct

517 -- arguments are correct

461 | (injectiveApp fx && fx == fy)

518 | (injectiveApp fx && fx == fy)

462− = un' False bnames ax ay

519+ = un' env False bnames ax ay

463 | (injectiveApp fx && injectiveApp fy)

520 | (injectiveApp fx && injectiveApp fy)

464 || (injectiveApp fx && metavarApp fy && ax == ay)

521 || (injectiveApp fx && metavarApp fy && ax == ay)

465 || (injectiveApp fy && metavarApp fx && ax == ay)

522 || (injectiveApp fy && metavarApp fx && ax == ay)

@@ -468,18 +525,18 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

468 -- fail quickly if the heads are disjoint

525 -- fail quickly if the heads are disjoint

469 checkHeads headx heady

526 checkHeads headx heady

470 uplus

527 uplus

471− (do hf <- un' True bnames fx fy

528+ (do hf <- un' env True bnames fx fy

472 let ax' = hnormalise hf ctxt env (substNames hf ax)

529 let ax' = hnormalise hf ctxt env (substNames hf ax)

473 let ay' = hnormalise hf ctxt env (substNames hf ay)

530 let ay' = hnormalise hf ctxt env (substNames hf ay)

474− ha <- un' False bnames ax' ay'

531+ ha <- un' env False bnames ax' ay'

475 sc 1

532 sc 1

476− combine bnames hf ha)

533+ combine env bnames hf ha)

477− (do ha <- un' False bnames ax ay

534+ (do ha <- un' env False bnames ax ay

478 let fx' = hnormalise ha ctxt env (substNames ha fx)

535 let fx' = hnormalise ha ctxt env (substNames ha fx)

479 let fy' = hnormalise ha ctxt env (substNames ha fy)

536 let fy' = hnormalise ha ctxt env (substNames ha fy)

480− hf <- un' False bnames fx' fy'

537+ hf <- un' env False bnames fx' fy'

481 sc 1

538 sc 1

482− combine bnames hf ha)

539+ combine env bnames hf ha)

483 | otherwise = unifyTmpFail appx appy

540 | otherwise = unifyTmpFail appx appy

484 where hnormalise [] _ _ t = t

541 where hnormalise [] _ _ t = t

485 hnormalise ns ctxt env t = normalise ctxt env t

542 hnormalise ns ctxt env t = normalise ctxt env t

@@ -497,8 +554,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

497 unArgs as (x : xs) (y : ys)

554 unArgs as (x : xs) (y : ys)

498 = do let x' = hnormalise as ctxt env (substNames as x)

555 = do let x' = hnormalise as ctxt env (substNames as x)

499 let y' = hnormalise as ctxt env (substNames as y)

556 let y' = hnormalise as ctxt env (substNames as y)

500− as' <- un' False bnames x' y'

557+ as' <- un' env False bnames x' y'

501− vs <- combine bnames as as'

558+ vs <- combine env bnames as as'

502 unArgs vs xs ys

559 unArgs vs xs ys

503

560

504 numArgs tm = let (f, args) = unApply tm in length args

561 numArgs tm = let (f, args) = unApply tm in length args

@@ -564,21 +621,22 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

564 lift $ tfail err

621 lift $ tfail err

565

622

566

623

567− uB bnames (Let tx vx) (Let ty vy)

624+ uB env bnames (Let tx vx) (Let ty vy)

568− = do h1 <- un' False bnames tx ty

625+ = do h1 <- un' env False bnames tx ty

569− h2 <- un' False bnames vx vy

626+ h2 <- un' env False bnames vx vy

570 sc 1

627 sc 1

571− combine bnames h1 h2

628+ combine env bnames h1 h2

572− uB bnames (Guess tx vx) (Guess ty vy)

629+ uB env bnames (Guess tx vx) (Guess ty vy)

573− = do h1 <- un' False bnames tx ty

630+ = do h1 <- un' env False bnames tx ty

574− h2 <- un' False bnames vx vy

631+ h2 <- un' env False bnames vx vy

575 sc 1

632 sc 1

576− combine bnames h1 h2

633+ combine env bnames h1 h2

577− uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty

634+ uB env bnames (Lam tx) (Lam ty) = do sc 1; un' env False bnames tx ty

578− uB bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' False bnames tx ty

635+ uB env bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' env False bnames tx ty

579− uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

636+ uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty

580− uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

637+ uB env bnames (PVar tx) (PVar ty) = un' env False bnames tx ty

638+ uB env bnames x y

581− uB bnames x y = do UI s f <- get

639+ = do UI s f <- get

582 let r = recoverable (normalise ctxt env (binderTy x))

640 let r = recoverable (normalise ctxt env (binderTy x))

583 (normalise ctxt env (binderTy y))

641 (normalise ctxt env (binderTy y))

584 let err = cantUnify from r (topx, xfrom) (topy, yfrom)

642 let err = cantUnify from r (topx, xfrom) (topy, yfrom)

@@ -613,20 +671,15 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

613 App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

671 App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

614 (P Bound x ty)

672 (P Bound x ty)

615

673

616− combineArgs bnames args = ca [] args where

617− ca acc [] = return acc

618− ca acc (x : xs) = do x' <- combine bnames acc x

619− ca x' xs

620−

621− combine bnames as [] = return as

674+ combine env bnames as [] = return as

622− combine bnames as ((n, t) : bs)

675+ combine env bnames as ((n, t) : bs)

623 = case lookup n as of

676 = case lookup n as of

624− Nothing -> combine bnames (as ++ [(n,t)]) bs

677+ Nothing -> combine env bnames (as ++ [(n,t)]) bs

625− Just t' -> do ns <- un' False bnames t t'

678+ Just t' -> do ns <- un' env False bnames t t'

626 -- make sure there's n mapping from n in ns

679 -- make sure there's n mapping from n in ns

627 let ns' = filter (\ (x, _) -> x/=n) ns

680 let ns' = filter (\ (x, _) -> x/=n) ns

628 sc 1

681 sc 1

629− combine bnames as (ns' ++ bs)

682+ combine env bnames as (ns' ++ bs)

630

683

631boundVs :: Int -> Term -> [Int]

684boundVs :: Int -> Term -> [Int]

632boundVs i (V j) | j < i = []

685boundVs i (V j) | j < i = []

test/basic014/basic014.idrnew file+44

@@ -0,0 +1,44 @@

1+-- Test pattern unification

3+import Data.Vect

5+comp : {A : Type} -> {B : (a : A) -> Type} ->

6+ {C : (a : A) -> (b : B a) -> Type} ->

7+ (f : {a : A} -> (b : B a) -> C a b) ->

8+ (g : (a : A) -> B a) ->

9+ (a : A) -> C a (g a)

10+comp f g a = f (g a)

11+

12+add2 : Nat -> Nat

13+add2 = comp S S

14+

15+data Foo = MkFoo

16+data Bar = MkBar

17+

18+foo : Foo -> Bar

19+

20+bar : Bar -> Nat

21+

22+baz : Foo -> Nat

23+baz = (comp bar foo)

24+

25+comp0 : (B : Nat -> Type) -> ((n : Nat) -> B n) -> Int

26+comp0 _ _ = 0

27+

28+test00 : Int

29+test00 = comp0 _ S

30+

31+comp2 : (B : Nat -> Type) ->

32+ ((n : Nat) -> (y : B n) -> Int) -> Int

33+comp2 _ _ = 0

34+

35+test20 : Int

36+test20 = comp2 _ dummy

37+ where

38+ dummy : (n : Nat) -> Vect n Int -> Int

39+ dummy _ _ = 0

40+

41+test03 : Int

42+test03 = comp0 _ dummy where

43+ dummy : (n : Nat) -> Int -> Int

44+ dummy _ = \x => x

test/basic014/expectednew file

No changes to the content.

test/basic014/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ basic014.idr --check

3+rm -f *.ibc