git.iko.soy/Idris-dev
on 717e854 help sign in
Idris-dev/src/Idris/Coverage.hs
364 lines 15 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 where
11import Idris.AbsSyntax
12import Idris.Core.CaseTree
13import Idris.Core.Evaluate
14import Idris.Core.TT
15import Idris.Delaborate
16import Idris.Error
17import Idris.Output (iWarn, iputStrLn)
19import Control.Monad.State.Strict
20import Data.Char
21import Data.Either
22import Data.List
23import Data.Maybe
24import Debug.Trace
26-- | Generate a pattern from an 'impossible' LHS.
27--
28-- We need this to eliminate the pattern clauses which have been
29-- provided explicitly from new clause generation.
30mkPatTm :: PTerm -> Idris Term
31mkPatTm t = do i <- getIState
32 let timp = addImpl' True [] [] [] i t
33 evalStateT (toTT (mapPT deNS timp)) 0
34 where
35 toTT (PRef _ _ n) = do i <- lift getIState
36 case lookupNameDef n (tt_ctxt i) of
37 [(n', TyDecl nt _)] -> return $ P nt n' Erased
38 _ -> return $ P Ref n Erased
39 toTT (PApp _ t args) = do t' <- toTT t
40 args' <- mapM (toTT . getTm) args
41 return $ mkApp t' args'
42 toTT (PDPair _ _ _ l _ r) = do l' <- toTT l
43 r' <- toTT r
44 return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
45 toTT (PPair _ _ _ l r) = do l' <- toTT l
46 r' <- toTT r
47 return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
48 -- For alternatives, pick the first and drop the namespaces. It doesn't
49 -- really matter which is taken since matching will ignore the namespace.
50 toTT (PAlternative _ _ (a : as)) = toTT a
51 toTT _ = do v <- get
52 put (v + 1)
53 return (P Bound (sMN v "imp") Erased)
55 deNS (PRef f hl (NS n _)) = PRef f hl n
56 deNS t = t
58-- | Given a list of LHSs, generate a extra clauses which cover the remaining
59-- cases. The ones which haven't been provided are marked 'absurd' so
60-- that the checker will make sure they can't happen.
61--
62-- This will only work after the given clauses have been typechecked and the
63-- names are fully explicit!
64genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
65genClauses fc n xs given
66 = do i <- getIState
67 let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs
68 -- if a placeholder was given, don't bother generating cases for it
69 let lhs_tms' = zipWith mergePlaceholders lhs_tms
70 (map (stripUnmatchable i) (map flattenArgs given))
71 let lhss = map pUnApply lhs_tms'
72 nty <- case lookupTyExact n (tt_ctxt i) of
73 Just t -> return (normalise (tt_ctxt i) [] t)
74 _ -> fail "Can't happen - genClauses, lookupTyExact"
76 let argss = transpose lhss
77 let all_args = map (genAll i) (zip (genPH i nty) argss)
78 logCoverage 5 $ "COVERAGE of " ++ show n
79 logCoverage 5 $ "using type " ++ show nty
80 logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)
82 logCoverage 5 $ show (lhs_tms, lhss)
83 logCoverage 5 $ "Args are: " ++ show argss
84 logCoverage 5 $ show (map length argss) ++ "\nAll args:\n" ++ show (map length all_args)
85 logCoverage 10 $ "All args are: " ++ show all_args
86 logCoverage 3 $ "Original: \n" ++
87 showSep "\n" (map (\t -> showTmImpls (delab' i t True True)) xs)
88 -- add an infinite supply of explicit arguments to update the possible
89 -- cases for (the return type may be variadic, or function type, so
90 -- there may be more case splitting that the idris_implicits record
91 -- suggests)
92 let parg = case lookupCtxt n (idris_implicits i) of
93 (p : _) ->
94 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
95 _ -> repeat (pexp Placeholder)
96 let tryclauses = mkClauses parg all_args
97 logCoverage 3 $ show (length tryclauses) ++ " initially to check"
98 logCoverage 2 $ showSep "\n" (map (showTm i) tryclauses)
100 let xsdelab = map (\x -> stripUnmatchable i (delab' i x True True)) xs
101 let new = filter (noMatch i xsdelab) tryclauses
102 logCoverage 2 $ show (length new) ++ " clauses to check for impossibility"
103 logCoverage 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
104-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
105 return new
106-- return (map (\t -> PClause n t [] PImpossible []) new)
107 where getLHS i term
108 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
109 | otherwise = []
111 -- if an argument has a non-concrete type (i.e. it's a function
112 -- that calculates something from a previous argument) we'll also
113 -- need to generate a placeholder pattern for it since it could be
114 -- anything based on earlier values
115 genPH :: IState -> Type -> [Bool]
116 genPH ist (Bind n (Pi _ ty _) sc) = notConcrete ist ty : genPH ist sc
117 genPH ist ty = []
119 notConcrete ist t | (P _ n _, args) <- unApply t,
120 not (isConName n (tt_ctxt ist)) = True
121 notConcrete _ _ = False
123 pUnApply (PApp _ f args) = map getTm args
124 pUnApply _ = []
126 flattenArgs (PApp fc (PApp _ f as) as')
127 = flattenArgs (PApp fc f (as ++ as'))
128 flattenArgs t = t
130 -- Return whether the given clause matches none of the input clauses
131 -- (xs)
132 noMatch i xs tm = all (\x -> case matchClause i x tm of
133 Right ms -> False
134 Left miss -> True) xs
137 mergePlaceholders :: PTerm -> PTerm -> PTerm
138 mergePlaceholders x Placeholder = Placeholder
139 mergePlaceholders (PApp fc f args) (PApp fc' f' args')
140 = PApp fc' f' (zipWith mergePArg args args')
141 where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in
142 x { getTm = xtm}
143 mergePlaceholders x _ = x
145 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
146 mkClauses parg args
147 | all (== [Placeholder]) args = []
148 mkClauses parg args
149 = do args' <- mkArg args
150 let tm = PApp fc (PRef fc [] n) (zipWith upd args' parg)
151 return tm
152 where
153 mkArg :: [[PTerm]] -> [[PTerm]]
154 mkArg [] = return []
155 mkArg (a : as) = do a' <- a
156 as' <- mkArg as
157 return (a':as')
159-- | Does this error result rule out a case as valid when coverage checking?
160validCoverageCase :: Context -> Err -> Bool
161validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
162 = let topx' = normalise ctxt [] topx
163 topy' = normalise ctxt [] topy in
164 not (sameFam topx' topy' || not (validCoverageCase ctxt e))
165 where sameFam topx topy
166 = case (unApply topx, unApply topy) of
167 ((P _ x _, _), (P _ y _, _)) -> x == y
168 _ -> False
169validCoverageCase ctxt (InfiniteUnify _ _ _) = False
170validCoverageCase ctxt (CantConvert _ _ _) = False
171validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
172validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e
173validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e
174validCoverageCase ctxt _ = True
176-- | Check whether an error is recoverable in the sense needed for
177-- coverage checking.
178recoverableCoverage :: Context -> Err -> Bool
179recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
180 = let topx' = normalise ctxt [] topx
181 topy' = normalise ctxt [] topy in
182 r || checkRec topx' topy'
183 where -- different notion of recoverable than in unification, since we
184 -- have no metavars -- just looking to see if a constructor is failing
185 -- to unify with a function that may be reduced later
186 checkRec (App _ f a) p@(P _ _ _) = checkRec f p
187 checkRec p@(P _ _ _) (App _ f a) = checkRec p f
188 checkRec fa@(App _ _ _) fa'@(App _ _ _)
189 | (f, as) <- unApply fa,
190 (f', as') <- unApply fa'
191 = if (length as /= length as')
192 then checkRec f f'
193 else checkRec f f' && and (zipWith checkRec as as')
194 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
195 checkRec _ _ = False
197 ntRec x y | Ref <- x = True
198 | Ref <- y = True
199 | (Bound, Bound) <- (x, y) = True
200 | otherwise = False -- name is different, unrecoverable
201recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
202recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
203recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
204recoverableCoverage _ _ = False
206genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
207genAll i (addPH, args)
208 = case filter (/=Placeholder) $ fnub $ mergePHs $ fnub (concatMap otherPats (fnub args)) of
209 [] -> [Placeholder]
210 xs -> ph xs
211 where
212 -- Add a placeholder - this is to account for the case where an argument
213 -- has a dependent type calculated from another argument, to make sure that
214 -- all dependencies are covered. If they are, any generated case will
215 -- match given cases.
216 -- (Also this helps when checking, because if we eliminate the placeholder
217 -- quickly then lots of other cases get ruled out fast)
218 ph ts = if addPH then Placeholder : ts else ts
220 -- Merge patterns with placeholders in other patterns, to ensure we've
221 -- covered all possible generated cases
222 -- e.g. if we have (True, _) (False, _) (_, True) (_, False)
223 -- we should merge these to get (True, True), (False, False)
224 -- (False, True) and (True, False)
225 mergePHs :: [PTerm] -> [PTerm]
226 mergePHs xs = mergePHs' xs xs
228 mergePHs' [] all = []
229 mergePHs' (x : xs) all = mergePH x all ++ mergePHs' xs all
231 mergePH :: PTerm -> [PTerm] -> [PTerm]
232 mergePH tm [] = []
233 mergePH tm (x : xs)
234 | Just merged <- mergePTerm tm x = merged : mergePH tm xs
235 | otherwise = mergePH tm xs
237 mergePTerm :: PTerm -> PTerm -> Maybe PTerm
238 mergePTerm x Placeholder = Just x
239 mergePTerm Placeholder x = Just x
240 mergePTerm tm@(PRef fc1 hl1 n1) (PRef fc2 hl2 n2)
241 | n1 == n2 = Just tm
242 mergePTerm (PPair fc1 hl1 p1 x1 y1) (PPair fc2 hl2 p2 x2 y2)
243 = do x <- mergePTerm x1 x2
244 y <- mergePTerm y1 y2
245 Just (PPair fc1 hl1 p1 x y)
246 mergePTerm (PDPair fc1 hl1 p1 x1 t1 y1) (PDPair fc2 hl2 p2 x2 t2 y2)
247 = do x <- mergePTerm x1 x2
248 y <- mergePTerm y1 y2
249 t <- mergePTerm t1 t2
250 Just (PDPair fc1 hl1 p1 x t y)
251 mergePTerm (PApp fc1 f1 args1) (PApp fc2 f2 args2)
252 = do fm <- mergePTerm f1 f2
253 margs <- mergeArgs args1 args2
254 Just (PApp fc1 fm margs)
255 where
256 mergeArgs [] [] = Just []
257 mergeArgs (a : as) (b : bs)
258 = do ma_in <- mergePTerm (getTm a) (getTm b)
259 let ma = a { getTm = ma_in }
260 mas <- mergeArgs as bs
261 Just (ma : mas)
262 mergeArgs _ _ = Nothing
263 mergePTerm x y | x == y = Just x
264 | otherwise = Nothing
266 -- for every constant in a term (at any level) take next one to make sure
267 -- that constants which are not explicitly handled are covered
268 nextConst (PConstant fc c) = PConstant NoFC (nc' c)
269 nextConst o = o
271 nc' (I c) = I (c + 1)
272 nc' (BI c) = BI (c + 1)
273 nc' (Fl c) = Fl (c + 1)
274 nc' (B8 c) = B8 (c + 1)
275 nc' (B16 c) = B16 (c + 1)
276 nc' (B32 c) = B32 (c + 1)
277 nc' (B64 c) = B64 (c + 1)
278 nc' (Ch c) = Ch (chr $ ord c + 1)
279 nc' (Str c) = Str (c ++ "'")
280 nc' o = o
282 otherPats :: PTerm -> [PTerm]
283 otherPats (PRef fc hl n) = ph $ ops fc n []
284 otherPats (PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs
285 otherPats (PPair fc hls _ l r)
286 = ph $ ops fc pairCon
287 ([pimp (sUN "A") Placeholder True,
288 pimp (sUN "B") Placeholder True] ++
289 [pexp l, pexp r])
290 otherPats (PDPair fc hls p t _ v)
291 = ph $ ops fc sigmaCon
292 ([pimp (sUN "a") Placeholder True,
293 pimp (sUN "P") Placeholder True] ++
294 [pexp t,pexp v])
295 otherPats o@(PConstant _ c) = ph [o, nextConst o]
296 otherPats arg = return Placeholder
298 ops fc n xs
299 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
300 = do xs' <- mapM otherPats (map getExpTm xs)
301 let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))
302 let tyn = getTy n (tt_ctxt i)
303 case lookupCtxt tyn (idris_datatypes i) of
304 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
305 _ -> [p]
306 ops fc n arg = return Placeholder
308 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
309 getExpTm t = getTm t
311 -- put it back to its original form
312 resugar (PApp _ (PRef fc hl n) [_,_,t,v])
313 | n == sigmaCon
314 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
315 resugar (PApp _ (PRef fc hl n) [_,_,l,r])
316 | n == pairCon
317 = PPair fc [] IsTerm (getTm l) (getTm r)
318 resugar t = t
320 dropForce force (x : xs) i | i `elem` force
321 = upd Placeholder x : dropForce force xs (i + 1)
322 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
323 dropForce _ [] _ = []
326 getTy n ctxt = case lookupTy n ctxt of
327 (t : _) -> case unApply (getRetTy t) of
328 (P _ tyn _, _) -> tyn
329 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
330 _ -> error "Can't happen getTy 2"
332 mkPat fc x = case lookupCtxt x (idris_implicits i) of
333 (pargs : _)
334 -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)
335 _ -> error "Can't happen - genAll"
337 fnub :: [PTerm] -> [PTerm]
338 fnub xs = fnub' [] xs
340 fnub' :: [PTerm] -> [PTerm] -> [PTerm]
341 fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
342 | otherwise = fnub' (x : acc) xs
343 fnub' acc [] = acc
345 -- quick check for constructor equality
346 quickEq :: PTerm -> PTerm -> Bool
347 quickEq (PConstant _ n) (PConstant _ n') = n == n'
348 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
349 quickEq (PPair _ _ _ l r) (PPair _ _ _ l' r') = quickEq l l' && quickEq r r'
350 quickEq (PApp _ t as) (PApp _ t' as')
351 | length as == length as'
352 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
353 quickEq Placeholder Placeholder = True
354 quickEq x y = False
356 qelem :: PTerm -> [PTerm] -> Bool
357 qelem x [] = False
358 qelem x (y : ys) | x `quickEq` y = True
359 | otherwise = qelem x ys
362upd :: t -> PArg' t -> PArg' t
363upd p' p = p { getTm = p' }