Refinery.Tactic.Internal

WARNING

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

Documentation

newtype TacticT jdg ext 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.
• 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 m) a

Instances

(MonadProvable jdg m, MonadState s m) => MonadState s (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

get :: TacticT jdg ext m s

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

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

(MonadReader env m, MonadProvable jdg m) => MonadReader env (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

ask :: TacticT jdg ext m env

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

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

(MonadError err m, MonadProvable jdg m) => MonadError err (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

throwError :: err -> TacticT jdg ext m a

catchError :: TacticT jdg ext m a -> (err -> TacticT jdg ext m a) -> TacticT jdg ext m a

MonadTrans (TacticT jdg ext)

Defined in Refinery.Tactic.Internal

Methods

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

MonadProvable jdg m => Monad (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: TacticT jdg ext m a -> (a -> TacticT jdg ext m b) -> TacticT jdg ext m b

(>>) :: TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m b

return :: a -> TacticT jdg ext m a

fail :: String -> TacticT jdg ext m a

Monad m => Functor (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

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

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

MonadProvable jdg m => Applicative (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

pure :: a -> TacticT jdg ext m a

(<*>) :: TacticT jdg ext m (a -> b) -> TacticT jdg ext m a -> TacticT jdg ext m b

liftA2 :: (a -> b -> c) -> TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m c

(*>) :: TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m b

(<*) :: TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m a

(MonadIO m, MonadProvable jdg m) => MonadIO (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

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

(MonadThrow m, MonadProvable jdg m) => MonadThrow (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

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

(MonadCatch m, MonadProvable jdg m) => MonadCatch (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

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

MonadError err m => Alt (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

(<!>) :: TacticT jdg ext m a -> TacticT jdg ext m a -> TacticT jdg ext m a

some :: Applicative (TacticT jdg ext m) => TacticT jdg ext m a -> TacticT jdg ext m [a]

many :: Applicative (TacticT jdg ext m) => TacticT jdg ext m a -> TacticT jdg ext m [a]

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

Map the unwrapped computation using the given function

stateful :: Monad m => TacticT jdg ext m a -> (jdg -> RuleT jdg ext (StateT s m) ext) -> s -> TacticT jdg ext m a

Helper function for making "stateful" tactics like "@"

asRule :: Monad m => jdg -> TacticT jdg ext m a -> RuleT jdg ext m ext

Transforms a tactic into a rule. Useful for doing things with stateful.

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 (ProvableT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ProvableT env m ext

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

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> RuleT jdg ext m ext

newtype RuleT jdg ext m a

A RuleT is a monad transformer for creating inference rules.

Constructors

RuleT

Fields

• unRuleT :: Client jdg ext m a

Instances

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

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> RuleT jdg ext m ext

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

Defined in Refinery.Tactic.Internal

Methods

get :: RuleT jdg ext m s

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

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

MonadReader env m => MonadReader env (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

ask :: RuleT jdg ext m env

local :: (env -> env) -> RuleT jdg ext m a -> RuleT jdg ext m a

reader :: (env -> a) -> RuleT jdg ext m a

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

Defined in Refinery.Tactic.Internal

Methods

throwError :: err -> RuleT jdg ext m a

catchError :: RuleT jdg ext m a -> (err -> RuleT jdg ext m a) -> RuleT jdg ext m a

MonadExtract ext m => MonadExtract ext (RuleT jdg ext m)

Defined in Refinery.Tactic

Methods

hole :: RuleT jdg ext m ext

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

Defined in Refinery.Tactic.Internal

Methods

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

MonadTrans (RuleT jdg ext)

Defined in Refinery.Tactic.Internal

Methods

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

Functor m => Monad (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: RuleT jdg ext m a -> (a -> RuleT jdg ext m b) -> RuleT jdg ext m b

(>>) :: RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m b

return :: a -> RuleT jdg ext m a

fail :: String -> RuleT jdg ext m a

Functor m => Functor (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

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

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

Functor m => Applicative (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

pure :: a -> RuleT jdg ext m a

(<*>) :: RuleT jdg ext m (a -> b) -> RuleT jdg ext m a -> RuleT jdg ext m b

liftA2 :: (a -> b -> c) -> RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m c

(*>) :: RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m b

(<*) :: RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m a

MonadIO m => MonadIO (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

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

MonadThrow m => MonadThrow (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

throwM :: Exception e => e -> RuleT jdg ext m a

MonadCatch m => MonadCatch (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

catch :: Exception e => RuleT jdg ext m a -> (e -> RuleT jdg ext m a) -> RuleT jdg ext m a

mapRuleT :: Monad m => (m a -> m b) -> RuleT jdg ext m a -> RuleT jdg ext m b

Map the unwrapped computation using the given function

class Monad m => MonadProvable jdg m | m -> jdg where

Minimal complete definition

Nothing

Methods

proving :: jdg -> m jdg

Applies a transformation of goals at every step of the tactic.

proving :: (MonadTrans t, MonadProvable jdg m1, m ~ t m1) => jdg -> m jdg

Applies a transformation of goals at every step of the tactic.

Instances

Monad m => MonadProvable jdg (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ProvableT jdg m jdg

MonadProvable jdg m => MonadProvable jdg (ExceptT err m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ExceptT err m jdg

MonadProvable jdg m => MonadProvable jdg (StateT s m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> StateT s m jdg

MonadProvable jdg m => MonadProvable jdg (ProofStateT ext m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ProofStateT ext m jdg

MonadProvable jdg m => MonadProvable jdg (ReaderT r m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ReaderT r m jdg

newtype ProvableT jdg m a

Helper newtype for when you don't have any need for the mechanisms of MonadProvable.

Constructors

ProvableT

Fields

• runProvableT :: m a

Instances

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

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ProvableT env m ext

MonadState s m => MonadState s (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

get :: ProvableT jdg m s

put :: s -> ProvableT jdg m ()

state :: (s -> (a, s)) -> ProvableT jdg m a

MonadError err m => MonadError err (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

throwError :: err -> ProvableT jdg m a

catchError :: ProvableT jdg m a -> (err -> ProvableT jdg m a) -> ProvableT jdg m a

Monad m => MonadProvable jdg (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ProvableT jdg m jdg

MonadTrans (ProvableT jdg)

Defined in Refinery.Tactic.Internal

Methods

lift :: Monad m => m a -> ProvableT jdg m a

Monad m => Monad (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: ProvableT jdg m a -> (a -> ProvableT jdg m b) -> ProvableT jdg m b

(>>) :: ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m b

return :: a -> ProvableT jdg m a

fail :: String -> ProvableT jdg m a

Functor m => Functor (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

fmap :: (a -> b) -> ProvableT jdg m a -> ProvableT jdg m b

(<$) :: a -> ProvableT jdg m b -> ProvableT jdg m a

Applicative m => Applicative (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

pure :: a -> ProvableT jdg m a

(<*>) :: ProvableT jdg m (a -> b) -> ProvableT jdg m a -> ProvableT jdg m b

liftA2 :: (a -> b -> c) -> ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m c

(*>) :: ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m b

(<*) :: ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m a

MonadIO m => MonadIO (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

liftIO :: IO a -> ProvableT jdg m a

type Provable jdg a = ProvableT jdg Identity a

runProvable :: Provable jdg a -> a