Copyright  (c) Reed Mullanix 2019 

License  BSDstyle 
Maintainer  reedmullanix@gmail.com 
Safe Haskell  None 
Language  Haskell2010 
Synopsis
 data TacticT jdg ext m a
 runTacticT :: MonadExtract ext m => TacticT jdg ext m () > jdg > m (ext, [jdg])
 (<@>) :: MonadProvable jdg m => TacticT jdg ext m () > [TacticT jdg ext m ()] > TacticT jdg ext m ()
 try :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () > TacticT jdg ext m ()
 many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () > TacticT jdg ext m ()
 choice :: (MonadProvable jdg m, MonadError err m) => err > [TacticT jdg ext m a] > TacticT jdg ext m a
 progress :: (MonadProvable jdg m, MonadError err m) => (jdg > jdg > Bool) > err > TacticT jdg ext m a > TacticT jdg ext m a
 goal :: Monad m => TacticT jdg ext m jdg
 focus :: (MonadProvable jdg m, Monad m) => TacticT jdg ext m () > Int > TacticT jdg ext m () > TacticT jdg ext m ()
 forSubgoals :: Monad m => TacticT jdg ext m a > (jdg > m b) > TacticT jdg ext m a
 class Monad m => MonadExtract ext m  m > ext where
 hole :: m ext
 class Monad m => MonadRule jdg ext m  m > jdg, m > ext where
 subgoal :: jdg > m ext
 data RuleT jdg ext m a
 rule :: Monad m => (jdg > RuleT jdg ext m ext) > TacticT jdg ext m ()
 class Monad m => MonadProvable jdg m  m > jdg where
 proving :: jdg > m jdg
 newtype ProvableT jdg m a = ProvableT {
 runProvableT :: m a
 type Provable jdg a = ProvableT jdg Identity a
 runProvable :: Provable jdg a > a
 class Functor f => Alt (f :: Type > Type) where
 (<!>) :: f a > f a > f a
 some :: Applicative f => f a > f [a]
 many :: Applicative f => f a > f [a]
Documentation
data TacticT jdg ext 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.m
 The base monad.a
 The return value. This to make
a monad, and will always beTacticT
'()'
Instances
runTacticT :: MonadExtract ext m => TacticT jdg ext m () > jdg > m (ext, [jdg]) Source #
Runs a tactic, producing the extract, along with a list of unsolved subgoals.
Tactic Combinators
(<@>) :: MonadProvable jdg m => TacticT jdg ext m () > [TacticT jdg ext m ()] > TacticT jdg ext m () Source #
Create a tactic that applies each of the tactics in the list to one subgoal.
When the number of subgoals is greater than the number of provided tactics, the identity tactic is applied to the remainder. When the number of subgoals is less than the number of provided tactics, the remaining tactics are ignored.
try :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () > TacticT jdg ext m () Source #
Tries to run a tactic, backtracking on failure
many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () > TacticT jdg ext m () Source #
Runs a tactic repeatedly until it fails
choice :: (MonadProvable jdg m, MonadError err m) => err > [TacticT jdg ext m a] > TacticT jdg ext m a Source #
choice err ts
tries to apply a series of tactics ts
, and commits to the
1st tactic that succeeds. If they all fail, then err
is thrown
progress :: (MonadProvable jdg m, MonadError err m) => (jdg > jdg > Bool) > err > TacticT jdg ext m a > TacticT jdg ext m a Source #
progress eq err t
applies the tactic t
, and checks to see if the
resulting subgoals are all equal to the initial goal by using eq
. If they
are, it throws err
.
Subgoal Manipulation
focus :: (MonadProvable jdg m, Monad m) => TacticT jdg ext m () > Int > TacticT jdg ext m () > TacticT jdg ext m () Source #
Apply the first tactic, and then apply the second tactic focused on the n
th subgoal.
forSubgoals :: Monad m => TacticT jdg ext m a > (jdg > m b) > TacticT jdg ext m a Source #
Applies f
to every subgoals resulting from the tactic t
.
Tactic Creation
class Monad m => MonadExtract ext m  m > ext where Source #
Nothing
Generates a "hole" of type ext
, which should represent
an incomplete extract.
hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext Source #
Generates a "hole" of type ext
, which should represent
an incomplete extract.
Instances
MonadExtract ext m => MonadExtract ext (ExceptT err m) Source #  
Defined in Refinery.Tactic  
MonadExtract ext m => MonadExtract ext (StateT s m) Source #  
Defined in Refinery.Tactic  
MonadExtract ext m => MonadExtract ext (RuleT jdg ext m) Source #  
Defined in Refinery.Tactic  
MonadExtract ext m => MonadExtract ext (ReaderT env m) Source #  
Defined in Refinery.Tactic  
MonadExtract ext m => MonadExtract ext (Proxy a' a b' b m) Source #  
Defined in Refinery.Tactic 
class Monad m => MonadRule jdg ext m  m > jdg, m > ext where Source #
Nothing
subgoal :: jdg > m ext Source #
Create a subgoal, and return the resulting extract.
subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg > m ext Source #
Create a subgoal, and return the resulting extract.
Instances
MonadRule jdg ext m => MonadRule jdg ext (ProvableT env m) Source #  
Defined in Refinery.Tactic.Internal  
MonadRule jdg ext m => MonadRule jdg ext (ExceptT env m) Source #  
Defined in Refinery.Tactic.Internal  
MonadRule jdg ext m => MonadRule jdg ext (StateT env m) Source #  
Defined in Refinery.Tactic.Internal  
MonadRule jdg ext m => MonadRule jdg ext (ReaderT env m) Source #  
Defined in Refinery.Tactic.Internal  
Monad m => MonadRule jdg ext (RuleT jdg ext m) Source #  
Defined in Refinery.Tactic.Internal 
data RuleT jdg ext m a Source #
A
is a monad transformer for creating inference rules.RuleT
Instances
Monad m => MonadRule jdg ext (RuleT jdg ext m) Source #  
Defined in Refinery.Tactic.Internal  
MonadState s m => MonadState s (RuleT jdg ext m) Source #  
MonadReader env m => MonadReader env (RuleT jdg ext m) Source #  
MonadError err m => MonadError err (RuleT jdg ext m) Source #  
Defined in Refinery.Tactic.Internal 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) Source #  
Defined in Refinery.Tactic  
MFunctor (RuleT jdg ext :: (Type > Type) > Type > Type) Source #  
MonadTrans (RuleT jdg ext) Source #  
Defined in Refinery.Tactic.Internal  
Functor m => Monad (RuleT jdg ext m) Source #  
Functor m => Functor (RuleT jdg ext m) Source #  
Functor m => Applicative (RuleT jdg ext m) Source #  
Defined in Refinery.Tactic.Internal 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) Source #  
Defined in Refinery.Tactic.Internal  
MonadThrow m => MonadThrow (RuleT jdg ext m) Source #  
Defined in Refinery.Tactic.Internal  
MonadCatch m => MonadCatch (RuleT jdg ext m) Source #  
rule :: Monad m => (jdg > RuleT jdg ext m ext) > TacticT jdg ext m () Source #
Turn an inference rule into a tactic.
class Monad m => MonadProvable jdg m  m > jdg where Source #
Nothing
proving :: jdg > m jdg Source #
Applies a transformation of goals at every step of the tactic.
proving :: (MonadTrans t, MonadProvable jdg m1, m ~ t m1) => jdg > m jdg Source #
Applies a transformation of goals at every step of the tactic.
Instances
Monad m => MonadProvable jdg (ProvableT jdg m) Source #  
Defined in Refinery.Tactic.Internal  
MonadProvable jdg m => MonadProvable jdg (ExceptT err m) Source #  
Defined in Refinery.Tactic.Internal  
MonadProvable jdg m => MonadProvable jdg (StateT s m) Source #  
Defined in Refinery.Tactic.Internal  
MonadProvable jdg m => MonadProvable jdg (ProofStateT ext m) Source #  
Defined in Refinery.Tactic.Internal proving :: jdg > ProofStateT ext m jdg Source #  
MonadProvable jdg m => MonadProvable jdg (ReaderT r m) Source #  
Defined in Refinery.Tactic.Internal 
newtype ProvableT jdg m a Source #
Helper newtype for when you don't have any need for the mechanisms of MonadProvable.
ProvableT  

