{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module Refinery.Tactic
( TacticT
, runTacticT
, (<@>)
, (<%>)
, commit
, try
, many_
, choice
, progress
, gather
, pruning
, ensure
, goal
, focus
, MonadExtract(..)
, MonadRule(..)
, RuleT
, rule
) where
import Control.Applicative
import Control.Monad.Except
import Control.Monad.State.Strict
import Refinery.ProofState
import Refinery.Tactic.Internal
(<@>) :: (Functor m) => TacticT jdg ext err s m a -> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
t <@> ts = tactic $ \j -> subgoals (fmap (\t' (_,j') -> proofState t' j') ts) (proofState t j)
infixr 3 <%>
(<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
t1 <%> t2 = tactic $ \j -> Interleave (proofState t1 j) (proofState t2 j)
commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit t1 t2 = tactic $ \j -> Commit (proofState t1 j) (proofState t2 j)
try :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try t = t <|> pure ()
many_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
many_ t = try (t >> many_ t)
goal :: (Functor m) => TacticT jdg ext err s m jdg
goal = TacticT $ get
choice :: (Monad m) => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice [] = empty
choice (t:ts) = t <%> choice ts
progress :: (Monad m) => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
progress eq err t = do
j <- goal
a <- t
j' <- goal
if j `eq` j' then pure a else throwError err
gather :: (MonadExtract ext m) => TacticT jdg ext err s m a -> ([(a, jdg)] -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a
gather t f = tactic $ \j -> do
s <- get
results <- lift $ proofs s $ proofState t j
msum $ flip fmap results $ \case
Left err -> throwError err
Right (_, _, jdgs) -> proofState (f jdgs) j
pruning
:: (MonadExtract ext m)
=> TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err)
-> TacticT jdg ext err s m ()
pruning t p = gather t $ maybe t throwError . p . fmap snd
ensure :: (Monad m) => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
ensure p f t = check >> t
where
check = rule $ \j -> do
e <- subgoal j
s <- get
modify f
case p s of
Just err -> throwError err
Nothing -> pure e
focus :: (Functor m) => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
focus t n t' = t <@> (replicate n (pure ()) ++ [t'] ++ repeat (pure ()))
runTacticT :: (MonadExtract ext m) => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, s, [jdg])]
runTacticT t j s = proofs s $ fmap snd $ proofState t j
rule :: (Monad m) => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule r = tactic $ \j -> fmap ((),) $ unRuleT (r j)