@@ -189,16 +189,23 @@ mkNewClauses ctxt fn ns sc
189189-- to the context, so can't do this itself).
190190-- Replaces any missing cases with explicit cases for the missing constructors
191191addMissingCons :: IState -> SC -> SC
192−addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
192+addMissingCons ist sc = evalState (addMissingConsSt ist sc) 0
193+
194+addMissingConsSt :: IState -> SC -> State Int SC
195+addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)
193196 where
194− addMissingAlt :: CaseAlt -> CaseAlt
195− addMissingAlt (ConCase n i ns sc) = ConCase n i ns (addMissingCons ist sc)
196− addMissingAlt (FnCase n ns sc) = FnCase n ns (addMissingCons ist sc)
197− addMissingAlt (ConstCase c sc) = ConstCase c (addMissingCons ist sc)
198− addMissingAlt (SucCase n sc) = SucCase n (addMissingCons ist sc)
199− addMissingAlt (DefaultCase sc) = DefaultCase (addMissingCons ist sc)
200−
201− -- TODO: deal with constants
197+ addMissingAlt :: CaseAlt -> State Int CaseAlt
198+ addMissingAlt (ConCase n i ns sc)
199+ = liftM (ConCase n i ns) (addMissingConsSt ist sc)
200+ addMissingAlt (FnCase n ns sc)
201+ = liftM (FnCase n ns) (addMissingConsSt ist sc)
202+ addMissingAlt (ConstCase c sc)
203+ = liftM (ConstCase c) (addMissingConsSt ist sc)
204+ addMissingAlt (SucCase n sc)
205+ = liftM (SucCase n) (addMissingConsSt ist sc)
206+ addMissingAlt (DefaultCase sc)
207+ = liftM DefaultCase (addMissingConsSt ist sc)
208+
202209 addMissingAlts argn as
203210-- | any hasDefault as = map addMissingAlt as
204211 | cons@(n:_) <- mapMaybe collectCons as,
@@ -208,24 +215,19 @@ addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
208215 -- things which were matched in other cases earlier can't be missing
209216 -- cases now
210217 = let missing = con_names ti \\ cons in
211− map addMissingAlt $ addCases missing as
218+ do as' <- addCases missing as
219+ mapM addMissingAlt as'
212220 | consts@(n:_) <- mapMaybe collectConsts as
213221 = let missing = nub (map nextConst consts) \\ consts in
214− map addMissingAlt $ addCons missing as
215− addMissingAlts n as = map addMissingAlt as
216−
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
222+ mapM addMissingAlt (addCons missing as)
223+ addMissingAlts n as = mapM addMissingAlt as
223224
224−
225− addCases missing [] = []
225+ addCases missing [] = return []
226226 addCases missing (DefaultCase rhs : rest)
227− = mapMaybe (genMissingAlt rhs) missing ++ rest
228− addCases missing (c : rest) = c : addCases missing rest
227+ = do missing' <- mapM (genMissingAlt rhs) missing
228+ return (mapMaybe id missing' ++ rest)
229+ addCases missing (c : rest)
230+ = liftM (c :) $ addCases missing rest
229231
230232 addCons missing [] = []
231233 addCons missing (DefaultCase rhs : rest)
@@ -234,9 +236,11 @@ addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
234236
235237 genMissingAlt rhs n
236238 | Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)
237− = Just $ ConCase n tag (map (\i -> sMN i "miss") [0..arity-1])
238− rhs
239− | otherwise = Nothing
239+ = do name <- get
240+ put (name + arity)
241+ let args = map (name +) [0..arity-1]
242+ return $ Just $ ConCase n tag (map (\i -> sMN i "m") args) rhs
243+ | otherwise = return Nothing
240244
241245 genMissingConAlt rhs n = ConstCase n rhs
242246
@@ -268,7 +272,7 @@ addMissingCons ist (Case t n alts) = Case t n (addMissingAlts n alts)
268272 nextConst (Str c) = Str (c ++ "'")
269273 nextConst o = o
270274
271−addMissingCons ist sc = sc
275+addMissingConsSt ist sc = return sc
272276
273277trimOverlapping :: SC -> SC
274278trimOverlapping sc = trim [] [] sc
@@ -279,8 +283,6 @@ trimOverlapping sc = trim [] [] sc
279283 trim mustbes nots (Case t vn alts)
280284 | Just (c, args) <- lookup vn mustbes
281285 = 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')
284286 | Just cantbe <- lookup vn nots
285287 = let alts' = filter (notConMatch cantbe) alts in
286288 Case t vn (trimAlts mustbes nots vn alts')
@@ -311,30 +313,19 @@ trimOverlapping sc = trim [] [] sc
311313
312314 substNames [] sc = sc
313315 substNames ((n, n') : ns) sc
314− | not (missName n || missName n') = substNames ns (substSC n n' sc)
315− | otherwise = substNames ns sc
316+ = substNames ns (substSC n n' sc)
316317
317318 notConMatch cs (ConCase cn t args sc) = cn `notElem` cs
318319 notConMatch cs _ = True
319320
320− addMatch vn (cn, _) cs | missName vn || missName cn = cs
321321 addMatch vn cn cs = (vn, cn) : cs
322322
323323 addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]
324− addCantBe vn cn nots | missName vn || missName cn = nots
325324 addCantBe vn cn [] = [(vn, [cn])]
326325 addCantBe vn cn ((n, cbs) : nots)
327326 | vn == n = ((n, nub (cn : cbs)) : nots)
328327 | otherwise = ((n, cbs) : addCantBe vn cn nots)
329328
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"
336− missName _ = False
337−
338329-- | Does this error result rule out a case as valid when coverage checking?
339330validCoverageCase :: Context -> Err -> Bool
340331validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)