@@ -59,10 +59,16 @@ genClauses fc n xs given
59 let lhs_tms' = zipWith mergePlaceholders lhs_tms
59 let lhs_tms' = zipWith mergePlaceholders lhs_tms
60 (map (stripUnmatchable i) (map flattenArgs given))
60 (map (stripUnmatchable i) (map flattenArgs given))
61 let lhss = map pUnApply lhs_tms'
61 let lhss = map pUnApply lhs_tms'
62+ nty <- case lookupTyExact n (tt_ctxt i) of
63+ Just t -> return (normalise (tt_ctxt i) [] t)
64+ _ -> fail "Can't happen - genClauses, lookupTyExact"
63 let argss = transpose lhss
66 let argss = transpose lhss
64− let all_args = map (genAll i) argss
67+ let all_args = map (genAll i) (zip (genPH i nty) argss)
65 logCoverage 5 $ "COVERAGE of " ++ show n
68 logCoverage 5 $ "COVERAGE of " ++ show n
69+ logCoverage 5 $ "using type " ++ show nty
70+ logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)
66 logCoverage 5 $ show (lhs_tms, lhss)
72 logCoverage 5 $ show (lhs_tms, lhss)
67 logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
73 logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
68 logCoverage 10 $ show argss ++ "\n" ++ show all_args
74 logCoverage 10 $ show argss ++ "\n" ++ show all_args
@@ -89,6 +95,18 @@ genClauses fc n xs given
89 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
95 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
90 | otherwise = []
96 | otherwise = []
98+ -- if an argument has a non-concrete type (i.e. it's a function
99+ -- that calculates something from a previous argument) we'll also
100+ -- need to generate a placeholder pattern for it since it could be
101+ -- anything based on earlier values
102+ genPH :: IState -> Type -> [Bool]
103+ genPH ist (Bind n (Pi _ ty _) sc) = notConcrete ist ty : genPH ist sc
106+ notConcrete ist t | (P _ n _, args) <- unApply t,
107+ not (isConName n (tt_ctxt ist)) = True
108+ notConcrete _ _ = False
92 pUnApply (PApp _ f args) = map getTm args
110 pUnApply (PApp _ f args) = map getTm args
93 pUnApply _ = []
111 pUnApply _ = []
@@ -172,16 +190,14 @@ recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
172recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
190recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
173recoverableCoverage _ _ = False
191recoverableCoverage _ _ = False
175−-- FIXME: Just look for which one is the deepest, then generate all
176−-- possibilities up to that depth.
177−-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.
178−-- https://github.com/idris-lang/Idris-dev/issues/1741
179−genAll :: IState -> [PTerm] -> [PTerm]
193+genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
180−genAll i args
194+genAll i (addPH, args)
181 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
195 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
182 [] -> [Placeholder]
196 [] -> [Placeholder]
183− xs -> inventConsts xs
197+ xs -> ph $ inventConsts xs
199+ ph ts = if addPH then Placeholder : ts else ts
185 -- if they're constants, invent a new one to make sure that
201 -- if they're constants, invent a new one to make sure that
186 -- constants which are not explicitly handled are covered
202 -- constants which are not explicitly handled are covered
187 inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
203 inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
@@ -204,7 +220,6 @@ genAll i args
204 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
220 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
205 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
221 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
206 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
222 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
207− -- TODO: Bit vectors
208 -- The rest are types with only one case
223 -- The rest are types with only one case
209 ic' xs = xs
224 ic' xs = xs
@@ -219,19 +234,19 @@ genAll i args
219 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
234 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
221 otherPats :: PTerm -> [PTerm]
236 otherPats :: PTerm -> [PTerm]
222− otherPats o@(PRef fc hl n) = ops fc n [] o
237+ otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
223− otherPats o@(PApp _ (PRef fc hl n) xs) = ops fc n xs o
238+ otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o
224 otherPats o@(PPair fc hls _ l r)
239 otherPats o@(PPair fc hls _ l r)
225− = ops fc pairCon
240+ = ph $ ops fc pairCon
226 ([pimp (sUN "A") Placeholder True,
241 ([pimp (sUN "A") Placeholder True,
227 pimp (sUN "B") Placeholder True] ++
242 pimp (sUN "B") Placeholder True] ++
228 [pexp l, pexp r]) o
243 [pexp l, pexp r]) o
229 otherPats o@(PDPair fc hls p t _ v)
244 otherPats o@(PDPair fc hls p t _ v)
230− = ops fc sigmaCon
245+ = ph $ ops fc sigmaCon
231 ([pimp (sUN "a") Placeholder True,
246 ([pimp (sUN "a") Placeholder True,
232 pimp (sUN "P") Placeholder True] ++
247 pimp (sUN "P") Placeholder True] ++
233 [pexp t,pexp v]) o
248 [pexp t,pexp v]) o
234− otherPats o@(PConstant _ c) = inventConsts [o] -- return o
249+ otherPats o@(PConstant _ c) = ph $ inventConsts [o] -- return o
235 otherPats arg = return Placeholder
250 otherPats arg = return Placeholder
237 ops fc n xs o
252 ops fc n xs o