@@ -130,8 +130,41 @@ genAll :: IState -> [PTerm] -> [PTerm]
130130genAll i args
131131 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
132132 [] -> [Placeholder]
133− xs -> xs
133+ xs -> inventConsts xs
134134 where
135+ -- if they're constants, invent a new one to make sure that
136+ -- constants which are not explicitly handled are covered
137+ inventConsts cs@(PConstant c : _) = map PConstant (ic' (mapMaybe getConst cs))
138+ where getConst (PConstant c) = Just c
139+ getConst _ = Nothing
140+ inventConsts xs = xs
141+
142+ -- try constants until they're not in the list.
143+ -- FIXME: It is, of course, possible that someone has enumerated all
144+ -- the constants and matched on them (maybe in generated code) and this
145+ -- will be really slow. This is sufficiently unlikely that we won't
146+ -- worry for now...
147+
148+ ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
149+ ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
150+ ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
151+ ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
152+ ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
153+ ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
154+ ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
155+ ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
156+ ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
157+ -- TODO: Bit vectors
158+ -- The rest are types with only one case
159+ ic' xs = xs
160+
161+ firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
162+ | otherwise = x : cs
163+
164+ lotsOfNums t = map t [0..]
165+ lotsOfChars = map Ch ['a'..]
166+ lotsOfStrings = map Str (map (("some string " ++).show) [1..])
167+
135168 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
136169 conForm (PRef fc n) = isConName n (tt_ctxt i)
137170 conForm _ = False
@@ -149,7 +182,8 @@ genAll i args
149182 otherPats o@(PDPair fc t _ v)
150183 = ops fc (UN "Ex_intro")
151184 ([pimp (UN "a") Placeholder, pimp (UN "P") Placeholder] ++
152− [pexp t,pexp v]) o
185+ [pexp t,pexp v]) o
186+ otherPats o@(PConstant c) = return o
153187 otherPats arg = return Placeholder
154188
155189 ops fc n xs_in o