Refinery.Tactic

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 : [e-mail]

Documentation

data TacticT jdg ext err s m a

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 'Prelude.()'

One of the most important things about this type is it's Monad instance. t1 >> t2 Will execute t1 against the current goal, and then execute t2 on _all_ of the subgoals generated by t2.

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.

Instances

Monad m => MonadState s (TacticT jdg ext err s m)

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

MFunctor (TacticT jdg ext err s :: (Type -> Type) -> Type -> Type)

Defined in Refinery.Tactic.Internal

Methods

hoist :: forall m n (b :: k). 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)

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)

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

Functor m => Functor (TacticT jdg ext err s m)

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)

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)

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)

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)

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)

Defined in Refinery.Tactic.Internal

Methods

throwM :: Exception e => e -> 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)

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)

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)

Defined in Refinery.Tactic.Internal

type Rep (TacticT jdg ext err s m a) = D1 ('MetaData "TacticT" "Refinery.Tactic.Internal" "refinery-0.4.0.0-E4mMDIorSqGEmfwVST0gYb" '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 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 backtrack on errors. If you want a version that provides partial proofs, use runPartialTacticT

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])

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 runTacticT.

Note that this version is inherently slower than runTacticT, as it needs to continue producing extracts.

evalTacticT :: MonadExtract meta ext err s m => TacticT jdg ext err s m () -> jdg -> s -> m [ext]

Run a tactic, and get just the list of extracts, ignoring any other information.

data Proof s meta goal ext

Represents a single result of the execution of some tactic.

Constructors

Proof

Fields

• pf_extract :: ext

  The extract of the tactic.

• pf_state :: s

  The state at the end of tactic execution.

• pf_unsolvedGoals :: [(meta, goal)]

  All the goals that were still unsolved by the end of tactic execution.

Instances

(Eq ext, Eq s, Eq meta, Eq goal) => Eq (Proof s meta goal ext)

Defined in Refinery.ProofState

Methods

(==) :: Proof s meta goal ext -> Proof s meta goal ext -> Bool

(/=) :: Proof s meta goal ext -> Proof s meta goal ext -> Bool

(Show ext, Show s, Show meta, Show goal) => Show (Proof s meta goal ext)

Defined in Refinery.ProofState

Methods

showsPrec :: Int -> Proof s meta goal ext -> ShowS

show :: Proof s meta goal ext -> String

showList :: [Proof s meta goal ext] -> ShowS

Generic (Proof s meta goal ext)

Defined in Refinery.ProofState

Associated Types

type Rep (Proof s meta goal ext) :: Type -> Type

Methods

from :: Proof s meta goal ext -> Rep (Proof s meta goal ext) x

to :: Rep (Proof s meta goal ext) x -> Proof s meta goal ext

type Rep (Proof s meta goal ext)

Defined in Refinery.ProofState

