ea88b5e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better choice of pattern to inspect in coverage

Add an 'Inferred' marker to TT, for building coverage trees only, which means that patterns which were inferred by the machine rather than written by the user are split later. This means that the coverage checker will generate cases from user-written terms first, which generally leads to more patterns being ruled out sooner.

commitea88b5eeef8d9d0edf369a397bfbe3e744e0a4f9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 3 Dec 2016, 16:16 (10 years ago) parent7c95173

12 files changed+146−7

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+1 src/Idris/Core/CaseTree.hs+40−2 src/Idris/Core/Evaluate.hs+1 src/Idris/Core/Execute.hs+1 src/Idris/Core/TT.hs+9 src/Idris/Core/WHNF.hs+1 src/Idris/Coverage.hs+5−3 src/Idris/Delaborate.hs+1 src/Idris/Elab/Clause.hs+1−1 src/Idris/Reflection.hs+5 test/regression001/coverage001.idr+79 test/regression001/run+2−1

src/Idris/Core/Binary.hs+1

@@ -639,6 +639,7 @@ instance {- (Binary n) => -} Binary (TT Name) where

639639 TType x1 -> do putWord8 7

640640 put x1

641641 Impossible -> putWord8 8

642+ Inferred x1 -> put x1 -- drop the 'Inferred'

642643 UType x1 -> do putWord8 10

643644 put x1

644645 get

src/Idris/Core/CaseTree.hs+40−2

@@ -349,6 +349,7 @@ isConstType _ _ = False

349349

350350data Pat = PCon Bool Name Int [Pat]

351351 | PConst Const

352+ | PInferred Pat

352353 | PV Name Type

353354 | PSuc Pat -- special case for n+1 on Integer

354355 | PReflected Name [Pat]

@@ -387,6 +388,7 @@ toPat reflect tc = map $ toPat' []

387388

388389 toPat' [] (P Bound n ty) = PV n ty

389390 toPat' args (App _ f a) = toPat' (a : args) f

391+ toPat' args (Inferred tm) = PInferred (toPat' args tm)

390392 toPat' [] (Constant x) | isTypeConst x = PTyPat

391393 | otherwise = PConst x

392394

@@ -502,6 +504,41 @@ order phase ns' cs cans

502504 numNames xs (_ : ps) = numNames xs ps

503505 numNames xs [] = length xs

504506

507+-- Reorder the patterns in the clause so that the PInferred patterns come

508+-- last. Also strip 'PInferred' from the top level patterns so that we can

509+-- go ahead and match.

510+orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])

511+orderByInf vs cs = let alwaysInf = getInf cs in

512+ (selectInf alwaysInf vs,

513+ map deInf (map (selectExp alwaysInf) cs))

514+ where

515+ getInf [] = []

516+ getInf [(pats, def)] = infPos 0 pats

517+ getInf ((pats, def) : cs) = infPos 0 pats `intersect` getInf cs

518+

519+ selectExp :: [Int] -> Clause -> Clause

520+ selectExp infs (pats, def)

521+ = let (notInf, inf) = splitPats 0 infs [] [] pats in

522+ (notInf ++ inf, def)

523+

524+ selectInf :: [Int] -> [a] -> [a]

525+ selectInf infs ns = let (notInf, inf) = splitPats 0 infs [] [] ns in

526+ notInf ++ inf

527+

528+ splitPats i infpos notInf inf [] = (reverse notInf, reverse inf)

529+ splitPats i infpos notInf inf (p : ps)

530+ | i `elem` infpos = splitPats (i + 1) infpos notInf (p : inf) ps

531+ | otherwise = splitPats (i + 1) infpos (p : notInf) inf ps

532+

533+ infPos i [] = []

534+ infPos i (PInferred p : ps) = i : infPos (i + 1) ps

535+ infPos i (_ : ps) = infPos (i + 1) ps

536+

