Refinery.ProofState

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

Documentation

data ProofStateT ext' ext err s m goal

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

Constructors

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 StateT here, as it doesn't play nice with backtracking.

Alt (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)

Combine together the results of two ProofStates, preserving the order that they were synthesized in.

Interleave (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)

Similar to Alt, but will interleave the results, rather than just appending them. This is useful if the first argument produces potentially infinite results.

Commit (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)

Commit runs the first proofstate, and only runs the second if the first does not produce any successful results.

Empty

Silent failure. Always causes a backtrack, unlike Failure.

Failure err (ext' -> ProofStateT ext' ext err s m goal)

This does double duty, depending on whether or not the user calls proofs or partialProofs. In the first case, we ignore the continutation, backtrack, and return an error in the result of proofs. In the second, we treat this as a sort of "unsolvable subgoal", and call the continuation with a hole.

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

Monad m => MonadState s (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

get :: ProofStateT ext ext err s m s

put :: s -> ProofStateT ext ext err s m ()

state :: (s -> (a, s)) -> ProofStateT ext ext err s m a

MFunctor (ProofStateT ext' ext err s :: (Type -> Type) -> Type -> Type)

Defined in Refinery.ProofState

Methods

hoist :: forall m n (b :: k). Monad m => (forall a. m a -> n a) -> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b

MonadTrans (ProofStateT ext ext err s)

Defined in Refinery.ProofState

Methods

lift :: Monad m => m a -> ProofStateT ext ext err s m a

Functor m => Monad (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

(>>=) :: ProofStateT ext ext err s m a -> (a -> ProofStateT ext ext err s m b) -> ProofStateT ext ext err s m b

(>>) :: ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m b

return :: a -> ProofStateT ext ext err s m a

Functor m => Functor (ProofStateT ext' ext err s m)

Defined in Refinery.ProofState

Methods

fmap :: (a -> b) -> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m b

(<$) :: a -> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s m a

Functor m => Applicative (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

pure :: a -> ProofStateT ext ext err s m a

(<*>) :: ProofStateT ext ext err s m (a -> b) -> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b

liftA2 :: (a -> b -> c) -> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m c

(*>) :: ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m b

(<*) :: ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m a

MonadIO m => MonadIO (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

liftIO :: IO a -> ProofStateT ext ext err s m a

Monad m => Alternative (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

empty :: ProofStateT ext ext err s m a

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

some :: ProofStateT ext ext err s m a -> ProofStateT ext ext err s m [a]

many :: ProofStateT ext ext err s m a -> ProofStateT ext ext err s m [a]

Monad m => MonadPlus (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

mzero :: ProofStateT ext ext err s m a

mplus :: ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a

MonadThrow m => MonadThrow (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

throwM :: Exception e => e -> ProofStateT ext ext err s m a

(Show goal, Show err, Show ext, Show (m (ProofStateT ext' ext err s m goal))) => Show (ProofStateT ext' ext err s m goal)

Defined in Refinery.ProofState

Methods

showsPrec :: Int -> ProofStateT ext' ext err s m goal -> ShowS

show :: ProofStateT ext' ext err s m goal -> String

showList :: [ProofStateT ext' ext err s m goal] -> ShowS

Generic (ProofStateT ext' ext err s m goal)

Defined in Refinery.ProofState

Associated Types

type Rep (ProofStateT ext' ext err s m goal) :: Type -> Type

Methods

from :: ProofStateT ext' ext err s m goal -> Rep (ProofStateT ext' ext err s m goal) x

to :: Rep (ProofStateT ext' ext err s m goal) x -> ProofStateT ext' ext err s m goal

type Rep (ProofStateT ext' ext err s m goal)

Defined in Refinery.ProofState

type Rep (ProofStateT ext' ext err s m goal) = D1 ('MetaData "ProofStateT" "Refinery.ProofState" "refinery-0.4.0.0-E4mMDIorSqGEmfwVST0gYb" 'False) (((C1 ('MetaCons "Subgoal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 goal) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ext' -> ProofStateT ext' ext err s m goal))) :+: C1 ('MetaCons "Effect" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (m (ProofStateT ext' ext err s m goal))))) :+: (C1 ('MetaCons "Stateful" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (s -> (s, ProofStateT ext' ext err s m goal)))) :+: (C1 ('MetaCons "Alt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext' ext err s m goal)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext' ext err s m goal))) :+: C1 ('MetaCons "Interleave" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext' ext err s m goal)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext' ext err s m goal)))))) :+: ((C1 ('MetaCons "Commit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext' ext err s m goal)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext' ext err s m goal))) :+: C1 ('MetaCons "Empty" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Failure" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 err) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ext' -> ProofStateT ext' ext err s m goal))) :+: (C1 ('MetaCons "Handle" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext' ext err s m goal)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (err -> m err))) :+: C1 ('MetaCons "Axiom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ext))))))

Proofstate Execution

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

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

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

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

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

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.

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

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.