b0899cc · Idris-dev · git.iko.soy

src/Idris/Coverage.hs+8−8

compare with master

unifiedsplit

@@ -280,22 +280,22 @@ genAll i (addPH, args)

280 nc' o = o

281

282 otherPats :: PTerm -> [PTerm]

283− otherPats o@(PRef fc hl n) = ph $ ops fc n [] o

283+ otherPats (PRef fc hl n) = ph $ ops fc n []

284− otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o

284+ otherPats (PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs

285− otherPats o@(PPair fc hls _ l r)

285+ otherPats (PPair fc hls _ l r)

286 = ph $ ops fc pairCon

287 ([pimp (sUN "A") Placeholder True,

288 pimp (sUN "B") Placeholder True] ++

289− [pexp l, pexp r]) o

289+ [pexp l, pexp r])

290− otherPats o@(PDPair fc hls p t _ v)

290+ otherPats (PDPair fc hls p t _ v)

291 = ph $ ops fc sigmaCon

292 ([pimp (sUN "a") Placeholder True,

293 pimp (sUN "P") Placeholder True] ++

294− [pexp t,pexp v]) o

294+ [pexp t,pexp v])

295 otherPats o@(PConstant _ c) = ph [o, nextConst o]

296 otherPats arg = return Placeholder

297

298− ops fc n xs o

298+ ops fc n xs

299 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)

300 = do xs' <- mapM otherPats (map getExpTm xs)

301 let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))

@@ -303,7 +303,7 @@ genAll i (addPH, args)

303 case lookupCtxt tyn (idris_datatypes i) of

304 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

305 _ -> [p]

306− ops fc n arg o = return Placeholder

306+ ops fc n arg = return Placeholder

307

308 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!

309 getExpTm t = getTm t

src/Idris/Elab/Clause.hs+12−5

@@ -566,7 +566,7 @@ checkPossible info fc tcgen fname lhs_in

566 = do ctxt <- getContext

567 i <- getIState

568 let lhs = addImplPat i lhs_in

569− logLvl 10 $ "Trying missing case: " ++ showTmImpls lhs

569+ logElab 10 $ "Trying missing case: " ++ showTmImpls lhs

570 -- if the LHS type checks, it is possible

571 case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

572 (erun fc (buildTC i info ELHS [] fname

@@ -577,10 +577,17 @@ checkPossible info fc tcgen fname lhs_in

577 processTacticDecls info newDecls

578 sendHighlighting highlights

579 updateIState $ \i -> i { idris_name = newGName }

580− let lhs_tm = orderPats (getInferTerm lhs')

580+ let lhs_tm = normalise ctxt [] (orderPats (getInferTerm lhs'))

581+ let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm

582+ if emptyPat then

583+ do logElab 10 $ "Empty type in pattern "

584+ return False

585+ else

581− case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of

586+ case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of

587+ OK _ -> do logElab 10 $ "Valid"

582− OK _ -> return True

588+ return True

589+ err -> do logElab 10 $ "Conversion failure"

583− err -> return False

590+ return False

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

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

585 Error err -> do logLvl 10 $ "Impossible case " ++ show err

592 Error err -> do logLvl 10 $ "Impossible case " ++ show err

586 if tcgen then return (recoverableCoverage ctxt err)

593 if tcgen then return (recoverableCoverage ctxt err)

src/Idris/Elab/Utils.hs+29−1

@@ -542,4 +542,32 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

542 return (App s f' a')

543 getPats t = return t

544

545−

545+isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool

546+isEmpty ctxt tyctxt ty

547+ | (P _ tyname _, args) <- unApply (getRetTy ty),

548+ Just tyinfo <- lookupCtxtExact tyname tyctxt

549+ -- Compare all the constructor types against the type we need

550+ -- If they *all* have an argument position where some constructor

551+ -- clases with the needed type, then the type we're looking for must

552+ -- be empty

553+ = let neededty = getRetTy ty

554+ contys = mapMaybe getConType (con_names tyinfo) in

555+ all (findClash neededty) contys

556+ where

557+ getConType n = do t <- lookupTyExact n ctxt

558+ return (getRetTy (normalise ctxt [] t))

559+

560+ findClash l r

561+ | (P _ n _, _) <- unApply l,

562+ (P _ n' _, _) <- unApply r,

563+ isConName n ctxt && isConName n' ctxt, n /= n'

564+ = True

565+ findClash (App _ f a) (App _ f' a') = findClash f f' || findClash a a'

566+ findClash l r = False

567+

568+isEmpty ctxt tyinfo ty = False

569+

570+hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool

571+hasEmptyPat ctxt tyctxt (Bind n (PVar ty) sc)

572+ = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc

573+hasEmptyPat ctxt tyctxt _ = False

test/TestData.hs+2−1

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

274 ( 14, ANY ),

275 ( 15, ANY ),

276 ( 16, ANY ),

277− ( 17, ANY )]),

277+ ( 17, ANY ),

278+ ( 18, ANY )]),

278 ("tutorial", "Tutorial examples",

279 ("tutorial", "Tutorial examples",

279 [ ( 1, ANY ),

280 [ ( 1, ANY ),

280 ( 2, ANY ),

281 ( 2, ANY ),

test/interfaces002/interfaces002.idr+2

@@ -1,5 +1,7 @@

1import Data.Vect

2

3+%default total

4+

3interface ArrayM where

5interface ArrayM where

4 Array : (n : Nat) -> (a : Type) -> Type

6 Array : (n : Nat) -> (a : Type) -> Type

5

7

test/totality018/expectednew file+1

@@ -0,0 +1 @@

1+totality018.idr:12:1:Main.bar is not total as there are missing cases

test/totality018/runnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc

test/totality018/totality018.idrnew file+15

@@ -0,0 +1,15 @@

1+import Data.Fin

2+

3+%default total

4+

5+foo : Fin 3 -> Nat

6+foo FZ = 0

7+foo (FS FZ) = 1

8+foo (FS (FS FZ)) = 2

9+-- testing that there is no need for an extra 'impossible'

10+

11+bar : Fin 4 -> Nat

12+bar FZ = 0

13+bar (FS FZ) = 1

14+bar (FS (FS FZ)) = 2

15+-- should be non-total