@@ -106,16 +106,29 @@ genClauses fc n xs given
106106
107107fnub xs = fnub' [] xs
108108
109−fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
109+fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
110110 | otherwise = fnub' (x : acc) xs
111111fnub' acc [] = acc
112112
113+-- quick check for constructor equality
114+quickEq :: PTerm -> PTerm -> Bool
115+quickEq (PRef _ n) (PRef _ n') = n == n'
116+quickEq (PApp _ t as) (PApp _ t' as')
117+ | length as == length as'
118+ = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
119+quickEq Placeholder Placeholder = True
120+quickEq _ _ = False
121+
122+qelem x [] = False
123+qelem x (y : ys) | x `quickEq` y = True
124+ | otherwise = qelem x ys
125+
113126-- FIXME: Just look for which one is the deepest, then generate all
114127-- possibilities up to that depth.
115128
116129genAll :: IState -> [PTerm] -> [PTerm]
117130genAll i args
118− = case filter (/=Placeholder) $ nubMap otherPats [] (fnub args) of
131+ = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
119132 [] -> [Placeholder]
120133 xs -> xs
121134 where
@@ -131,9 +144,11 @@ genAll i args
131144 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
132145 otherPats arg = return Placeholder
133146
134− ops fc n xs o
147+ ops fc n xs_in o
135148 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
136− = do xs' <- mapM otherPats (map getTm xs)
149+ = do let force = getForceable i n -- no need to generate forceable positions
150+ let xs = dropForce force xs_in 0
151+ xs' <- mapM otherPats (map getTm xs)
137152 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
138153 let tyn = getTy n (tt_ctxt i)
139154 case lookupCtxt tyn (idris_datatypes i) of
@@ -141,6 +156,16 @@ genAll i args
141156 _ -> [p]
142157 ops fc n arg o = return Placeholder
143158
159+ getForceable i n = case lookupCtxt n (idris_optimisation i) of
160+ [Optimise _ fs _] -> fs
161+ _ -> []
162+
163+ dropForce force (x : xs) i | i `elem` force
164+ = upd Placeholder x : dropForce force xs (i + 1)
165+ dropForce force (x : xs) i = x : dropForce force xs (i + 1)
166+ dropForce _ [] _ = []
167+
168+
144169 getTy n ctxt = case lookupTy n ctxt of
145170 (t : _) -> case unApply (getRetTy t) of
146171 (P _ tyn _, _) -> tyn