@@ -46,7 +46,8 @@ genClauses fc n xs given
46 let lhss = map (getLHS i) xs
46 let lhss = map (getLHS i) xs
47 let argss = transpose lhss
47 let argss = transpose lhss
48 let all_args = map (genAll i) argss
48 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)
50 logLvl 10 $ show argss ++ "\n" ++ show all_args
51 logLvl 10 $ show argss ++ "\n" ++ show all_args
51 logLvl 10 $ "Original: \n" ++
52 logLvl 10 $ "Original: \n" ++
52 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
53 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
@@ -61,7 +62,7 @@ genClauses fc n xs given
61 logLvl 2 $ show (length tryclauses) ++ " initially to check"
62 logLvl 2 $ show (length tryclauses) ++ " initially to check"
62 let new = mnub i $ filter (noMatch i) tryclauses
63 let new = mnub i $ filter (noMatch i) tryclauses
63 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
64 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)
65-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
66-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
66 return new
67 return new
67-- return (map (\t -> PClause n t [] PImpossible []) new)
68-- return (map (\t -> PClause n t [] PImpossible []) new)
@@ -98,23 +99,28 @@ genClauses fc n xs given
98 as' <- mkArg as
99 as' <- mkArg as
99 return (a':as')
100 return (a':as')
101−fnub xs = fnub' [] xs where
102+fnub xs = fnub' [] xs
102− fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
104+fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
103− | otherwise = fnub' (x : acc) xs
105+ | otherwise = fnub' (x : acc) xs
104− fnub' acc [] = acc
106+fnub' acc [] = acc
106-- FIXME: Just look for which one is the deepest, then generate all
108-- FIXME: Just look for which one is the deepest, then generate all
107-- possibilities up to that depth.
109-- possibilities up to that depth.
109genAll :: IState -> [PTerm] -> [PTerm]
111genAll :: IState -> [PTerm] -> [PTerm]
110−genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
113+ = case filter (/=Placeholder) $ nubMap otherPats [] (fnub args) of
111− [] -> [Placeholder]
114+ [] -> [Placeholder]
112− xs -> nub xs
115+ xs -> xs
114 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
117 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
115 conForm (PRef fc n) = isConName n (tt_ctxt i)
118 conForm (PRef fc n) = isConName n (tt_ctxt i)
116 conForm _ = False
119 conForm _ = False
121+ nubMap f acc [] = acc
122+ nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
118 otherPats :: PTerm -> [PTerm]
124 otherPats :: PTerm -> [PTerm]
119 otherPats o@(PRef fc n) = ops fc n [] o
125 otherPats o@(PRef fc n) = ops fc n [] o
120 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
126 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o