Instances
runProvable :: Provable jdg a > a Source #
ReExports
class Functor f => Alt (f :: Type > Type) where #
Laws:
<!> is associative: (a <!> b) <!> c = a <!> (b <!> c) <$> leftdistributes over <!>: f <$> (a <!> b) = (f <$> a) <!> (f <$> b)
If extended to an Alternative
then <!>
should equal <>
.
Ideally, an instance of Alt
also satisfies the "left distributon" law of
MonadPlus with respect to <.>
:
<.> rightdistributes over <!>: (a <!> b) <.> c = (a <.> c) <!> (b <.> c)
But Maybe
, IO
,
, Either
a
, and ErrorT
e mSTM
satisfy the alternative
"left catch" law instead:
pure a <!> b = pure a
However, this variation cannot be stated purely in terms of the dependencies of Alt
.
When and if MonadPlus is successfully refactored, this class should also be refactored to remove these instances.
The right distributive law should extend in the cases where the a Bind
or Monad
is
provided to yield variations of the right distributive law:
(m <!> n) >> f = (m >> f) <!> (m >> f) (m <!> n) >>= f = (m >>= f) <!> (m >>= f)
(<!>) :: f a > f a > f a infixl 3 #
<>
without a required empty
some :: Applicative f => f a > f [a] #
many :: Applicative f => f a > f [a] #