@@ -82,8 +82,9 @@ genClauses fc n xs given
8282 logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)
8383
8484 logCoverage 5 $ show (lhs_tms, lhss)
85− logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
86− logCoverage 10 $ show argss ++ "\n" ++ show all_args
85+ logCoverage 5 $ "Args are: " ++ show argss
86+ logCoverage 5 $ show (map length argss) ++ "\nAll args:\n" ++ show (map length all_args)
87+ logCoverage 10 $ "All args are: " ++ show all_args
8788 logCoverage 3 $ "Original: \n" ++
8889 showSep "\n" (map (\t -> showTmImpls (delab' i t True True)) xs)
8990 -- add an infinite supply of explicit arguments to update the possible
@@ -204,12 +205,58 @@ recoverableCoverage _ _ = False
204205
205206genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
206207genAll i (addPH, args)
207− = case filter (/=Placeholder) $ fnub $ enrichPats $ fnub (concatMap otherPats (fnub args)) of
208+ = case filter (/=Placeholder) $ fnub $ mergePHs $ fnub (concatMap otherPats (fnub args)) of
208209 [] -> [Placeholder]
209210 xs -> ph xs
210211 where
211212 ph ts = if addPH then Placeholder : ts else ts
212213
214+ -- Merge patterns with placeholders in other patterns, to ensure we've
215+ -- covered all possible generated cases
216+ -- e.g. if we have (True, _) (False, _) (_, True) (_, False)
217+ -- we should merge these to get (True, True), (False, False)
218+ -- (False, True) and (True, False)
219+ mergePHs :: [PTerm] -> [PTerm]
220+ mergePHs xs = mergePHs' xs xs
221+
222+ mergePHs' [] all = []
223+ mergePHs' (x : xs) all = mergePH x all ++ mergePHs' xs all
224+
225+ mergePH :: PTerm -> [PTerm] -> [PTerm]
226+ mergePH tm [] = []
227+ mergePH tm (x : xs)
228+ | Just merged <- mergePTerm tm x = merged : mergePH tm xs
229+ | otherwise = mergePH tm xs
230+
231+ mergePTerm :: PTerm -> PTerm -> Maybe PTerm
232+ mergePTerm x Placeholder = Just x
233+ mergePTerm Placeholder x = Just x
234+ mergePTerm tm@(PRef fc1 hl1 n1) (PRef fc2 hl2 n2)
235+ | n1 == n2 = Just tm
236+ mergePTerm (PPair fc1 hl1 p1 x1 y1) (PPair fc2 hl2 p2 x2 y2)
237+ = do x <- mergePTerm x1 x2
238+ y <- mergePTerm y1 y2
239+ Just (PPair fc1 hl1 p1 x y)
240+ mergePTerm (PDPair fc1 hl1 p1 x1 t1 y1) (PDPair fc2 hl2 p2 x2 t2 y2)
241+ = do x <- mergePTerm x1 x2
242+ y <- mergePTerm y1 y2
243+ t <- mergePTerm t1 t2
244+ Just (PDPair fc1 hl1 p1 x t y)
245+ mergePTerm (PApp fc1 f1 args1) (PApp fc2 f2 args2)
246+ = do fm <- mergePTerm f1 f2
247+ margs <- mergeArgs args1 args2
248+ Just (PApp fc1 fm margs)
249+ where
250+ mergeArgs [] [] = Just []
251+ mergeArgs (a : as) (b : bs)
252+ = do ma_in <- mergePTerm (getTm a) (getTm b)
253+ let ma = a { getTm = ma_in }
254+ mas <- mergeArgs as bs
255+ Just (ma : mas)
256+ mergeArgs _ _ = Nothing
257+ mergePTerm x y | x == y = Just x
258+ | otherwise = Nothing
259+
213260 -- for every constant in a term (at any level) take next one to make sure
214261 -- that constants which are not explicitly handled are covered
215262 nextConst (PConstant fc c) = PConstant NoFC (nc' c)
@@ -226,41 +273,6 @@ genAll i (addPH, args)
226273 nc' (Str c) = Str (c ++ "'")
227274 nc' o = o
228275
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
263−
264276 otherPats :: PTerm -> [PTerm]
265277 otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
266278 otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o