git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Coverage.hs
480 lines 20 kB history raw
1{-|
2Module : Idris.Coverage
3Description : Clause generation for coverage checking
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE FlexibleContexts, 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.Elab.Utils
18import Idris.Error
20import Control.Monad.State.Strict
21import Data.Char
22import Data.List
23import Data.Maybe
25-- | Generate a pattern from an 'impossible' LHS.
26--
27-- We need this to eliminate the pattern clauses which have been
28-- provided explicitly from new clause generation.
29--
30-- This takes a type directed approach to disambiguating names. If we
31-- can't immediately disambiguate by looking at the expected type, it's an
32-- error (we can't do this the usual way of trying it to see what type checks
33-- since the whole point of an impossible case is that it won't type check!)
34mkPatTm :: PTerm -> Idris Term
35mkPatTm t = do i <- getIState
36 let timp = addImpl' True [] [] [] i t
37 evalStateT (toTT Nothing timp) 0
38 where
39 toTT :: Maybe Type -> PTerm -> StateT Int Idris Term
40 toTT ty (PRef _ _ n)
41 = do i <- lift getIState
42 case lookupDefExact n (tt_ctxt i) of
43 Just (TyDecl nt _) -> return $ P nt n Erased
44 _ -> return $ P Ref n Erased
45 toTT ty (PApp _ t@(PRef _ _ n) args)
46 = do i <- lift getIState
47 let aTys = case lookupTyExact n (tt_ctxt i) of
48 Just nty -> map (Just . snd) (getArgTys nty)
49 Nothing -> map (const Nothing) args
50 args' <- zipWithM toTT aTys (map getTm args)
51 t' <- toTT Nothing t
52 return $ mkApp t' args'
53 toTT ty (PApp _ t args)
54 = do t' <- toTT Nothing t
55 args' <- mapM (toTT Nothing . getTm) args
56 return $ mkApp t' args'
57 toTT ty (PDPair _ _ _ l _ r)
58 = do l' <- toTT Nothing l
59 r' <- toTT Nothing r
60 return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
61 toTT ty (PPair _ _ _ l r)
62 = do l' <- toTT Nothing l
63 r' <- toTT Nothing r
64 return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
65 -- For alternatives, pick the first and drop the namespaces. It doesn't
66 -- really matter which is taken since matching will ignore the namespace.
67 toTT (Just ty) (PAlternative _ _ as)
68 | (hd, _) <- unApply ty
69 = do i <- lift getIState
70 case pruneByType True [] hd ty i as of
71 [a] -> toTT (Just ty) a
72 _ -> lift $ ierror $ CantResolveAlts (map getAltName as)
73 toTT Nothing (PAlternative _ _ as)
74 = lift $ ierror $ CantResolveAlts (map getAltName as)
75 toTT ty _
76 = do v <- get
77 put (v + 1)
78 return (P Bound (sMN v "imp") Erased)
80 getAltName (PApp _ (PRef _ _ (UN l)) [_, _, arg])
81 | l == txt "Delay" = getAltName (getTm arg)
82 getAltName (PApp _ (PRef _ _ n) _) = n
83 getAltName (PRef _ _ n) = n
84 getAltName (PApp _ h _) = getAltName h
85 getAltName (PHidden h) = getAltName h
86 getAltName x = sUN "_" -- should never happen here
88-- | Given a list of LHSs, generate a extra clauses which cover the remaining
89-- cases. The ones which haven't been provided are marked 'absurd' so
90-- that the checker will make sure they can't happen.
91--
92-- This will only work after the given clauses have been typechecked and the
93-- names are fully explicit!
94genClauses :: FC -> Name -> [([Name], Term)] -> -- (Argument names, LHS)
95 [PTerm] -> Idris [PTerm]
96-- No clauses (only valid via elab reflection). We should probably still do
97-- a check here somehow, e.g. that one of the arguments is an obviously
98-- empty type. In practice, this should only really be used for Void elimination.
99genClauses fc n lhs_tms [] = return []
100genClauses fc n lhs_tms given
101 = do i <- getIState
103 let lhs_given = zipWith removePlaceholders lhs_tms
104 (map (stripUnmatchable i) (map flattenArgs given))
106 logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map showTmImpls given)
107 logCoverage 10 $ "Building coverage tree for:\n" ++ showSep "\n" (map show lhs_given)
108 logCoverage 10 $ "From terms:\n" ++ showSep "\n" (map show lhs_tms)
109 let givenpos = mergePos (map getGivenPos given)
111 (cns, ctree_in) <-
112 case simpleCase False (UnmatchedCase "Undefined") False
113 (CoverageCheck givenpos) emptyFC [] []
114 lhs_given
115 (const []) of
116 OK (CaseDef cns ctree_in _) ->
117 return (cns, ctree_in)
118 Error e -> tclift $ tfail $ At fc e
120 let ctree = trimOverlapping (addMissingCons i ctree_in)
121 let (coveredas, missingas) = mkNewClauses (tt_ctxt i) n cns ctree
122 let covered = map (\t -> delab' i t True True) coveredas
123 let missing = filter (\x -> x `notElem` covered) $
124 map (\t -> delab' i t True True) missingas
126 logCoverage 5 $ "Coverage from case tree for " ++ show n ++ ": " ++ show ctree
127 logCoverage 2 $ show (length missing) ++ " missing clauses for " ++ show n
128 logCoverage 3 $ "Missing clauses:\n" ++ showSep "\n"
129 (map showTmImpls missing)
130 logCoverage 10 $ "Covered clauses:\n" ++ showSep "\n"
131 (map showTmImpls covered)
132 return missing
133 where
134 flattenArgs (PApp fc (PApp _ f as) as')
135 = flattenArgs (PApp fc f (as ++ as'))
136 flattenArgs t = t
138getGivenPos :: PTerm -> [Int]
139getGivenPos (PApp _ _ pargs) = getGiven 0 (map getTm pargs)
140 where
141 getGiven i (Placeholder : tms) = getGiven (i + 1) tms
142 getGiven i (_ : tms) = i : getGiven (i + 1) tms
143 getGiven i [] = []
144getGivenPos _ = []
146-- Return a list of Ints which are in every list
147mergePos :: [[Int]] -> [Int]
148mergePos [] = []
149mergePos [x] = x
150mergePos (x : xs) = intersect x (mergePos xs)
152removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
153removePlaceholders (ns, tm) ptm = (ns, rp tm ptm, Erased)
154 where
155 rp Erased Placeholder = Erased
156 rp tm Placeholder = Inferred tm
157 rp tm (PApp _ pf pargs)
158 | (tf, targs) <- unApply tm
159 = let tf' = rp tf pf
160 targs' = zipWith rp targs (map getTm pargs) in
161 mkApp tf' targs'
162 rp tm (PPair _ _ _ pl pr)
163 | (tf, [tyl, tyr, tl, tr]) <- unApply tm
164 = let tl' = rp tl pl
165 tr' = rp tr pr in
166 mkApp tf [Erased, Erased, tl', tr']
167 rp tm (PDPair _ _ _ pl pt pr)
168 | (tf, [tyl, tyr, tl, tr]) <- unApply tm
169 = let tl' = rp tl pl
170 tr' = rp tr pr in
171 mkApp tf [Erased, Erased, tl', tr']
172 rp tm _ = tm
174mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
175mkNewClauses ctxt fn ns sc
176 = (map (mkPlApp (P Ref fn Erased)) $
177 mkFromSC True (map (\n -> P Ref n Erased) ns) sc,
178 map (mkPlApp (P Ref fn Erased)) $
179 mkFromSC False (map (\n -> P Ref n Erased) ns) sc)
180 where
181 mkPlApp f args = mkApp f (map erasePs args)
183 erasePs ap@(App t f a)
184 | (f, args) <- unApply ap = mkApp f (map erasePs args)
185 erasePs (P _ n _) | not (isConName n ctxt) = Erased
186 erasePs tm = tm
188 mkFromSC cov args sc = evalState (mkFromSC' cov args sc) []
190 mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]
191 mkFromSC' cov args (STerm _)
192 = if cov then return [args] else return [] -- leaf of provided case
193 mkFromSC' cov args (UnmatchedCase _)
194 = if cov then return [] else return [args] -- leaf of missing case
195 mkFromSC' cov args ImpossibleCase = return []
196 mkFromSC' cov args (Case _ x alts)
197 = do done <- get
198 if (args `elem` done)
199 then return []
200 else do alts' <- mapM (mkFromAlt cov args x) alts
201 put (args : done)
202 return (concat alts')
203 mkFromSC' cov args _ = return [] -- Should never happen
205 mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> State [[Term]] [[Term]]
206 mkFromAlt cov args x (ConCase c t conargs sc)
207 = let argrep = mkApp (P (DCon t (length args) False) c Erased)
208 (map (\n -> P Ref n Erased) conargs)
209 args' = map (subst x argrep) args in
210 mkFromSC' cov args' sc
211 mkFromAlt cov args x (ConstCase c sc)
212 = let argrep = Constant c
213 args' = map (subst x argrep) args in
214 mkFromSC' cov args' sc
215 mkFromAlt cov args x (DefaultCase sc)
216 = mkFromSC' cov args sc
217 mkFromAlt cov _ _ _ = return []
219-- Modify the generated case tree (the case tree builder doesn't have access
220-- to the context, so can't do this itself).
221-- Replaces any missing cases with explicit cases for the missing constructors
222addMissingCons :: IState -> SC -> SC
223addMissingCons ist sc = evalState (addMissingConsSt ist sc) 0
225addMissingConsSt :: IState -> SC -> State Int SC
226addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)
227 where
228 addMissingAlt :: CaseAlt -> State Int CaseAlt
229 addMissingAlt (ConCase n i ns sc)
230 = liftM (ConCase n i ns) (addMissingConsSt ist sc)
231 addMissingAlt (FnCase n ns sc)
232 = liftM (FnCase n ns) (addMissingConsSt ist sc)
233 addMissingAlt (ConstCase c sc)
234 = liftM (ConstCase c) (addMissingConsSt ist sc)
235 addMissingAlt (SucCase n sc)
236 = liftM (SucCase n) (addMissingConsSt ist sc)
237 addMissingAlt (DefaultCase sc)
238 = liftM DefaultCase (addMissingConsSt ist sc)
240 addMissingAlts argn as
241-- | any hasDefault as = map addMissingAlt as
242 | cons@(n:_) <- mapMaybe collectCons as,
243 Just tyn <- getConType n,
244 Just ti <- lookupCtxtExact tyn (idris_datatypes ist)
245 -- If we've fallen through on this argument earlier, then the
246 -- things which were matched in other cases earlier can't be missing
247 -- cases now
248 = let missing = con_names ti \\ cons in
249 do as' <- addCases missing as
250 mapM addMissingAlt as'
251 | consts@(n:_) <- mapMaybe collectConsts as
252 = let missing = nub (map nextConst consts) \\ consts in
253 mapM addMissingAlt (addCons missing as)
254 addMissingAlts n as = mapM addMissingAlt as
256 addCases missing [] = return []
257 addCases missing (DefaultCase rhs : rest)
258 = do missing' <- mapM (genMissingAlt rhs) missing
259 return (mapMaybe id missing' ++ rest)
260 addCases missing (c : rest)
261 = liftM (c :) $ addCases missing rest
263 addCons missing [] = []
264 addCons missing (DefaultCase rhs : rest)
265 = map (genMissingConAlt rhs) missing ++ rest
266 addCons missing (c : rest) = c : addCons missing rest
268 genMissingAlt rhs n
269 | Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)
270 = do name <- get
271 put (name + arity)
272 let args = map (name +) [0..arity-1]
273 return $ Just $ ConCase n tag (map (\i -> sMN i "m") args) rhs
274 | otherwise = return Nothing
276 genMissingConAlt rhs n = ConstCase n rhs
278 collectCons (ConCase n i args sc) = Just n
279 collectCons _ = Nothing
281 collectConsts (ConstCase c sc) = Just c
282 collectConsts _ = Nothing
284 getConType n = do ty <- lookupTyExact n (tt_ctxt ist)
285 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of
286 (P _ tyn _, _) -> Just tyn
287 _ -> Nothing
289 -- for every constant in a term (at any level) take next one to make sure
290 -- that constants which are not explicitly handled are covered
291 nextConst (I c) = I (c + 1)
292 nextConst (BI c) = BI (c + 1)
293 nextConst (Fl c) = Fl (c + 1)
294 nextConst (B8 c) = B8 (c + 1)
295 nextConst (B16 c) = B16 (c + 1)
296 nextConst (B32 c) = B32 (c + 1)
297 nextConst (B64 c) = B64 (c + 1)
298 nextConst (Ch c) = Ch (chr $ ord c + 1)
299 nextConst (Str c) = Str (c ++ "'")
300 nextConst o = o
302addMissingConsSt ist sc = return sc
304trimOverlapping :: SC -> SC
305trimOverlapping sc = trim [] [] sc
306 where
307 trim :: [(Name, (Name, [Name]))] -> -- Variable - constructor+args already matched
308 [(Name, [Name])] -> -- Variable - constructors which it can't be
309 SC -> SC
310 trim mustbes nots (Case t vn alts)
311 | Just (c, args) <- lookup vn mustbes
312 = Case t vn (trimAlts mustbes nots vn (substMatch (c, args) alts))
313 | Just cantbe <- lookup vn nots
314 = let alts' = filter (notConMatch cantbe) alts in
315 Case t vn (trimAlts mustbes nots vn alts')
316 | otherwise = Case t vn (trimAlts mustbes nots vn alts)
317 trim cs nots sc = sc
319 trimAlts cs nots vn [] = []
320 trimAlts cs nots vn (ConCase cn t args sc : rest)
321 = ConCase cn t args (trim (addMatch vn (cn, args) cs) nots sc) :
322 trimAlts cs (addCantBe vn cn nots) vn rest
323 trimAlts cs nots vn (FnCase n ns sc : rest)
324 = FnCase n ns (trim cs nots sc) : trimAlts cs nots vn rest
325 trimAlts cs nots vn (ConstCase c sc : rest)
326 = ConstCase c (trim cs nots sc) : trimAlts cs nots vn rest
327 trimAlts cs nots vn (SucCase n sc : rest)
328 = SucCase n (trim cs nots sc) : trimAlts cs nots vn rest
329 trimAlts cs nots vn (DefaultCase sc : rest)
330 = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest
332 substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]
333 substMatch ca [] = []
334 substMatch (c,args) (ConCase cn t args' sc : _)
335 | c == cn = [ConCase c t args (substNames (zip args' args) sc)]
336 substMatch ca (_:cs) = substMatch ca cs
338 substNames [] sc = sc
339 substNames ((n, n') : ns) sc
340 = substNames ns (substSC n n' sc)
342 notConMatch cs (ConCase cn t args sc) = cn `notElem` cs
343 notConMatch cs _ = True
345 addMatch vn cn cs = (vn, cn) : cs
347 addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
348 addCantBe vn cn [] = [(vn, [cn])]
349 addCantBe vn cn ((n, cbs) : nots)
350 | vn == n = ((n, nub (cn : cbs)) : nots)
351 | otherwise = ((n, cbs) : addCantBe vn cn nots)
353-- | Does this error result rule out a case as valid when coverage checking?
354validCoverageCase :: Context -> Err -> Bool
355validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
356 = let topx' = normalise ctxt [] topx
357 topy' = normalise ctxt [] topy in
358 not (sameFam topx' topy' || not (validCoverageCase ctxt e))
359 where sameFam topx topy
360 = case (unApply topx, unApply topy) of
361 ((P _ x _, _), (P _ y _, _)) -> x == y
362 _ -> False
363validCoverageCase ctxt (InfiniteUnify _ _ _) = False
364validCoverageCase ctxt (CantConvert topx topy _)
365 = let topx' = normalise ctxt [] topx
366 topy' = normalise ctxt [] topy in
367 not (sameFam topx' topy')
368 where sameFam topx topy
369 = case (unApply topx, unApply topy) of
370 ((P _ x _, _), (P _ y _, _)) -> x == y
371 _ -> False
372validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
373validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e
374validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e
375validCoverageCase ctxt _ = True
377-- | Check whether an error is recoverable in the sense needed for
378-- coverage checking.
379recoverableCoverage :: Context -> Err -> Bool
380recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
381 = let topx' = normalise ctxt [] topx
382 topy' = normalise ctxt [] topy in
383 evalState (checkRec topx' topy') []
384recoverableCoverage ctxt (CantConvert topx topy _)
385 = let topx' = normalise ctxt [] topx
386 topy' = normalise ctxt [] topy in
387 evalState (checkRec topx' topy') []
388recoverableCoverage ctxt (InfiniteUnify _ _ _) = False -- always unrecoverable
389recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
390recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
391recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
392recoverableCoverage _ _ = False
394-- different notion of recoverable than in unification, since we
395-- have no metavars -- just looking to see if a constructor is failing
396-- to unify with a function that may be reduced later, or if any
397-- variables need to have two different constructor forms
399-- The state is a mapping of name to what it has failed to unify
400-- with
401checkRec :: Term -> Term -> State [(Name, Term)] Bool
402checkRec (P Bound x _) tm
403 | isCon tm = do nmap <- get
404 case lookup x nmap of
405 Nothing -> do put ((x, tm) : nmap)
406 return True
407 Just y' -> checkRec tm y'
408 where
409 isCon tm
410 | (P yt _ _, _) <- unApply tm,
411 conType yt = True
412 isCon (Constant _) = True
413 isCon _ = False
415 conType (DCon _ _ _) = True
416 conType (TCon _ _) = True
417 conType _ = False
419checkRec tm (P Bound y _)
420 | isCon tm = do nmap <- get
421 case lookup y nmap of
422 Nothing -> do put ((y, tm) : nmap)
423 return True
424 Just x' -> checkRec tm x'
425 where
426 isCon tm
427 | (P yt _ _, _) <- unApply tm,
428 conType yt = True
429 isCon (Constant _) = True
430 isCon _ = False
432 conType (DCon _ _ _) = True
433 conType (TCon _ _) = True
434 conType _ = False
436checkRec (App _ f a) p@(P _ _ _) = checkRec f p
437checkRec (App _ f a) p@(Constant _) = checkRec f p
438checkRec p@(P _ _ _) (App _ f a) = checkRec p f
439checkRec p@(Constant _) (App _ f a) = checkRec p f
440checkRec fa@(App _ _ _) fa'@(App _ _ _)
441 | (f, as) <- unApply fa,
442 (f', as') <- unApply fa'
443 = if (length as /= length as')
444 then checkRec f f'
445 -- Same function but different args is recoverable,
446 -- and vice versa, if it's an ordinary function
447 -- If a constructor, everything has to be recoverable
448 else do fok <- checkRec f f'
449 argok <- checkRecs (f : as) (f : as')
450 return (if conType f then fok && argok
451 else fok || argok)
452 where
453 checkRecs [] [] = return True
454 checkRecs (a : as) (b : bs) = do aok <- checkRec a b
455 asok <- checkRecs as bs
456 return (aok && asok)
457 conType (P (DCon _ _ _) _ _) = True
458 conType (P (TCon _ _) _ _) = True
459 conType (Constant _) = True
460 conType _ = False
462checkRec (P xt x _) (P yt y _)
463 | x == y = return True
464 | ntRec xt yt = return True
465 where
466 -- If either name is a reference or a bound variable, then further
467 -- development may fix the error, so consider it recoverable.
468 -- If both names are constructors, and the name is different, then
469 -- it's not recoverable
470 ntRec x y | Ref <- x = True
471 | Ref <- y = True
472 | Bound <- x = True
473 | Bound <- y = True
474 | otherwise = False -- name is different, unrecoverable
475-- A function reference against a constant might be recoverable if we get to
476-- reduce the function
477checkRec (P Ref _ _) (Constant _) = return True
478checkRec (Constant _) (P Ref _ _) = return True
479checkRec (TType _) (TType _) = return True
480checkRec _ _ = return False