Safe Haskell  None 

Language  Haskell2010 
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 : BSDstyle Maintainer : reedmullanix@gmail.com
Synopsis
 data TacticT jdg 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])
 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])
 evalTacticT :: MonadExtract meta ext err s m => TacticT jdg ext err s m () > jdg > s > m [ext]
 data Proof s meta goal ext = Proof {
 pf_extract :: ext
 pf_state :: s
 pf_unsolvedGoals :: [(meta, goal)]
 data PartialProof s err meta goal ext = PartialProof ext s [(meta, goal)] [(meta, err)]
 (<@>) :: 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
 try :: Monad m => TacticT jdg ext err s m () > TacticT jdg ext err s m ()
 commit :: TacticT jdg ext err s m a > TacticT jdg ext err s m a > TacticT jdg ext err s m a
 many_ :: Monad m => TacticT jdg ext err s m () > TacticT jdg ext err s m ()
 some_ :: 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
 ensure :: Monad m => (s > Maybe err) > (s > s) > TacticT jdg ext err s m () > TacticT jdg ext err s m ()
 failure :: err > TacticT jdg ext err s m a
 handler :: (err > m err) > TacticT jdg ext err s m ()
 handler_ :: Functor m => (err > m ()) > TacticT jdg ext err s m ()
 tweak :: Functor m => (ext > ext) > TacticT jdg ext err s m () > TacticT jdg ext err s m ()
 goal :: Functor m => TacticT jdg ext err s m jdg
 inspect :: Functor m => (jdg > a) > TacticT jdg ext err s m a
 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 meta ext err s m  m > ext, m > err, ext > meta where
 hole :: StateT s m (meta, ext)
 unsolvableHole :: err > StateT s m (meta, 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 ()
 rule_ :: Monad m => RuleT jdg ext err s m ext > TacticT jdg ext err s m ()
 subgoal :: jdg > RuleT jdg ext err s m ext
 unsolvable :: err > RuleT jdg ext err s m ext
 class MetaSubst meta ext  ext > meta where
 substMeta :: meta > ext > ext > ext
 class MetaSubst meta ext => DependentMetaSubst meta jdg ext where
 dependentSubst :: meta > ext > jdg > jdg
 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 ()
 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' :: forall meta jdg ext err s m. (MetaSubst meta ext, Monad m) => Proof s meta jdg ext > TacticT jdg ext err s m ()
 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 ()
 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 ()
 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 ()
Documentation
data TacticT jdg ext err s m a Source #
A
is a monad transformer that performs proof refinement.
The type variables signifiy:TacticT
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 usethrowError
to abort the computation with a provided errors
 The state type.m
 The base monad.a
 The return value. This to make
a monad, and will always beTacticT
'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 NonDeterminisitic 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) Source #  
MFunctor (TacticT jdg ext err s :: (Type > Type) > Type > Type) Source #  
MonadTrans (TacticT jdg ext err s) Source #  
Defined in Refinery.Tactic.Internal  
Functor m => Monad (TacticT jdg ext err s m) Source #  
Functor m => Functor (TacticT jdg ext err s m) Source #  
Functor m => Applicative (TacticT jdg ext err s m) Source #  
Defined in Refinery.Tactic.Internal 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 #  
Defined in Refinery.Tactic.Internal  
Monad m => Alternative (TacticT jdg ext err s m) Source #  
Monad m => MonadPlus (TacticT jdg ext err s m) Source #  
MonadThrow m => MonadThrow (TacticT jdg ext err s m) Source #  
Defined in Refinery.Tactic.Internal  
(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 #  
Generic (TacticT jdg ext err s m a) Source #  
type Rep (TacticT jdg ext err s m a) Source #  
Defined in Refinery.Tactic.Internal type Rep (TacticT jdg ext err s m a) = D1 ('MetaData "TacticT" "Refinery.Tactic.Internal" "refinery0.4.0.0E4mMDIorSqGEmfwVST0gYb" '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]) Source #
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]) Source #
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] Source #
Run a tactic, and get just the list of extracts, ignoring any other information.
data Proof s meta goal ext Source #
Represents a single result of the execution of some tactic.
Proof  

