Copyright | (c) Reed Mullanix 2019 |
---|---|
License | BSD-style |
Maintainer | reedmullanix@gmail.com |
Safe Haskell | None |
Language | Haskell2010 |
Synopsis
- data TacticT jdg ext err s m a
- runTacticT :: MonadExtract ext m => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, s, [jdg])]
- (<@>) :: 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
- commit :: 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 ()
- many_ :: 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
- gather :: MonadExtract ext m => TacticT jdg ext err s m a -> ([(a, jdg)] -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a
- pruning :: MonadExtract ext m => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
- ensure :: Monad m => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
- goal :: Functor m => TacticT jdg ext err s m jdg
- 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 ext m | m -> ext where
- hole :: m ext
- class Monad m => MonadRule jdg ext m | m -> jdg, m -> ext where
- subgoal :: jdg -> m 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 ()
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
'()'
Instances
Monad m => MonadState s (TacticT jdg ext err s m) Source # | |
MonadReader env m => MonadReader env (TacticT jdg ext err s m) Source # | |
Monad m => MonadError err (TacticT jdg ext err s m) Source # | |
Defined in Refinery.Tactic.Internal throwError :: err -> TacticT jdg ext err s m a # catchError :: TacticT jdg ext err s m a -> (err -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a # | |
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 # | |
Defined in Refinery.Tactic.Internal | |
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 | |
MonadCatch m => MonadCatch (TacticT jdg ext err s m) Source # | |
(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" "refinery-0.3.0.0-Fdcu2SHDGUb4nunxmlwjIU" 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 ext m => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, s, [jdg])] Source #
Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.
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 #
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 only run t2
if t1
failed to produce any extracts.
try :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #
Tries to run a tactic, backtracking on failure
many_ :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #
Runs a tactic repeatedly until it fails
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
.
gather :: MonadExtract ext m => TacticT jdg ext err s m a -> ([(a, jdg)] -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a Source #
gather t f
runs the tactic t
, then runs f
with all of the generated subgoals to determine
the next tactic to run.
pruning :: MonadExtract ext m => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m () Source #
pruning t f
runs the tactic t
, and then applies a predicate to all of the generated subgoals.
ensure :: Monad m => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #
filterT 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.
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 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 |
class Monad m => MonadRule jdg ext m | m -> jdg, m -> ext where Source #
Nothing
subgoal :: jdg -> m ext Source #
Create a subgoal, and return the resulting extract.
subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext Source #
Create a subgoal, and return the resulting extract.
Instances
MonadRule jdg ext m => MonadRule jdg ext (ExceptT env m) Source # | |
Defined in Refinery.Tactic.Internal | |
MonadRule jdg ext m => MonadRule jdg ext (StateT env m) Source # | |
Defined in Refinery.Tactic.Internal | |
MonadRule jdg ext m => MonadRule jdg ext (ReaderT env m) Source # | |
Defined in Refinery.Tactic.Internal | |
Monad m => MonadRule jdg ext (RuleT jdg ext err s m) Source # | |
Defined in Refinery.Tactic.Internal |
data RuleT jdg ext err s m a Source #
A
is a monad transformer for creating inference rules.RuleT
Instances
Monad m => MonadRule jdg ext (RuleT jdg ext err s m) Source # | |
Defined in Refinery.Tactic.Internal | |
Monad m => MonadState s (RuleT jdg ext err s m) Source # | |
MonadReader r m => MonadReader r (RuleT jdg ext err s m) Source # | |
Monad m => MonadError err (RuleT jdg ext err s m) Source # | |
Defined in Refinery.Tactic.Internal throwError :: err -> RuleT jdg ext err s m a # catchError :: RuleT jdg ext err s m a -> (err -> RuleT jdg ext err s m a) -> RuleT jdg ext err s m a # | |
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 # | |
Defined in Refinery.Tactic.Internal | |
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 | |
(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" "refinery-0.3.0.0-Fdcu2SHDGUb4nunxmlwjIU" True) (C1 (MetaCons "RuleT" PrefixI True) (S1 (MetaSel (Just "unRuleT") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ProofStateT ext a err s m jdg)))) |