Refinery.ProofState

Documentation

data ProofStateT ext' ext err s m goal

Constructors

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

Axiom ext

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

MonadReader r m => MonadReader r (ProofStateT ext ext err s m)

Defined in Refinery.ProofState

Methods

ask :: ProofStateT ext ext err s m r

local :: (r -> r) -> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a

reader :: (r -> a) -> ProofStateT ext ext err s m a

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

Defined in Refinery.ProofState

Methods

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

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

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

Defined in Refinery.ProofState

Methods

hoist :: 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

fail :: String -> 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

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

Defined in Refinery.ProofState

Methods

catch :: Exception e => ProofStateT ext ext err s m a -> (e -> ProofStateT ext ext err s m a) -> 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.3.0.0-Fdcu2SHDGUb4nunxmlwjIU" 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)) :+: C1 (MetaCons "Axiom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ext))))))

applyCont :: Functor m => (ext -> ProofStateT ext' ext err s m a) -> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a

class Monad m => MonadExtract ext m | m -> ext where

Minimal complete definition

Nothing

Methods

hole :: m ext

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

hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext

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

Instances

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

Defined in Refinery.ProofState

Methods

hole :: ExceptT err m ext

(MonadExtract ext m, Monoid w) => MonadExtract ext (WriterT w m)

Defined in Refinery.ProofState

Methods

hole :: WriterT w m ext

(MonadExtract ext m, Monoid w) => MonadExtract ext (WriterT w m)

Defined in Refinery.ProofState

Methods

hole :: WriterT w m ext

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

Defined in Refinery.ProofState

Methods

hole :: StateT s m ext

MonadExtract ext m => MonadExtract ext (ReaderT r m)

Defined in Refinery.ProofState

Methods

hole :: ReaderT r m ext

proofs :: forall ext err s m goal. MonadExtract ext m => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, s, [goal])]

accumEither :: (Semigroup a, Semigroup b) => Either a b -> Either a b -> Either a b

axiom :: ext -> ProofStateT ext' ext err s m jdg

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 => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext ext err s m jdg -> ProofStateT ext' ext' err s m jdg

mapExtract' :: Functor m => (a -> b) -> ProofStateT ext' a err s m jdg -> ProofStateT ext' b err s m jdg