-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Toolkit for building proof automation systems
--   
--   Please see the README on GitHub at
--   <a>https://github.com/githubuser/refinery#readme</a>
@package refinery
@version 0.4.0.0


-- | The datatype that drives both Rules and Tactics
--   
--   If you just want to build tactics, you probably want to use
--   <a>Tactic</a> instead. However, if you need to get involved in the
--   core of the library, this is the place to start.
--   
--   Module : Refinery.ProofState Copyright : (c) Reed Mullanix 2019
--   License : BSD-style Maintainer : reedmullanix@gmail.com
module Refinery.ProofState

-- | The core data type of the library. This represents a reified,
--   in-progress proof strategy for a particular goal.
--   
--   NOTE: We need to split up the extract type into <tt>ext'</tt> and
--   <tt>ext</tt>, as we want to be functorial (and monadic) in
--   <tt>ext</tt>, but it shows up in both co and contravariant positions.
--   Splitting the type variable up into two solves this problem, at the
--   cost of looking ugly.
data ProofStateT ext' ext err s m goal

-- | Represents a subgoal, and a continuation that tells us what to do with
--   the resulting extract.
Subgoal :: goal -> (ext' -> ProofStateT ext' ext err s m goal) -> ProofStateT ext' ext err s m goal

-- | Run an effect.
Effect :: m (ProofStateT ext' ext err s m goal) -> ProofStateT ext' ext err s m goal

-- | Run a stateful computation. We don't want to use <a>StateT</a> here,
--   as it doesn't play nice with backtracking.
Stateful :: (s -> (s, ProofStateT ext' ext err s m goal)) -> ProofStateT ext' ext err s m goal

-- | Combine together the results of two <tt>ProofState</tt>s, preserving
--   the order that they were synthesized in.
Alt :: ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal

-- | Similar to <a>Alt</a>, but will interleave the results, rather than
--   just appending them. This is useful if the first argument produces
--   potentially infinite results.
Interleave :: ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal

-- | <a>Commit</a> runs the first proofstate, and only runs the second if
--   the first does not produce any successful results.
Commit :: ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal

-- | Silent failure. Always causes a backtrack, unlike <a>Failure</a>.
Empty :: ProofStateT ext' ext err s m goal

-- | This does double duty, depending on whether or not the user calls
--   <a>proofs</a> or <a>partialProofs</a>. In the first case, we ignore
--   the continutation, backtrack, and return an error in the result of
--   <a>proofs</a>. In the second, we treat this as a sort of "unsolvable
--   subgoal", and call the continuation with a hole.
Failure :: err -> (ext' -> ProofStateT ext' ext err s m goal) -> ProofStateT ext' ext err s m goal

-- | An installed error handler. These allow us to add annotations to
--   errors, or run effects.
Handle :: ProofStateT ext' ext err s m goal -> (err -> m err) -> ProofStateT ext' ext err s m goal

-- | Represents a simple extract.
Axiom :: ext -> ProofStateT ext' ext err s m goal

-- | <a>MonadExtract</a> describes the effects required to generate named
--   holes. The <tt>meta</tt> type parameter here is a so called
--   "metavariable", which can be thought of as a name for a hole.
class (Monad m) => MonadExtract meta ext err s m | m -> ext, m -> err, ext -> meta

-- | Generates a named "hole" of type <tt>ext</tt>, which should represent
--   an incomplete extract.
hole :: MonadExtract meta ext err s m => StateT s m (meta, ext)

-- | Generates a named "hole" of type <tt>ext</tt>, which should represent
--   an incomplete extract.
hole :: (MonadExtract meta ext err s m, MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => StateT s m (meta, ext)

-- | Generates an "unsolvable hole" of type <tt>err</tt>, which should
--   represent an incomplete extract that we have no hope of solving.
--   
--   These will get generated when you generate partial extracts via
--   <a>runPartialTacticT</a>.
unsolvableHole :: MonadExtract meta ext err s m => err -> StateT s m (meta, ext)

-- | Generates an "unsolvable hole" of type <tt>err</tt>, which should
--   represent an incomplete extract that we have no hope of solving.
--   
--   These will get generated when you generate partial extracts via
--   <a>runPartialTacticT</a>.
unsolvableHole :: (MonadExtract meta ext err s m, MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => err -> StateT s m (meta, ext)

-- | Represents a single result of the execution of some tactic.
data Proof s meta goal ext
Proof :: ext -> s -> [(meta, goal)] -> Proof s meta goal ext

-- | The extract of the tactic.
[pf_extract] :: Proof s meta goal ext -> ext

-- | The state at the end of tactic execution.
[pf_state] :: Proof s meta goal ext -> s

-- | All the goals that were still unsolved by the end of tactic execution.
[pf_unsolvedGoals] :: Proof s meta goal ext -> [(meta, goal)]

-- | The result of executing <a>partialProofs</a>.
data PartialProof s err meta goal ext

-- | A so called "partial proof". These are proofs that encountered errors
--   during execution.
PartialProof :: ext -> s -> [(meta, goal)] -> [(meta, err)] -> PartialProof s err meta goal ext

-- | Interpret a <a>ProofStateT</a> into a list of (possibly incomplete)
--   extracts. This function will cause a proof to terminate when it
--   encounters a <a>Failure</a>, and will return a <a>Left</a>. If you
--   want to still recieve an extract even when you encounter a failure,
--   you should use <a>partialProofs</a>.
proofs :: forall ext err s m goal meta. MonadExtract meta ext err s m => s -> ProofStateT ext ext err s m goal -> m (Either [err] [Proof s meta goal ext])

-- | Interpret a <a>ProofStateT</a> into a list of (possibly incomplete)
--   extracts. This function will continue producing an extract when it
--   encounters a <a>Failure</a>, leaving a hole in the extract in it's
--   place. If you want the extraction to terminate when you encounter an
--   error, you should use <a>proofs</a>.
partialProofs :: forall meta ext err s m goal. MonadExtract meta ext err s m => s -> ProofStateT ext ext err s m goal -> m (Either [PartialProof s err meta goal ext] [Proof s meta goal ext])

-- | <tt>subgoals fs p</tt> will apply a list of functions producing a new
--   <a>ProofStateT</a> to each of the subgoals of <tt>p</tt> in order. If
--   the list of functions is longer than the number of subgoals, then the
--   extra functions are ignored. If the list of functions is shorter, then
--   we simply apply <tt>pure</tt> to all of the remaining subgoals.
subgoals :: Functor m => [jdg -> ProofStateT ext ext err s m jdg] -> ProofStateT ext ext err s m jdg -> ProofStateT ext ext err s m jdg

-- | <tt>mapExtract f g p</tt> allows yout to modify the extract type of a
--   ProofState. This witness the <tt>Profunctor</tt> instance of
--   <a>ProofStateT</a>, which we can't write without a newtype due to the
--   position of the type variables
mapExtract :: Functor m => (a -> ext') -> (ext -> b) -> ProofStateT ext' ext err s m jdg -> ProofStateT a b err s m jdg

-- | <a>MetaSubst</a> captures the notion of substituting metavariables of
--   type <tt>meta</tt> into an extract of type <tt>ext</tt>. Note that
--   these substitutions should most likely _not_ be capture avoiding.
class MetaSubst meta ext | ext -> meta

-- | <tt>substMeta meta e1 e2</tt> will substitute all occurances of
--   <tt>meta</tt> in <tt>e2</tt> with <tt>e1</tt>.
substMeta :: MetaSubst meta ext => meta -> ext -> ext -> ext

-- | <a>DependentMetaSubst</a> captures the notion of substituting
--   metavariables of type <tt>meta</tt> into judgements of type
--   <tt>jdg</tt>. This really only matters when you are dealing with
--   dependent types, specifically existentials. For instance, consider the
--   goal Σ (x : A) (B x) The type of the second goal we would produce here
--   _depends_ on the solution to the first goal, so we need to know how to
--   substitute holes in judgements in order to properly implement
--   <a>resume</a>.
class MetaSubst meta ext => DependentMetaSubst meta jdg ext

-- | <tt>dependentSubst meta e j</tt> will substitute all occurances of
--   <tt>meta</tt> in <tt>j</tt> with <tt>e</tt>. This method only really
--   makes sense if you have goals that depend on earlier extracts. If this
--   isn't the case, don't implement this.
dependentSubst :: DependentMetaSubst meta jdg ext => meta -> ext -> jdg -> jdg

-- | <tt>speculate s p</tt> will record the current state of the proof as
--   part of the extraction process. In doing so, this will also remove any
--   subgoal constructors by filling them with holes.
speculate :: forall meta ext err s m jdg x. MonadExtract meta ext err s m => s -> ProofStateT ext ext err s m jdg -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
instance GHC.Base.Functor m => GHC.Base.Functor (Refinery.ProofState.ProofStateT ext' ext err s m)
instance GHC.Generics.Generic (Refinery.ProofState.ProofStateT ext' ext err s m goal)
instance GHC.Generics.Generic (Refinery.ProofState.Proof s meta goal ext)
instance (GHC.Show.Show ext, GHC.Show.Show s, GHC.Show.Show meta, GHC.Show.Show goal) => GHC.Show.Show (Refinery.ProofState.Proof s meta goal ext)
instance (GHC.Classes.Eq ext, GHC.Classes.Eq s, GHC.Classes.Eq meta, GHC.Classes.Eq goal) => GHC.Classes.Eq (Refinery.ProofState.Proof s meta goal ext)
instance GHC.Generics.Generic (Refinery.ProofState.PartialProof s err meta goal ext)
instance (GHC.Show.Show ext, GHC.Show.Show s, GHC.Show.Show meta, GHC.Show.Show goal, GHC.Show.Show err) => GHC.Show.Show (Refinery.ProofState.PartialProof s err meta goal ext)
instance (GHC.Classes.Eq ext, GHC.Classes.Eq s, GHC.Classes.Eq meta, GHC.Classes.Eq goal, GHC.Classes.Eq err) => GHC.Classes.Eq (Refinery.ProofState.PartialProof s err meta goal ext)
instance Refinery.ProofState.MonadExtract meta ext err s m => Refinery.ProofState.MonadExtract meta ext err s (Control.Monad.Trans.Reader.ReaderT r m)
instance Refinery.ProofState.MonadExtract meta ext err s m => Refinery.ProofState.MonadExtract meta ext err s (Control.Monad.Trans.State.Lazy.StateT s m)
instance (Refinery.ProofState.MonadExtract meta ext err s m, GHC.Base.Monoid w) => Refinery.ProofState.MonadExtract meta ext err s (Control.Monad.Trans.Writer.Lazy.WriterT w m)
instance (Refinery.ProofState.MonadExtract meta ext err s m, GHC.Base.Monoid w) => Refinery.ProofState.MonadExtract meta ext err s (Control.Monad.Trans.Writer.Strict.WriterT w m)
instance Refinery.ProofState.MonadExtract meta ext err s m => Refinery.ProofState.MonadExtract meta ext err s (Control.Monad.Trans.Except.ExceptT err m)
instance (GHC.Show.Show goal, GHC.Show.Show err, GHC.Show.Show ext, GHC.Show.Show (m (Refinery.ProofState.ProofStateT ext' ext err s m goal))) => GHC.Show.Show (Refinery.ProofState.ProofStateT ext' ext err s m goal)
instance GHC.Base.Functor m => GHC.Base.Applicative (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Morph.MFunctor (Refinery.ProofState.ProofStateT ext' ext err s)
instance GHC.Base.Functor m => GHC.Base.Monad (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Trans.Class.MonadTrans (Refinery.ProofState.ProofStateT ext ext err s)
instance GHC.Base.Monad m => GHC.Base.Alternative (Refinery.ProofState.ProofStateT ext ext err s m)
instance GHC.Base.Monad m => GHC.Base.MonadPlus (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Catch.MonadThrow m => Control.Monad.Catch.MonadThrow (Refinery.ProofState.ProofStateT ext ext err s m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState s (Refinery.ProofState.ProofStateT ext ext err s m)


-- | <h1>WARNING</h1>
--   
--   This module is considered <b>internal</b>, and can change at any given
--   time.
module Refinery.Tactic.Internal

-- | A <tt><a>TacticT</a></tt> is a monad transformer that performs proof
--   refinement. The type variables signifiy:
--   
--   <ul>
--   <li><tt>jdg</tt> - The goal type. This is the thing we are trying to
--   construct a proof of.</li>
--   <li><tt>ext</tt> - The extract type. This is what we will recieve
--   after running the tactic.</li>
--   <li><tt>err</tt> - The error type. We can use <a>throwError</a> to
--   abort the computation with a provided error</li>
--   <li><tt>s</tt> - The state type.</li>
--   <li><tt>m</tt> - The base monad.</li>
--   <li><tt>a</tt> - The return value. This to make
--   <tt><a>TacticT</a></tt> a monad, and will always be
--   <tt>'Prelude.()'</tt></li>
--   </ul>
--   
--   One of the most important things about this type is it's <a>Monad</a>
--   instance. <tt>t1 &gt;&gt; t2</tt> Will execute <tt>t1</tt> against the
--   current goal, and then execute <tt>t2</tt> on _all_ of the subgoals
--   generated by <tt>t2</tt>.
--   
--   This Monad instance is lawful, and has been tested thouroughly, and a
--   version of it has been formally verified in Agda. _However_, just
--   because it is correct doesn't mean that it lines up with your
--   intuitions of how Monads behave! In practice, it feels like a
--   combination of the Non-Determinisitic Monads and some of the Time
--   Travelling ones. That doesn't mean that it's impossible to understand,
--   just that it may push the boundaries of you intuitions.
newtype TacticT jdg ext err s m a
TacticT :: StateT jdg (ProofStateT ext ext err s m) a -> TacticT jdg ext err s m a
[unTacticT] :: TacticT jdg ext err s m a -> StateT jdg (ProofStateT ext ext err s m) a

-- | Helper function for producing a tactic.
tactic :: (jdg -> ProofStateT ext ext err s m (a, jdg)) -> TacticT jdg ext err s m a

-- | <tt>proofState t j</tt> will deconstruct a tactic <tt>t</tt> into a
--   <a>ProofStateT</a> by running it at <tt>j</tt>.
proofState :: TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m (a, jdg)

-- | Like <a>proofState</a>, but we discard the return value of <tt>t</tt>.
proofState_ :: Functor m => TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg

-- | Map the unwrapped computation using the given function
mapTacticT :: Monad m => (m a -> m b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b

-- | A <tt><a>RuleT</a></tt> is a monad transformer for creating inference
--   rules.
newtype RuleT jdg ext err s m a
RuleT :: ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
[unRuleT] :: RuleT jdg ext err s m a -> ProofStateT ext a err s m jdg

-- | Create a subgoal, and return the resulting extract.
subgoal :: jdg -> RuleT jdg ext err s m ext

-- | Create an "unsolvable" hole. These holes are ignored by subsequent
--   tactics, but do not cause a backtracking failure.
unsolvable :: err -> RuleT jdg ext err s m ext
instance GHC.Generics.Generic (Refinery.Tactic.Internal.TacticT jdg ext err s m a)
instance Control.Monad.Catch.MonadThrow m => Control.Monad.Catch.MonadThrow (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.MonadPlus (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Functor m => GHC.Base.Monad (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.Alternative (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Functor m => GHC.Base.Applicative (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Functor m => GHC.Base.Functor (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Generics.Generic (Refinery.Tactic.Internal.RuleT jdg ext err s m a)
instance (GHC.Show.Show jdg, GHC.Show.Show err, GHC.Show.Show a, GHC.Show.Show (m (Refinery.ProofState.ProofStateT ext a err s m jdg))) => GHC.Show.Show (Refinery.Tactic.Internal.RuleT jdg ext err s m a)
instance GHC.Base.Functor m => GHC.Base.Functor (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.Alternative (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.Monad (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState s (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance Control.Monad.Trans.Class.MonadTrans (Refinery.Tactic.Internal.RuleT jdg ext err s)
instance Control.Monad.Morph.MFunctor (Refinery.Tactic.Internal.RuleT jdg ext err s)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance (GHC.Base.Monoid jdg, GHC.Show.Show a, GHC.Show.Show jdg, GHC.Show.Show err, GHC.Show.Show ext, GHC.Show.Show (m (Refinery.ProofState.ProofStateT ext ext err s m (a, jdg)))) => GHC.Show.Show (Refinery.Tactic.Internal.TacticT jdg ext err s m a)
instance Control.Monad.Morph.MFunctor (Refinery.Tactic.Internal.TacticT jdg ext err s)
instance Control.Monad.Trans.Class.MonadTrans (Refinery.Tactic.Internal.TacticT jdg ext err s)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState s (Refinery.Tactic.Internal.TacticT jdg ext err s m)


-- | Tactics and Tactic Combinators
--   
--   This module contains everything you need to start defining tactics and
--   tactic combinators. Module : Refinery.Tactic Copyright : (c) Reed
--   Mullanix 2019 License : BSD-style Maintainer : reedmullanix@gmail.com
module Refinery.Tactic

-- | A <tt><a>TacticT</a></tt> is a monad transformer that performs proof
--   refinement. The type variables signifiy:
--   
--   <ul>
--   <li><tt>jdg</tt> - The goal type. This is the thing we are trying to
--   construct a proof of.</li>
--   <li><tt>ext</tt> - The extract type. This is what we will recieve
--   after running the tactic.</li>
--   <li><tt>err</tt> - The error type. We can use <a>throwError</a> to
--   abort the computation with a provided error</li>
--   <li><tt>s</tt> - The state type.</li>
--   <li><tt>m</tt> - The base monad.</li>
--   <li><tt>a</tt> - The return value. This to make
--   <tt><a>TacticT</a></tt> a monad, and will always be
--   <tt>'Prelude.()'</tt></li>
--   </ul>
--   
--   One of the most important things about this type is it's <a>Monad</a>
--   instance. <tt>t1 &gt;&gt; t2</tt> Will execute <tt>t1</tt> against the
--   current goal, and then execute <tt>t2</tt> on _all_ of the subgoals
--   generated by <tt>t2</tt>.
--   
--   This Monad instance is lawful, and has been tested thouroughly, and a
--   version of it has been formally verified in Agda. _However_, just
--   because it is correct doesn't mean that it lines up with your
--   intuitions of how Monads behave! In practice, it feels like a
--   combination of the Non-Determinisitic Monads and some of the Time
--   Travelling ones. That doesn't mean that it's impossible to understand,
--   just that it may push the boundaries of you intuitions.
data TacticT jdg ext err s m a

-- | Runs a tactic, producing a list of possible extracts, along with a
--   list of unsolved subgoals. Note that this function will backtrack on
--   errors. If you want a version that provides partial proofs, use
--   <a>runPartialTacticT</a>
runTacticT :: MonadExtract meta ext err s m => TacticT jdg ext err s m () -> jdg -> s -> m (Either [err] [Proof s meta jdg ext])

-- | Runs a tactic, producing a list of possible extracts, along with a
--   list of unsolved subgoals. Note that this function will produce a so
--   called "Partial Proof". This means that we no longer backtrack on
--   errors, but rather leave an unsolved hole, and continue synthesizing a
--   extract. If you want a version that backgracks on errors, see
--   <a>runTacticT</a>.
--   
--   Note that this version is inherently slower than <a>runTacticT</a>, as
--   it needs to continue producing extracts.
runPartialTacticT :: MonadExtract meta ext err s m => TacticT jdg ext err s m () -> jdg -> s -> m (Either [PartialProof s err meta jdg ext] [Proof s meta jdg ext])

-- | Run a tactic, and get just the list of extracts, ignoring any other
--   information.
evalTacticT :: MonadExtract meta ext err s m => TacticT jdg ext err s m () -> jdg -> s -> m [ext]

-- | Represents a single result of the execution of some tactic.
data Proof s meta goal ext
Proof :: ext -> s -> [(meta, goal)] -> Proof s meta goal ext

-- | The extract of the tactic.
[pf_extract] :: Proof s meta goal ext -> ext

-- | The state at the end of tactic execution.
[pf_state] :: Proof s meta goal ext -> s

-- | All the goals that were still unsolved by the end of tactic execution.
[pf_unsolvedGoals] :: Proof s meta goal ext -> [(meta, goal)]

-- | The result of executing <a>partialProofs</a>.
data PartialProof s err meta goal ext

-- | A so called "partial proof". These are proofs that encountered errors
--   during execution.
PartialProof :: ext -> s -> [(meta, goal)] -> [(meta, err)] -> PartialProof s err meta goal ext

-- | 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.
(<@>) :: Functor m => TacticT jdg ext err s m a -> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a

-- | <tt>t1 <a>%</a> t2</tt> will interleave the execution of <tt>t1</tt>
--   and <tt>t2</tt>. This is useful if <tt>t1</tt> will produce an
--   infinite number of extracts, as we will still run <tt>t2</tt>. This is
--   contrasted with <tt>t1 <a>|</a> t2</tt>, which will not ever consider
--   <tt>t2</tt> if <tt>t1</tt> produces an infinite number of extracts.
(<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
infixr 3 <%>

-- | Tries to run a tactic, backtracking on failure
try :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

-- | <tt>commit t1 t2</tt> will run <tt>t1</tt>, and then run <tt>t2</tt>
--   only if <tt>t1</tt> (and all subsequent tactics) failed to produce any
--   successes.
--   
--   NOTE: <tt>commit</tt> does have some sneaky semantics that you have to
--   be aware of. Specifically, it interacts a bit surprisingly with
--   <a>&gt;&gt;=</a>. Namely, the following algebraic law holds <tt>
--   commit t1 t2 &gt;&gt;= f = commit (t1 &gt;&gt;= f) (t2 &gt;&gt;= f)
--   </tt> For instance, if you have something like <tt>commit t1 t2
--   &gt;&gt;= somethingThatMayFail</tt>, then this law implies that this
--   is the same as <tt>commit (t1 &gt;&gt;= somethingThatMayFail) (t2
--   &gt;&gt;= somethingThatMayFail)</tt>, which means that we might
--   execute <tt>t2</tt> _even if_ <tt>t1</tt> seemingly succeeds.
commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a

-- | Runs a tactic 0 or more times until it fails. Note that <a>many_</a>
--   is almost always the right choice over <a>many</a>. Due to the
--   semantics of <a>Alternative</a>, <a>many</a> will create a bunch of
--   partially solved goals along the way, one for each iteration.
many_ :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

-- | Runs a tactic 1 or more times until it fails. Note that <a>some_</a>
--   is almost always the right choice over <a>some</a>. Due to the
--   semantics of <a>Alternative</a>, <a>some</a> will create a bunch of
--   partially solved goals along the way, one for each iteration.
some_ :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

-- | <tt>choice ts</tt> will run all of the tactics in the list against the
--   current subgoals, and interleave their extracts in a manner similar to
--   <a>&lt;%&gt;</a>.
choice :: Monad m => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a

-- | <tt>progress eq err t</tt> applies the tactic <tt>t</tt>, and checks
--   to see if the resulting subgoals are all equal to the initial goal by
--   using <tt>eq</tt>. If they are, it throws <tt>err</tt>.
progress :: Monad m => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a

-- | <tt>ensure p f t</tt> runs the tactic <tt>t</tt>, and applies a
--   predicate to the state after the execution of <tt>t</tt>. We also run
--   a "cleanup" function <tt>f</tt>. Note that the predicate is applied to
--   the state _before_ the cleanup function is run.
ensure :: Monad m => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

-- | <tt>failure err</tt> will create an unsolvable hole that will be
--   ignored by subsequent tactics.
failure :: err -> TacticT jdg ext err s m a

-- | <tt>handler f</tt> will install an "error handler". These let you add
--   more context to errors, and potentially run effects. For instance, you
--   may want to take note that a particular situation is unsolvable, and
--   that we shouldn't attempt to run this series of tactics against a
--   given goal again.
--   
--   Note that handlers further down the stack get run before those higher
--   up the stack. For instance, consider the following example: <tt>
--   handler f &gt;&gt; handler g &gt;&gt; failure err </tt> Here,
--   <tt>g</tt> will get run before <tt>f</tt>.
handler :: (err -> m err) -> TacticT jdg ext err s m ()

-- | A variant of <a>handler</a> that doesn't modify the error at all, and
--   solely exists to run effects.
handler_ :: Functor m => (err -> m ()) -> TacticT jdg ext err s m ()

-- | <tt>tweak f t</tt> lets us modify the extract produced by the tactic
--   <tt>t</tt>.
tweak :: Functor m => (ext -> ext) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

-- | Get the current goal
goal :: Functor m => TacticT jdg ext err s m jdg

-- | Inspect the current goal.
inspect :: Functor m => (jdg -> a) -> TacticT jdg ext err s m a

-- | Apply the first tactic, and then apply the second tactic focused on
--   the <tt>n</tt>th subgoal.
focus :: Functor m => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

-- | <a>MonadExtract</a> describes the effects required to generate named
--   holes. The <tt>meta</tt> type parameter here is a so called
--   "metavariable", which can be thought of as a name for a hole.
class (Monad m) => MonadExtract meta ext err s m | m -> ext, m -> err, ext -> meta

-- | Generates a named "hole" of type <tt>ext</tt>, which should represent
--   an incomplete extract.
hole :: MonadExtract meta ext err s m => StateT s m (meta, ext)

-- | Generates a named "hole" of type <tt>ext</tt>, which should represent
--   an incomplete extract.
hole :: (MonadExtract meta ext err s m, MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => StateT s m (meta, ext)

-- | Generates an "unsolvable hole" of type <tt>err</tt>, which should
--   represent an incomplete extract that we have no hope of solving.
--   
--   These will get generated when you generate partial extracts via
--   <a>runPartialTacticT</a>.
unsolvableHole :: MonadExtract meta ext err s m => err -> StateT s m (meta, ext)

-- | Generates an "unsolvable hole" of type <tt>err</tt>, which should
--   represent an incomplete extract that we have no hope of solving.
--   
--   These will get generated when you generate partial extracts via
--   <a>runPartialTacticT</a>.
unsolvableHole :: (MonadExtract meta ext err s m, MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => err -> StateT s m (meta, ext)

-- | A <tt><a>RuleT</a></tt> is a monad transformer for creating inference
--   rules.
data RuleT jdg ext err s m a

-- | Turn an inference rule that examines the current goal into a tactic.
rule :: Monad m => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()

-- | Turn an inference rule into a tactic.
rule_ :: Monad m => RuleT jdg ext err s m ext -> TacticT jdg ext err s m ()

-- | Create a subgoal, and return the resulting extract.
subgoal :: jdg -> RuleT jdg ext err s m ext

-- | Create an "unsolvable" hole. These holes are ignored by subsequent
--   tactics, but do not cause a backtracking failure.
unsolvable :: err -> RuleT jdg ext err s m ext

-- | <a>MetaSubst</a> captures the notion of substituting metavariables of
--   type <tt>meta</tt> into an extract of type <tt>ext</tt>. Note that
--   these substitutions should most likely _not_ be capture avoiding.
class MetaSubst meta ext | ext -> meta

-- | <tt>substMeta meta e1 e2</tt> will substitute all occurances of
--   <tt>meta</tt> in <tt>e2</tt> with <tt>e1</tt>.
substMeta :: MetaSubst meta ext => meta -> ext -> ext -> ext

-- | <a>DependentMetaSubst</a> captures the notion of substituting
--   metavariables of type <tt>meta</tt> into judgements of type
--   <tt>jdg</tt>. This really only matters when you are dealing with
--   dependent types, specifically existentials. For instance, consider the
--   goal Σ (x : A) (B x) The type of the second goal we would produce here
--   _depends_ on the solution to the first goal, so we need to know how to
--   substitute holes in judgements in order to properly implement
--   <a>resume</a>.
class MetaSubst meta ext => DependentMetaSubst meta jdg ext

-- | <tt>dependentSubst meta e j</tt> will substitute all occurances of
--   <tt>meta</tt> in <tt>j</tt> with <tt>e</tt>. This method only really
--   makes sense if you have goals that depend on earlier extracts. If this
--   isn't the case, don't implement this.
dependentSubst :: DependentMetaSubst meta jdg ext => meta -> ext -> jdg -> jdg

-- | <tt>reify t f</tt> will execute the tactic <tt>t</tt>, and resolve all
--   of it's subgoals by filling them with holes. The resulting subgoals
--   and partial extract are then passed to <tt>f</tt>.
reify :: forall meta jdg ext err s m. MonadExtract meta ext err s m => TacticT jdg ext err s m () -> (Proof s meta jdg ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()

-- | <tt>resume goals partial</tt> allows for resumption of execution after
--   a call to <a>reify</a>. If your language doesn't support dependent
--   subgoals, consider using <tt>resume'</tt> instead.
resume :: forall meta jdg ext err s m. (DependentMetaSubst meta jdg ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m ()

-- | A version of <tt>resume</tt> that doesn't perform substitution into
--   the goal types. This only makes sense if your language doesn't support
--   dependent subgoals. If it does, use <tt>resume</tt> instead, as this
--   will leave the dependent subgoals with holes in them.
resume' :: forall meta jdg ext err s m. (MetaSubst meta ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m ()

-- | <tt>pruning t p</tt> will execute <tt>t</tt>, and then apply
--   <tt>p</tt> to any subgoals it generates. If this predicate returns an
--   error, we terminate the execution. Otherwise, we resume execution via
--   <a>resume'</a>.
pruning :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()

-- | <tt>peek t p</tt> will execute <tt>t</tt>, and then apply <tt>p</tt>
--   to the extract it produces. If this predicate returns an error, we
--   terminate the execution. Otherwise, we resume execution via
--   <a>resume'</a>.
--   
--   Note that the extract produced may contain holes, as it is the extract
--   produced by running _just_ <tt>t</tt> against the current goal.
peek :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> (ext -> Maybe err) -> TacticT jdg ext err s m ()

-- | <tt>attempt t1 t2</tt> will partially execute <tt>t1</tt>, inspect
--   it's result, and only run <tt>t2</tt> if it fails. If <tt>t1</tt>
--   succeeded, we will <a>resume'</a> execution of it.
attempt :: (MonadExtract meta ext err s m, MetaSubst meta ext) => TacticT jdg ext err s m () -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()