@@ -6,7 +6,8 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88{-# LANGUAGE PatternGuards #-}
9−module Idris.Coverage where
9+module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
10+ mkPatTm) where
1011
1112import Idris.AbsSyntax
1213import Idris.Core.CaseTree
@@ -61,100 +62,267 @@ mkPatTm t = do i <- getIState
6162--
6263-- This will only work after the given clauses have been typechecked and the
6364-- names are fully explicit!
64−genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
65−genClauses fc n xs given
65+genClauses :: FC -> Name -> [([Name], Term)] -> -- (Argument names, LHS)
66+ [PTerm] -> Idris [PTerm]
67+-- No clauses (only valid via elab reflection). We should probably still do
68+-- a check here somehow, e.g. that one of the arguments is an obviously
69+-- empty type. In practice, this should only really be used for Void elimination.
70+genClauses fc n lhs_tms [] = return []
71+genClauses fc n lhs_tms given
6672 = do i <- getIState
67− let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs
68− -- if a placeholder was given, don't bother generating cases for it
69− let lhs_tms' = zipWith mergePlaceholders lhs_tms
70− (map (stripUnmatchable i) (map flattenArgs given))
71− let lhss = map pUnApply lhs_tms'
72− nty <- case lookupTyExact n (tt_ctxt i) of
73− Just t -> return (normalise (tt_ctxt i) [] t)
74− _ -> fail "Can't happen - genClauses, lookupTyExact"
75−
76− let argss = transpose lhss
77− let all_args = map (genAll i) (zip (genPH i nty) argss)
78− logCoverage 5 $ "COVERAGE of " ++ show n
79− logCoverage 5 $ "using type " ++ show nty
80− logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)
81−
82− logCoverage 5 $ show (lhs_tms, lhss)
83− logCoverage 5 $ "Args are: " ++ show argss
84− logCoverage 5 $ show (map length argss) ++ "\nAll args:\n" ++ show (map length all_args)
85− logCoverage 10 $ "All args are: " ++ show all_args
86− logCoverage 3 $ "Original: \n" ++
87− showSep "\n" (map (\t -> showTmImpls (delab' i t True True)) xs)
88− -- add an infinite supply of explicit arguments to update the possible
89− -- cases for (the return type may be variadic, or function type, so
90− -- there may be more case splitting that the idris_implicits record
91− -- suggests)
92− let parg = case lookupCtxt n (idris_implicits i) of
93− (p : _) ->
94− p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
95− _ -> repeat (pexp Placeholder)
96− let tryclauses = mkClauses parg all_args
97− logCoverage 3 $ show (length tryclauses) ++ " initially to check"
98− logCoverage 2 $ showSep "\n" (map (showTm i) tryclauses)
99−
100− let xsdelab = map (\x -> stripUnmatchable i (delab' i x True True)) xs
101− let new = filter (noMatch i xsdelab) tryclauses
102− logCoverage 2 $ show (length new) ++ " clauses to check for impossibility"
103− logCoverage 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
104−-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
105− return new
106−-- return (map (\t -> PClause n t [] PImpossible []) new)
107− where getLHS i term
108− | (f, args) <- unApply term = map (\t -> delab' i t True True) args
109− | otherwise = []
110−
111− -- if an argument has a non-concrete type (i.e. it's a function
112− -- that calculates something from a previous argument) we'll also
113− -- need to generate a placeholder pattern for it since it could be
114− -- anything based on earlier values
115− genPH :: IState -> Type -> [Bool]
116− genPH ist (Bind n (Pi _ ty _) sc) = notConcrete ist ty : genPH ist sc
117− genPH ist ty = []
118−
119− notConcrete ist t | (P _ n _, args) <- unApply t,
120− not (isConName n (tt_ctxt ist)) = True
121− notConcrete _ _ = False
122−
123− pUnApply (PApp _ f args) = map getTm args
124− pUnApply _ = []
125−
73+
74+ let lhs_given = zipWith removePlaceholders lhs_tms
75+ (map (stripUnmatchable i) (map flattenArgs given))
76+
77+ let givenpos = mergePos (map getGivenPos given)
78+
79+ (cns, ctree_in) <-
80+ case simpleCase False (UnmatchedCase "Undefined") False
81+ (CoverageCheck givenpos) emptyFC [] []
82+ lhs_given
83+ (const []) of
84+ OK (CaseDef cns ctree_in _) ->
85+ return (cns, ctree_in)
86+ Error e -> tclift $ tfail $ At fc e
87+
88+ let ctree = trimOverlapping (addMissingCons i ctree_in)
89+ let (coveredas, missingas) = mkNewClauses (tt_ctxt i) n cns ctree
90+ let covered = map (\t -> delab' i t True True) coveredas
91+ let missing = filter (\x -> x `notElem` covered) $
92+ map (\t -> delab' i t True True) missingas
93+
94+ logCoverage 5 $ "Coverage from case tree for " ++ show n ++ ": " ++ show ctree
95+ logCoverage 2 $ show (length missing) ++ " missing clauses for " ++ show n
96+ logCoverage 3 $ "Missing clauses:\n" ++ showSep "\n"
97+ (map showTmImpls missing)
98+ logCoverage 10 $ "Covered clauses:\n" ++ showSep "\n"
99+ (map showTmImpls covered)
100+ return missing
101+ where
126102 flattenArgs (PApp fc (PApp _ f as) as')
127103 = flattenArgs (PApp fc f (as ++ as'))
128104 flattenArgs t = t
129105
130− -- Return whether the given clause matches none of the input clauses
131− -- (xs)
132− noMatch i xs tm = all (\x -> case matchClause i x tm of
133− Right ms -> False
134− Left miss -> True) xs
135−
136−
137− mergePlaceholders :: PTerm -> PTerm -> PTerm
138− mergePlaceholders x Placeholder = Placeholder
139− mergePlaceholders (PApp fc f args) (PApp fc' f' args')
140− = PApp fc' f' (zipWith mergePArg args args')
141− where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in
142− x { getTm = xtm}
143− mergePlaceholders x _ = x
144−
145− mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
146− mkClauses parg args
147− | all (== [Placeholder]) args = []
148− mkClauses parg args
149− = do args' <- mkArg args
150− let tm = PApp fc (PRef fc [] n) (zipWith upd args' parg)
151− return tm
152− where
153− mkArg :: [[PTerm]] -> [[PTerm]]
154− mkArg [] = return []
155− mkArg (a : as) = do a' <- a
156− as' <- mkArg as
157− return (a':as')
106+getGivenPos :: PTerm -> [Int]
107+getGivenPos (PApp _ _ pargs) = getGiven 0 (map getTm pargs)
108+ where
109+ getGiven i (Placeholder : tms) = getGiven (i + 1) tms
110+ getGiven i (_ : tms) = i : getGiven (i + 1) tms
111+ getGiven i [] = []
112+getGivenPos _ = []
113+
114+-- Return a list of Ints which are in every list
115+mergePos :: [[Int]] -> [Int]
116+mergePos [] = []
117+mergePos [x] = x
118+mergePos (x : xs) = intersect x (mergePos xs)
119+
120+removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)
121+removePlaceholders (ns, tm) ptm = (ns, tm, Erased) -- rp tm ptm, Erased)
122+ where
123+ rp tm Placeholder = Erased
124+ rp tm (PApp _ pf pargs)
125+ | (tf, targs) <- unApply tm
126+ = let tf' = rp tf pf
127+ targs' = zipWith rp targs (map getTm pargs) in
128+ mkApp tf' targs'
129+ rp tm (PPair _ _ _ pl pr)
130+ | (tf, [tyl, tyr, tl, tr]) <- unApply tm
131+ = let tl' = rp tl pl
132+ tr' = rp tr pr in
133+ mkApp tf [Erased, Erased, tl', tr']
134+ rp tm (PDPair _ _ _ pl pt pr)
135+ | (tf, [tyl, tyr, tl, tr]) <- unApply tm
136+ = let tl' = rp tl pl
137+ tr' = rp tr pr in
138+ mkApp tf [Erased, Erased, tl', tr']
139+ rp tm _ = tm
140+
141+mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])
142+mkNewClauses ctxt fn ns sc
143+ = (map (mkPlApp (P Ref fn Erased)) $
144+ mkFromSC True (map (\n -> P Ref n Erased) ns) sc,
145+ map (mkPlApp (P Ref fn Erased)) $
146+ mkFromSC False (map (\n -> P Ref n Erased) ns) sc)
147+ where
148+ mkPlApp f args = mkApp f (map erasePs args)
149+
150+ erasePs ap@(App t f a)
151+ | (f, args) <- unApply ap = mkApp f (map erasePs args)
152+ erasePs (P _ n _) | not (isConName n ctxt) = Erased
153+ erasePs tm = tm
154+
155+ mkFromSC :: Bool -> [Term] -> SC -> [[Term]]
156+ mkFromSC cov args (STerm _) = if cov then [args] else [] -- leaf of provided case
157+ mkFromSC cov args (UnmatchedCase _) = if cov then [] else [args] -- leaf of missing case
158+ mkFromSC cov args ImpossibleCase = []
159+ mkFromSC cov args (Case _ x alts)
160+ = concatMap (mkFromAlt cov args x) alts
161+ mkFromSC cov args _ = [] -- Should never happen
162+
163+ mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> [[Term]]
164+ mkFromAlt cov args x (ConCase c t conargs sc)
165+ = let argrep = mkApp (P (DCon t (length args) False) c Erased)
166+ (map (\n -> P Ref n Erased) conargs)
167+ args' = map (subst x argrep) args in
168+ mkFromSC cov args' sc
169+ mkFromAlt cov args x (ConstCase c sc)
170+ = let argrep = Constant c
171+ args' = map (subst x argrep) args in
172+ mkFromSC cov args' sc
173+ mkFromAlt cov args x (DefaultCase sc)
174+ = mkFromSC cov args sc
175+ mkFromAlt cov _ _ _ = []
176+
177+-- Modify the generated case tree (the case tree builder doesn't have access
178+-- to the context, so can't do this itself).
179+-- Replaces any missing cases with explicit cases for the missing constructors
180+addMissingCons :: IState -> SC -> SC
181+addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
182+ where
183+ addMissingAlt :: CaseAlt -> CaseAlt
184+ addMissingAlt (ConCase n i ns sc) = ConCase n i ns (addMissingCons ist sc)
185+ addMissingAlt (FnCase n ns sc) = FnCase n ns (addMissingCons ist sc)
186+ addMissingAlt (ConstCase c sc) = ConstCase c (addMissingCons ist sc)
187+ addMissingAlt (SucCase n sc) = SucCase n (addMissingCons ist sc)
188+ addMissingAlt (DefaultCase sc) = DefaultCase (addMissingCons ist sc)
189+
190+ -- TODO: deal with constants
191+ addMissingAlts argn as
192+-- | any hasDefault as = map addMissingAlt as
193+ | cons@(n:_) <- mapMaybe collectCons as,
194+ Just tyn <- getConType n,
195+ Just ti <- lookupCtxtExact tyn (idris_datatypes ist)
196+ -- If we've fallen through on this argument earlier, then the
197+ -- things which were matched in other cases earlier can't be missing
198+ -- cases now
199+ = let missing = con_names ti \\ cons in
200+ map addMissingAlt $ addCases missing as
201+ | consts@(n:_) <- mapMaybe collectConsts as
202+ = let missing = nub (map nextConst consts) \\ consts in
203+ map addMissingAlt $ addCons missing as
204+ addMissingAlts n as = map addMissingAlt as
205+
206+ -- Add the constructors already ruled out for an argument (because
207+ -- we've fallen through those cases)
208+ addArgCons argn cons [] = [(argn, cons)]
209+ addArgCons argn cons ((a, cs) : ms)
210+ | a == argn = ((a, nub (cons ++ cs)) : ms)
211+ addArgCons argn cons (m : ms) = m : addArgCons argn cons ms
212+
213+
214+ addCases missing [] = []
215+ addCases missing (DefaultCase rhs : rest)
216+ = mapMaybe (genMissingAlt rhs) missing ++ rest
217+ addCases missing (c : rest) = c : addCases missing rest
218+
219+ addCons missing [] = []
220+ addCons missing (DefaultCase rhs : rest)
221+ = map (genMissingConAlt rhs) missing ++ rest
222+ addCons missing (c : rest) = c : addCons missing rest
223+
224+ genMissingAlt rhs n
225+ | Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)
226+ = Just $ ConCase n tag (map (\i -> sMN i "miss") [0..arity-1])
227+ rhs
228+ | otherwise = Nothing
229+
230+ genMissingConAlt rhs n = ConstCase n rhs
231+
232+ collectCons (ConCase n i args sc) = Just n
233+ collectCons _ = Nothing
234+
235+ collectConsts (ConstCase c sc) = Just c
236+ collectConsts _ = Nothing
237+
238+ hasDefault (DefaultCase (UnmatchedCase _)) = False
239+ hasDefault (DefaultCase _) = True
240+ hasDefault _ = False
241+
242+ getConType n = do ty <- lookupTyExact n (tt_ctxt ist)
243+ case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of
244+ (P _ tyn _, _) -> Just tyn
245+ _ -> Nothing
246+
247+ -- for every constant in a term (at any level) take next one to make sure
248+ -- that constants which are not explicitly handled are covered
249+ nextConst (I c) = I (c + 1)
250+ nextConst (BI c) = BI (c + 1)
251+ nextConst (Fl c) = Fl (c + 1)
252+ nextConst (B8 c) = B8 (c + 1)
253+ nextConst (B16 c) = B16 (c + 1)
254+ nextConst (B32 c) = B32 (c + 1)
255+ nextConst (B64 c) = B64 (c + 1)
256+ nextConst (Ch c) = Ch (chr $ ord c + 1)
257+ nextConst (Str c) = Str (c ++ "'")
258+ nextConst o = o
259+
260+addMissingCons ist sc = sc
261+
262+trimOverlapping :: SC -> SC
263+trimOverlapping sc = trim [] [] sc
264+ where
265+ trim :: [(Name, (Name, [Name]))] -> -- Variable - constructor+args already matched
266+ [(Name, [Name])] -> -- Variable - constructors which it can't be
267+ SC -> SC
268+ trim mustbes nots (Case t vn alts)
269+ | Just (c, args) <- lookup vn mustbes
270+ = Case t vn (trimAlts mustbes nots vn (substMatch (c, args) alts))
271+-- = let alts' = filter (isConMatch c) alts in
272+-- Case t vn (trimAlts mustbes nots vn alts')
273+ | Just cantbe <- lookup vn nots
274+ = let alts' = filter (notConMatch cantbe) alts in
275+ Case t vn (trimAlts mustbes nots vn alts')
276+ | otherwise = Case t vn (trimAlts mustbes nots vn alts)
277+ trim cs nots sc = sc
278+
279+ trimAlts cs nots vn [] = []
280+ trimAlts cs nots vn (ConCase cn t args sc : rest)
281+ = ConCase cn t args (trim (addMatch vn (cn, args) cs) nots sc) :
282+ trimAlts cs (addCantBe vn cn nots) vn rest
283+ trimAlts cs nots vn (FnCase n ns sc : rest)
284+ = FnCase n ns (trim cs nots sc) : trimAlts cs nots vn rest
285+ trimAlts cs nots vn (ConstCase c sc : rest)
286+ = ConstCase c (trim cs nots sc) : trimAlts cs nots vn rest
287+ trimAlts cs nots vn (SucCase n sc : rest)
288+ = SucCase n (trim cs nots sc) : trimAlts cs nots vn rest
289+ trimAlts cs nots vn (DefaultCase sc : rest)
290+ = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest
291+
292+ isConMatch c (ConCase cn t args sc) = c == cn
293+ isConMatch _ _ = False
294+
295+ substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]
296+ substMatch ca [] = []
297+ substMatch (c,args) (ConCase cn t args' sc : _)
298+ | c == cn = [ConCase c t args (substNames (zip args' args) sc)]
299+ substMatch ca (_:cs) = substMatch ca cs
300+
301+ substNames [] sc = sc
302+ substNames ((n, n') : ns) sc
303+ | not (missName n || missName n') = substNames ns (substSC n n' sc)
304+ | otherwise = substNames ns sc
305+
306+ notConMatch cs (ConCase cn t args sc) = cn `notElem` cs
307+ notConMatch cs _ = True
308+
309+ addMatch vn (cn, _) cs | missName vn || missName cn = cs
310+ addMatch vn cn cs = (vn, cn) : cs
311+
312+ addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
313+ addCantBe vn cn nots | missName vn || missName cn = nots
314+ addCantBe vn cn [] = [(vn, [cn])]
315+ addCantBe vn cn ((n, cbs) : nots)
316+ | vn == n = ((n, nub (cn : cbs)) : nots)
317+ | otherwise = ((n, cbs) : addCantBe vn cn nots)
318+
319+ -- "miss" names are inserted by addMissingCons, and are treated as
320+ -- placeholders throughout, so we need to make a note to treat them as
321+ -- placeholders here too (otherwise we might substitute them and end up
322+ -- matching on them, and that'd be a disaster because we don't take care
323+ -- to make unique names...)
324+ missName (MN i miss) = miss == txt "miss"
325+ missName _ = False
158326
159327-- | Does this error result rule out a case as valid when coverage checking?
160328validCoverageCase :: Context -> Err -> Bool
@@ -203,162 +371,3 @@ recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
203371recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
204372recoverableCoverage _ _ = False
205373
206−genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
207−genAll i (addPH, args)
208− = case filter (/=Placeholder) $ fnub $ mergePHs $ fnub (concatMap otherPats (fnub args)) of
209− [] -> [Placeholder]
210− xs -> ph xs
211− where
212− -- Add a placeholder - this is to account for the case where an argument
213− -- has a dependent type calculated from another argument, to make sure that
214− -- all dependencies are covered. If they are, any generated case will
215− -- match given cases.
216− -- (Also this helps when checking, because if we eliminate the placeholder
217− -- quickly then lots of other cases get ruled out fast)
218− ph ts = if addPH then Placeholder : ts else ts
219−
220− -- Merge patterns with placeholders in other patterns, to ensure we've
221− -- covered all possible generated cases
222− -- e.g. if we have (True, _) (False, _) (_, True) (_, False)
223− -- we should merge these to get (True, True), (False, False)
224− -- (False, True) and (True, False)
225− mergePHs :: [PTerm] -> [PTerm]
226− mergePHs xs = mergePHs' xs xs
227−
228− mergePHs' [] all = []
229− mergePHs' (x : xs) all = mergePH x all ++ mergePHs' xs all
230−
231− mergePH :: PTerm -> [PTerm] -> [PTerm]
232− mergePH tm [] = []
233− mergePH tm (x : xs)
234− | Just merged <- mergePTerm tm x = merged : mergePH tm xs
235− | otherwise = mergePH tm xs
236−
237− mergePTerm :: PTerm -> PTerm -> Maybe PTerm
238− mergePTerm x Placeholder = Just x
239− mergePTerm Placeholder x = Just x
240− mergePTerm tm@(PRef fc1 hl1 n1) (PRef fc2 hl2 n2)
241− | n1 == n2 = Just tm
242− mergePTerm (PPair fc1 hl1 p1 x1 y1) (PPair fc2 hl2 p2 x2 y2)
243− = do x <- mergePTerm x1 x2
244− y <- mergePTerm y1 y2
245− Just (PPair fc1 hl1 p1 x y)
246− mergePTerm (PDPair fc1 hl1 p1 x1 t1 y1) (PDPair fc2 hl2 p2 x2 t2 y2)
247− = do x <- mergePTerm x1 x2
248− y <- mergePTerm y1 y2
249− t <- mergePTerm t1 t2
250− Just (PDPair fc1 hl1 p1 x t y)
251− mergePTerm (PApp fc1 f1 args1) (PApp fc2 f2 args2)
252− = do fm <- mergePTerm f1 f2
253− margs <- mergeArgs args1 args2
254− Just (PApp fc1 fm margs)
255− where
256− mergeArgs [] [] = Just []
257− mergeArgs (a : as) (b : bs)
258− = do ma_in <- mergePTerm (getTm a) (getTm b)
259− let ma = a { getTm = ma_in }
260− mas <- mergeArgs as bs
261− Just (ma : mas)
262− mergeArgs _ _ = Nothing
263− mergePTerm x y | x == y = Just x
264− | otherwise = Nothing
265−
266− -- for every constant in a term (at any level) take next one to make sure
267− -- that constants which are not explicitly handled are covered
268− nextConst (PConstant fc c) = PConstant NoFC (nc' c)
269− nextConst o = o
270−
271− nc' (I c) = I (c + 1)
272− nc' (BI c) = BI (c + 1)
273− nc' (Fl c) = Fl (c + 1)
274− nc' (B8 c) = B8 (c + 1)
275− nc' (B16 c) = B16 (c + 1)
276− nc' (B32 c) = B32 (c + 1)
277− nc' (B64 c) = B64 (c + 1)
278− nc' (Ch c) = Ch (chr $ ord c + 1)
279− nc' (Str c) = Str (c ++ "'")
280− nc' o = o
281−
282− otherPats :: PTerm -> [PTerm]
283− otherPats (PRef fc hl n) = ph $ ops fc n []
284− otherPats (PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs
285− otherPats (PPair fc hls _ l r)
286− = ph $ ops fc pairCon
287− ([pimp (sUN "A") Placeholder True,
288− pimp (sUN "B") Placeholder True] ++
289− [pexp l, pexp r])
290− otherPats (PDPair fc hls p t _ v)
291− = ph $ ops fc sigmaCon
292− ([pimp (sUN "a") Placeholder True,
293− pimp (sUN "P") Placeholder True] ++
294− [pexp t,pexp v])
295− otherPats o@(PConstant _ c) = ph [o, nextConst o]
296− otherPats arg = return Placeholder
297−
298− ops fc n xs
299− | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
300− = do xs' <- mapM otherPats (map getExpTm xs)
301− let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))
302− let tyn = getTy n (tt_ctxt i)
303− case lookupCtxt tyn (idris_datatypes i) of
304− (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
305− _ -> [p]
306− ops fc n arg = return Placeholder
307−
308− getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
309− getExpTm t = getTm t
310−
311− -- put it back to its original form
312− resugar (PApp _ (PRef fc hl n) [_,_,t,v])
313− | n == sigmaCon
314− = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
315− resugar (PApp _ (PRef fc hl n) [_,_,l,r])
316− | n == pairCon
317− = PPair fc [] IsTerm (getTm l) (getTm r)
318− resugar t = t
319−
320− dropForce force (x : xs) i | i `elem` force
321− = upd Placeholder x : dropForce force xs (i + 1)
322− dropForce force (x : xs) i = x : dropForce force xs (i + 1)
323− dropForce _ [] _ = []
324−
325−
326− getTy n ctxt = case lookupTy n ctxt of
327− (t : _) -> case unApply (getRetTy t) of
328− (P _ tyn _, _) -> tyn
329− x -> error $ "Can't happen getTy 1 " ++ show (n, x)
330− _ -> error "Can't happen getTy 2"
331−
332− mkPat fc x = case lookupCtxt x (idris_implicits i) of
333− (pargs : _)
334− -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)
335− _ -> error "Can't happen - genAll"
336−
337− fnub :: [PTerm] -> [PTerm]
338− fnub xs = fnub' [] xs
339−
340− fnub' :: [PTerm] -> [PTerm] -> [PTerm]
341− fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
342− | otherwise = fnub' (x : acc) xs
343− fnub' acc [] = acc
344−
345− -- quick check for constructor equality
346− quickEq :: PTerm -> PTerm -> Bool
347− quickEq (PConstant _ n) (PConstant _ n') = n == n'
348− quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
349− quickEq (PPair _ _ _ l r) (PPair _ _ _ l' r') = quickEq l l' && quickEq r r'
350− quickEq (PApp _ t as) (PApp _ t' as')
351− | length as == length as'
352− = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
353− quickEq Placeholder Placeholder = True
354− quickEq x y = False
355−
356− qelem :: PTerm -> [PTerm] -> Bool
357− qelem x [] = False
358− qelem x (y : ys) | x `quickEq` y = True
359− | otherwise = qelem x ys
360−
361−
362−upd :: t -> PArg' t -> PArg' t
363−upd p' p = p { getTm = p' }
364−