Instances
(Eq ext, Eq s, Eq meta, Eq goal) => Eq (Proof s meta goal ext) Source #  
(Show ext, Show s, Show meta, Show goal) => Show (Proof s meta goal ext) Source #  
Generic (Proof s meta goal ext) Source #  
type Rep (Proof s meta goal ext) Source #  
Defined in Refinery.ProofState type Rep (Proof s meta goal ext) = D1 ('MetaData "Proof" "Refinery.ProofState" "refinery0.4.0.0E4mMDIorSqGEmfwVST0gYb" '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 Source #
The result of executing partialProofs
.
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) Source #  
Defined in Refinery.ProofState (==) :: 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) Source #  
Defined in Refinery.ProofState 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) Source #  
Defined in Refinery.ProofState type Rep (PartialProof s err meta goal ext) :: Type > Type # 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) Source #  
Defined in Refinery.ProofState type Rep (PartialProof s err meta goal ext) = D1 ('MetaData "PartialProof" "Refinery.ProofState" "refinery0.4.0.0E4mMDIorSqGEmfwVST0gYb" '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 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 #
try :: Monad m => TacticT jdg ext err s m () > TacticT jdg ext err s m () Source #
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 Source #
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 () Source #
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 () Source #
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 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
.
ensure :: Monad m => (s > Maybe err) > (s > s) > TacticT jdg ext err s m () > TacticT jdg ext err s m () Source #
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 Source #
failure err
will create an unsolvable hole that will be ignored by subsequent tactics.
handler :: (err > m err) > TacticT jdg ext err s m () Source #
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 () Source #
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 () Source #
tweak f t
lets us modify the extract produced by the tactic t
.
Subgoal Manipulation
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 n
th subgoal.
Tactic Creation
class Monad m => MonadExtract meta ext err s m  m > ext, m > err, ext > meta where Source #
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.
Nothing
hole :: StateT s m (meta, ext) Source #
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) Source #
unsolvableHole :: err > StateT s m (meta, ext) Source #
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) Source #
Instances
MonadExtract meta ext err s m => MonadExtract meta ext err s (ExceptT err m) Source #  
(MonadExtract meta ext err s m, Monoid w) => MonadExtract meta ext err s (WriterT w m) Source #  
(MonadExtract meta ext err s m, Monoid w) => MonadExtract meta ext err s (WriterT w m) Source #  
MonadExtract meta ext err s m => MonadExtract meta ext err s (StateT s m) Source #  
MonadExtract meta ext err s m => MonadExtract meta ext err s (ReaderT r m) Source #  
data RuleT jdg ext err s m a Source #
A
is a monad transformer for creating inference rules.RuleT
Instances
Monad m => MonadState s (RuleT jdg ext err s m) Source #  
MFunctor (RuleT jdg ext err s :: (Type > Type) > Type > Type) Source #  
MonadTrans (RuleT jdg ext err s) Source #  
Defined in Refinery.Tactic.Internal  
Monad m => Monad (RuleT jdg ext err s m) Source #  
Functor m => Functor (RuleT jdg ext err s m) Source #  
Monad m => Applicative (RuleT jdg ext err s m) Source #  
Defined in Refinery.Tactic.Internal 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 #  
Defined in Refinery.Tactic.Internal  
Monad m => Alternative (RuleT jdg ext err s m) Source #  
(Show jdg, Show err, Show a, Show (m (ProofStateT ext a err s m jdg))) => Show (RuleT jdg ext err s m a) Source #  
Generic (RuleT jdg ext err s m a) Source #  
type Rep (RuleT jdg ext err s m a) Source #  
Defined in Refinery.Tactic.Internal type Rep (RuleT jdg ext err s m a) = D1 ('MetaData "RuleT" "Refinery.Tactic.Internal" "refinery0.4.0.0E4mMDIorSqGEmfwVST0gYb" '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 that examines the current goal into a tactic.
rule_ :: Monad m => RuleT jdg ext err s m ext > TacticT jdg ext err s m () Source #
Turn an inference rule into a tactic.
subgoal :: jdg > RuleT jdg ext err s m ext Source #
Create a subgoal, and return the resulting extract.
unsolvable :: err > RuleT jdg ext err s m ext Source #
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 Source #
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.
class MetaSubst meta ext => DependentMetaSubst meta jdg ext where Source #
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
.
dependentSubst :: meta > ext > jdg > jdg Source #
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 () Source #
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 () Source #
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 () Source #
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 () Source #
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 () Source #
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 () Source #
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.