ea88b5e · Idris-dev · git.iko.soy

src/Idris/Core/Binary.hs+1

compare with master

unifiedsplit

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

639 TType x1 -> do putWord8 7

640 put x1

641 Impossible -> putWord8 8

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

642 UType x1 -> do putWord8 10

643 UType x1 -> do putWord8 10

643 put x1

644 put x1

644 get

645 get

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

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

349

350data Pat = PCon Bool Name Int [Pat]

351 | PConst Const

352+ | PInferred Pat

352 | PV Name Type

353 | PV Name Type

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

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

354 | PReflected Name [Pat]

355 | PReflected Name [Pat]

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

387

388

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

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

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

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

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

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

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

391 | otherwise = PConst x

393 | otherwise = PConst x

392

394

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

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

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

503 numNames xs [] = length xs

505 numNames xs [] = length xs

504

506

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+

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

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

506 -> CaseBuilder SC

543 -> CaseBuilder SC

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

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

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

510 case snd ret of

547 case snd ret of

511 Impossible -> return ImpossibleCase

548 Impossible -> return ImpossibleCase

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

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

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

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

551+ ps = partition de_inf

514− mixture vs ps err

552+ mixture vs' ps err

515

553

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

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

517mixture vs [] err = return err

555mixture 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

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

367 ev ntimes stk top env Erased = return VErased

368 ev ntimes stk top env Impossible = return VImpossible

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

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

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

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

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

371

372

src/Idris/Core/Execute.hs+1

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

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

213doExec env ctxt Erased = return EErased

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

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

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

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

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

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

217

218

src/Idris/Core/TT.hs+9

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

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

1009 | Erased -- ^ an erased term

1010 | 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

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

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

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

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

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

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

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

1055 size (TType u) = 1 + size u

1058 size (TType u) = 1 + size u

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

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

1057 size Impossible = 1

1060 size Impossible = 1

1061+ size (Inferred t) = size t

1058 size (UType u) = 1 + size u

1062 size (UType u) = 1 + size u

1059

1063

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

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

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

1379termSmallerThan x (Constant c) = True

1383termSmallerThan x (Constant c) = True

1380termSmallerThan x Erased = True

1384termSmallerThan x Erased = True

1381termSmallerThan x Impossible = True

1385termSmallerThan x Impossible = True

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

1382termSmallerThan x (TType u) = True

1387termSmallerThan x (TType u) = True

1383termSmallerThan x (UType u) = True

1388termSmallerThan x (UType u) = True

1384

1389

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

1421safeForgetEnv env Erased = Just $ RConstant Forgot

1426safeForgetEnv env Erased = Just $ RConstant Forgot

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

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

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

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

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

1424

1430

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

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

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

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

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

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

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

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

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

1585 prettySe p env Impossible debug = text "Impossible"

1591 prettySe p env Impossible debug = text "Impossible"

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

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

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

1587

1594

1588 -- Render a `Binder` and its name

1595 -- Render a `Binder` and its name

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

1628 se p env (Constant c) = show c

1635 se p env (Constant c) = show c

1629 se p env Erased = "[__]"

1636 se p env Erased = "[__]"

1630 se p env Impossible = "[impossible]"

1637 se p env Impossible = "[impossible]"

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

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

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

1632 se p env (UType u) = show u

1640 se p env (UType u) = show u

1633

1641

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

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

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

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

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

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

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

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

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

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

1740 text "Type"

1749 text "Type"

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

1750 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

107

108 eval env stk Erased = unload WErased stk

109 eval env stk Impossible = unload WImpossible stk

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

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

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

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

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

112

113

src/Idris/Coverage.hs+5−3

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

73

74 let lhs_given = zipWith removePlaceholders lhs_tms

75 (map (stripUnmatchable i) (map flattenArgs given))

76−

76+

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

77 let givenpos = mergePos (map getGivenPos given)

78 let givenpos = mergePos (map getGivenPos given)

78

79

79 (cns, ctree_in) <-

80 (cns, ctree_in) <-

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

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

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

119

120

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

121removePlaceholders :: ([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)

122 where

123 where

123− rp tm Placeholder = Erased

124+ rp Erased Placeholder = Erased

125+ rp tm Placeholder = Inferred tm

124 rp tm (PApp _ pf pargs)

126 rp tm (PApp _ pf pargs)

125 | (tf, targs) <- unApply tm

127 | (tf, targs) <- unApply tm

126 = let tf' = rp tf pf

128 = let tf' = rp tf pf

src/Idris/Delaborate.hs+1

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

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

174 de env _ Erased = Placeholder

175 de env _ Impossible = Placeholder

176+ de env _ (Inferred t) = Placeholder

176 de env _ (TType i) = PType un

177 de env _ (TType i) = PType un

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

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

178

179

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

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

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

598 return Nothing

599 -- 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)

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

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

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

src/Idris/Reflection.hs+5

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

491reflectTTQuotePattern unq Impossible

492 = lift . tfail . InternalMsg $

493 "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."

494reflectTTQuotePattern unq (TType exp)

497reflectTTQuotePattern unq (TType exp)

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

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

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

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

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

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

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

655reflectTTQuote _ Impossible =

658reflectTTQuote _ Impossible =

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

659 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."

657

662

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

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

659reflectRawQuote unq (Var n)

664reflectRawQuote unq (Var n)

test/regression001/coverage001.idrnew file+79

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

1+module Data.AVL.Tree

2+

3+%default total

4+%access export

5+

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 \

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

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

5 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

7

8

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

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

9 eff001.idr -p effects

10 eff001.idr -p effects