b0899cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Look deeper when coverage checking

If there is a pattern variable with an obviously empty type, because all of the constructors are in a different part of the family due to disjoint indices, then reject the clause as impossible.

commitb0899cc080d48b4317219335602b72278550d02b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 20 Nov 2016, 20:22 (10 years ago) parent3275efd

8 files changed+72−15

compare with master

unifiedsplit

src/Idris/Coverage.hs+8−8 src/Idris/Elab/Clause.hs+12−5 src/Idris/Elab/Utils.hs+29−1 test/TestData.hs+2−1 test/interfaces002/interfaces002.idr+2 test/totality018/expected+1 test/totality018/run+3 test/totality018/totality018.idr+15

src/Idris/Coverage.hs+8−8

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

280280 nc' o = o

281281

282282 otherPats :: PTerm -> [PTerm]

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

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

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

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

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

285+ otherPats (PPair fc hls _ l r)

286286 = ph $ ops fc pairCon

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

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

289− [pexp l, pexp r]) o

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

289+ [pexp l, pexp r])

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

291291 = ph $ ops fc sigmaCon

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

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

294− [pexp t,pexp v]) o

294+ [pexp t,pexp v])

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

296296 otherPats arg = return Placeholder

297297

298− ops fc n xs o

298+ ops fc n xs

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

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

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

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

303303 case lookupCtxt tyn (idris_datatypes i) of

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

305305 _ -> [p]

306− ops fc n arg o = return Placeholder

306+ ops fc n arg = return Placeholder

307307

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

309309 getExpTm t = getTm t

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

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

566566 = do ctxt <- getContext

567567 i <- getIState

568568 let lhs = addImplPat i lhs_in

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

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

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

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

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

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

577577 processTacticDecls info newDecls

578578 sendHighlighting highlights

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

580− let lhs_tm = orderPats (getInferTerm lhs')

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

582− OK _ -> return True

583− err -> return False

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

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

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

588+ return True

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

590+ return False

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

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

586593 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

542542 return (App s f' a')

543543 getPats t = return t

544544

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 = [

274274 ( 14, ANY ),

275275 ( 15, ANY ),

276276 ( 16, ANY ),

277− ( 17, ANY )]),

277+ ( 17, ANY ),

278+ ( 18, ANY )]),

278279 ("tutorial", "Tutorial examples",

279280 [ ( 1, ANY ),

280281 ( 2, ANY ),

test/interfaces002/interfaces002.idr+2

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

11import Data.Vect

3+%default total

35interface ArrayM where

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

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

3+%default total

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