95d226f · Idris-dev · git.iko.soy

src/Idris/Coverage.hs+11−1

compare with master

unifiedsplit

@@ -440,12 +440,22 @@ checkRec fa@(App _ _ _) fa'@(App _ _ _)

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

441 = if (length as /= length as')

442 then checkRec f f'

443+ -- Same function but different args is recoverable,

444+ -- and vice versa, if it's an ordinary function

445+ -- If a constructor, everything has to be recoverable

446+ else do fok <- checkRec f f'

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

447+ argok <- checkRecs (f : as) (f : as')

448+ return (if conType f then fok && argok

449+ else fok || argok)

444 where

450 where

445 checkRecs [] [] = return True

451 checkRecs [] [] = return True

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

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

447 asok <- checkRecs as bs

453 asok <- checkRecs as bs

448 return (aok && asok)

454 return (aok && asok)

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

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

457+ conType _ = False

458+

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

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

450 | x == y = return True

460 | x == y = return True

451 | ntRec xt yt = return True

461 | ntRec xt yt = return True

src/Idris/Elab/Clause.hs+2

@@ -611,6 +611,8 @@ checkPossible info fc tcgen fname lhs_in

611 return Nothing

612 -- if it's a recoverable error, the case may become possible

613 Error err -> do logLvl 10 $ "Impossible case " ++ (pshow i err)

614+ ++ "\n" ++ show (recoverableCoverage ctxt err,

615+ validCoverageCase ctxt err)

614 -- tcgen means that it was generated by genClauses,

616 -- tcgen means that it was generated by genClauses,

615 -- so only looking for an error. Otherwise, it

617 -- so only looking for an error. Otherwise, it

616 -- needs to be the right kind of error (a type mismatch

618 -- needs to be the right kind of error (a type mismatch

test/TestData.hs+2−1

@@ -284,7 +284,8 @@ testFamiliesData = [

284 ( 18, ANY ),

285 ( 19, ANY ),

286 ( 20, ANY ),

287− ( 21, ANY )]),

287+ ( 21, ANY ),

288+ ( 22, ANY )]),

288 ("tutorial", "Tutorial examples",

289 ("tutorial", "Tutorial examples",

289 [ ( 1, ANY ),

290 [ ( 1, ANY ),

290 ( 2, ANY ),

291 ( 2, ANY ),

test/totality022/expectednew file+1

@@ -0,0 +1 @@

1+totality022.idr:7:3:f _ [] (RSnoc _ _) is a valid case

test/totality022/runnew file+3

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ totality022.idr --check

3+rm -f *.ibc

test/totality022/totality022.idrnew file+11

@@ -0,0 +1,11 @@

1+data Rev : List a -> Type where

2+ RSnoc : (x : a) -> Rev xs -> Rev (xs ++ [x])

3+ RNil : Rev []

4+

5+total

6+f : (x : a) -> (ys : List a) -> (rxs : Rev (ys ++ [x])) -> Void

7+f _ [] (RSnoc _ _) impossible -- = ?wat

8+f _ [] RNil impossible

9+f _ (_ :: _) (RSnoc _ _) impossible

10+f _ (_ :: _) RNil impossible

11+