@@ -15,6 +15,7 @@ import Idris.Error
15import Control.Applicative ((<$>))
15import Control.Applicative ((<$>))
16import Control.Monad
16import Control.Monad
17import Control.Monad.State.Strict
17import Control.Monad.State.Strict
18+import qualified Data.Set as S
18import Data.List
19import Data.List
19import Debug.Trace
20import Debug.Trace
@@ -91,7 +92,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
91 if ambigok || argsok then
92 if ambigok || argsok then
92 case lookupCtxt nroot (idris_tyinfodata ist) of
93 case lookupCtxt nroot (idris_tyinfodata ist) of
93 [TISolution ts] -> findInferredTy ts
94 [TISolution ts] -> findInferredTy ts
94− _ -> psRec rec maxDepth []
95+ _ -> psRec rec maxDepth [] S.empty
95 else autoArg (sUN "auto") -- not enough info in the type yet
96 else autoArg (sUN "auto") -- not enough info in the type yet
97 findInferredTy (t : _) = elab (delab ist (toUN t))
98 findInferredTy (t : _) = elab (delab ist (toUN t))
@@ -134,13 +135,21 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
134 -- (so we don't try a pointless application of something to itself,
135 -- (so we don't try a pointless application of something to itself,
135 -- which obviously won't work anyway but might lead us on a wild
136 -- which obviously won't work anyway but might lead us on a wild
136 -- goose chase...)
137 -- goose chase...)
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
141+ psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
137− psRec _ 0 locs | fromProver = cantSolveGoal
142+ psRec _ 0 locs tys | fromProver = cantSolveGoal
138− psRec rec 0 locs = do attack; defer [] nroot; solve --fail "Maximum depth reached"
143+ psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
139− psRec False d locs = tryCons d locs hints
144+ psRec False d locs tys = tryCons d locs tys hints
140− psRec True d locs
145+ psRec True d locs tys
141 = do compute
146 = do compute
148+ when (S.member ty tys) $ fail "Been here before"
149+ let tys' = S.insert ty tys
142 try' (trivial elab ist)
150 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')
145 -- if all else fails, make a new metavariable
154 -- if all else fails, make a new metavariable
146 (if fromProver
155 (if fromProver
@@ -151,7 +160,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
151 getFn d (Just f) | d < maxDepth-1 = [f]
160 getFn d (Just f) | d < maxDepth-1 = [f]
152 | otherwise = []
161 | otherwise = []
154− resolveByCon d locs
163+ resolveByCon d locs tys
155 = do t <- goal
164 = do t <- goal
156 let (f, _) = unApply t
165 let (f, _) = unApply t
157 case f of
166 case f of
@@ -160,7 +169,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
160 Nothing -> []
169 Nothing -> []
161 Just hs -> hs
170 Just hs -> hs
162 case lookupCtxtExact n (idris_datatypes ist) of
171 case lookupCtxtExact n (idris_datatypes ist) of
163− Just t -> tryCons d locs (hints ++
172+ Just t -> tryCons d locs tys
164 con_names t ++
174 con_names t ++
165 autohints ++
175 autohints ++
166 getFn d fn)
176 getFn d fn)
@@ -169,28 +179,31 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
170 -- if there are local variables which have a function type, try
180 -- if there are local variables which have a function type, try
171 -- applying them too
181 -- applying them too
172− resolveByLocals d locs
182+ resolveByLocals d locs tys
173 = do env <- get_env
183 = do env <- get_env
174− tryLocals d locs env
184+ tryLocals d locs tys env
176− tryLocals d locs [] = fail "Locals failed"
186+ tryLocals d locs tys [] = fail "Locals failed"
177− tryLocals d locs ((x, t) : xs)
187+ tryLocals d locs tys ((x, t) : xs)
178− | x `elem` locs = tryLocals d locs xs
188+ | x `elem` locs = tryLocals d locs tys xs
179− | otherwise = try' (tryLocal d (x : locs) x t) (tryLocals d locs xs) True
189+ | otherwise = try' (tryLocal d (x : locs) tys x t)
190+ (tryLocals d locs tys xs) True
181− tryCons d locs [] = fail "Constructors failed"
192+ tryCons d locs tys [] = fail "Constructors failed"
193+ tryCons d locs tys (c : cs)
182− tryCons d locs (c : cs) = try' (tryCon d locs c) (tryCons d locs cs) True
194+ = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
184− tryLocal d locs n t
196+ tryLocal d locs tys n t
185 = do let a = getPArity (delab ist (binderTy t))
197 = do let a = getPArity (delab ist (binderTy t))
186− tryLocalArg d locs n a
198+ tryLocalArg d locs tys n a
188− tryLocalArg d locs n 0 = elab (PRef (fileFC "prf") n)
200+ tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") n)
201+ tryLocalArg d locs tys n i
189− tryLocalArg d locs n i = simple_app False (tryLocalArg d locs n (i - 1))
202+ = simple_app False (tryLocalArg d locs tys n (i - 1))
190− (psRec True d locs) "proof search local apply"
203+ (psRec True d locs tys) "proof search local apply"
192 -- Like type class resolution, but searching with constructors
205 -- Like type class resolution, but searching with constructors
193− tryCon d locs n =
206+ tryCon d locs tys n =
194 do ty <- goal
207 do ty <- goal
195 let imps = case lookupCtxtExact n (idris_implicits ist) of
208 let imps = case lookupCtxtExact n (idris_implicits ist) of
196 Nothing -> []
209 Nothing -> []
@@ -204,7 +217,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
204 when (length ps < length ps') $ fail "Can't apply constructor"
217 when (length ps < length ps') $ fail "Can't apply constructor"
205 mapM_ (\ (_, h) -> do focus h
218 mapM_ (\ (_, h) -> do focus h
206 aty <- goal
219 aty <- goal
207− psRec True d locs)
220+ psRec True d locs tys)
208 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
221 (filter (\ (x, y) -> not x) (zip (map fst imps) args))