Safe Haskell  SafeInferred 

Language  Haskell2010 
The datatype that drives both Rules and Tactics
If you just want to build tactics, you probably want to use Tactic
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 : BSDstyle Maintainer : reedmullanix@gmail.com
Synopsis
 data ProofStateT ext' ext err s m goal
 = Subgoal goal (ext' > ProofStateT ext' ext err s m goal)
  Effect (m (ProofStateT ext' ext err s m goal))
  Stateful (s > (s, ProofStateT ext' ext err s m goal))
  Alt (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
  Interleave (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
  Commit (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
  Empty
  Failure err (ext' > ProofStateT ext' ext err s m goal)
  Handle (ProofStateT ext' ext err s m goal) (err > m err)
  Axiom ext
 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 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)]
 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])
 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])
 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
 mapExtract :: Functor m => (a > ext') > (ext > b) > ProofStateT ext' ext err s m jdg > ProofStateT a b err s m jdg
 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
 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
Documentation
data ProofStateT ext' ext err s m goal Source #
The core data type of the library. This represents a reified, inprogress proof strategy for a particular goal.
NOTE: We need to split up the extract type into ext'
and ext
, as
we want to be functorial (and monadic) in ext
, 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.
Subgoal goal (ext' > ProofStateT ext' ext err s m goal)  Represents a subgoal, and a continuation that tells us what to do with the resulting extract. 
Effect (m (ProofStateT ext' ext err s m goal))  Run an effect. 
Stateful (s > (s, ProofStateT ext' ext err s m goal))  Run a stateful computation. We don't want to use 
Alt (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)  Combine together the results of two 
Interleave (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)  Similar to 
Commit (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal) 

Empty  Silent failure. Always causes a backtrack, unlike 
Failure err (ext' > ProofStateT ext' ext err s m goal)  This does double duty, depending on whether or not the user calls 
Handle (ProofStateT ext' ext err s m goal) (err > m err)  An installed error handler. These allow us to add annotations to errors, or run effects. 
Axiom ext  Represents a simple extract. 
Instances
Proofstate Execution
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 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)])))) 
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]) Source #
Interpret a ProofStateT
into a list of (possibly incomplete) extracts.
This function will cause a proof to terminate when it encounters a Failure
, and will return a Left
.
If you want to still recieve an extract even when you encounter a failure, you should use partialProofs
.
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]) Source #
Interpret a ProofStateT
into a list of (possibly incomplete) extracts.
This function will continue producing an extract when it encounters a Failure
, 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 proofs
.
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 Source #
subgoals fs p
will apply a list of functions producing a new ProofStateT
to each of the subgoals of p
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 pure
to all of the remaining subgoals.
Extract Manipulation
mapExtract :: Functor m => (a > ext') > (ext > b) > ProofStateT ext' ext err s m jdg > ProofStateT a b err s m jdg Source #
mapExtract f g p
allows yout to modify the extract type of a ProofState.
This witness the Profunctor
instance of ProofStateT
, which we can't write without a newtype due to
the position of the type variables
Speculative Execution
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.
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 Source #
speculate s p
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.