d1f3be2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use conversion errors in coverage check

d1f3be2Edwin Brady10 years ago

src/Idris/Coverage.hs+71−54

compare with master

unifiedsplit

@@ -337,7 +337,14 @@ validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

337 ((P _ x _, _), (P _ y _, _)) -> x == y

338 _ -> False

339validCoverageCase ctxt (InfiniteUnify _ _ _) = False

340−validCoverageCase ctxt (CantConvert _ _ _) = False

340+validCoverageCase ctxt (CantConvert topx topy _)

341+ = let topx' = normalise ctxt [] topx

342+ topy' = normalise ctxt [] topy in

343+ not (sameFam topx' topy')

344+ where sameFam topx topy

345+ = case (unApply topx, unApply topy) of

346+ ((P _ x _, _), (P _ y _, _)) -> x == y

347+ _ -> False

341validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e

348validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e

342validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e

349validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e

343validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e

350validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e

@@ -350,62 +357,72 @@ recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

350 = let topx' = normalise ctxt [] topx

357 = let topx' = normalise ctxt [] topx

351 topy' = normalise ctxt [] topy in

358 topy' = normalise ctxt [] topy in

352 evalState (checkRec topx' topy') []

359 evalState (checkRec topx' topy') []

353− where -- different notion of recoverable than in unification, since we

360+recoverableCoverage ctxt (CantConvert topx topy _)

354− -- have no metavars -- just looking to see if a constructor is failing

361+ = let topx' = normalise ctxt [] topx

355− -- to unify with a function that may be reduced later, or if any

362+ topy' = normalise ctxt [] topy in

356− -- variables need to have two different constructor forms

363+ evalState (checkRec topx' topy') []

357−

358− -- The state is a mapping of name to what it has failed to unify

359− -- with

360− checkRec :: Term -> Term -> State [(Name, Term)] Bool

361− checkRec (P Bound x _) tm

362− | (P yt _ _, _) <- unApply tm,

363− conType yt = do nmap <- get

364− case lookup x nmap of

365− Nothing -> do put ((x, tm) : nmap)

366− return True

367− Just y' -> checkRec tm y'

368− checkRec tm (P Bound y _)

369− | (P xt _ _, _) <- unApply tm,

370− conType xt = do nmap <- get

371− case lookup y nmap of

372− Nothing -> do put ((y, tm) : nmap)

373− return True

374− Just x' -> checkRec tm x'

375− checkRec (App _ f a) p@(P _ _ _) = checkRec f p

376− checkRec p@(P _ _ _) (App _ f a) = checkRec p f

377− checkRec fa@(App _ _ _) fa'@(App _ _ _)

378− | (f, as) <- unApply fa,

379− (f', as') <- unApply fa'

380− = if (length as /= length as')

381− then checkRec f f'

382− else checkRecs (f : as) (f' : as')

383− where

384− checkRecs [] [] = return True

385− checkRecs (a : as) (b : bs) = do aok <- checkRec a b

386− asok <- checkRecs as bs

387− return (aok && asok)

388− checkRec (P xt x _) (P yt y _)

389− | x == y = return True

390− | ntRec xt yt = return True

391− checkRec _ _ = return False

392−

393− conType (DCon _ _ _) = True

394− conType (TCon _ _) = True

395− conType _ = False

396−

397− -- If either name is a reference or a bound variable, then further

398− -- development may fix the error, so consider it recoverable.

399− -- If both names are constructors, and the name is different, then

400− -- it's not recoverable

401− ntRec x y | Ref <- x = True

402− | Ref <- y = True

403− | Bound <- x = True

404− | Bound <- y = True

405− | otherwise = False -- name is different, unrecoverable

406recoverableCoverage ctxt (InfiniteUnify _ _ _) = False -- always unrecoverable

364recoverableCoverage ctxt (InfiniteUnify _ _ _) = False -- always unrecoverable

407recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e

365recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e

408recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e

366recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e

409recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e

367recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e

410recoverableCoverage _ _ = False

368recoverableCoverage _ _ = False

411

369

370+-- different notion of recoverable than in unification, since we

371+-- have no metavars -- just looking to see if a constructor is failing

372+-- to unify with a function that may be reduced later, or if any

373+-- variables need to have two different constructor forms

374+

375+-- The state is a mapping of name to what it has failed to unify

376+-- with

377+checkRec :: Term -> Term -> State [(Name, Term)] Bool

378+checkRec (P Bound x _) tm

379+ | (P yt _ _, _) <- unApply tm,

380+ conType yt = do nmap <- get

381+ case lookup x nmap of

382+ Nothing -> do put ((x, tm) : nmap)

383+ return True

384+ Just y' -> checkRec tm y'

385+ where

386+ conType (DCon _ _ _) = True

387+ conType (TCon _ _) = True

388+ conType _ = False

389+

390+checkRec tm (P Bound y _)

391+ | (P xt _ _, _) <- unApply tm,

392+ conType xt = do nmap <- get

393+ case lookup y nmap of

394+ Nothing -> do put ((y, tm) : nmap)

395+ return True

396+ Just x' -> checkRec tm x'

397+ where

398+ conType (DCon _ _ _) = True

399+ conType (TCon _ _) = True

400+ conType _ = False

401+

402+checkRec (App _ f a) p@(P _ _ _) = checkRec f p

403+checkRec p@(P _ _ _) (App _ f a) = checkRec p f

404+checkRec fa@(App _ _ _) fa'@(App _ _ _)

405+ | (f, as) <- unApply fa,

406+ (f', as') <- unApply fa'

407+ = if (length as /= length as')

408+ then checkRec f f'

409+ else checkRecs (f : as) (f' : as')

410+ where

411+ checkRecs [] [] = return True

412+ checkRecs (a : as) (b : bs) = do aok <- checkRec a b

413+ asok <- checkRecs as bs

414+ return (aok && asok)

415+checkRec (P xt x _) (P yt y _)

416+ | x == y = return True

417+ | ntRec xt yt = return True

418+ where

419+ -- If either name is a reference or a bound variable, then further

420+ -- development may fix the error, so consider it recoverable.

421+ -- If both names are constructors, and the name is different, then

422+ -- it's not recoverable

423+ ntRec x y | Ref <- x = True

424+ | Ref <- y = True

425+ | Bound <- x = True

426+ | Bound <- y = True

427+ | otherwise = False -- name is different, unrecoverable

428+checkRec _ _ = return False

test/totality020/expected+1

@@ -1 +1,2 @@

1totality020.idr:4:5:bug _ _ Refl is a valid case

2+totality020.idr:7:5:foo a b Refl is a valid case

test/totality020/totality020.idr+7

@@ -2,3 +2,10 @@

3bug : (n, m : Nat) -> n + m = n -> Void

4bug _ _ Refl impossible

6+foo : (a : Bool) -> (b : Bool) -> Not (const a b = b)

7+foo a b Refl impossible

9+myVoid : Void

10+myVoid = foo True True Refl

11+