@@ -189,16 +189,23 @@ mkNewClauses ctxt fn ns sc
189-- to the context, so can't do this itself).
189-- to the context, so can't do this itself).
190-- Replaces any missing cases with explicit cases for the missing constructors
190-- Replaces any missing cases with explicit cases for the missing constructors
191addMissingCons :: IState -> SC -> SC
191addMissingCons :: IState -> SC -> SC
192+addMissingCons ist sc = evalState (addMissingConsSt ist sc) 0
194+addMissingConsSt :: IState -> SC -> State Int SC
192−addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
195+addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)
194− addMissingAlt :: CaseAlt -> CaseAlt
197+ addMissingAlt :: CaseAlt -> State Int CaseAlt
195− addMissingAlt (ConCase n i ns sc) = ConCase n i ns (addMissingCons ist sc)
198+ addMissingAlt (ConCase n i ns sc)
199+ = liftM (ConCase n i ns) (addMissingConsSt ist sc)
196− addMissingAlt (FnCase n ns sc) = FnCase n ns (addMissingCons ist sc)
200+ addMissingAlt (FnCase n ns sc)
201+ = liftM (FnCase n ns) (addMissingConsSt ist sc)
197− addMissingAlt (ConstCase c sc) = ConstCase c (addMissingCons ist sc)
202+ addMissingAlt (ConstCase c sc)
203+ = liftM (ConstCase c) (addMissingConsSt ist sc)
198− addMissingAlt (SucCase n sc) = SucCase n (addMissingCons ist sc)
204+ addMissingAlt (SucCase n sc)
205+ = liftM (SucCase n) (addMissingConsSt ist sc)
199− addMissingAlt (DefaultCase sc) = DefaultCase (addMissingCons ist sc)
206+ addMissingAlt (DefaultCase sc)
200−
207+ = liftM DefaultCase (addMissingConsSt ist sc)
201− -- TODO: deal with constants
208+
202 addMissingAlts argn as
209 addMissingAlts argn as
203-- | any hasDefault as = map addMissingAlt as
210-- | any hasDefault as = map addMissingAlt as
204 | cons@(n:_) <- mapMaybe collectCons as,
211 | cons@(n:_) <- mapMaybe collectCons as,
@@ -208,24 +215,19 @@ addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
208 -- things which were matched in other cases earlier can't be missing
215 -- things which were matched in other cases earlier can't be missing
209 -- cases now
216 -- cases now
210 = let missing = con_names ti \\ cons in
217 = let missing = con_names ti \\ cons in
211− map addMissingAlt $ addCases missing as
218+ do as' <- addCases missing as
219+ mapM addMissingAlt as'
212 | consts@(n:_) <- mapMaybe collectConsts as
220 | consts@(n:_) <- mapMaybe collectConsts as
213 = let missing = nub (map nextConst consts) \\ consts in
221 = let missing = nub (map nextConst consts) \\ consts in
214− map addMissingAlt $ addCons missing as
222+ mapM addMissingAlt (addCons missing as)
215− addMissingAlts n as = map addMissingAlt as
223+ addMissingAlts n as = mapM addMissingAlt as
217− -- Add the constructors already ruled out for an argument (because
218− -- we've fallen through those cases)
219− addArgCons argn cons [] = [(argn, cons)]
220− addArgCons argn cons ((a, cs) : ms)
221− | a == argn = ((a, nub (cons ++ cs)) : ms)
222− addArgCons argn cons (m : ms) = m : addArgCons argn cons ms
225− addCases missing [] = []
225+ addCases missing [] = return []
226 addCases missing (DefaultCase rhs : rest)
226 addCases missing (DefaultCase rhs : rest)
227− = mapMaybe (genMissingAlt rhs) missing ++ rest
227+ = do missing' <- mapM (genMissingAlt rhs) missing
228+ return (mapMaybe id missing' ++ rest)
228− addCases missing (c : rest) = c : addCases missing rest
229+ addCases missing (c : rest)
230+ = liftM (c :) $ addCases missing rest
230 addCons missing [] = []
232 addCons missing [] = []
231 addCons missing (DefaultCase rhs : rest)
233 addCons missing (DefaultCase rhs : rest)
@@ -234,9 +236,11 @@ addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
235 genMissingAlt rhs n
237 genMissingAlt rhs n
236 | Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)
238 | Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)
241+ let args = map (name +) [0..arity-1]
237− = Just $ ConCase n tag (map (\i -> sMN i "miss") [0..arity-1])
242+ return $ Just $ ConCase n tag (map (\i -> sMN i "m") args) rhs
239− | otherwise = Nothing
243+ | otherwise = return Nothing
241 genMissingConAlt rhs n = ConstCase n rhs
245 genMissingConAlt rhs n = ConstCase n rhs
@@ -268,7 +272,7 @@ addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
268 nextConst (Str c) = Str (c ++ "'")
272 nextConst (Str c) = Str (c ++ "'")
269 nextConst o = o
273 nextConst o = o
271−addMissingCons ist sc = sc
275+addMissingConsSt ist sc = return sc
273trimOverlapping :: SC -> SC
277trimOverlapping :: SC -> SC
274trimOverlapping sc = trim [] [] sc
278trimOverlapping sc = trim [] [] sc
@@ -279,8 +283,6 @@ trimOverlapping sc = trim [] [] sc
279 trim mustbes nots (Case t vn alts)
283 trim mustbes nots (Case t vn alts)
280 | Just (c, args) <- lookup vn mustbes
284 | Just (c, args) <- lookup vn mustbes
281 = Case t vn (trimAlts mustbes nots vn (substMatch (c, args) alts))
285 = Case t vn (trimAlts mustbes nots vn (substMatch (c, args) alts))
282−-- = let alts' = filter (isConMatch c) alts in
283−-- Case t vn (trimAlts mustbes nots vn alts')
284 | Just cantbe <- lookup vn nots
286 | Just cantbe <- lookup vn nots
285 = let alts' = filter (notConMatch cantbe) alts in
287 = let alts' = filter (notConMatch cantbe) alts in
286 Case t vn (trimAlts mustbes nots vn alts')
288 Case t vn (trimAlts mustbes nots vn alts')
@@ -311,30 +313,19 @@ trimOverlapping sc = trim [] [] sc
312 substNames [] sc = sc
314 substNames [] sc = sc
313 substNames ((n, n') : ns) sc
315 substNames ((n, n') : ns) sc
314− | not (missName n || missName n') = substNames ns (substSC n n' sc)
316+ = substNames ns (substSC n n' sc)
315− | otherwise = substNames ns sc
317 notConMatch cs (ConCase cn t args sc) = cn `notElem` cs
318 notConMatch cs (ConCase cn t args sc) = cn `notElem` cs
318 notConMatch cs _ = True
319 notConMatch cs _ = True
320− addMatch vn (cn, _) cs | missName vn || missName cn = cs
321 addMatch vn cn cs = (vn, cn) : cs
321 addMatch vn cn cs = (vn, cn) : cs
323 addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
323 addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
324− addCantBe vn cn nots | missName vn || missName cn = nots
325 addCantBe vn cn [] = [(vn, [cn])]
324 addCantBe vn cn [] = [(vn, [cn])]
326 addCantBe vn cn ((n, cbs) : nots)
325 addCantBe vn cn ((n, cbs) : nots)
327 | vn == n = ((n, nub (cn : cbs)) : nots)
326 | vn == n = ((n, nub (cn : cbs)) : nots)
328 | otherwise = ((n, cbs) : addCantBe vn cn nots)
327 | otherwise = ((n, cbs) : addCantBe vn cn nots)
330− -- "miss" names are inserted by addMissingCons, and are treated as
331− -- placeholders throughout, so we need to make a note to treat them as
332− -- placeholders here too (otherwise we might substitute them and end up
333− -- matching on them, and that'd be a disaster because we don't take care
334− -- to make unique names...)
335− missName (MN i miss) = miss == txt "miss"
338-- | Does this error result rule out a case as valid when coverage checking?
329-- | Does this error result rule out a case as valid when coverage checking?
339validCoverageCase :: Context -> Err -> Bool
330validCoverageCase :: Context -> Err -> Bool
340validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
331validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)