537+ deInf (pats, def) = (map deInfPat pats, def)

538+

539+ deInfPat (PInferred p) = p

540+ deInfPat p = p

541+

505542match :: [Name] -> [Clause] -> SC -- error case

506543 -> CaseBuilder SC

507544match [] (([], ret) : xs) err

@@ -510,8 +547,9 @@ match [] (([], ret) : xs) err

510547 case snd ret of

511548 Impossible -> return ImpossibleCase

512549 tm -> return $ STerm tm -- run out of arguments

513−match vs cs err = do let ps = partition cs

514− mixture vs ps err

550+match vs cs err = do let (vs', de_inf) = orderByInf vs cs

551+ ps = partition de_inf

552+ mixture vs' ps err

515553

516554mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC

517555mixture vs [] err = return err

src/Idris/Core/Evaluate.hs+1

@@ -366,6 +366,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

366366 ev ntimes stk top env (Constant c) = return $ VConstant c

367367 ev ntimes stk top env Erased = return VErased

368368 ev ntimes stk top env Impossible = return VImpossible

369+ ev ntimes stk top env (Inferred tm) = ev ntimes stk top env tm

369370 ev ntimes stk top env (TType i) = return $ VType i

370371 ev ntimes stk top env (UType u) = return $ VUType u

371372

src/Idris/Core/Execute.hs+1

@@ -212,6 +212,7 @@ doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

212212 doExec env ctxt ((x:xs) !! i)

213213doExec env ctxt Erased = return EErased

214214doExec env ctxt Impossible = fail "Tried to execute an impossible case"

215+doExec env ctxt (Inferred t) = doExec env ctxt t

215216doExec env ctxt (TType u) = return (EType u)

216217doExec env ctxt (UType u) = return (EUType u)

217218

src/Idris/Core/TT.hs+9

@@ -1008,6 +1008,9 @@ data TT n = P NameType n (TT n) -- ^ named references with type

10081008 -- (-1) is a special case for 'subtract one from BI'

10091009 | Erased -- ^ an erased term

10101010 | Impossible -- ^ special case for totality checking

1011+ | Inferred (TT n) -- ^ For building case trees when coverage checkimg only.

1012+ -- Marks a term as being inferred by the machine, rather than

1013+ -- given by the programmer

10111014 | TType UExp -- ^ the type of types at some level

10121015 | UType Universe -- ^ Uniqueness type universe (disjoint from TType)

10131016 deriving (Ord, Functor, Data, Generic, Typeable)

@@ -1055,6 +1058,7 @@ instance Sized a => Sized (TT a) where

10551058 size (TType u) = 1 + size u

10561059 size (Proj a _) = 1 + size a

10571060 size Impossible = 1

1061+ size (Inferred t) = size t

10581062 size (UType u) = 1 + size u

10591063

10601064instance Pretty a o => Pretty (TT a) o where

@@ -1379,6 +1383,7 @@ termSmallerThan x (V i) = True

13791383termSmallerThan x (Constant c) = True

13801384termSmallerThan x Erased = True

13811385termSmallerThan x Impossible = True

1386+termSmallerThan x (Inferred t) = termSmallerThan x t

13821387termSmallerThan x (TType u) = True

13831388termSmallerThan x (UType u) = True

13841389

@@ -1421,6 +1426,7 @@ safeForgetEnv env (UType u) = Just $ RUType u

14211426safeForgetEnv env Erased = Just $ RConstant Forgot

14221427safeForgetEnv env (Proj tm i) = error "Don't know how to forget a projection"

14231428safeForgetEnv env Impossible = error "Don't know how to forget Impossible"

1429+safeForgetEnv env (Inferred t) = safeForgetEnv env t

14241430

14251431-- | Introduce a 'Bind' into the given term for each element of the

14261432-- given list of (name, binder) pairs.

@@ -1583,6 +1589,7 @@ prettyEnv env t = prettyEnv' env t False

15831589 prettySe p env Erased debug = text "[_]"

15841590 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)

