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 'Prelude.()'

One of the most important things about this type is it's Monad instance. t1 >> t2 Will execute t1 against the current goal, and then execute t2 on _all_ of the subgoals generated by t2.

This Monad instance is lawful, and has been tested thouroughly, and a version of it has been formally verified in Agda. _However_, just because it is correct doesn't mean that it lines up with your intuitions of how Monads behave! In practice, it feels like a combination of the Non-Determinisitic Monads and some of the Time Travelling ones. That doesn't mean that it's impossible to understand, just that it may push the boundaries of you intuitions.

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

MFunctor (TacticT jdg ext err s :: (Type -> Type) -> Type -> Type)

Defined in Refinery.Tactic.Internal

Methods

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

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

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

(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.4.0.0-E4mMDIorSqGEmfwVST0gYb" '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)

proofState t j will deconstruct a tactic t into a ProofStateT by running it at j.

proofState_ :: Functor m => TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg

Like proofState, but we discard the return value of t.

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

Rules

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

MFunctor (RuleT jdg ext err s :: (Type -> Type) -> Type -> Type)

Defined in Refinery.Tactic.Internal

Methods

hoist :: forall m n (b :: k). 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

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

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

Defined in Refinery.Tactic.Internal

Methods

empty :: RuleT jdg ext err s m a

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

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

many :: RuleT jdg ext err s m 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.4.0.0-E4mMDIorSqGEmfwVST0gYb" 'True) (C1 ('MetaCons "RuleT" 'PrefixI 'True) (S1 ('MetaSel ('Just "unRuleT") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ProofStateT ext a err s m jdg))))

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

Create a subgoal, and return the resulting extract.

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

Create an "unsolvable" hole. These holes are ignored by subsequent tactics, but do not cause a backtracking failure.