@@ -15,6 +15,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
1515import Idris.Core.TT
1616import Idris.Core.Evaluate
1717import Idris.Core.Unify
18+import Idris.Core.ProofTerm (getProofTerm)
1819import Idris.Core.Typecheck (check, recheck, isType)
1920import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
2021import Idris.ErrReverse (errReverse)
@@ -1156,7 +1157,7 @@ elab ist info emode opts fn tm
11561157 focus n
11571158 elab' ina (Just fc') tm
11581159 env <- get_env
1159− runTactical (maybe fc' id fc) env (P Bound n' Erased)
1160+ runTactical ist (maybe fc' id fc) env (P Bound n' Erased)
11601161 solve
11611162 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
11621163
@@ -1470,12 +1471,12 @@ proofSearch' ist rec ambigok depth prv top n hints
14701471
14711472-- | Resolve type classes. This will only pick up 'normal' instances, never
14721473-- named instances (which is enforced by 'findInstances').
1473−resolveTC :: Bool -- using default Int
1474− -> Bool -- allow metavariables in the goal
1475− -> Int -- depth
1476− -> Term -- top level goal
1477− -> Name -- top level function name
1478− -> IState -> ElabD ()
1474+resolveTC :: Bool -- ^ using default Int
1475+ -> Bool -- ^ allow metavariables in the goal
1476+ -> Int -- ^ depth
1477+ -> Term -- ^ top level goal, for error messages
1478+ -> Name -- ^ top level function name, to prevent loops
1479+ -> IState -> ElabD ()
14791480resolveTC def mvok depth top fn ist
14801481 = do hs <- get_holes
14811482 resTC' [] def hs depth top fn ist
@@ -1671,16 +1672,16 @@ case_ ind autoSolve ist fn tm = do
16711672 when autoSolve solveAll
16721673
16731674
1674−runTactical :: FC -> Env -> Term -> ElabD ()
1675−runTactical fc env tm = do tm' <- eval tm
1676− runTacTm tm'
1677− return ()
1675+runTactical :: IState -> FC -> Env -> Term -> ElabD ()
1676+runTactical ist fc env tm = do tm' <- eval tm
1677+ runTacTm tm'
1678+ return ()
16781679 where
16791680 eval tm = do ctxt <- get_context
16801681 env <- get_env
16811682 return $ normaliseAll ctxt env (finalise tm)
16821683
1683− returnUnit = fmap fst $ get_type_val (Var unitCon)
1684+ returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
16841685
16851686 patvars :: [Name] -> Term -> ([Name], Term)
16861687 patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)
@@ -1892,6 +1893,11 @@ runTactical fc env tm = do tm' <- eval tm
18921893 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
18931894 new_tyDecls e}
18941895 returnUnit
1896+ | n == tacN "prim__ResolveTC", [fn] <- args
1897+ = do g <- goal
1898+ fn <- reifyTTName fn
1899+ resolveTC False True 100 g fn ist
1900+ returnUnit
18951901 | n == tacN "prim__RecursiveElab", [goal, script] <- args
18961902 = do goal' <- reifyRaw goal
18971903 ctxt <- get_context
@@ -1902,9 +1908,10 @@ runTactical fc env tm = do tm' <- eval tm
19021908 aux <- getAux
19031909 datatypes <- get_datatypes
19041910 env <- get_env
1905− (tm_out, ES (_, aux') _ _) <-
1906− lift $ runElab aux (runTactical fc env script >> solve >> get_term)
1911+ (_, ES (p, aux') _ _) <-
1912+ lift $ runElab aux (runTactical ist fc [] script)
19071913 (newProof recH ctxt datatypes goalTT)
1914+ let tm_out = getProofTerm (pterm p)
19081915 updateAux $ const aux'
19091916 env' <- get_env
19101917 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out