@@ -1,4 +1,4 @@
1−{-# LANGUAGE PatternGuards #-}
1+{-# LANGUAGE PatternGuards, ViewPatterns #-}
22
33module Idris.ElabTerm where
44
@@ -1029,6 +1029,20 @@ elab ist info emode opts fn tm
10291029 delayElab $ do focus h
10301030 dotterm
10311031 elab' ina fc t
1032+ elab' ina fc (PRunTactics tm) =
1033+ do attack
1034+ n <- getNameFrom (sMN 0 "tacticScript")
1035+ n' <- getNameFrom (sMN 0 "tacticExpr")
1036+ let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)
1037+ claim n scriptTy
1038+ movelast n
1039+ letbind n' scriptTy (Var n)
1040+ focus n
1041+ elab' ina fc tm
1042+ env <- get_env
1043+ ctxt <- get_context
1044+ runTactical ctxt env (P Bound n' Erased)
1045+ solve
10321046 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
10331047
10341048 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
@@ -1451,6 +1465,86 @@ case_ ind autoSolve ist fn tm = do
14511465 else casetac (forget val)
14521466 when autoSolve solveAll
14531467
1468+runTactical :: Context -> Env -> Term -> ElabD ()
1469+runTactical ctxt env tm = runTacTm (eval tm) >> return ()
1470+ where
1471+ eval = normaliseAll ctxt env
1472+ tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1473+ returnUnit = fmap fst $ get_type_val (Var unitCon)
1474+
1475+ -- | Do a step in the reflected elaborator monad. The input is the
1476+ -- step, the output is the (reflected) term returned.
1477+ runTacTm :: Term -> ElabD Term
1478+ runTacTm (unApply -> tac@(P _ n _, args))
1479+ | n == tacN "Solve", [] <- args
1480+ = do solve
1481+ returnUnit
1482+ | n == tacN "Goal", [] <- args
1483+ = do (h:_) <- get_holes
1484+ t <- goal
1485+ fmap fst . get_type_val $
1486+ rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1487+ (reflectName h, reflect t)
1488+ | n == tacN "Holes", [] <- args
1489+ = do hs <- get_holes
1490+ fmap fst . get_type_val $
1491+ mkList (Var $ reflm "TTName") (map reflectName hs)
1492+ | n == tacN "Guess", [] <- args
1493+ = do ok <- is_guess
1494+ if ok
1495+ then do guess <- fmap forget get_guess
1496+ fmap fst . get_type_val $
1497+ RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1498+ (Var (reflm "TT")))
1499+ guess
1500+ else fmap fst . get_type_val $
1501+ RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1502+ (Var (reflm "TT"))
1503+ | n == tacN "Env", [] <- args
1504+ = do env <- get_env
1505+ fmap fst . get_type_val $ reflectEnv env
1506+ | n == tacN "Fail", [_a, errs] <- args
1507+ = do parts <- reifyReportParts (eval errs)
1508+ lift . tfail $ ReflectionError [parts] (Msg "")
1509+ | n == tacN "PureTactical", [_a, tm] <- args
1510+ = return tm
1511+ | n == tacN "BindTactical", [_a, _b, first, andThen] <- args
1512+ = do let first' = eval first
1513+ res <- runTacTm first'
1514+ let next = eval (App andThen res)
1515+ runTacTm next
1516+ | n == tacN "Try", [_a, first, alt] <- args
1517+ = do let first' = eval first
1518+ let alt' = eval alt
1519+ try' (runTacTm first') (runTacTm alt') True
1520+ | n == tacN "Fill", [raw] <- args
1521+ = do raw' <- reifyRaw raw
1522+ apply raw' []
1523+ returnUnit
1524+ | n == tacN "Gensym", [eval -> Constant (Str hint)] <- args
1525+ = do n <- getNameFrom (sMN 0 hint)
1526+ fmap fst $ get_type_val (reflectName n)
1527+ | n == tacN "Claim", [n, ty] <- args
1528+ = do n' <- reifyTTName n
1529+ ty' <- reifyRaw ty
1530+ claim n' ty'
1531+ returnUnit
1532+ | n == tacN "Forget", [tt] <- args
1533+ = do tt' <- reifyTT tt
1534+ fmap fst . get_type_val $ reflect tt'
1535+ | n == tacN "Attack", [] <- args
1536+ = do attack
1537+ returnUnit
1538+ | n == tacN "Focus", [what] <- args
1539+ = do n' <- reifyTTName what
1540+ focus n'
1541+ returnUnit
1542+ | n == tacN "Unfocus", [what] <- args
1543+ = do n' <- reifyTTName what
1544+ movelast n'
1545+ returnUnit
1546+ runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1547+
14541548-- Running tactics directly
14551549-- if a tactic adds unification problems, return an error
14561550
@@ -1776,16 +1870,20 @@ reifyApp ist t [n, tt', t']
17761870 t'' <- reifyTT t'
17771871 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
17781872reifyApp ist t [errs]
1779− | t == reflm "Fail" = case unList errs of
1780− Nothing -> fail "Failed to reify errors"
1781− Just errs' ->
1782− let parts = mapM reifyReportPart errs' in
1783− case parts of
1784− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1785− Right errs'' ->
1786− return $ TFail errs''
1873+ | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
17871874reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
17881875
1876+reifyReportParts :: Term -> ElabD [ErrorReportPart]
1877+reifyReportParts errs =
1878+ case unList errs of
1879+ Nothing -> fail "Failed to reify errors"
1880+ Just errs' ->
1881+ let parts = mapM reifyReportPart errs' in
1882+ case parts of
1883+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1884+ Right errs'' ->
1885+ return errs''
1886+
17891887-- | Reify terms from their reflected representation
17901888reifyTT :: Term -> ElabD Term
17911889reifyTT t@(App _ _)