@@ -250,21 +250,44 @@ goal h tm = g [] tm where
251tactic :: Hole -> RunTactic -> StateT TState TC ()
251tactic :: Hole -> RunTactic -> StateT TState TC ()
252tactic h f = do ps <- get
252tactic h f = do ps <- get
253− tm' <- atH (context ps) [] (pterm ps)
253+ (tm', _) <- atH (context ps) [] (pterm ps)
254 ps <- get -- might have changed while processing
254 ps <- get -- might have changed while processing
255 put (ps { pterm = tm' })
255 put (ps { pterm = tm' })
257+ updated o = do o' <- o
261+ = do (b', u) <- atH c env b
262+ if u then return (op a b', True)
263+ else do (a', u) <- atH c env a
264+ return (op a' b', u)
266+ -- Search the things most likely to contain the binding first!
268+ atH :: Context -> Env -> Term -> StateT TState TC (Term, Bool)
257− atH c env binder@(Bind n b sc)
269+ atH c env binder@(Bind n b@(Guess t v) sc)
258− | hole b && same h n = f c env binder
270+ | same h n = updated (f c env binder)
259 | otherwise
271 | otherwise
260− = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
272+ = do -- binder first
273+ (b', u) <- ulift2 c env Guess t v
274+ if u then return (Bind n b' sc, True)
275+ else do (sc', u) <- atH c ((n, b) : env) sc
276+ return (Bind n b' sc', u)
277+ atH c env binder@(Bind n b sc)
278+ | hole b && same h n = updated (f c env binder)
279+ | otherwise -- scope first
280+ = do (sc', u) <- atH c ((n, b) : env) sc
281+ if u then return (Bind n b sc', True)
282+ else do (b', u) <- atHb c env b
283+ return (Bind n b' sc', u)
261− atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
284+ atH c env (App f a) = ulift2 c env App f a
262− atH c env t = return t
285+ atH c env t = return (t, False)
264− atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
287+ atHb c env (Let t v) = ulift2 c env Let t v
265− atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
288+ atHb c env (Guess t v) = ulift2 c env Guess t v
266− atHb c env t = do ty' <- atH c env (binderTy t)
289+ atHb c env t = do (ty', u) <- atH c env (binderTy t)
267− return $ t { binderTy = ty' }
290+ return (t { binderTy = ty' }, u)
269computeLet :: Context -> Name -> Term -> Term
292computeLet :: Context -> Name -> Term -> Term
270computeLet ctxt n tm = cl [] tm where
293computeLet ctxt n tm = cl [] tm where
@@ -453,8 +476,8 @@ solve ctxt env (Bind x (Guess ty val) sc)
453 -- dontunify = dontunify ps \\ [x],
476 -- dontunify = dontunify ps \\ [x],
454 -- unified = (uh, uns ++ [(x, val)]),
477 -- unified = (uh, uns ++ [(x, val)]),
455 instances = instances ps \\ [x] })
478 instances = instances ps \\ [x] })
456− return $ {- Bind x (Let ty val) sc -}
457− instantiate val (pToV x sc)
479+ let tm' = instantiate val (pToV x sc) in
458 | otherwise = lift $ tfail $ IncompleteTerm val
481 | otherwise = lift $ tfail $ IncompleteTerm val
459solve _ _ h@(Bind x t sc)
482solve _ _ h@(Bind x t sc)
460 = do ps <- get
483 = do ps <- get