@@ -17,6 +17,7 @@ import Idris.Delaborate
1717import Idris.Error
1818import Idris.Output (iWarn, iputStrLn)
1919
20+import Data.Char
2021import Data.List
2122import Data.Either
2223import Data.Maybe
@@ -203,46 +204,62 @@ recoverableCoverage _ _ = False
203204
204205genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
205206genAll 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
207208 [] -> [Placeholder]
208− xs -> ph $ inventConsts xs
209+ xs -> ph xs
209210 where
210211 ph ts = if addPH then Placeholder : ts else ts
211212
212− -- if they're constants, invent a new one to make sure that
213− -- constants which are not explicitly handled are covered
214− inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
215− where getConst (PConstant _ c) = Just c
216− getConst _ = Nothing
217− inventConsts xs = xs
218−
219− -- try constants until they're not in the list.
220− -- FIXME: It is, of course, possible that someone has enumerated all
221− -- the constants and matched on them (maybe in generated code) and this
222− -- will be really slow. This is sufficiently unlikely that we won't
223− -- worry for now...
224−
225− ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
226− ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
227− ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
228− ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
229− ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
230− ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
231− ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
232− ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
233− ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
234− -- The rest are types with only one case
235− ic' xs = xs
236−
237− firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
238− | otherwise = x : cs
239−
240− lotsOfNums t = map t [0..]
241− lotsOfChars = map Ch ['a'..]
242− lotsOfStrings = map Str (map (("some string " ++).show) [1..])
243−
244− nubMap f acc [] = acc
245− nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
213+ -- for every constant in a term (at any level) take next one to make sure
214+ -- that constants which are not explicitly handled are covered
215+ nextConst (PConstant fc c) = PConstant NoFC (nc' c)
216+ nextConst o = o
217+
218+ nc' (I c) = I (c + 1)
219+ nc' (BI c) = BI (c + 1)
220+ nc' (Fl c) = Fl (c + 1)
221+ nc' (B8 c) = B8 (c + 1)
222+ nc' (B16 c) = B16 (c + 1)
223+ nc' (B32 c) = B32 (c + 1)
224+ nc' (B64 c) = B64 (c + 1)
225+ nc' (Ch c) = Ch (chr $ ord c + 1)
226+ nc' (Str c) = Str (c ++ "'")
227+ nc' o = o
228+
229+ -- enrich patterns with cartesian products so that
230+ -- (True, _) and (_, True) give (True, True)
231+ -- with all other combinations to be checked for coverage later
232+ enrichPats :: [PTerm] -> [PTerm]
233+ enrichPats xs = xs ++ enrichPats' xs
234+
235+ enrichPats' :: [PTerm] -> [PTerm]
236+ enrichPats' [] = []
237+ enrichPats' [x] = [x]
238+ enrichPats' (x : xs) = concatMap (combinePHPats x) xs ++ enrichPats' xs
239+
240+ combinePHPats :: PTerm -> PTerm -> [PTerm]
241+ combinePHPats Placeholder x = [x]
242+ combinePHPats x Placeholder = [x]
243+ combinePHPats (PPair fc1 hls1 pi1 l1 r1) (PPair fc2 hls2 pi2 l2 r2) =
244+ let ls = enrichPats $ combinePHPats l1 l2
245+ rs = enrichPats $ combinePHPats r1 r2
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]
258+
259+ cph :: [[PTerm]] -> [[PTerm]]
260+ cph [] = []
261+ cph [x] = [x]
262+ cph (xs : xss) = concatMap (\x -> map (x:) $ cph xss) xs
246263
247264 otherPats :: PTerm -> [PTerm]
248265 otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
@@ -257,7 +274,7 @@ genAll i (addPH, args)
257274 ([pimp (sUN "a") Placeholder True,
258275 pimp (sUN "P") Placeholder True] ++
259276 [pexp t,pexp v]) o
260− otherPats o@(PConstant _ c) = ph $ inventConsts [o] -- return o
277+ otherPats o@(PConstant _ c) = ph [o, nextConst o]
261278 otherPats arg = return Placeholder
262279
263280 ops fc n xs o
@@ -311,6 +328,7 @@ genAll i (addPH, args)
311328 quickEq :: PTerm -> PTerm -> Bool
312329 quickEq (PConstant _ n) (PConstant _ n') = n == n'
313330 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
331+ quickEq (PPair _ _ _ l r) (PPair _ _ _ l' r') = quickEq l l' && quickEq r r'
314332 quickEq (PApp _ t as) (PApp _ t' as')
315333 | length as == length as'
316334 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))