15851591 prettySe p env Impossible debug = text "Impossible"

1592+ prettySe p env (Inferred tm) debug = text "<" <+> prettySe p env tm debug <+> text ">"

15861593 prettySe p env (UType u) debug = text (show u)

15871594

15881595 -- Render a `Binder` and its name

@@ -1628,6 +1635,7 @@ showEnv' env t dbg = se 10 env t where

16281635 se p env (Constant c) = show c

16291636 se p env Erased = "[__]"

16301637 se p env Impossible = "[impossible]"

1638+ se p env (Inferred t) = "<" ++ se p env t ++ ">"

16311639 se p env (TType i) = "Type " ++ show i

16321640 se p env (UType u) = show u

16331641

@@ -1736,6 +1744,7 @@ pprintTT bound tm = pp startPrec bound tm

17361744 text "!" <> text (show i)

17371745 pp p bound Erased = text "<<<erased>>>"

17381746 pp p bound Impossible = text "<<<impossible>>>"

1747+ pp p bound (Inferred t) = text "<" <+> pp p bound t <+> text ">"

17391748 pp p bound (TType ue) = annotate (AnnType "Type" "The type of types") $

17401749 text "Type"

17411750 pp p bound (UType u) = text (show u)

src/Idris/Core/WHNF.hs+1

@@ -107,6 +107,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

107107

108108 eval env stk Erased = unload WErased stk

109109 eval env stk Impossible = unload WImpossible stk

110+ eval env stk (Inferred tm) = eval env stk tm

110111 eval env stk (TType u) = unload (WType u) stk

111112 eval env stk (UType u) = unload (WUType u) stk

112113

src/Idris/Coverage.hs+5−3

@@ -73,7 +73,8 @@ genClauses fc n lhs_tms given

7373

7474 let lhs_given = zipWith removePlaceholders lhs_tms

7575 (map (stripUnmatchable i) (map flattenArgs given))

76−

76+

77+ logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map show (lhs_given))

7778 let givenpos = mergePos (map getGivenPos given)

7879

7980 (cns, ctree_in) <-

@@ -118,9 +119,10 @@ mergePos [x] = x

118119mergePos (x : xs) = intersect x (mergePos xs)

119120

120121removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)

121−removePlaceholders (ns, tm) ptm = (ns, tm, Erased) -- rp tm ptm, Erased)

122+removePlaceholders (ns, tm) ptm = (ns, rp tm ptm, Erased)

122123 where

123− rp tm Placeholder = Erased

124+ rp Erased Placeholder = Erased

125+ rp tm Placeholder = Inferred tm

124126 rp tm (PApp _ pf pargs)

125127 | (tf, targs) <- unApply tm

126128 = let tf' = rp tf pf

src/Idris/Delaborate.hs+1

@@ -173,6 +173,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

173173 de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

174174 de env _ Erased = Placeholder

175175 de env _ Impossible = Placeholder

176+ de env _ (Inferred t) = Placeholder

176177 de env _ (TType i) = PType un

177178 de env _ (UType u) = PUniverse un u

178179

src/Idris/Elab/Clause.hs+1−1

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

597597 err -> do logElab 10 $ "Conversion failure"

598598 return Nothing

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

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

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

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

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

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

src/Idris/Reflection.hs+5

@@ -491,6 +491,9 @@ reflectTTQuotePattern unq Erased

491491reflectTTQuotePattern unq Impossible

492492 = lift . tfail . InternalMsg $

493493 "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."

494+reflectTTQuotePattern unq (Inferred t)

495+ = lift . tfail . InternalMsg $

496+ "Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."

494497reflectTTQuotePattern unq (TType exp)

495498 = do ue <- getNameFrom (sMN 0 "uexp")

496499 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

@@ -654,6 +657,8 @@ reflectTTQuote _ (Proj _ _) =

