Copyright | (c) Reed Mullanix 2019 |
---|---|
License | BSD-style |
Maintainer | reedmullanix@gmail.com |
Safe Haskell | Safe |
Language | Haskell2010 |
Documentation
data ProofStateT ext' ext err s m goal Source #
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) | |
Empty | |
Failure err | |
Axiom ext |
Instances
Monad m => MonadState s (ProofStateT ext ext err s m) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState lift :: Monad m => m a -> ProofStateT ext ext err s m a # | |
Functor m => Monad (ProofStateT ext ext err s m) Source # | |
Defined in Refinery.ProofState (>>=) :: 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) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState liftIO :: IO a -> ProofStateT ext ext err s m a # | |
Monad m => Alternative (ProofStateT ext ext err s m) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState throwM :: Exception e => e -> ProofStateT ext ext err s m a # | |
MonadCatch m => MonadCatch (ProofStateT ext ext err s m) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState 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) Source # | |
Defined in Refinery.ProofState type Rep (ProofStateT ext' ext err s m goal) :: Type -> Type # 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) Source # | |
Defined in Refinery.ProofState type Rep (ProofStateT ext' ext err s m goal) = D1 (MetaData "ProofStateT" "Refinery.ProofState" "refinery-0.2.0.0-2c8JRgW6Bhs8bC5T1tIgRK" 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 "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 Source #
class Monad m => MonadExtract ext m | m -> ext where Source #
Nothing
Generates a "hole" of type ext
, which should represent
an incomplete extract.
hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext Source #
Generates a "hole" of type ext
, which should represent
an incomplete extract.
Instances
MonadExtract ext m => MonadExtract ext (ExceptT err m) Source # | |
Defined in Refinery.ProofState | |
(MonadExtract ext m, Monoid w) => MonadExtract ext (WriterT w m) Source # | |
Defined in Refinery.ProofState | |
(MonadExtract ext m, Monoid w) => MonadExtract ext (WriterT w m) Source # | |
Defined in Refinery.ProofState | |
MonadExtract ext m => MonadExtract ext (StateT s m) Source # | |
Defined in Refinery.ProofState | |
MonadExtract ext m => MonadExtract ext (ReaderT r m) Source # | |
Defined in Refinery.ProofState |
proofs :: forall ext err s m goal. MonadExtract ext m => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, [goal])] Source #
axiom :: ext -> ProofStateT ext' ext err s m jdg Source #
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 #
mapExtract :: Functor m => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext ext err s m jdg -> ProofStateT ext' ext' err s m jdg Source #
mapExtract' :: Functor m => (a -> b) -> ProofStateT ext' a err s m jdg -> ProofStateT ext' b err s m jdg Source #