-- 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 -- https://github.com/githubuser/refinery#readme @package refinery @version 0.3.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 Commit :: 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 ext, which should represent an -- incomplete extract. hole :: MonadExtract ext m => m ext -- | Generates a "hole" of type ext, 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, s, [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) -- |

WARNING

-- -- This module is considered internal, and can change at any given -- time. module Refinery.Tactic.Internal -- | A TacticT is a monad transformer that performs proof -- refinement. The type variables signifiy: -- -- 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 RuleT 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.Morph.MFunctor (Refinery.Tactic.Internal.TacticT jdg ext err s) 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 TacticT is a monad transformer that performs proof -- refinement. The type variables signifiy: -- -- 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, s, [jdg])] -- | 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. (<@>) :: Functor m => TacticT jdg ext err s m a -> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a -- | t1 % t2 will interleave the execution of t1 -- and t2. This is useful if t1 will produce an -- infinite number of extracts, as we will still run t2. This is -- contrasted with t1 | t2, which will not ever consider -- t2 if t1 produces an infinite number of extracts. (<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a infixr 3 <%> -- | commit t1 t2 will run t1, and then only run -- t2 if t1 failed to produce any extracts. commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a -- | 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 ts will run all of the tactics in the list against the -- current subgoals, and interleave their extracts in a manner similar to -- <%>. choice :: Monad m => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a -- | 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. progress :: Monad m => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a -- | gather t f runs the tactic t, then runs f -- with all of the generated subgoals to determine the next tactic to -- run. gather :: MonadExtract ext m => TacticT jdg ext err s m a -> ([(a, jdg)] -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a -- | pruning t f runs the tactic t, and then applies a -- predicate to all of the generated subgoals. pruning :: MonadExtract ext m => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m () -- | filterT p f t runs the tactic t, and applies a -- predicate to the state after the execution of t. We also run -- a "cleanup" function f. Note that the predicate is applied to -- the state _before_ the cleanup function is run. ensure :: Monad m => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m () -- | Get the current goal goal :: Functor m => TacticT jdg ext err s m jdg -- | Apply the first tactic, and then apply the second tactic focused on -- the nth subgoal. 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 ext, which should represent an -- incomplete extract. hole :: MonadExtract ext m => m ext -- | Generates a "hole" of type ext, 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 RuleT 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 ()