3fba96b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remember constants when checking recoverability

3fba96bEdwin Brady9 years ago

src/Idris/Coverage.hs+29−12

compare with master

unifiedsplit

@@ -410,31 +410,43 @@ recoverableCoverage _ _ = False

410-- with

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

412checkRec (P Bound x _) tm

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

414− conType yt = do nmap <- get

413+ | isCon tm = do nmap <- get

415− case lookup x nmap of

414+ case lookup x nmap of

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

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

417− return True

416+ return True

418− Just y' -> checkRec tm y'

417+ Just y' -> checkRec tm y'

419 where

418 where

419+ isCon tm

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

421+ conType yt = True

422+ isCon (Constant _) = True

423+ isCon _ = False

424+

420 conType (DCon _ _ _) = True

425 conType (DCon _ _ _) = True

421 conType (TCon _ _) = True

426 conType (TCon _ _) = True

422 conType _ = False

427 conType _ = False

423

428

424checkRec tm (P Bound y _)

429checkRec tm (P Bound y _)

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

426− conType xt = do nmap <- get

430+ | isCon tm = do nmap <- get

427− case lookup y nmap of

431+ case lookup y nmap of

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

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

429− return True

433+ return True

430− Just x' -> checkRec tm x'

434+ Just x' -> checkRec tm x'

431 where

435 where

436+ isCon tm

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

438+ conType yt = True

439+ isCon (Constant _) = True

440+ isCon _ = False

441+

432 conType (DCon _ _ _) = True

442 conType (DCon _ _ _) = True

433 conType (TCon _ _) = True

443 conType (TCon _ _) = True

434 conType _ = False

444 conType _ = False

435

445

436checkRec (App _ f a) p@(P _ _ _) = checkRec f p

446checkRec (App _ f a) p@(P _ _ _) = checkRec f p

447+checkRec (App _ f a) p@(Constant _) = checkRec f p

437checkRec p@(P _ _ _) (App _ f a) = checkRec p f

448checkRec p@(P _ _ _) (App _ f a) = checkRec p f

449+checkRec p@(Constant _) (App _ f a) = checkRec p f

438checkRec fa@(App _ _ _) fa'@(App _ _ _)

450checkRec fa@(App _ _ _) fa'@(App _ _ _)

439 | (f, as) <- unApply fa,

451 | (f, as) <- unApply fa,

440 (f', as') <- unApply fa'

452 (f', as') <- unApply fa'

@@ -454,6 +466,7 @@ checkRec fa@(App _ _ _) fa'@(App _ _ _)

454 return (aok && asok)

466 return (aok && asok)

455 conType (P (DCon _ _ _) _ _) = True

467 conType (P (DCon _ _ _) _ _) = True

456 conType (P (TCon _ _) _ _) = True

468 conType (P (TCon _ _) _ _) = True

469+ conType (Constant _) = True

457 conType _ = False

470 conType _ = False

458

471

459checkRec (P xt x _) (P yt y _)

472checkRec (P xt x _) (P yt y _)

@@ -469,4 +482,8 @@ checkRec (P xt x _) (P yt y _)

469 | Bound <- x = True

482 | Bound <- x = True

470 | Bound <- y = True

483 | Bound <- y = True

471 | otherwise = False -- name is different, unrecoverable

484 | otherwise = False -- name is different, unrecoverable

485+-- A function reference against a constant might be recoverable if we get to

486+-- reduce the function

487+checkRec (P Ref _ _) (Constant _) = return True

488+checkRec (Constant _) (P Ref _ _) = return True

472checkRec _ _ = return False

489checkRec _ _ = return False

test/regression002/Canonicity.idrnew file+13

@@ -0,0 +1,13 @@

1+module Canonicity

2+%default total

4+data ZeroSumList : Integer -> Type where

5+ Cons : (m : Integer) -> ZeroSumList n -> ZeroSumList (m + n)

6+ Nil : ZeroSumList 0

8+f : ZeroSumList 0 -> Nat

9+f Nil = 0

10+

11+NaN : Nat

12+NaN = f (Cons 0 Nil)

13+

test/regression002/expected+2

@@ -145,3 +145,5 @@ When checking argument value to function Prelude.Basics.the:

145 -0.0

146 and

147 0.0

148+Canonicity.idr:9:1:Canonicity.f is not total as there are missing cases

149+Canonicity.idr:12:1:Canonicity.NaN is possibly not total due to: Canonicity.f

test/regression002/run+1

@@ -32,6 +32,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet --port none <<!

32:load reg076.idr

33:load reg077.idr

34:load DoubleEquality.idr

35+:load Canonicity.idr

35!

36!

37rm -f *.ibc

38rm -f *.ibc