Copyright	(c) Reed Mullanix 2019
License	BSD-style
Maintainer	reedmullanix@gmail.com
Safe Haskell	None
Language	Haskell2010

Refinery.Tactic

Contents

Tactic Combinators
Subgoal Manipulation
Tactic Creation

Description

Synopsis

data TacticT jdg ext err s m a
runTacticT :: MonadExtract ext m => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, s, [jdg])]
(<@>) :: Functor m => TacticT jdg ext err s m a -> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
(<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
try :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
many_ :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
choice :: Monad m => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
progress :: Monad m => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
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
pruning :: MonadExtract ext m => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
ensure :: Monad m => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
goal :: Functor m => TacticT jdg ext err s m jdg
focus :: Functor m => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
class Monad m => MonadExtract ext m | m -> ext where
- hole :: m ext
class Monad m => MonadRule jdg ext m | m -> jdg, m -> ext where
- subgoal :: jdg -> m ext
data RuleT jdg ext err s m a
rule :: Monad m => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()

Documentation

data TacticT jdg ext err s m a Source #

A TacticT is a monad transformer that performs proof refinement. The type variables signifiy:

jdg - The goal type. This is the thing we are trying to construct a proof of.
ext - The extract type. This is what we will recieve after running the tactic.
err - The error type. We can use throwError to abort the computation with a provided error
s - The state type.
m - The base monad.
a - The return value. This to make TacticT a monad, and will always be '()'

Instances

Monad m => MonadState s (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods get :: TacticT jdg ext err s m s # put :: s -> TacticT jdg ext err s m () # state :: (s -> (a, s)) -> TacticT jdg ext err s m a #
MonadReader env m => MonadReader env (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods ask :: TacticT jdg ext err s m env # local :: (env -> env) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a # reader :: (env -> a) -> TacticT jdg ext err s m a #
Monad m => MonadError err (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods throwError :: err -> TacticT jdg ext err s m a # catchError :: TacticT jdg ext err s m a -> (err -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a #
MFunctor (TacticT jdg ext err s :: (Type -> Type) -> Type -> Type) Source #
Instance details Defined in Refinery.Tactic.Internal Methods hoist :: Monad m => (forall a. m a -> n a) -> TacticT jdg ext err s m b -> TacticT jdg ext err s n b #
MonadTrans (TacticT jdg ext err s) Source #
Instance details Defined in Refinery.Tactic.Internal Methods lift :: Monad m => m a -> TacticT jdg ext err s m a #
Functor m => Monad (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods (>>=) :: TacticT jdg ext err s m a -> (a -> TacticT jdg ext err s m b) -> TacticT jdg ext err s m b # (>>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m b # return :: a -> TacticT jdg ext err s m a # fail :: String -> TacticT jdg ext err s m a #
Functor m => Functor (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods fmap :: (a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b # (<$) :: a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a #
Functor m => Applicative (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods pure :: a -> TacticT jdg ext err s m a # (<>) :: TacticT jdg ext err s m (a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b # liftA2 :: (a -> b -> c) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m c # (>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m b # (<*) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a #
MonadIO m => MonadIO (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods liftIO :: IO a -> TacticT jdg ext err s m a #
Monad m => Alternative (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods empty :: TacticT jdg ext err s m a # (<\|>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a # some :: TacticT jdg ext err s m a -> TacticT jdg ext err s m [a] # many :: TacticT jdg ext err s m a -> TacticT jdg ext err s m [a] #
Monad m => MonadPlus (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods mzero :: TacticT jdg ext err s m a # mplus :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a #
MonadThrow m => MonadThrow (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods throwM :: Exception e => e -> TacticT jdg ext err s m a #
MonadCatch m => MonadCatch (TacticT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods catch :: Exception e => TacticT jdg ext err s m a -> (e -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a #
(Monoid jdg, Show a, Show jdg, Show err, Show ext, Show (m (ProofStateT ext ext err s m (a, jdg)))) => Show (TacticT jdg ext err s m a) Source #
Instance details Defined in Refinery.Tactic.Internal Methods showsPrec :: Int -> TacticT jdg ext err s m a -> ShowS # show :: TacticT jdg ext err s m a -> String # showList :: [TacticT jdg ext err s m a] -> ShowS #
Generic (TacticT jdg ext err s m a) Source #
Instance details Defined in Refinery.Tactic.Internal Associated Types type Rep (TacticT jdg ext err s m a) :: Type -> Type # Methods from :: TacticT jdg ext err s m a -> Rep (TacticT jdg ext err s m a) x # to :: Rep (TacticT jdg ext err s m a) x -> TacticT jdg ext err s m a #
type Rep (TacticT jdg ext err s m a) Source #
Instance details Defined in Refinery.Tactic.Internal type Rep (TacticT jdg ext err s m a) = D1 (MetaData "TacticT" "Refinery.Tactic.Internal" "refinery-0.3.0.0-Fdcu2SHDGUb4nunxmlwjIU" True) (C1 (MetaCons "TacticT" PrefixI True) (S1 (MetaSel (Just "unTacticT") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (StateT jdg (ProofStateT ext ext err s m) a))))

runTacticT :: MonadExtract ext m => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, s, [jdg])] Source #

Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.

Tactic Combinators

(<@>) :: Functor m => TacticT jdg ext err s m a -> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a Source #

Create a tactic that applies each of the tactics in the list to one subgoal.

When the number of subgoals is greater than the number of provided tactics, the identity tactic is applied to the remainder. When the number of subgoals is less than the number of provided tactics, the remaining tactics are ignored.

(<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a infixr 3 Source #

t1 % t2 will interleave the execution of t1 and t2. This is useful if t1 will produce an infinite number of extracts, as we will still run t2. This is contrasted with t1 | t2, which will not ever consider t2 if t1 produces an infinite number of extracts.

commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a Source #

commit t1 t2 will run t1, and then only run t2 if t1 failed to produce any extracts.

try :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #

Tries to run a tactic, backtracking on failure

many_ :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #

Runs a tactic repeatedly until it fails

choice :: Monad m => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a Source #

choice ts will run all of the tactics in the list against the current subgoals, and interleave their extracts in a manner similar to <%>.

progress :: Monad m => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a Source #

progress eq err t applies the tactic t, and checks to see if the resulting subgoals are all equal to the initial goal by using eq. If they are, it throws 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 Source #

gather t f runs the tactic t, then runs f with all of the generated subgoals to determine the next tactic to run.

pruning :: MonadExtract ext m => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m () Source #

pruning t f runs the tactic t, and then applies a predicate to all of the generated subgoals.

ensure :: Monad m => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #

filterT p f t runs the tactic t, and applies a predicate to the state after the execution of t. We also run a "cleanup" function f. Note that the predicate is applied to the state _before_ the cleanup function is run.

Subgoal Manipulation

goal :: Functor m => TacticT jdg ext err s m jdg Source #

Get the current goal

focus :: Functor m => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #

Apply the first tactic, and then apply the second tactic focused on the nth subgoal.

Tactic Creation

class Monad m => MonadExtract ext m | m -> ext where Source #

Minimal complete definition

Nothing

Methods

hole :: m ext Source #

Generates a "hole" of type ext, which should represent an incomplete extract.

hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext Source #

Generates a "hole" of type ext, which should represent an incomplete extract.

Instances

MonadExtract ext m => MonadExtract ext (ExceptT err m) Source #
Instance details Defined in Refinery.ProofState Methods hole :: ExceptT err m ext Source #
(MonadExtract ext m, Monoid w) => MonadExtract ext (WriterT w m) Source #
Instance details Defined in Refinery.ProofState Methods hole :: WriterT w m ext Source #
(MonadExtract ext m, Monoid w) => MonadExtract ext (WriterT w m) Source #
Instance details Defined in Refinery.ProofState Methods hole :: WriterT w m ext Source #
MonadExtract ext m => MonadExtract ext (StateT s m) Source #
Instance details Defined in Refinery.ProofState Methods hole :: StateT s m ext Source #
MonadExtract ext m => MonadExtract ext (ReaderT r m) Source #
Instance details Defined in Refinery.ProofState Methods hole :: ReaderT r m ext Source #

class Monad m => MonadRule jdg ext m | m -> jdg, m -> ext where Source #

Minimal complete definition

Nothing

Methods

subgoal :: jdg -> m ext Source #

Create a subgoal, and return the resulting extract.

subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext Source #

Create a subgoal, and return the resulting extract.

Instances

MonadRule jdg ext m => MonadRule jdg ext (ExceptT env m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods subgoal :: jdg -> ExceptT env m ext Source #
MonadRule jdg ext m => MonadRule jdg ext (StateT env m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods subgoal :: jdg -> StateT env m ext Source #
MonadRule jdg ext m => MonadRule jdg ext (ReaderT env m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods subgoal :: jdg -> ReaderT env m ext Source #
Monad m => MonadRule jdg ext (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods subgoal :: jdg -> RuleT jdg ext err s m ext Source #

data RuleT jdg ext err s m a Source #

A RuleT is a monad transformer for creating inference rules.

Instances

Monad m => MonadRule jdg ext (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods subgoal :: jdg -> RuleT jdg ext err s m ext Source #
Monad m => MonadState s (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods get :: RuleT jdg ext err s m s # put :: s -> RuleT jdg ext err s m () # state :: (s -> (a, s)) -> RuleT jdg ext err s m a #
MonadReader r m => MonadReader r (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods ask :: RuleT jdg ext err s m r # local :: (r -> r) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m a # reader :: (r -> a) -> RuleT jdg ext err s m a #
Monad m => MonadError err (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods throwError :: err -> RuleT jdg ext err s m a # catchError :: RuleT jdg ext err s m a -> (err -> RuleT jdg ext err s m a) -> RuleT jdg ext err s m a #
MFunctor (RuleT jdg ext err s :: (Type -> Type) -> Type -> Type) Source #
Instance details Defined in Refinery.Tactic.Internal Methods hoist :: Monad m => (forall a. m a -> n a) -> RuleT jdg ext err s m b -> RuleT jdg ext err s n b #
MonadTrans (RuleT jdg ext err s) Source #
Instance details Defined in Refinery.Tactic.Internal Methods lift :: Monad m => m a -> RuleT jdg ext err s m a #
Monad m => Monad (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods (>>=) :: RuleT jdg ext err s m a -> (a -> RuleT jdg ext err s m b) -> RuleT jdg ext err s m b # (>>) :: RuleT jdg ext err s m a -> RuleT jdg ext err s m b -> RuleT jdg ext err s m b # return :: a -> RuleT jdg ext err s m a # fail :: String -> RuleT jdg ext err s m a #
Functor m => Functor (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods fmap :: (a -> b) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m b # (<$) :: a -> RuleT jdg ext err s m b -> RuleT jdg ext err s m a #
Monad m => Applicative (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods pure :: a -> RuleT jdg ext err s m a # (<>) :: RuleT jdg ext err s m (a -> b) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m b # liftA2 :: (a -> b -> c) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m b -> RuleT jdg ext err s m c # (>) :: RuleT jdg ext err s m a -> RuleT jdg ext err s m b -> RuleT jdg ext err s m b # (<*) :: RuleT jdg ext err s m a -> RuleT jdg ext err s m b -> RuleT jdg ext err s m a #
MonadIO m => MonadIO (RuleT jdg ext err s m) Source #
Instance details Defined in Refinery.Tactic.Internal Methods liftIO :: IO a -> RuleT jdg ext err s m a #
(Show jdg, Show err, Show a, Show (m (ProofStateT ext a err s m jdg))) => Show (RuleT jdg ext err s m a) Source #
Instance details Defined in Refinery.Tactic.Internal Methods showsPrec :: Int -> RuleT jdg ext err s m a -> ShowS # show :: RuleT jdg ext err s m a -> String # showList :: [RuleT jdg ext err s m a] -> ShowS #
Generic (RuleT jdg ext err s m a) Source #
Instance details Defined in Refinery.Tactic.Internal Associated Types type Rep (RuleT jdg ext err s m a) :: Type -> Type # Methods from :: RuleT jdg ext err s m a -> Rep (RuleT jdg ext err s m a) x # to :: Rep (RuleT jdg ext err s m a) x -> RuleT jdg ext err s m a #
type Rep (RuleT jdg ext err s m a) Source #
Instance details Defined in Refinery.Tactic.Internal type Rep (RuleT jdg ext err s m a) = D1 (MetaData "RuleT" "Refinery.Tactic.Internal" "refinery-0.3.0.0-Fdcu2SHDGUb4nunxmlwjIU" True) (C1 (MetaCons "RuleT" PrefixI True) (S1 (MetaSel (Just "unRuleT") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ProofStateT ext a err s m jdg))))

rule :: Monad m => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m () Source #

Turn an inference rule into a tactic.