@@ -15,6 +15,7 @@ import Idris.Error
1515import Control.Applicative ((<$>))
1616import Control.Monad
1717import Control.Monad.State.Strict
18+import qualified Data.Set as S
1819import Data.List
1920import Debug.Trace
2021
@@ -91,7 +92,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
9192 if ambigok || argsok then
9293 case lookupCtxt nroot (idris_tyinfodata ist) of
9394 [TISolution ts] -> findInferredTy ts
94− _ -> psRec rec maxDepth []
95+ _ -> psRec rec maxDepth [] S.empty
9596 else autoArg (sUN "auto") -- not enough info in the type yet
9697 where
9798 findInferredTy (t : _) = elab (delab ist (toUN t))
@@ -134,13 +135,21 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
134135 -- (so we don't try a pointless application of something to itself,
135136 -- which obviously won't work anyway but might lead us on a wild
136137 -- goose chase...)
137− psRec _ 0 locs | fromProver = cantSolveGoal
138− psRec rec 0 locs = do attack; defer [] nroot; solve --fail "Maximum depth reached"
139− psRec False d locs = tryCons d locs hints
140− psRec True d locs
138+ -- Also keep track of the types we've proved so far in this branch
139+ -- (if we get back to one we've been to before, we're just in a cycle and
140+ -- that's no use)
141+ psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
142+ psRec _ 0 locs tys | fromProver = cantSolveGoal
143+ psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
144+ psRec False d locs tys = tryCons d locs tys hints
145+ psRec True d locs tys
141146 = do compute
147+ ty <- goal
148+ when (S.member ty tys) $ fail "Been here before"
149+ let tys' = S.insert ty tys
142150 try' (trivial elab ist)
143− (try' (try' (resolveByCon (d - 1) locs) (resolveByLocals (d - 1) locs)
151+ (try' (try' (resolveByCon (d - 1) locs tys')
152+ (resolveByLocals (d - 1) locs tys')
144153 True)
145154 -- if all else fails, make a new metavariable
146155 (if fromProver
@@ -151,7 +160,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
151160 getFn d (Just f) | d < maxDepth-1 = [f]
152161 | otherwise = []
153162
154− resolveByCon d locs
163+ resolveByCon d locs tys
155164 = do t <- goal
156165 let (f, _) = unApply t
157166 case f of
@@ -160,7 +169,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
160169 Nothing -> []
161170 Just hs -> hs
162171 case lookupCtxtExact n (idris_datatypes ist) of
163− Just t -> tryCons d locs (hints ++
172+ Just t -> tryCons d locs tys
173+ (hints ++
164174 con_names t ++
165175 autohints ++
166176 getFn d fn)
@@ -169,28 +179,31 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
169179
170180 -- if there are local variables which have a function type, try
171181 -- applying them too
172− resolveByLocals d locs
182+ resolveByLocals d locs tys
173183 = do env <- get_env
174− tryLocals d locs env
184+ tryLocals d locs tys env
175185
176− tryLocals d locs [] = fail "Locals failed"
177− tryLocals d locs ((x, t) : xs)
178− | x `elem` locs = tryLocals d locs xs
179− | otherwise = try' (tryLocal d (x : locs) x t) (tryLocals d locs xs) True
186+ tryLocals d locs tys [] = fail "Locals failed"
187+ tryLocals d locs tys ((x, t) : xs)
188+ | x `elem` locs = tryLocals d locs tys xs
189+ | otherwise = try' (tryLocal d (x : locs) tys x t)
190+ (tryLocals d locs tys xs) True
180191
181− tryCons d locs [] = fail "Constructors failed"
182− tryCons d locs (c : cs) = try' (tryCon d locs c) (tryCons d locs cs) True
192+ tryCons d locs tys [] = fail "Constructors failed"
193+ tryCons d locs tys (c : cs)
194+ = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
183195
184− tryLocal d locs n t
196+ tryLocal d locs tys n t
185197 = do let a = getPArity (delab ist (binderTy t))
186− tryLocalArg d locs n a
198+ tryLocalArg d locs tys n a
187199
188− tryLocalArg d locs n 0 = elab (PRef (fileFC "prf") n)
189− tryLocalArg d locs n i = simple_app False (tryLocalArg d locs n (i - 1))
190− (psRec True d locs) "proof search local apply"
200+ tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") n)
201+ tryLocalArg d locs tys n i
202+ = simple_app False (tryLocalArg d locs tys n (i - 1))
203+ (psRec True d locs tys) "proof search local apply"
191204
192205 -- Like type class resolution, but searching with constructors
193− tryCon d locs n =
206+ tryCon d locs tys n =
194207 do ty <- goal
195208 let imps = case lookupCtxtExact n (idris_implicits ist) of
196209 Nothing -> []
@@ -204,7 +217,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
204217 when (length ps < length ps') $ fail "Can't apply constructor"
205218 mapM_ (\ (_, h) -> do focus h
206219 aty <- goal
207− psRec True d locs)
220+ psRec True d locs tys)
208221 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
209222 solve
210223