type Rep (Proof s meta goal ext) = D1 ('MetaData "Proof" "Refinery.ProofState" "refinery-0.4.0.0-E4mMDIorSqGEmfwVST0gYb" 'False) (C1 ('MetaCons "Proof" 'PrefixI 'True) (S1 ('MetaSel ('Just "pf_extract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ext) :*: (S1 ('MetaSel ('Just "pf_state") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s) :*: S1 ('MetaSel ('Just "pf_unsolvedGoals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(meta, goal)]))))

data PartialProof s err meta goal ext

The result of executing partialProofs.

Constructors

PartialProof ext s [(meta, goal)] [(meta, err)]

A so called "partial proof". These are proofs that encountered errors during execution.

Instances

(Eq ext, Eq s, Eq meta, Eq goal, Eq err) => Eq (PartialProof s err meta goal ext)

Defined in Refinery.ProofState

Methods

(==) :: PartialProof s err meta goal ext -> PartialProof s err meta goal ext -> Bool

(/=) :: PartialProof s err meta goal ext -> PartialProof s err meta goal ext -> Bool

(Show ext, Show s, Show meta, Show goal, Show err) => Show (PartialProof s err meta goal ext)

Defined in Refinery.ProofState

Methods

showsPrec :: Int -> PartialProof s err meta goal ext -> ShowS

show :: PartialProof s err meta goal ext -> String

showList :: [PartialProof s err meta goal ext] -> ShowS

Generic (PartialProof s err meta goal ext)

Defined in Refinery.ProofState

Associated Types

type Rep (PartialProof s err meta goal ext) :: Type -> Type

Methods

from :: PartialProof s err meta goal ext -> Rep (PartialProof s err meta goal ext) x

to :: Rep (PartialProof s err meta goal ext) x -> PartialProof s err meta goal ext

type Rep (PartialProof s err meta goal ext)

Defined in Refinery.ProofState

type Rep (PartialProof s err meta goal ext) = D1 ('MetaData "PartialProof" "Refinery.ProofState" "refinery-0.4.0.0-E4mMDIorSqGEmfwVST0gYb" 'False) (C1 ('MetaCons "PartialProof" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ext) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(meta, goal)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(meta, err)]))))

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

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

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.

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

Tries to run a tactic, backtracking on failure

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 will run t1, and then run t2 only if t1 (and all subsequent tactics) failed to produce any successes.

NOTE: commit does have some sneaky semantics that you have to be aware of. Specifically, it interacts a bit surprisingly with >>=. Namely, the following algebraic law holds commit t1 t2 >>= f = commit (t1 >>= f) (t2 >>= f) For instance, if you have something like commit t1 t2 >>= somethingThatMayFail, then this law implies that this is the same as commit (t1 >>= somethingThatMayFail) (t2 >>= somethingThatMayFail), which means that we might execute t2 _even if_ t1 seemingly succeeds.

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

Runs a tactic 0 or more times until it fails. Note that many_ is almost always the right choice over many. Due to the semantics of Alternative, many 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 ()

Runs a tactic 1 or more times until it fails. Note that some_ is almost always the right choice over some. Due to the semantics of Alternative, some will create a bunch of partially solved goals along the way, one for each iteration.

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

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

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.

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

ensure 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.

Errors and Error Handling

failure :: err -> TacticT jdg ext err s m a

failure err will create an unsolvable hole that will be ignored by subsequent tactics.

handler :: (err -> m err) -> TacticT jdg ext err s m ()

handler f 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: handler f >> handler g >> failure err Here, g will get run before f.

handler_ :: Functor m => (err -> m ()) -> TacticT jdg ext err s m ()

A variant of handler that doesn't modify the error at all, and solely exists to run effects.

Extract Manipulation

tweak :: Functor m => (ext -> ext) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

tweak f t lets us modify the extract produced by the tactic t.

Subgoal Manipulation

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

Get the current goal

inspect :: Functor m => (jdg -> a) -> TacticT jdg ext err s m a

Inspect 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 ()

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

Tactic Creation

class Monad m => MonadExtract meta ext err s m | m -> ext, m -> err, ext -> meta where

MonadExtract describes the effects required to generate named holes. The meta type parameter here is a so called "metavariable", which can be thought of as a name for a hole.

Minimal complete definition

Nothing

Methods

hole :: StateT s m (meta, ext)

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

default hole :: (MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => StateT s m (meta, ext)

unsolvableHole :: err -> StateT s m (meta, ext)

Generates an "unsolvable hole" of type err, which should represent an incomplete extract that we have no hope of solving.

These will get generated when you generate partial extracts via runPartialTacticT.

default unsolvableHole :: (MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => err -> StateT s m (meta, ext)

Instances

MonadExtract meta ext err s m => MonadExtract meta ext err s (ExceptT err m)

Defined in Refinery.ProofState

Methods

hole :: StateT s (ExceptT err m) (meta, ext)

unsolvableHole :: err -> StateT s (ExceptT err m) (meta, ext)

(MonadExtract meta ext err s m, Monoid w) => MonadExtract meta ext err s (WriterT w m)

Defined in Refinery.ProofState

Methods

hole :: StateT s (WriterT w m) (meta, ext)

unsolvableHole :: err -> StateT s (WriterT w m) (meta, ext)

(MonadExtract meta ext err s m, Monoid w) => MonadExtract meta ext err s (WriterT w m)

Defined in Refinery.ProofState

Methods

hole :: StateT s (WriterT w m) (meta, ext)

unsolvableHole :: err -> StateT s (WriterT w m) (meta, ext)

MonadExtract meta ext err s m => MonadExtract meta ext err s (StateT s m)

Defined in Refinery.ProofState

Methods

hole :: StateT s (StateT s m) (meta, ext)

unsolvableHole :: err -> StateT s (StateT s m) (meta, ext)

MonadExtract meta ext err s m => MonadExtract meta ext err s (ReaderT r m)

Defined in Refinery.ProofState

Methods

hole :: StateT s (ReaderT r m) (meta, ext)

unsolvableHole :: err -> StateT s (ReaderT r m) (meta, ext)

data RuleT jdg ext err s m a

A RuleT is a monad transformer for creating inference rules.

Instances

Monad m => MonadState s (RuleT jdg ext err s m)

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

MFunctor (RuleT jdg ext err s :: (Type -> Type) -> Type -> Type)

Defined in Refinery.Tactic.Internal

Methods

hoist :: forall m n (b :: k). 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)

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)

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

Functor m => Functor (RuleT jdg ext err s m)

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)

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)

Defined in Refinery.Tactic.Internal

Methods

liftIO :: IO a -> RuleT jdg ext err s m a

Monad m => Alternative (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

empty :: RuleT jdg ext err s m a

(<|>) :: RuleT jdg ext err s m a -> RuleT jdg ext err s m a -> RuleT jdg ext err s m a

some :: RuleT jdg ext err s m a -> RuleT jdg ext err s m [a]

many :: RuleT jdg ext err s m 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)

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)

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)

Defined in Refinery.Tactic.Internal

type Rep (RuleT jdg ext err s m a) = D1 ('MetaData "RuleT" "Refinery.Tactic.Internal" "refinery-0.4.0.0-E4mMDIorSqGEmfwVST0gYb" '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 ()

Turn an inference rule that examines the current goal into a tactic.

rule_ :: Monad m => RuleT jdg ext err s m ext -> TacticT jdg ext err s m ()

Turn an inference rule into a tactic.

subgoal :: jdg -> RuleT jdg ext err s m ext

Create a subgoal, and return the resulting extract.

unsolvable :: err -> 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.

Introspection

class MetaSubst meta ext | ext -> meta where

MetaSubst captures the notion of substituting metavariables of type meta into an extract of type ext. Note that these substitutions should most likely _not_ be capture avoiding.

Methods

substMeta :: meta -> ext -> ext -> ext

substMeta meta e1 e2 will substitute all occurances of meta in e2 with e1.

class MetaSubst meta ext => DependentMetaSubst meta jdg ext where

DependentMetaSubst captures the notion of substituting metavariables of type meta into judgements of type jdg. 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 resume.

Methods

dependentSubst :: meta -> ext -> jdg -> jdg

dependentSubst meta e j will substitute all occurances of meta in j with e. 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.

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 ()

reify t f will execute the tactic t, and resolve all of it's subgoals by filling them with holes. The resulting subgoals and partial extract are then passed to f.

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 ()

resume goals partial allows for resumption of execution after a call to reify. If your language doesn't support dependent subgoals, consider using resume' instead.

resume' :: forall meta jdg ext err s m. (MetaSubst meta ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m ()

A version of resume 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 resume instead, as this will leave the dependent subgoals with holes in them.

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 ()

pruning t p will execute t, and then apply p to any subgoals it generates. If this predicate returns an error, we terminate the execution. Otherwise, we resume execution via resume'.

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 ()

peek t p will execute t, and then apply p to the extract it produces. If this predicate returns an error, we terminate the execution. Otherwise, we resume execution via resume'.

Note that the extract produced may contain holes, as it is the extract produced by running _just_ t against the current goal.

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 ()

attempt t1 t2 will partially execute t1, inspect it's result, and only run t2 if it fails. If t1 succeeded, we will resume' execution of it.