-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Toolkit for building proof automation systems
--   
--   Please see the README on GitHub at
--   <a>https://github.com/githubuser/refinery#readme</a>
@package refinery
@version 0.2.0.0


module Refinery.ProofState
data ProofStateT ext' ext err s m goal
Subgoal :: goal -> (ext' -> ProofStateT ext' ext err s m goal) -> ProofStateT ext' ext err s m goal
Effect :: m (ProofStateT ext' ext err s m goal) -> ProofStateT ext' ext err s m goal
Stateful :: (s -> (s, ProofStateT ext' ext err s m goal)) -> ProofStateT ext' ext err s m goal
Alt :: ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal
Interleave :: ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal -> ProofStateT ext' ext err s m goal
Empty :: ProofStateT ext' ext err s m goal
Failure :: err -> ProofStateT ext' ext err s m goal
Axiom :: ext -> ProofStateT ext' ext err s m goal
applyCont :: Functor m => (ext -> ProofStateT ext ext err s m a) -> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a
class (Monad m) => MonadExtract ext m | m -> ext

-- | Generates a "hole" of type <tt>ext</tt>, which should represent an
--   incomplete extract.
hole :: MonadExtract ext m => m ext

-- | Generates a "hole" of type <tt>ext</tt>, which should represent an
--   incomplete extract.
hole :: (MonadExtract ext m, MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext
proofs :: forall ext err s m goal. MonadExtract ext m => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, [goal])]
accumEither :: (Semigroup a, Semigroup b) => Either a b -> Either a b -> Either a b
axiom :: ext -> ProofStateT ext' ext err s m jdg
subgoals :: Functor m => [jdg -> ProofStateT ext ext err s m jdg] -> ProofStateT ext ext err s m jdg -> ProofStateT ext ext err s m jdg
mapExtract :: Functor m => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext ext err s m jdg -> ProofStateT ext' ext' err s m jdg
mapExtract' :: Functor m => (a -> b) -> ProofStateT ext' a err s m jdg -> ProofStateT ext' b err s m jdg
instance GHC.Generics.Generic (Refinery.ProofState.ProofStateT ext' ext err s m goal)
instance Refinery.ProofState.MonadExtract ext m => Refinery.ProofState.MonadExtract ext (Control.Monad.Trans.Reader.ReaderT r m)
instance Refinery.ProofState.MonadExtract ext m => Refinery.ProofState.MonadExtract ext (Control.Monad.Trans.State.Lazy.StateT s m)
instance (Refinery.ProofState.MonadExtract ext m, GHC.Base.Monoid w) => Refinery.ProofState.MonadExtract ext (Control.Monad.Trans.Writer.Lazy.WriterT w m)
instance (Refinery.ProofState.MonadExtract ext m, GHC.Base.Monoid w) => Refinery.ProofState.MonadExtract ext (Control.Monad.Trans.Writer.Strict.WriterT w m)
instance Refinery.ProofState.MonadExtract ext m => Refinery.ProofState.MonadExtract ext (Control.Monad.Trans.Except.ExceptT err m)
instance (GHC.Show.Show goal, GHC.Show.Show err, GHC.Show.Show ext, GHC.Show.Show (m (Refinery.ProofState.ProofStateT ext' ext err s m goal))) => GHC.Show.Show (Refinery.ProofState.ProofStateT ext' ext err s m goal)
instance GHC.Base.Functor m => GHC.Base.Functor (Refinery.ProofState.ProofStateT ext' ext err s m)
instance GHC.Base.Functor m => GHC.Base.Applicative (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Morph.MFunctor (Refinery.ProofState.ProofStateT ext' ext err s)
instance GHC.Base.Functor m => GHC.Base.Monad (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Trans.Class.MonadTrans (Refinery.ProofState.ProofStateT ext ext err s)
instance GHC.Base.Monad m => GHC.Base.Alternative (Refinery.ProofState.ProofStateT ext ext err s m)
instance GHC.Base.Monad m => GHC.Base.MonadPlus (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Catch.MonadThrow m => Control.Monad.Catch.MonadThrow (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Catch.MonadCatch m => Control.Monad.Catch.MonadCatch (Refinery.ProofState.ProofStateT ext ext err s m)
instance GHC.Base.Monad m => Control.Monad.Error.Class.MonadError err (Refinery.ProofState.ProofStateT ext ext err s m)
instance Control.Monad.Reader.Class.MonadReader r m => Control.Monad.Reader.Class.MonadReader r (Refinery.ProofState.ProofStateT ext ext err s m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState s (Refinery.ProofState.ProofStateT ext ext err s m)


-- | <h1>WARNING</h1>
--   
--   This module is considered <b>internal</b>, and can change at any given
--   time.
module Refinery.Tactic.Internal

-- | A <tt><a>TacticT</a></tt> is a monad transformer that performs proof
--   refinement. The type variables signifiy:
--   
--   <ul>
--   <li><tt>jdg</tt> - The goal type. This is the thing we are trying to
--   construct a proof of.</li>
--   <li><tt>ext</tt> - The extract type. This is what we will recieve
--   after running the tactic.</li>
--   <li><tt>err</tt> - The error type. We can use <a>throwError</a> to
--   abort the computation with a provided error</li>
--   <li><tt>s</tt> - The state type.</li>
--   <li><tt>m</tt> - The base monad.</li>
--   <li><tt>a</tt> - The return value. This to make
--   <tt><a>TacticT</a></tt> a monad, and will always be <tt>'()'</tt></li>
--   </ul>
newtype TacticT jdg ext err s m a
TacticT :: StateT jdg (ProofStateT ext ext err s m) a -> TacticT jdg ext err s m a
[unTacticT] :: TacticT jdg ext err s m a -> StateT jdg (ProofStateT ext ext err s m) a

-- | Helper function for producing a tactic.
tactic :: (jdg -> ProofStateT ext ext err s m (a, jdg)) -> TacticT jdg ext err s m a

-- | Helper function for deconstructing a tactic.
proofState :: TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m (a, jdg)

-- | Map the unwrapped computation using the given function
mapTacticT :: Monad m => (m a -> m b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
class (Monad m) => MonadRule jdg ext m | m -> jdg, m -> ext

-- | Create a subgoal, and return the resulting extract.
subgoal :: MonadRule jdg ext m => jdg -> m ext

-- | Create a subgoal, and return the resulting extract.
subgoal :: (MonadRule jdg ext m, MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext

-- | A <tt><a>RuleT</a></tt> is a monad transformer for creating inference
--   rules.
newtype RuleT jdg ext err s m a
RuleT :: ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
[unRuleT] :: RuleT jdg ext err s m a -> ProofStateT ext a err s m jdg
instance GHC.Generics.Generic (Refinery.Tactic.Internal.RuleT jdg ext err s m a)
instance GHC.Generics.Generic (Refinery.Tactic.Internal.TacticT jdg ext err s m a)
instance Control.Monad.Catch.MonadCatch m => Control.Monad.Catch.MonadCatch (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance Control.Monad.Catch.MonadThrow m => Control.Monad.Catch.MonadThrow (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Monad m => Control.Monad.Error.Class.MonadError err (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance Control.Monad.Reader.Class.MonadReader env m => Control.Monad.Reader.Class.MonadReader env (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.MonadPlus (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Functor m => GHC.Base.Monad (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.Alternative (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Functor m => GHC.Base.Applicative (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Functor m => GHC.Base.Functor (Refinery.Tactic.Internal.TacticT jdg ext err s m)
instance GHC.Base.Monad m => Refinery.Tactic.Internal.MonadRule jdg ext (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance Refinery.Tactic.Internal.MonadRule jdg ext m => Refinery.Tactic.Internal.MonadRule jdg ext (Control.Monad.Trans.Reader.ReaderT env m)
instance Refinery.Tactic.Internal.MonadRule jdg ext m => Refinery.Tactic.Internal.MonadRule jdg ext (Control.Monad.Trans.State.Strict.StateT env m)
instance Refinery.Tactic.Internal.MonadRule jdg ext m => Refinery.Tactic.Internal.MonadRule jdg ext (Control.Monad.Trans.Except.ExceptT env m)
instance (GHC.Show.Show jdg, GHC.Show.Show err, GHC.Show.Show a, GHC.Show.Show (m (Refinery.ProofState.ProofStateT ext a err s m jdg))) => GHC.Show.Show (Refinery.Tactic.Internal.RuleT jdg ext err s m a)
instance GHC.Base.Functor m => GHC.Base.Functor (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => GHC.Base.Monad (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState s (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance Control.Monad.Reader.Class.MonadReader r m => Control.Monad.Reader.Class.MonadReader r (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance Control.Monad.Trans.Class.MonadTrans (Refinery.Tactic.Internal.RuleT jdg ext err s)
instance Control.Monad.Morph.MFunctor (Refinery.Tactic.Internal.RuleT jdg ext err s)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance GHC.Base.Monad m => Control.Monad.Error.Class.MonadError err (Refinery.Tactic.Internal.RuleT jdg ext err s m)
instance (GHC.Base.Monoid jdg, GHC.Show.Show a, GHC.Show.Show jdg, GHC.Show.Show err, GHC.Show.Show ext, GHC.Show.Show (m (Refinery.ProofState.ProofStateT ext ext err s m (a, jdg)))) => GHC.Show.Show (Refinery.Tactic.Internal.TacticT jdg ext err s m a)
instance Control.Monad.Trans.Class.MonadTrans (Refinery.Tactic.Internal.TacticT jdg ext err s)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState s (Refinery.Tactic.Internal.TacticT jdg ext err s m)


module Refinery.Tactic

-- | A <tt><a>TacticT</a></tt> is a monad transformer that performs proof
--   refinement. The type variables signifiy:
--   
--   <ul>
--   <li><tt>jdg</tt> - The goal type. This is the thing we are trying to
--   construct a proof of.</li>
--   <li><tt>ext</tt> - The extract type. This is what we will recieve
--   after running the tactic.</li>
--   <li><tt>err</tt> - The error type. We can use <a>throwError</a> to
--   abort the computation with a provided error</li>
--   <li><tt>s</tt> - The state type.</li>
--   <li><tt>m</tt> - The base monad.</li>
--   <li><tt>a</tt> - The return value. This to make
--   <tt><a>TacticT</a></tt> a monad, and will always be <tt>'()'</tt></li>
--   </ul>
data TacticT jdg ext err s m a

-- | Runs a tactic, producing a list of possible extracts, along with a
--   list of unsolved subgoals.
runTacticT :: MonadExtract ext m => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, [jdg])]
(<@>) :: Functor m => 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 -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
infixr 3 <%>

-- | Tries to run a tactic, backtracking on failure
try :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()

-- | Runs a tactic repeatedly until it fails
many_ :: Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
choice :: Monad m => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
progress :: Monad m => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a

-- | Minimal implementation: msplit
class MonadPlus m => MonadLogic (m :: Type -> Type)

-- | Attempts to split the computation, giving access to the first result.
--   Satisfies the following laws:
--   
--   <pre>
--   msplit mzero                == return Nothing
--   msplit (return a `mplus` m) == return (Just (a, m))
--   </pre>
msplit :: MonadLogic m => m a -> m (Maybe (a, m a))

-- | Fair disjunction. It is possible for a logical computation to have an
--   infinite number of potential results, for instance:
--   
--   <pre>
--   odds = return 1 `mplus` liftM (2+) odds
--   </pre>
--   
--   Such computations can cause problems in some circumstances. Consider:
--   
--   <pre>
--   do x &lt;- odds `mplus` return 2
--      if even x then return x else mzero
--   </pre>
--   
--   Such a computation may never consider the 'return 2', and will
--   therefore never terminate. By contrast, interleave ensures fair
--   consideration of both branches of a disjunction
interleave :: MonadLogic m => m a -> m a -> m a

-- | Fair conjunction. Similarly to the previous function, consider the
--   distributivity law for MonadPlus:
--   
--   <pre>
--   (mplus a b) &gt;&gt;= k = (a &gt;&gt;= k) `mplus` (b &gt;&gt;= k)
--   </pre>
--   
--   If 'a &gt;&gt;= k' can backtrack arbitrarily many tmes, (b &gt;&gt;=
--   k) may never be considered. (&gt;&gt;-) takes similar care to consider
--   both branches of a disjunctive computation.
(>>-) :: MonadLogic m => m a -> (a -> m b) -> m b

-- | Logical conditional. The equivalent of Prolog's soft-cut. If its first
--   argument succeeds at all, then the results will be fed into the
--   success branch. Otherwise, the failure branch is taken. satisfies the
--   following laws:
--   
--   <pre>
--   ifte (return a) th el           == th a
--   ifte mzero th el                == el
--   ifte (return a `mplus` m) th el == th a `mplus` (m &gt;&gt;= th)
--   </pre>
ifte :: MonadLogic m => m a -> (a -> m b) -> m b -> m b

-- | Pruning. Selects one result out of many. Useful for when multiple
--   results of a computation will be equivalent, or should be treated as
--   such.
once :: MonadLogic m => m a -> m a

-- | Inverts a logic computation. If <tt>m</tt> succeeds with at least one
--   value, <tt>lnot m</tt> fails. If <tt>m</tt> fails, then <tt>lnot
--   m</tt> succeeds the value <tt>()</tt>.
lnot :: MonadLogic m => m a -> m ()
infixl 1 >>-

-- | Get the current goal
goal :: Functor m => TacticT jdg ext err s m jdg
focus :: Functor m => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
class (Monad m) => MonadExtract ext m | m -> ext

-- | Generates a "hole" of type <tt>ext</tt>, which should represent an
--   incomplete extract.
hole :: MonadExtract ext m => m ext

-- | Generates a "hole" of type <tt>ext</tt>, which should represent an
--   incomplete extract.
hole :: (MonadExtract ext m, MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext
class (Monad m) => MonadRule jdg ext m | m -> jdg, m -> ext

-- | Create a subgoal, and return the resulting extract.
subgoal :: MonadRule jdg ext m => jdg -> m ext

-- | Create a subgoal, and return the resulting extract.
subgoal :: (MonadRule jdg ext m, MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext

-- | A <tt><a>RuleT</a></tt> is a monad transformer for creating inference
--   rules.
data RuleT jdg ext err s m a

-- | Turn an inference rule into a tactic.
rule :: Monad m => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()