Refinery.Tactic.Internal

WARNING

This module is considered internal, and can change at any given time.

Documentation

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

Constructors

TacticT

Fields

• unTacticT :: StateT jdg (ProofStateT ext ext err s m) a

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

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

Helper function for producing a tactic.

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

Helper function for deconstructing a tactic.

mapTacticT :: Monad m => (m a -> m b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b

Map the unwrapped computation using the given function

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

newtype RuleT jdg ext err s m a

A RuleT is a monad transformer for creating inference rules.

Constructors

RuleT

Fields

• unRuleT :: ProofStateT ext a err s m jdg

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