Refinery.Tactic

Documentation

data TacticT jdg ext err s m a

A TacticT is a monad transformer that performs proof refinement. The type variables signifiy:

• 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 use throwError to abort the computation with a provided error
• s - The state type.
• m - The base monad.
• a - The return value. This to make TacticT a monad, and will always be '()'

Instances

Monad m => MonadState s (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

get :: TacticT jdg ext err s m s

put :: s -> TacticT jdg ext err s m ()

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

MonadReader env m => MonadReader env (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

ask :: TacticT jdg ext err s m env

local :: (env -> env) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a

reader :: (env -> a) -> TacticT jdg ext err s m a

Monad m => MonadError err (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

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

MonadTrans (TacticT jdg ext err s)

Defined in Refinery.Tactic.Internal

Methods

lift :: Monad m => m a -> TacticT jdg ext err s m a

Functor m => Monad (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: TacticT jdg ext err s m a -> (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 b

return :: a -> TacticT jdg ext err s m a

fail :: String -> TacticT jdg ext err s m a

Functor m => Functor (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

fmap :: (a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b

(<$) :: a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a

Functor m => Applicative (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

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)

Defined in Refinery.Tactic.Internal

Methods

liftIO :: IO a -> TacticT jdg ext err s m a

Monad m => Alternative (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

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

some :: TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]

many :: TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]

Monad m => MonadPlus (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

mzero :: TacticT jdg ext err s m a

mplus :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a

MonadThrow m => MonadThrow (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

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

MonadCatch m => MonadCatch (TacticT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

catch :: Exception e => TacticT jdg ext err s m a -> (e -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a

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

Defined in Refinery.Tactic.Internal

Methods

showsPrec :: Int -> TacticT jdg ext err s m a -> ShowS

show :: TacticT jdg ext err s m a -> String

showList :: [TacticT jdg ext err s m a] -> ShowS

Generic (TacticT jdg ext err s m a)

Defined in Refinery.Tactic.Internal

Associated Types

type Rep (TacticT jdg ext err s m a) :: Type -> Type

Methods

from :: TacticT jdg ext err s m a -> Rep (TacticT jdg ext err s m a) x

to :: Rep (TacticT jdg ext err s m a) x -> TacticT jdg ext err s m a

type Rep (TacticT jdg ext err s m a)

Defined in Refinery.Tactic.Internal

type Rep (TacticT jdg ext err s m a) = D1 (MetaData "TacticT" "Refinery.Tactic.Internal" "refinery-0.2.0.0-2c8JRgW6Bhs8bC5T1tIgRK" 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, [jdg])]

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

(<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a infixr 3

try :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

Tries to run a tactic, backtracking on failure

many_ :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

Runs a tactic repeatedly until it fails

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

class MonadPlus m => MonadLogic (m :: Type -> Type) where

Minimal implementation: msplit

Minimal complete definition

msplit

Methods

msplit :: m a -> m (Maybe (a, m a))

Attempts to split the computation, giving access to the first result. Satisfies the following laws:

msplit mzero                == return Nothing
msplit (return a `mplus` m) == return (Just (a, m))

interleave :: m a -> m a -> m a

Fair disjunction. It is possible for a logical computation to have an infinite number of potential results, for instance:

odds = return 1 `mplus` liftM (2+) odds

Such computations can cause problems in some circumstances. Consider:

do x <- odds `mplus` return 2
   if even x then return x else mzero

Such a computation may never consider the 'return 2', and will therefore never terminate. By contrast, interleave ensures fair consideration of both branches of a disjunction

(>>-) :: m a -> (a -> m b) -> m b infixl 1

Fair conjunction. Similarly to the previous function, consider the distributivity law for MonadPlus:

(mplus a b) >>= k = (a >>= k) `mplus` (b >>= k)

If 'a >>= k' can backtrack arbitrarily many tmes, (b >>= k) may never be considered. (>>-) takes similar care to consider both branches of a disjunctive computation.

ifte :: m a -> (a -> m b) -> m b -> m b

Logical conditional. The equivalent of Prolog's soft-cut. If its first argument succeeds at all, then the results will be fed into the success branch. Otherwise, the failure branch is taken. satisfies the following laws:

ifte (return a) th el           == th a
ifte mzero th el                == el
ifte (return a `mplus` m) th el == th a `mplus` (m >>= th)

once :: m a -> m a

Pruning. Selects one result out of many. Useful for when multiple results of a computation will be equivalent, or should be treated as such.

lnot :: m a -> m ()

Inverts a logic computation. If m succeeds with at least one value, lnot m fails. If m fails, then lnot m succeeds the value ().

Instances

MonadLogic []

Defined in Control.Monad.Logic.Class

Methods

msplit :: [a] -> [Maybe (a, [a])]

interleave :: [a] -> [a] -> [a]

(>>-) :: [a] -> (a -> [b]) -> [b]

ifte :: [a] -> (a -> [b]) -> [b] -> [b]

once :: [a] -> [a]

lnot :: [a] -> [()]

Monad m => MonadLogic (LogicT m)

Defined in Control.Monad.Logic

Methods

msplit :: LogicT m a -> LogicT m (Maybe (a, LogicT m a))

interleave :: LogicT m a -> LogicT m a -> LogicT m a

(>>-) :: LogicT m a -> (a -> LogicT m b) -> LogicT m b

ifte :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b

once :: LogicT m a -> LogicT m a

lnot :: LogicT m a -> LogicT m ()

MonadLogic m => MonadLogic (StateT s m)

See note on splitting above.

Defined in Control.Monad.Logic.Class

Methods

msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a))

interleave :: StateT s m a -> StateT s m a -> StateT s m a

(>>-) :: StateT s m a -> (a -> StateT s m b) -> StateT s m b

ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b

once :: StateT s m a -> StateT s m a

lnot :: StateT s m a -> StateT s m ()

MonadLogic m => MonadLogic (StateT s m)

See note on splitting above.

Defined in Control.Monad.Logic.Class

Methods

msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a))

interleave :: StateT s m a -> StateT s m a -> StateT s m a

(>>-) :: StateT s m a -> (a -> StateT s m b) -> StateT s m b

ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b

once :: StateT s m a -> StateT s m a

lnot :: StateT s m a -> StateT s m ()

MonadLogic m => MonadLogic (ReaderT e m)

Note that splitting a transformer does not allow you to provide different input to the monadic object returned. For instance, in:

let Just (_, rm') = runReaderT (msplit rm) r in runReaderT rm' r'

r' will be ignored, because r was already threaded through the computation.

Defined in Control.Monad.Logic.Class

Methods

msplit :: ReaderT e m a -> ReaderT e m (Maybe (a, ReaderT e m a))

interleave :: ReaderT e m a -> ReaderT e m a -> ReaderT e m a

(>>-) :: ReaderT e m a -> (a -> ReaderT e m b) -> ReaderT e m b

ifte :: ReaderT e m a -> (a -> ReaderT e m b) -> ReaderT e m b -> ReaderT e m b

once :: ReaderT e m a -> ReaderT e m a

lnot :: ReaderT e m a -> ReaderT e m ()

Subgoal Manipulation

goal :: Functor m => TacticT jdg ext err s m jdg

Get the current goal

focus :: Functor m => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

Tactic Creation

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

class Monad m => MonadRule jdg ext m | m -> jdg, m -> ext where

Minimal complete definition

Nothing

Methods

subgoal :: jdg -> m ext

Create a subgoal, and return the resulting extract.

subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext

Create a subgoal, and return the resulting extract.

Instances

MonadRule jdg ext m => MonadRule jdg ext (ExceptT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ExceptT env m ext

MonadRule jdg ext m => MonadRule jdg ext (StateT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> StateT env m ext

MonadRule jdg ext m => MonadRule jdg ext (ReaderT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ReaderT env m ext

Monad m => MonadRule jdg ext (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> RuleT jdg ext err s m ext

data RuleT jdg ext err s m a

A RuleT is a monad transformer for creating inference rules.

Instances

Monad m => MonadRule jdg ext (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> RuleT jdg ext err s m ext

Monad m => MonadState s (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

get :: RuleT jdg ext err s m s

put :: s -> RuleT jdg ext err s m ()

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

MonadReader r m => MonadReader r (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

ask :: RuleT jdg ext err s m r

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

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

Monad m => MonadError err (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

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)

Defined in Refinery.Tactic.Internal

Methods

hoist :: Monad m => (forall a. m a -> n a) -> RuleT jdg ext err s m b -> RuleT jdg ext err s n b

MonadTrans (RuleT jdg ext err s)

Defined in Refinery.Tactic.Internal

Methods

lift :: Monad m => m a -> RuleT jdg ext err s m a

Monad m => Monad (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: RuleT jdg ext err s m a -> (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 b

return :: a -> RuleT jdg ext err s m a

fail :: String -> RuleT jdg ext err s m a

Functor m => Functor (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

fmap :: (a -> b) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m b

(<$) :: a -> RuleT jdg ext err s m b -> RuleT jdg ext err s m a

Monad m => Applicative (RuleT jdg ext err s m)

Defined in Refinery.Tactic.Internal

Methods

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)

Defined in Refinery.Tactic.Internal

Methods

liftIO :: IO a -> RuleT jdg ext err s m a

(Show jdg, Show err, Show a, Show (m (ProofStateT ext a err s m jdg))) => Show (RuleT jdg ext err s m a)

Defined in Refinery.Tactic.Internal

Methods

showsPrec :: Int -> RuleT jdg ext err s m a -> ShowS

show :: RuleT jdg ext err s m a -> String

showList :: [RuleT jdg ext err s m a] -> ShowS

Generic (RuleT jdg ext err s m a)

Defined in Refinery.Tactic.Internal

Associated Types

type Rep (RuleT jdg ext err s m a) :: Type -> Type

Methods

from :: RuleT jdg ext err s m a -> Rep (RuleT jdg ext err s m a) x

to :: Rep (RuleT jdg ext err s m a) x -> RuleT jdg ext err s m a

type Rep (RuleT jdg ext err s m a)

Defined in Refinery.Tactic.Internal

type Rep (RuleT jdg ext err s m a) = D1 (MetaData "RuleT" "Refinery.Tactic.Internal" "refinery-0.2.0.0-2c8JRgW6Bhs8bC5T1tIgRK" True) (C1 (MetaCons "RuleT" PrefixI True) (S1 (MetaSel (Just "unRuleT") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ProofStateT ext a err s m jdg))))

rule :: Monad m => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()

Turn an inference rule into a tactic.