@@ -54,16 +54,16 @@ mkPatTm t = do i <- getIState
5454genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
5555genClauses fc n xs given
5656 = do i <- getIState
57− let lhs_tms = map (\x -> delab' i x True True) xs
57+ let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs
5858 -- if a placeholder was given, don't bother generating cases for it
5959 let lhs_tms' = zipWith mergePlaceholders lhs_tms
60− (map (stripUnmatchable i) given)
60+ (map (stripUnmatchable i) (map flattenArgs given))
6161 let lhss = map pUnApply lhs_tms'
6262
6363 let argss = transpose lhss
6464 let all_args = map (genAll i) argss
6565 logLvl 5 $ "COVERAGE of " ++ show n
66− logLvl 5 $ show lhss
66+ logLvl 5 $ show (lhs_tms, lhss)
6767 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
6868 logLvl 10 $ show argss ++ "\n" ++ show all_args
6969 logLvl 3 $ "Original: \n" ++
@@ -89,9 +89,13 @@ genClauses fc n xs given
8989 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
9090 | otherwise = []
9191
92− pUnApply (PApp _ _ args) = map getTm args
92+ pUnApply (PApp _ f args) = map getTm args
9393 pUnApply _ = []
9494
95+ flattenArgs (PApp fc (PApp _ f as) as')
96+ = flattenArgs (PApp fc f (as ++ as'))
97+ flattenArgs t = t
98+
9599 -- Return whether the given clause matches none of the input clauses
96100 -- (xs)
97101 noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of