@@ -17,6 +17,7 @@ import Idris.Delaborate
17import Idris.Error
17import Idris.Error
18import Idris.Output (iWarn, iputStrLn)
18import Idris.Output (iWarn, iputStrLn)
20import Data.List
21import Data.List
21import Data.Either
22import Data.Either
22import Data.Maybe
23import Data.Maybe
@@ -203,46 +204,62 @@ recoverableCoverage _ _ = False
204genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
205genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
205genAll i (addPH, args)
206genAll i (addPH, args)
206− = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
207+ = case filter (/=Placeholder) $ fnub $ enrichPats $ fnub (concatMap otherPats (fnub args)) of
207 [] -> [Placeholder]
208 [] -> [Placeholder]
208− xs -> ph $ inventConsts xs
209+ xs -> ph xs
210 ph ts = if addPH then Placeholder : ts else ts
211 ph ts = if addPH then Placeholder : ts else ts
212− -- if they're constants, invent a new one to make sure that
213+ -- for every constant in a term (at any level) take next one to make sure
213− -- constants which are not explicitly handled are covered
214+ -- that constants which are not explicitly handled are covered
214− inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
215+ nextConst (PConstant fc c) = PConstant NoFC (nc' c)
215− where getConst (PConstant _ c) = Just c
216+ nextConst o = o
216− getConst _ = Nothing
217+
217− inventConsts xs = xs
218+ nc' (I c) = I (c + 1)
218−
219+ nc' (BI c) = BI (c + 1)
219− -- try constants until they're not in the list.
220+ nc' (Fl c) = Fl (c + 1)
220− -- FIXME: It is, of course, possible that someone has enumerated all
221+ nc' (B8 c) = B8 (c + 1)
221− -- the constants and matched on them (maybe in generated code) and this
222+ nc' (B16 c) = B16 (c + 1)
222− -- will be really slow. This is sufficiently unlikely that we won't
223+ nc' (B32 c) = B32 (c + 1)
223− -- worry for now...
224+ nc' (B64 c) = B64 (c + 1)
224−
225+ nc' (Ch c) = Ch (chr $ ord c + 1)
225− ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
226+ nc' (Str c) = Str (c ++ "'")
226− ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
227+ nc' o = o
227− ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
228+
228− ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
229+ -- enrich patterns with cartesian products so that
229− ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
230+ -- (True, _) and (_, True) give (True, True)
230− ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
231+ -- with all other combinations to be checked for coverage later
231− ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
232+ enrichPats :: [PTerm] -> [PTerm]
232− ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
233+ enrichPats xs = xs ++ enrichPats' xs
233− ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
234+
234− -- The rest are types with only one case
235+ enrichPats' :: [PTerm] -> [PTerm]
235− ic' xs = xs
236+ enrichPats' [] = []
236−
237+ enrichPats' [x] = [x]
237− firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
238+ enrichPats' (x : xs) = concatMap (combinePHPats x) xs ++ enrichPats' xs
238− | otherwise = x : cs
239+
239−
240+ combinePHPats :: PTerm -> PTerm -> [PTerm]
240− lotsOfNums t = map t [0..]
241+ combinePHPats Placeholder x = [x]
241− lotsOfChars = map Ch ['a'..]
242+ combinePHPats x Placeholder = [x]
242− lotsOfStrings = map Str (map (("some string " ++).show) [1..])
243+ combinePHPats (PPair fc1 hls1 pi1 l1 r1) (PPair fc2 hls2 pi2 l2 r2) =
243−
244+ let ls = enrichPats $ combinePHPats l1 l2
244− nubMap f acc [] = acc
245+ rs = enrichPats $ combinePHPats r1 r2
245− nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
246+ in [ PPair fc1 hls1 pi1 l r | l <- ls, r <- rs]
247+ combinePHPats (PDPair fc1 hls1 p1 t1 t v1) (PDPair fc2 hls2 p2 t2 _ v2) =
248+ let ts = enrichPats $ combinePHPats t1 t2
249+ vs = enrichPats $ combinePHPats v1 v2
250+ in [ PDPair fc1 hls1 p1 t' t v' | t' <- ts, v' <- vs]
251+ combinePHPats p1@(PApp fc x xs@(_:_)) p2@(PApp _ x' xs')
252+ | quickEq x x' && length xs == length xs' =
253+ let ls = map getExpTm xs
254+ rs = map getExpTm xs'
255+ pss = cph $ zipWith combinePHPats ls rs
256+ in (map (\ps -> resugar (PApp fc x $ zipWith upd ps xs)) pss)
257+ combinePHPats x y = [x, y]
259+ cph :: [[PTerm]] -> [[PTerm]]
262+ cph (xs : xss) = concatMap (\x -> map (x:) $ cph xss) xs
247 otherPats :: PTerm -> [PTerm]
264 otherPats :: PTerm -> [PTerm]
248 otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
265 otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
@@ -257,7 +274,7 @@ genAll i (addPH, args)
257 ([pimp (sUN "a") Placeholder True,
274 ([pimp (sUN "a") Placeholder True,
258 pimp (sUN "P") Placeholder True] ++
275 pimp (sUN "P") Placeholder True] ++
259 [pexp t,pexp v]) o
276 [pexp t,pexp v]) o
260− otherPats o@(PConstant _ c) = ph $ inventConsts [o] -- return o
277+ otherPats o@(PConstant _ c) = ph [o, nextConst o]
261 otherPats arg = return Placeholder
278 otherPats arg = return Placeholder
263 ops fc n xs o
280 ops fc n xs o
@@ -311,6 +328,7 @@ genAll i (addPH, args)
311 quickEq :: PTerm -> PTerm -> Bool
328 quickEq :: PTerm -> PTerm -> Bool
312 quickEq (PConstant _ n) (PConstant _ n') = n == n'
329 quickEq (PConstant _ n) (PConstant _ n') = n == n'
313 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
330 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
331+ quickEq (PPair _ _ _ l r) (PPair _ _ _ l' r') = quickEq l l' && quickEq r r'
314 quickEq (PApp _ t as) (PApp _ t' as')
332 quickEq (PApp _ t as) (PApp _ t' as')
315 | length as == length as'
333 | length as == length as'
316 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
334 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))