Copyright  (c) Reed Mullanix 2019 

License  BSDstyle 
Maintainer  reedmullanix@gmail.com 
Safe Haskell  None 
Language  Haskell2010 
WARNING
This module is considered internal, and can change at any given time.
Synopsis
 newtype TacticT jdg ext err s m a = TacticT {
 unTacticT :: 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
 proofState :: TacticT jdg ext err s m a > jdg > ProofStateT ext ext err s m (a, jdg)
 proofState_ :: Functor m => TacticT jdg ext err s m a > jdg > ProofStateT ext ext err s m jdg
 mapTacticT :: Monad m => (m a > m b) > TacticT jdg ext err s m a > TacticT jdg ext err s m b
 newtype RuleT jdg ext err s m a = RuleT {
 unRuleT :: ProofStateT ext a err s m jdg
 subgoal :: jdg > RuleT jdg ext err s m ext
 unsolvable :: err > RuleT jdg ext err s m ext
Documentation
newtype 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
'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 NonDeterminisitic 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.
TacticT  

Instances
Monad m => MonadState s (TacticT jdg ext err s m) Source #  
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 #  
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  
(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" "refinery0.4.0.0E4mMDIorSqGEmfwVST0gYb" '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 Source #
Helper function for producing a tactic.
proofState :: TacticT jdg ext err s m a > jdg > ProofStateT ext ext err s m (a, jdg) Source #
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 Source #
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 Source #
Map the unwrapped computation using the given function
Rules
newtype RuleT jdg ext err s m a Source #
A
is a monad transformer for creating inference rules.RuleT
RuleT  

Instances
Monad m => MonadState s (RuleT jdg ext err s m) Source #  
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 #  
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  
Monad m => Alternative (RuleT jdg ext err s m) Source #  
(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" "refinery0.4.0.0E4mMDIorSqGEmfwVST0gYb" '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 Source #
Create a subgoal, and return the resulting extract.
unsolvable :: err > RuleT jdg ext err s m ext Source #
Create an "unsolvable" hole. These holes are ignored by subsequent tactics, but do not cause a backtracking failure.