git.iko.soy/Idris-dev
on b817deb help sign in
Idris-dev/src/Idris/Coverage.hs
375 lines 16 kB history raw
1{-|
2Module : Idris.Coverage
3Description : Clause generation for coverage checking
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
9module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
10 mkPatTm) where
12import Idris.AbsSyntax
13import Idris.Core.CaseTree
14import Idris.Core.Evaluate
15import Idris.Core.TT
16import Idris.Delaborate
17import Idris.Error
18import Idris.Output (iWarn, iputStrLn)
20import Control.Monad.State.Strict
21import Data.Char
22import Data.Either
23import Data.List
24import Data.Maybe
25import Debug.Trace
27-- | Generate a pattern from an 'impossible' LHS.
28--
29-- We need this to eliminate the pattern clauses which have been
30-- provided explicitly from new clause generation.
31mkPatTm :: PTerm -> Idris Term
32mkPatTm t = do i <- getIState
33 let timp = addImpl' True [] [] [] i t
34 evalStateT (toTT (mapPT deNS timp)) 0
35 where
36 toTT (PRef _ _ n) = do i <- lift getIState
37 case lookupNameDef n (tt_ctxt i) of
38 [(n', TyDecl nt _)] -> return $ P nt n' Erased
39 _ -> return $ P Ref n Erased
40 toTT (PApp _ t args) = do t' <- toTT t
41 args' <- mapM (toTT . getTm) args
42 return $ mkApp t' args'
43 toTT (PDPair _ _ _ l _ r) = do l' <- toTT l
44 r' <- toTT r
45 return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
46 toTT (PPair _ _ _ l r) = do l' <- toTT l
47 r' <- toTT r
48 return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
49 -- For alternatives, pick the first and drop the namespaces. It doesn't
50 -- really matter which is taken since matching will ignore the namespace.
51 toTT (PAlternative _ _ (a : as)) = toTT a
52 toTT _ = do v <- get
53 put (v + 1)
54 return (P Bound (sMN v "imp") Erased)
56 deNS (PRef f hl (NS n _)) = PRef f hl n
57 deNS t = t
59-- | Given a list of LHSs, generate a extra clauses which cover the remaining
60-- cases. The ones which haven't been provided are marked 'absurd' so
61-- that the checker will make sure they can't happen.
62--
63-- This will only work after the given clauses have been typechecked and the
64-- names are fully explicit!
65genClauses :: FC -> Name -> [([Name], Term)] -> -- (Argument names, LHS)
66 [PTerm] -> Idris [PTerm]
67-- No clauses (only valid via elab reflection). We should probably still do
68-- a check here somehow, e.g. that one of the arguments is an obviously
69-- empty type. In practice, this should only really be used for Void elimination.
70genClauses fc n lhs_tms [] = return []
71genClauses fc n lhs_tms given
72 = do i <- getIState
74 let lhs_given = zipWith removePlaceholders lhs_tms
75 (map (stripUnmatchable i) (map flattenArgs given))
77 logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map show (lhs_given))
78 let givenpos = mergePos (map getGivenPos given)
80 (cns, ctree_in) <-
81 case simpleCase False (UnmatchedCase "Undefined") False
82 (CoverageCheck givenpos) emptyFC [] []
83 lhs_given
84 (const []) of
85 OK (CaseDef cns ctree_in _) ->
86 return (cns, ctree_in)
87 Error e -> tclift $ tfail $ At fc e
89 let ctree = trimOverlapping (addMissingCons i ctree_in)
90 let (coveredas, missingas) = mkNewClauses (tt_ctxt i) n cns ctree
91 let covered = map (\t -> delab' i t True True) coveredas
92 let missing = filter (\x -> x `notElem` covered) $
93 map (\t -> delab' i t True True) missingas
95 logCoverage 5 $ "Coverage from case tree for " ++ show n ++ ": " ++ show ctree
96 logCoverage 2 $ show (length missing) ++ " missing clauses for " ++ show n
97 logCoverage 3 $ "Missing clauses:\n" ++ showSep "\n"
98 (map showTmImpls missing)
99 logCoverage 10 $ "Covered clauses:\n" ++ showSep "\n"
100 (map showTmImpls covered)
101 return missing
102 where
103 flattenArgs (PApp fc (PApp _ f as) as')
104 = flattenArgs (PApp fc f (as ++ as'))
105 flattenArgs t = t
107getGivenPos :: PTerm -> [Int]
108getGivenPos (PApp _ _ pargs) = getGiven 0 (map getTm pargs)
109 where
110 getGiven i (Placeholder : tms) = getGiven (i + 1) tms
111 getGiven i (_ : tms) = i : getGiven (i + 1) tms
112 getGiven i [] = []
113getGivenPos _ = []
115-- Return a list of Ints which are in every list
116mergePos :: [[Int]] -> [Int]
117mergePos [] = []
118mergePos [x] = x
119mergePos (x : xs) = intersect x (mergePos xs)
121removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
122removePlaceholders (ns, tm) ptm = (ns, rp tm ptm, Erased)
123 where
124 rp Erased Placeholder = Erased
125 rp tm Placeholder = Inferred tm
126 rp tm (PApp _ pf pargs)
127 | (tf, targs) <- unApply tm
128 = let tf' = rp tf pf
129 targs' = zipWith rp targs (map getTm pargs) in
130 mkApp tf' targs'
131 rp tm (PPair _ _ _ pl pr)
132 | (tf, [tyl, tyr, tl, tr]) <- unApply tm
133 = let tl' = rp tl pl
134 tr' = rp tr pr in
135 mkApp tf [Erased, Erased, tl', tr']
136 rp tm (PDPair _ _ _ pl pt pr)
137 | (tf, [tyl, tyr, tl, tr]) <- unApply tm
138 = let tl' = rp tl pl
139 tr' = rp tr pr in
140 mkApp tf [Erased, Erased, tl', tr']
141 rp tm _ = tm
143mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
144mkNewClauses ctxt fn ns sc
145 = (map (mkPlApp (P Ref fn Erased)) $
146 mkFromSC True (map (\n -> P Ref n Erased) ns) sc,
147 map (mkPlApp (P Ref fn Erased)) $
148 mkFromSC False (map (\n -> P Ref n Erased) ns) sc)
149 where
150 mkPlApp f args = mkApp f (map erasePs args)
152 erasePs ap@(App t f a)
153 | (f, args) <- unApply ap = mkApp f (map erasePs args)
154 erasePs (P _ n _) | not (isConName n ctxt) = Erased
155 erasePs tm = tm
157 mkFromSC cov args sc = evalState (mkFromSC' cov args sc) []
159 mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]
160 mkFromSC' cov args (STerm _)
161 = if cov then return [args] else return [] -- leaf of provided case
162 mkFromSC' cov args (UnmatchedCase _)
163 = if cov then return [] else return [args] -- leaf of missing case
164 mkFromSC' cov args ImpossibleCase = return []
165 mkFromSC' cov args (Case _ x alts)
166 = do done <- get
167 if (args `elem` done)
168 then return []
169 else do alts' <- mapM (mkFromAlt cov args x) alts
170 put (args : done)
171 return (concat alts')
172 mkFromSC' cov args _ = return [] -- Should never happen
174 mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> State [[Term]] [[Term]]
175 mkFromAlt cov args x (ConCase c t conargs sc)
176 = let argrep = mkApp (P (DCon t (length args) False) c Erased)
177 (map (\n -> P Ref n Erased) conargs)
178 args' = map (subst x argrep) args in
179 mkFromSC' cov args' sc
180 mkFromAlt cov args x (ConstCase c sc)
181 = let argrep = Constant c
182 args' = map (subst x argrep) args in
183 mkFromSC' cov args' sc
184 mkFromAlt cov args x (DefaultCase sc)
185 = mkFromSC' cov args sc
186 mkFromAlt cov _ _ _ = return []
188-- Modify the generated case tree (the case tree builder doesn't have access
189-- to the context, so can't do this itself).
190-- Replaces any missing cases with explicit cases for the missing constructors
191addMissingCons :: IState -> SC -> SC
192addMissingCons ist sc = evalState (addMissingConsSt ist sc) 0
194addMissingConsSt :: IState -> SC -> State Int SC
195addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)
196 where
197 addMissingAlt :: CaseAlt -> State Int CaseAlt
198 addMissingAlt (ConCase n i ns sc)
199 = liftM (ConCase n i ns) (addMissingConsSt ist sc)
200 addMissingAlt (FnCase n ns sc)
201 = liftM (FnCase n ns) (addMissingConsSt ist sc)
202 addMissingAlt (ConstCase c sc)
203 = liftM (ConstCase c) (addMissingConsSt ist sc)
204 addMissingAlt (SucCase n sc)
205 = liftM (SucCase n) (addMissingConsSt ist sc)
206 addMissingAlt (DefaultCase sc)
207 = liftM DefaultCase (addMissingConsSt ist sc)
209 addMissingAlts argn as
210-- | any hasDefault as = map addMissingAlt as
211 | cons@(n:_) <- mapMaybe collectCons as,
212 Just tyn <- getConType n,
213 Just ti <- lookupCtxtExact tyn (idris_datatypes ist)
214 -- If we've fallen through on this argument earlier, then the
215 -- things which were matched in other cases earlier can't be missing
216 -- cases now
217 = let missing = con_names ti \\ cons in
218 do as' <- addCases missing as
219 mapM addMissingAlt as'
220 | consts@(n:_) <- mapMaybe collectConsts as
221 = let missing = nub (map nextConst consts) \\ consts in
222 mapM addMissingAlt (addCons missing as)
223 addMissingAlts n as = mapM addMissingAlt as
225 addCases missing [] = return []
226 addCases missing (DefaultCase rhs : rest)
227 = do missing' <- mapM (genMissingAlt rhs) missing
228 return (mapMaybe id missing' ++ rest)
229 addCases missing (c : rest)
230 = liftM (c :) $ addCases missing rest
232 addCons missing [] = []
233 addCons missing (DefaultCase rhs : rest)
234 = map (genMissingConAlt rhs) missing ++ rest
235 addCons missing (c : rest) = c : addCons missing rest
237 genMissingAlt rhs n
238 | Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)
239 = do name <- get
240 put (name + arity)
241 let args = map (name +) [0..arity-1]
242 return $ Just $ ConCase n tag (map (\i -> sMN i "m") args) rhs
243 | otherwise = return Nothing
245 genMissingConAlt rhs n = ConstCase n rhs
247 collectCons (ConCase n i args sc) = Just n
248 collectCons _ = Nothing
250 collectConsts (ConstCase c sc) = Just c
251 collectConsts _ = Nothing
253 hasDefault (DefaultCase (UnmatchedCase _)) = False
254 hasDefault (DefaultCase _) = True
255 hasDefault _ = False
257 getConType n = do ty <- lookupTyExact n (tt_ctxt ist)
258 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of
259 (P _ tyn _, _) -> Just tyn
260 _ -> Nothing
262 -- for every constant in a term (at any level) take next one to make sure
263 -- that constants which are not explicitly handled are covered
264 nextConst (I c) = I (c + 1)
265 nextConst (BI c) = BI (c + 1)
266 nextConst (Fl c) = Fl (c + 1)
267 nextConst (B8 c) = B8 (c + 1)
268 nextConst (B16 c) = B16 (c + 1)
269 nextConst (B32 c) = B32 (c + 1)
270 nextConst (B64 c) = B64 (c + 1)
271 nextConst (Ch c) = Ch (chr $ ord c + 1)
272 nextConst (Str c) = Str (c ++ "'")
273 nextConst o = o
275addMissingConsSt ist sc = return sc
277trimOverlapping :: SC -> SC
278trimOverlapping sc = trim [] [] sc
279 where
280 trim :: [(Name, (Name, [Name]))] -> -- Variable - constructor+args already matched
281 [(Name, [Name])] -> -- Variable - constructors which it can't be
282 SC -> SC
283 trim mustbes nots (Case t vn alts)
284 | Just (c, args) <- lookup vn mustbes
285 = Case t vn (trimAlts mustbes nots vn (substMatch (c, args) alts))
286 | Just cantbe <- lookup vn nots
287 = let alts' = filter (notConMatch cantbe) alts in
288 Case t vn (trimAlts mustbes nots vn alts')
289 | otherwise = Case t vn (trimAlts mustbes nots vn alts)
290 trim cs nots sc = sc
292 trimAlts cs nots vn [] = []
293 trimAlts cs nots vn (ConCase cn t args sc : rest)
294 = ConCase cn t args (trim (addMatch vn (cn, args) cs) nots sc) :
295 trimAlts cs (addCantBe vn cn nots) vn rest
296 trimAlts cs nots vn (FnCase n ns sc : rest)
297 = FnCase n ns (trim cs nots sc) : trimAlts cs nots vn rest
298 trimAlts cs nots vn (ConstCase c sc : rest)
299 = ConstCase c (trim cs nots sc) : trimAlts cs nots vn rest
300 trimAlts cs nots vn (SucCase n sc : rest)
301 = SucCase n (trim cs nots sc) : trimAlts cs nots vn rest
302 trimAlts cs nots vn (DefaultCase sc : rest)
303 = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest
305 isConMatch c (ConCase cn t args sc) = c == cn
306 isConMatch _ _ = False
308 substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]
309 substMatch ca [] = []
310 substMatch (c,args) (ConCase cn t args' sc : _)
311 | c == cn = [ConCase c t args (substNames (zip args' args) sc)]
312 substMatch ca (_:cs) = substMatch ca cs
314 substNames [] sc = sc
315 substNames ((n, n') : ns) sc
316 = substNames ns (substSC n n' sc)
318 notConMatch cs (ConCase cn t args sc) = cn `notElem` cs
319 notConMatch cs _ = True
321 addMatch vn cn cs = (vn, cn) : cs
323 addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
324 addCantBe vn cn [] = [(vn, [cn])]
325 addCantBe vn cn ((n, cbs) : nots)
326 | vn == n = ((n, nub (cn : cbs)) : nots)
327 | otherwise = ((n, cbs) : addCantBe vn cn nots)
329-- | Does this error result rule out a case as valid when coverage checking?
330validCoverageCase :: Context -> Err -> Bool
331validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
332 = let topx' = normalise ctxt [] topx
333 topy' = normalise ctxt [] topy in
334 not (sameFam topx' topy' || not (validCoverageCase ctxt e))
335 where sameFam topx topy
336 = case (unApply topx, unApply topy) of
337 ((P _ x _, _), (P _ y _, _)) -> x == y
338 _ -> False
339validCoverageCase ctxt (InfiniteUnify _ _ _) = False
340validCoverageCase ctxt (CantConvert _ _ _) = False
341validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
342validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e
343validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e
344validCoverageCase ctxt _ = True
346-- | Check whether an error is recoverable in the sense needed for
347-- coverage checking.
348recoverableCoverage :: Context -> Err -> Bool
349recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
350 = let topx' = normalise ctxt [] topx
351 topy' = normalise ctxt [] topy in
352 checkRec topx' topy'
353 where -- different notion of recoverable than in unification, since we
354 -- have no metavars -- just looking to see if a constructor is failing
355 -- to unify with a function that may be reduced later
356 checkRec (App _ f a) p@(P _ _ _) = checkRec f p
357 checkRec p@(P _ _ _) (App _ f a) = checkRec p f
358 checkRec fa@(App _ _ _) fa'@(App _ _ _)
359 | (f, as) <- unApply fa,
360 (f', as') <- unApply fa'
361 = if (length as /= length as')
362 then checkRec f f'
363 else checkRec f f' && and (zipWith checkRec as as')
364 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
365 checkRec _ _ = False
367 ntRec x y | Ref <- x = True
368 | Ref <- y = True
369 | (Bound, Bound) <- (x, y) = True
370 | otherwise = False -- name is different, unrecoverable
371recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
372recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
373recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
374recoverableCoverage _ _ = False