@@ -46,7 +46,8 @@ genClauses fc n xs given
4646 let lhss = map (getLHS i) xs
4747 let argss = transpose lhss
4848 let all_args = map (genAll i) argss
49− logLvl 7 $ "COVERAGE of " ++ show n
49+ logLvl 5 $ "COVERAGE of " ++ show n
50+ logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
5051 logLvl 10 $ show argss ++ "\n" ++ show all_args
5152 logLvl 10 $ "Original: \n" ++
5253 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
@@ -61,7 +62,7 @@ genClauses fc n xs given
6162 logLvl 2 $ show (length tryclauses) ++ " initially to check"
6263 let new = mnub i $ filter (noMatch i) tryclauses
6364 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
64− logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
65+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
6566-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
6667 return new
6768-- return (map (\t -> PClause n t [] PImpossible []) new)
@@ -98,23 +99,28 @@ genClauses fc n xs given
9899 as' <- mkArg as
99100 return (a':as')
100101
101−fnub xs = fnub' [] xs where
102− fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
103− | otherwise = fnub' (x : acc) xs
104− fnub' acc [] = acc
102+fnub xs = fnub' [] xs
103+
104+fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
105+ | otherwise = fnub' (x : acc) xs
106+fnub' acc [] = acc
105107
106108-- FIXME: Just look for which one is the deepest, then generate all
107109-- possibilities up to that depth.
108110
109111genAll :: IState -> [PTerm] -> [PTerm]
110−genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
111− [] -> [Placeholder]
112− xs -> nub xs
112+genAll i args
113+ = case filter (/=Placeholder) $ nubMap otherPats [] (fnub args) of
114+ [] -> [Placeholder]
115+ xs -> xs
113116 where
114117 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
115118 conForm (PRef fc n) = isConName n (tt_ctxt i)
116119 conForm _ = False
117120
121+ nubMap f acc [] = acc
122+ nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
123+
118124 otherPats :: PTerm -> [PTerm]
119125 otherPats o@(PRef fc n) = ops fc n [] o
120126 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o