@@ -408,6 +408,8 @@ instanceArg n ctxt env (Bind x (Hole t) sc)
408 ps { holes = (hs \\ [x]) ++ [x],
408 ps { holes = (hs \\ [x]) ++ [x],
409 instances = x:is })
409 instances = x:is })
410 return (Bind x (Hole t) sc)
410 return (Bind x (Hole t) sc)
411+instanceArg n ctxt env _
412+ = fail "The current focus is not a hole."
412autoArg :: Name -> RunTactic
414autoArg :: Name -> RunTactic
413autoArg n ctxt env (Bind x (Hole t) sc)
415autoArg n ctxt env (Bind x (Hole t) sc)
@@ -418,6 +420,8 @@ autoArg n ctxt env (Bind x (Hole t) sc)
418 autos = (x, (while_elaborating ps, refsIn t)) : autos ps }
420 autos = (x, (while_elaborating ps, refsIn t)) : autos ps }
419 Just _ -> ps)
421 Just _ -> ps)
420 return (Bind x (Hole t) sc)
422 return (Bind x (Hole t) sc)
424+ = fail "The current focus not a hole."
422setinj :: Name -> RunTactic
426setinj :: Name -> RunTactic
423setinj n ctxt env (Bind x b sc)
427setinj n ctxt env (Bind x b sc)
@@ -439,6 +443,7 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
439 mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
443 mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
441 getP (n, b) = P Bound n (binderTy b)
445 getP (n, b) = P Bound n (binderTy b)
446+defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."
443-- as defer, but build the type and application explicitly
448-- as defer, but build the type and application explicitly
444deferType :: Name -> Raw -> [Name] -> RunTactic
449deferType :: Name -> Raw -> [Name] -> RunTactic
@@ -454,6 +459,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
454 getP n = case lookup n env of
459 getP n = case lookup n env of
455 Just b -> P Bound n (binderTy b)
460 Just b -> P Bound n (binderTy b)
456 Nothing -> error ("deferType can't find " ++ show n)
461 Nothing -> error ("deferType can't find " ++ show n)
462+deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."
458regret :: RunTactic
464regret :: RunTactic
459regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
465regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
@@ -462,12 +468,14 @@ regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
462 return sc
468 return sc
463regret ctxt env (Bind x (Hole t) _)
469regret ctxt env (Bind x (Hole t) _)
464 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
470 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
471+regret _ _ _ = fail "The current focus is not a hole."
466unifyGoal :: Raw -> RunTactic
473unifyGoal :: Raw -> RunTactic
467unifyGoal tm ctxt env h@(Bind x b sc) =
474unifyGoal tm ctxt env h@(Bind x b sc) =
468 do (tmv, _) <- lift $ check ctxt env tm
475 do (tmv, _) <- lift $ check ctxt env tm
469 ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
476 ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
478+unifyGoal _ _ _ _ = fail "The focus is not a binder."
472exact :: Raw -> RunTactic
480exact :: Raw -> RunTactic
473exact guess ctxt env (Bind x (Hole ty) sc) =
481exact guess ctxt env (Bind x (Hole ty) sc) =