654657reflectTTQuote unq Erased = Var (reflm "Erased")

655658reflectTTQuote _ Impossible =

656659 error "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."

660+reflectTTQuote _ (Inferred tm) =

661+ error "Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."

657662

658663reflectRawQuote :: [Name] -> Raw -> Raw

659664reflectRawQuote unq (Var n)

test/regression001/coverage001.idrnew file+79

@@ -0,0 +1,79 @@

1+module Data.AVL.Tree

3+%default total

4+%access export

6+data Balance : Nat -> Nat -> Type where

7+ LHeavy : Balance (S n) n

8+ RHeavy : Balance n (S n)

9+ Balanced : Balance n n

10+

11+%name Balance b, bal

12+

13+height : Balance n m -> Nat

14+height b = S (height' b)

15+ where

16+ height' : Balance n m -> Nat

17+ height' (LHeavy {n}) = S n

18+ height' (RHeavy {n}) = S n

19+ height' {n} (Balanced {n}) = n

20+

21+public export

22+data Tree : (keyTy : Type) -> (valTy : Type) -> Type

23+ where

24+ ||| An empty Tree node.

25+ Empty : Tree k v

26+

27+ Node : (key : k)

28+ -> (val : v)

29+ -> (left : Tree k v)

30+ -> (right : Tree k v)

31+ -> Tree k v

32+

33+%name Tree t, tree

34+

35+public export

36+data AVLInvariant : (height : Nat)

37+ -> (tree : Tree k v)

38+ -> Type

39+ where

40+ AVLEmpty : AVLInvariant 0 Empty

41+

42+ AVLNode : (left : AVLInvariant n l) ->

43+ (right : AVLInvariant m r) ->

44+ (b : Balance n m) ->

45+ AVLInvariant (height b) (Node k v l r)

46+

47+%name AVLInvariant inv

48+

49+public export

50+AVLTree : (height : Nat) -> (keyTy : Type) -> (valueTy : Type) -> Type

51+AVLTree n k v = Subset (Tree k v) (AVLInvariant n)

52+

53+-- --------------------------------------------------------------- [ Rotations ]

54+private

55+data InsertRes : Nat -> (k : Type) -> Type -> Type where

56+ Same : AVLTree n k v -> InsertRes n k v

57+ Grew : AVLTree (S n) k v -> InsertRes n k v

58+

59+%name InsertRes res, r

60+

61+private

62+runInsertRes : InsertRes n k v -> (n : Nat ** AVLTree n k v)

63+runInsertRes (Same t) = (_ ** t)

64+runInsertRes (Grew t) = (_ ** t)

65+

66+||| Perform a Left roation.

67+private

68+rotLeft : k

69+ -> v

70+ -> AVLTree n k v

71+ -> AVLTree (S (S n)) k v

72+ -> InsertRes (S (S n)) k v

73+-- Impossible because Empty has depth 0 and we know the depth is at least 2 from the type

74+rotLeft key val l (Element Empty AVLEmpty) impossible

75+rotLeft key val (Element l invl) (Element (Node key' val' rl rr) (AVLNode invrl invrr Balanced)) = ?rl1

76+rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr LHeavy) invrr LHeavy)) = ?rl2

77+rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr RHeavy) invrr LHeavy)) = ?rl3

78+rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr Balanced) invrr LHeavy)) = ?rl4

79+rotLeft key val (Element l invl) (Element (Node key' val' rl rr) (AVLNode invrl invrr RHeavy)) = ?rl5

test/regression001/run+2−1

@@ -3,7 +3,8 @@ ${IDRIS:-idris} $@ --check \

33 reg001.idr reg036.idr reg037.idr reg038.idr reg046.idr \

44 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \

55 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \

6− reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr

6+ reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \

7+ coverage001.idr

89${IDRIS:-idris} $@ --check \

910 eff001.idr -p effects