git.iko.soy/Idris-dev
on master help sign in
Coverage checker

Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverage

commit1112fe49b2152cdfc8174bdb255923e908811cd5 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 12 Jan 2012, 11:34 (15 years ago) parent3f18d02
12 files changed+189−47
compare with master
unifiedsplit
lib/prelude/vect.idr+3 src/Core/CaseTree.hs+26−23 src/Core/Evaluate.hs+4−3 src/Core/TT.hs+6 src/Idris/AbsSyntax.hs+18−2 src/Idris/Compiler.hs+8 src/Idris/Coverage.hs+89−3 src/Idris/DataOpts.hs+7 src/Idris/ElabDecls.hs+22−13 src/Idris/IBC.hs+1−1 src/Idris/Prover.hs+2−2 src/Main.hs+3
lib/prelude/vect.idr+3
@@ -11,6 +11,9 @@ data Vect : Set -> Nat -> Set where
1111 Nil : Vect a O
1212 (::) : a -> Vect a k -> Vect a (S k)
1313
14+tail : Vect a (S n) -> Vect a n
15+tail (x :: xs) = xs
16+
1417lookup : Fin n -> Vect a n -> a
1518lookup fO (x :: xs) = x
1619lookup (fS k) (x :: xs) = lookup k xs
src/Core/CaseTree.hs+26−23
@@ -34,13 +34,18 @@ small :: SC -> Bool
3434-- small (STerm t) = True
3535small _ = False
3636
37−simpleCase :: Bool -> [(Term, Term)] -> CaseDef
38−simpleCase tc [] = CaseDef [] (UnmatchedCase "No pattern clauses")
39−simpleCase tc cs = let pats = map (\ (l, r) -> (toPats tc l, r)) cs
37+simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef
38+simpleCase tc cover []
39+ = CaseDef [] (UnmatchedCase "No pattern clauses")
40+simpleCase tc cover cs
41+ = let pats = map (\ (l, r) -> (toPats tc l, r)) cs
4042 numargs = length (fst (head pats))
41− ns = take numargs args in
42− CaseDef ns (evalState (match ns pats (UnmatchedCase "Error")) numargs)
43+ ns = take numargs args
44+ tree = evalState (match ns pats (defaultCase cover)) numargs in
45+ CaseDef ns (prune tree)
4346 where args = map (\i -> MN i "e") [0..]
47+ defaultCase True = STerm Erased
48+ defaultCase False = UnmatchedCase "Error"
4449
4550data Pat = PCon Name Int [Pat]
4651 | PConst Const
@@ -193,21 +198,19 @@ varRule (v : vs) alts err =
193198 repVar v (PV p : ps , res) = (ps, subst p (P Bound v (V 0)) res)
194199 repVar v (PAny : ps , res) = (ps, res)
195200
196−{-
197−mkOperator :: CaseDef -> [Value] -> Maybe Value
198−mkOperator (CaseDef ns casetree) args
199− | length args /= length ns = Nothing
200− | otherwise = evalArgs (zip ns args) casetree
201− where
202− evalArgs map (Case n alts) =
203− do v <- lookup n map
204− (altmap, tm) <- findAlt (getValArgs v) alts map
205− evalArgs altmap tm
206− evalArgs map (STerm tm) =
207− evalArgs map (UnmatchedCase _) = Nothing
208−
209− getValArgs tm = getValArgs' tm []
210− getValArgs' (VApp f a) as = getValArgs' f (a:as)
211− getValArgs' f as = (f, as)
212−
213−-}
201+prune :: SC -> SC
202+prune (Case n alts)
203+ = let alts' = map pruneAlt $
204+ filter notErased alts in
205+ case alts' of
206+ [] -> STerm Erased
207+ as -> Case n as
208+ where pruneAlt (ConCase n i ns sc) = ConCase n i ns (prune sc)
209+ pruneAlt (ConstCase c sc) = ConstCase c (prune sc)
210+ pruneAlt (DefaultCase sc) = DefaultCase (prune sc)
211+
212+ notErased (DefaultCase (STerm Erased)) = False
213+ notErased _ = True
214+prune t = t
215+
216+
src/Core/Evaluate.hs+4−3
@@ -522,12 +522,13 @@ addDatatype (Data n tag ty cons) uctxt
522522 addCons (tag+1) cons (addDef n
523523 (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)
524524
525−addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->
525+addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->
526526 Type -> Context -> Context
527−addCasedef n alwaysInline tcase ps psrt ty uctxt
527+addCasedef n alwaysInline tcase covering ps psrt ty uctxt
528528 = let ctxt = definitions uctxt
529529 ps' = ps -- simpl ps in
530− ctxt' = case (simpleCase tcase ps', simpleCase tcase psrt) of
530+ ctxt' = case (simpleCase tcase covering ps',
531+ simpleCase tcase covering psrt) of
531532 (CaseDef args sc, CaseDef args' sc') ->
532533 let inl = alwaysInline in
533534 addDef n (CaseOp inl ty ps args sc args' sc',
src/Core/TT.hs+6
@@ -449,6 +449,12 @@ getArgTys :: TT n -> [(n, TT n)]
449449getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
450450getArgTys _ = []
451451
452+getRetTy :: TT n -> TT n
453+getRetTy (Bind n (PVar _) sc) = getRetTy sc
454+getRetTy (Bind n (PVTy _) sc) = getRetTy sc
455+getRetTy (Bind n (Pi _) sc) = getRetTy sc
456+getRetTy sc = sc
457+
452458uniqueName :: Name -> [Name] -> Name
453459uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
454460 | otherwise = n
src/Idris/AbsSyntax.hs+18−2
@@ -20,13 +20,14 @@ import qualified Epic.Epic as E
2020data IOption = IOption { opt_logLevel :: Int,
2121 opt_typecase :: Bool,
2222 opt_typeintype :: Bool,
23+ opt_coverage :: Bool,
2324 opt_showimp :: Bool,
2425 opt_repl :: Bool,
2526 opt_verbose :: Bool
2627 }
2728 deriving (Show, Eq)
2829
29−defaultOpts = IOption 0 False False False True True
30+defaultOpts = IOption 0 False False True False True True
3031
3132-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
3233-- without typechecking).
@@ -245,6 +246,16 @@ setTypeInType t = do i <- get
245246 let opt' = opts { opt_typeintype = t }
246247 put (i { idris_options = opt' })
247248
249+coverage :: Idris Bool
250+coverage = do i <- get
251+ return (opt_coverage (idris_options i))
252+
253+setCoverage :: Bool -> Idris ()
254+setCoverage t = do i <- get
255+ let opts = idris_options i
256+ let opt' = opts { opt_coverage = t }
257+ put (i { idris_options = opt' })
258+
248259impShow :: Idris Bool
249260impShow = do i <- get
250261 return (opt_showimp (idris_options i))
@@ -1205,6 +1216,9 @@ matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where
12051216 return (mf ++ concat ms)
12061217-- match (PRef _ n) (PRef _ n') | n == n' = return []
12071218-- | otherwise = Nothing
1219+ match (PRef f n) (PApp _ x []) = match (PRef f n) x
1220+ match (PApp _ x []) (PRef f n) = match x (PRef f n)
1221+ match (PRef _ n) (PRef _ n') | n == n' = return []
12081222 match (PRef _ n) tm = return [(n, tm)]
12091223 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
12101224 mr <- match' r r'
@@ -1246,13 +1260,15 @@ matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where
12461260 return (mt ++ mty ++ ms)
12471261 match (PHidden x) (PHidden y) = match' x y
12481262 match Placeholder _ = return []
1263+ match _ Placeholder = return []
12491264 match (PResolveTC _) _ = return []
12501265 match a b | a == b = return []
12511266 | otherwise = LeftErr (a, b)
12521267
12531268 checkRpts (RightOK ms) = check ms where
12541269 check ((n,t):xs)
1255− | Just t' <- lookup n xs = if t/=t' then Left (t, t')
1270+ | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1271+ then Left (t, t')
12561272 else check xs
12571273 check (_:xs) = check xs
12581274 check [] = Right ms
src/Idris/Compiler.hs+8
@@ -168,6 +168,14 @@ instance ToEpic ([Name], SC) where
168168 return $ term (map ename args, tree')
169169
170170instance ToEpic SC where
171+ epic (Case n [ConCase _ i ns sc])
172+ = epicLet n ns 0 sc
173+ where
174+ epicLet x [] _ sc = epic sc
175+ epicLet x (n:ns) i sc
176+ = do sc' <- epicLet x ns (i+1) sc
177+ return $ let_ (ref (ename x) !. i) (ename n, sc')
178+
171179 epic (STerm t) = epic t
172180 epic (UnmatchedCase str) = return $ error_ str
173181 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
src/Idris/Coverage.hs+89−3
@@ -1,11 +1,97 @@
1+{-# LANGUAGE PatternGuards #-}
2+
13module Idris.Coverage where
24
5+import Core.TT
6+import Core.Evaluate
37import Idris.AbsSyntax
8+import Idris.Delaborate
9+
10+import Data.List
11+import Debug.Trace
412
5−-- Given a list of LHSs, generate a complete collection of clauses which cover all
13+-- Given a list of LHSs, generate a extra clauses which cover the remaining
614-- cases. The ones which haven't been provided are marked 'absurd' so that the
715-- checker will make sure they can't happen.
816
9−genClauses :: [PClause] -> [PClause]
10−genClauses xs = xs
17+-- This will only work after the given clauses have been typechecked and the
18+-- names are fully explicit!
19+
20+genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PClause]
21+genClauses fc n xs given
22+ = do i <- getIState
23+ let lhss = map (getLHS i) xs
24+ let argss = transpose lhss
25+ let all_args = map (genAll i) argss
26+ logLvl 7 $ "COVERAGE of " ++ show n
27+ logLvl 10 $ show argss ++ "\n" ++ show all_args
28+ logLvl 10 $ "Original: \n" ++
29+ showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
30+ let parg = case lookupCtxt Nothing n (idris_implicits i) of
31+ (p : _) -> p
32+ _ -> repeat (pexp Placeholder)
33+ let new = mnub i $ filter (noMatch i) $ mkClauses parg all_args
34+ logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
35+ return (map (\t -> PClause n t [] PImpossible []) new)
36+ where getLHS i term
37+ | (f, args) <- unApply term = map (\t -> delab' i t True) args
38+ | otherwise = []
39+
40+ lhsApp (PClause _ l _ _ _) = l
41+ lhsApp (PWith _ l _ _ _) = l
42+
43+ mnub i [] = []
44+ mnub i (x : xs) =
45+ if (any (\t -> case matchClause x t of
46+ Right _ -> True
47+ Left _ -> False) xs) then mnub i xs
48+ else x : mnub i xs
49+
50+ noMatch i tm = all (\x -> case matchClause (delab' i x True) tm of
51+ Right _ -> False
52+ Left miss -> True) xs
53+
54+
55+ mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
56+ mkClauses parg args
57+ = do args' <- mkArg args
58+ let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
59+ return tm
60+ where
61+ mkArg :: [[PTerm]] -> [[PTerm]]
62+ mkArg [] = return []
63+ mkArg (a : as) = do a' <- a
64+ as' <- mkArg as
65+ return (a':as')
66+
67+genAll :: IState -> [PTerm] -> [PTerm]
68+genAll i args = concatMap otherPats (nub args)
69+ where
70+ otherPats :: PTerm -> [PTerm]
71+ otherPats o@(PRef fc n) = ops fc n [] o
72+ otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
73+ otherPats arg = return arg
74+
75+ ops fc n xs o
76+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
77+ = do xs' <- mapM otherPats (map getTm xs)
78+ let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
79+ let tyn = getTy n (tt_ctxt i)
80+ case lookupCtxt Nothing tyn (idris_datatypes i) of
81+ (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])
82+ _ -> [p]
83+ ops fc n arg o = return o
84+
85+ getTy n ctxt = case lookupTy Nothing n ctxt of
86+ (t : _) -> case unApply (getRetTy t) of
87+ (P _ tyn _, _) -> tyn
88+ x -> error $ "Can't happen getTy 1 " ++ show (n, x)
89+ _ -> error "Can't happen getTy 2"
90+
91+ mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of
92+ (pargs : _)
93+ -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
94+ _ -> error "Can't happen - genAll"
95+
96+upd p' p = p { getTm = p' }
1197
src/Idris/DataOpts.hs+7
@@ -45,6 +45,13 @@ forceArgs n t = do let fargs = force 0 t
4545 = mapMaybe isF args ++ concatMap guarded args
4646 guarded t = mapMaybe isF [t]
4747
48+-- Calculate whether a collection of constructors is collapsible
49+
50+collapseCons :: Name -> [(Name, Type)] -> Idris ()
51+collapseCons ty cons =
52+ do i <- getIState
53+ return ()
54+
4855class Optimisable term where
4956 applyOpts :: term -> Idris term
5057
src/Idris/ElabDecls.hs+22−13
@@ -76,6 +76,7 @@ elabData info syn fc (PDatadecl n t_in dcons)
7676 (idris_datatypes i) })
7777 addIBC (IBCDef n)
7878 addIBC (IBCData n)
79+ collapseCons n cons
7980 updateContext (addDatatype (Data n ttag cty cons))
8081
8182elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)
@@ -100,9 +101,8 @@ elabCon info syn (n, t_in, fc)
100101 return (n, cty)
101102
102103elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
103−elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
104− do let cs = genClauses cs_in
105− pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs
104+elabClauses info fc opts n_in cs = let n = liftname info n_in in
105+ do pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs
106106 solveDeferred n
107107 let pats = mapMaybe id pats_in
108108 logLvl 3 (showSep "\n" (map (\ (l,r) ->
@@ -111,9 +111,19 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
111111 ist <- get
112112 let tcase = opt_typecase (idris_options ist)
113113 let pdef = map debind (map (simpl (tt_ctxt ist)) pats)
114+ cov <- coverage
115+ pcover <-
116+ if cov
117+ then idrisCatch
118+ (do missing <- genClauses fc n (map fst pdef) cs
119+ mapM_ (elabClause info fc True) missing
120+ return True)
121+ (\c -> do -- iputStrLn $ "Warning: " ++ show c
122+ return False)
123+ else return False
114124 pdef' <- applyOpts pdef
115− let tree = simpleCase tcase pdef
116− let tree' = simpleCase tcase pdef'
125+ let tree = simpleCase tcase pcover pdef
126+ let tree' = simpleCase tcase pcover pdef'
117127 tclift $ sameLength pdef
118128 logLvl 3 (show tree)
119129 logLvl 3 $ "Optimised: " ++ show tree'
@@ -122,7 +132,7 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
122132 put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })
123133 case lookupTy (namespace info) n ctxt of
124134 [ty] -> do updateContext (addCasedef n (inlinable opts)
125− tcase pdef pdef' ty)
135+ tcase pcover pdef pdef' ty)
126136 addIBC (IBCDef n)
127137 [] -> return ()
128138 where
@@ -160,7 +170,11 @@ elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])
160170 -- if the LHS type checks, it is possible, so report an error
161171 case elaborate ctxt (MN 0 "patLHS") infP []
162172 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of
163− OK _ -> fail $ show fc ++ ":" ++ show lhs ++ " is a possible case"
173+ OK ((lhs', _, _), _) ->
174+ do let lhs_tm = orderPats (getInferTerm lhs')
175+ checkInferred fc (delab' i lhs_tm True) lhs
176+ fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++ " is a possible case"
177+ ++ "\n" ++ showImp True lhs
164178 Error _ -> return ()
165179 return Nothing
166180elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)
@@ -555,11 +569,6 @@ pbty _ tm = tm
555569getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc
556570getPBtys _ = []
557571
558−getRetTy (Bind n (PVar _) sc) = getRetTy sc
559−getRetTy (Bind n (PVTy _) sc) = getRetTy sc
560−getRetTy (Bind n (Pi _) sc) = getRetTy sc
561−getRetTy sc = sc
562−
563572psolve (Bind n (PVar t) sc) = do solve; psolve sc
564573psolve tm = return ()
565574
@@ -617,7 +626,7 @@ checkInferred fc inf user =
617626 do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++
618627 showImp True user
619628 tclift $ case matchClause user inf of
620− Right _ -> return ()
629+ Right vs -> return ()
621630 Left (x, y) -> tfail $ At fc
622631 (Msg $ "The type-checked term and given term do not match: "
623632 ++ show x ++ " and " ++ show y)
src/Idris/IBC.hs+1−1
@@ -22,7 +22,7 @@ import System.Directory
2222import Paths_idris
2323
2424ibcVersion :: Word8
25−ibcVersion = 7
25+ibcVersion = 8
2626
2727data IBCFile = IBCFile { ver :: Word8,
2828 sourcefile :: FilePath,
src/Idris/Prover.hs+2−2
@@ -39,11 +39,11 @@ prove ctxt n ty
3939 iputStrLn $ showProof n prf
4040 i <- get
4141 put (i { last_proof = Just (n, prf) })
42− let tree = simpleCase False [(P Ref n ty, tm)]
42+ let tree = simpleCase False True [(P Ref n ty, tm)]
4343 logLvl 3 (show tree)
4444 (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm
4545 ptm' <- applyOpts ptm
46− updateContext (addCasedef n True False [(P Ref n ty, ptm)]
46+ updateContext (addCasedef n True False True [(P Ref n ty, ptm)]
4747 [(P Ref n ty, ptm')] ty)
4848 solveDeferred n
4949
src/Main.hs+3
@@ -38,6 +38,7 @@ data Opt = Filename String
3838 | Output String
3939 | TypeCase
4040 | TypeInType
41+ | NoCoverage
4142 | Verbose
4243 deriving Eq
4344
@@ -73,6 +74,7 @@ runIdris opts =
7374 makeOption (OLogging i) = setLogLevel i
7475 makeOption TypeCase = setTypeCase True
7576 makeOption TypeInType = setTypeInType True
77+ makeOption NoCoverage = setCoverage False
7678 makeOption _ = return ()
7779
7880getFile :: Opt -> Maybe String
@@ -100,6 +102,7 @@ parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
100102parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
101103parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
102104parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
105+parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)
103106parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
104107parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
105108parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)