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