refinery 0.1.0.0 → 0.2.0.0

raw patch · 7 files changed

+619/−242 lines, 7 filesdep +QuickCheckdep +checkersdep +hspecdep −containersdep −pipesdep −semigroupoidsPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck, checkers, hspec, logict

Dependencies removed: containers, pipes, semigroupoids

API changes (from Hackage documentation)

Files

• ChangeLog.md +7/−0
• refinery.cabal +12/−11
• src/Refinery/ProofState.hs +209/−47
• src/Refinery/Tactic.hs +37/−86
• src/Refinery/Tactic/Internal.hs +105/−97
• test/Checkers.hs +41/−0
• test/Spec.hs +208/−1

@@ -1,3 +1,10 @@ # Changelog for refinery ++* 0.1.0.0+  Initial Release of the library+ ## Unreleased changes++* 0.2.0.0+  Added Alternative/MonadPlus instances to ProofStateT, TacticT, RuleT

@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.1.+-- This file has been generated from package.yaml by hpack version 0.33.0. -- -- see: https://github.com/sol/hpack ----- hash: f61ff60d97eac2723f257e2cb25ede1205a5cb260049a1708c66c7ab0d4669f8+-- hash: 47bfe1a8a6266a80890a145e94605cb2fc4b85749382b27f0f5ed1db65241473  name:           refinery-version:        0.1.0.0+version:        0.2.0.0 synopsis:       Toolkit for building proof automation systems description:    Please see the README on GitHub at <https://github.com/githubuser/refinery#readme> category:       Language@@ -36,31 +36,32 @@       Paths_refinery   hs-source-dirs:       src+  ghc-options: -Wall -Wredundant-constraints   build-depends:       base >=4.7 && <5-    , containers >=0.5     , exceptions >=0.10+    , logict >=0.6     , mmorph >=1     , mtl >=2-    , pipes >=4-    , semigroupoids >=5   default-language: Haskell2010  test-suite refinery-test   type: exitcode-stdio-1.0   main-is: Spec.hs   other-modules:+      Checkers       Paths_refinery   hs-source-dirs:       test-  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N   build-depends:-      base >=4.7 && <5-    , containers >=0.5+      QuickCheck+    , base >=4.7 && <5+    , checkers     , exceptions >=0.10+    , hspec+    , logict >=0.6     , mmorph >=1     , mtl >=2-    , pipes >=4     , refinery-    , semigroupoids >=5   default-language: Haskell2010

@@ -1,7 +1,18 @@-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-name-shadowing #-}++{-# LANGUAGE TupleSections          #-}+{-# LANGUAGE DefaultSignatures      #-}+{-# LANGUAGE DeriveGeneric          #-}+{-# LANGUAGE DerivingStrategies     #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE LambdaCase             #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE UndecidableInstances   #-}+ ----------------------------------------------------------------------------- -- | -- Module      :  Refinery.ProofState@@ -11,62 +22,213 @@ -- -- module Refinery.ProofState-  ( ProofStateT(..)-  , axiom-  , mapExtract-  ) where -import Control.Applicative-import Control.Monad-import Control.Monad.Trans-import Control.Monad.Catch-import Control.Monad.Except-import Control.Monad.Reader.Class-import Control.Monad.State.Class-import Control.Monad.IO.Class+import           Control.Applicative+import           Control.Monad+import           Control.Monad.Catch hiding (handle)+import           Control.Monad.Except+import qualified Control.Monad.Writer.Lazy as LW+import qualified Control.Monad.Writer.Strict as SW+import           Control.Monad.State+import           Control.Monad.Logic+import           Control.Monad.Morph+import           Control.Monad.Reader -import Pipes.Core+import           GHC.Generics -newtype ProofStateT ext m jdg = ProofStateT { unProofStateT :: Client jdg ext m ext }+data ProofStateT ext' ext err s m goal+    = Subgoal goal (ext' -> ProofStateT ext' ext err s m goal)+    | Effect (m (ProofStateT ext' ext err s m goal))+    | Stateful (s -> (s, ProofStateT ext' ext err s m goal))+    | Alt (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)+    | Empty+    | Failure err+    | Axiom ext+    deriving stock (Generic) -instance (Monad m) => Functor (ProofStateT ext m) where-  fmap f (ProofStateT p) = ProofStateT $ (request . f) >\\ p+instance (Show goal, Show err, Show ext, Show (m (ProofStateT ext' ext err s m goal))) => Show (ProofStateT ext' ext err s m goal) where+  show (Subgoal goal _) = "(Subgoal " <> show goal <> " <k>)"+  show (Effect m) = "(Effect " <> show m <> ")"+  show (Stateful _) = "(Stateful <s>)"+  show (Alt p1 p2) = "(Alt " <> show p1 <> " " <> show p2 <> ")"+  show (Interleave p1 p2) = "(Interleave " <> show p1 <> " " <> show p2 <> ")"+  show Empty = "Empty"+  show (Failure err) = "(Failure " <> show err <> ")"+  show (Axiom ext) = "(Axiom " <> show ext <> ")" -instance (Monad m) => Applicative (ProofStateT ext m) where-  pure a = ProofStateT $ request a-  (ProofStateT pf) <*> (ProofStateT pa) = ProofStateT $ (\f -> (request . f) >\\ pa) >\\ pf+instance Functor m => Functor (ProofStateT ext' ext err s m) where+    fmap f (Subgoal goal k) = Subgoal (f goal) (fmap f . k)+    fmap f (Effect m) = Effect (fmap (fmap f) m)+    fmap f (Stateful s) = Stateful $ fmap (fmap f) . s+    fmap f (Alt p1 p2) = Alt (fmap f p1) (fmap f p2)+    fmap f (Interleave p1 p2) = Interleave (fmap f p1) (fmap f p2)+    fmap _ Empty = Empty+    fmap _ (Failure err) = Failure err+    fmap _ (Axiom ext) = Axiom ext -instance (Monad m) => Monad (ProofStateT ext m) where-  return = pure-  (ProofStateT p) >>= k = ProofStateT $ (unProofStateT . k) >\\ p+instance Functor m => Applicative (ProofStateT ext ext err s m) where+    pure = return+    (<*>) = ap -instance MonadTrans (ProofStateT ext) where-  lift m = ProofStateT $ request =<< (lift m)+instance MFunctor (ProofStateT ext' ext err s) where+  hoist nat (Subgoal a k) = Subgoal a $ fmap (hoist nat) k+  hoist nat (Effect m)    = Effect $ nat $ fmap (hoist nat) m+  hoist nat (Stateful f)    = Stateful $ fmap (hoist nat) . f+  hoist nat (Alt p1 p2)   = Alt (hoist nat p1) (hoist nat p2)+  hoist nat (Interleave p1 p2)   = Interleave (hoist nat p1) (hoist nat p2)+  hoist _ (Failure err) = Failure err+  hoist _ Empty         = Empty+  hoist _ (Axiom ext)   = Axiom ext -instance (MonadIO m) => MonadIO (ProofStateT ext m) where-  liftIO m = ProofStateT $ request =<< (liftIO m)+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+applyCont k (Subgoal goal k') = Subgoal goal (applyCont k . k')+applyCont k (Effect m) = Effect (fmap (applyCont k) m)+applyCont k (Stateful s) = Stateful $ fmap (applyCont k) . s+applyCont k (Alt p1 p2) = Alt (applyCont k p1) (applyCont k p2)+applyCont k (Interleave p1 p2) = Interleave (applyCont k p1) (applyCont k p2)+applyCont _ Empty = Empty+applyCont _ (Failure err) = (Failure err)+applyCont k (Axiom ext) = k ext -instance (MonadError err m) => MonadError err (ProofStateT ext m) where-  throwError e = ProofStateT $ lift $ throwError e-  catchError (ProofStateT m) h = ProofStateT $ catchError m (unProofStateT . h)+instance Functor m => Monad (ProofStateT ext ext err s m) where+    return goal = Subgoal goal Axiom+    (Subgoal a k) >>= f = applyCont ((>>= f) . k) (f a)+    (Effect m)    >>= f = Effect (fmap (>>= f) m)+    (Stateful s)  >>= f = Stateful $ fmap (>>= f) . s+    (Alt p1 p2)   >>= f = Alt (p1 >>= f) (p2 >>= f)+    (Interleave p1 p2)   >>= f = Interleave (p1 >>= f) (p2 >>= f)+    (Failure err) >>= _ = Failure err+    Empty         >>= _ = Empty+    (Axiom ext)   >>= _ = Axiom ext -instance (MonadThrow m) => MonadThrow (ProofStateT ext m) where-  throwM e = ProofStateT $ lift $ throwM e+instance MonadTrans (ProofStateT ext ext err s) where+    lift m = Effect (fmap pure m) -instance (MonadCatch m) => MonadCatch (ProofStateT ext m) where-  catch (ProofStateT m) h = ProofStateT $ catch m (unProofStateT . h)+instance (Monad m) => Alternative (ProofStateT ext ext err s m) where+    empty = Empty+    (<|>) = Alt -instance (MonadReader env m) => MonadReader env (ProofStateT ext m) where-  ask = lift ask-  local f (ProofStateT m) = ProofStateT $ local f m+instance (Monad m) => MonadPlus (ProofStateT ext ext err s m) where+    mzero = empty+    mplus = (<|>) -instance (MonadState s m) => MonadState s (ProofStateT ext m) where-  get = lift get-  put = lift . put+class (Monad m) => MonadExtract ext m | m -> ext where+  -- | Generates a "hole" of type @ext@, which should represent+  -- an incomplete extract.+  hole :: m ext+  default hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext+  hole = lift hole -axiom :: (Monad m) => ext -> ProofStateT ext m jdg-axiom e = ProofStateT $ return e+instance (MonadExtract ext m) => MonadExtract ext (ReaderT r m)+instance (MonadExtract ext m) => MonadExtract ext (StateT s m)+instance (MonadExtract ext m, Monoid w) => MonadExtract ext (LW.WriterT w m)+instance (MonadExtract ext m, Monoid w) => MonadExtract ext (SW.WriterT w m)+instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m) -mapExtract :: (Monad m) => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext m jdg -> ProofStateT ext' m jdg-mapExtract into out p = ProofStateT $ fmap into ((\j ->  fmap out $ request j) >\\ (unProofStateT p))+proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, [goal])]+proofs s p = go s [] p+    where+      go s goals (Subgoal goal k) = do+         h <- hole+         (go s (goals ++ [goal]) $ k h)+      go s goals (Effect m) = go s goals =<< m+      go s goals (Stateful f) =+          let (s', p) = f s+          in go s' goals p+      go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)+      go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)+      go _ _ Empty = pure []+      go _ _ (Failure err) = pure [throwError err]+      go _ goals (Axiom ext) = pure [Right (ext, goals)]++accumEither :: (Semigroup a, Semigroup b) => Either a b -> Either a b -> Either a b+accumEither (Left a1) (Left a2)   = Left (a1 <> a2)+accumEither (Right b1) (Right b2) = Right (b1 <> b2)+accumEither Left{} x              = x+accumEither x Left{}              = x++instance (MonadIO m) => MonadIO (ProofStateT ext ext err s m) where+  liftIO = lift . liftIO++instance (MonadThrow m) => MonadThrow (ProofStateT ext ext err s m) where+  throwM = lift . throwM++instance (MonadCatch m) => MonadCatch (ProofStateT ext ext err s m) where+    catch (Subgoal goal k) handle = Subgoal goal (flip catch handle . k)+    catch (Effect m) handle = Effect . catch m $ pure . handle+    catch (Stateful s) handle = Stateful (fmap (flip catch handle) . s)+    catch (Alt p1 p2) handle = Alt (catch p1 handle) (catch p2 handle)+    catch (Interleave p1 p2) handle = Interleave (catch p1 handle) (catch p2 handle)+    catch Empty _ = Empty+    catch (Failure err) _ = Failure err+    catch (Axiom e) _ = (Axiom e)++instance (Monad m) => MonadError err (ProofStateT ext ext err s m) where+    throwError = Failure+    catchError (Subgoal goal k) handle = Subgoal goal (flip catchError handle . k)+    catchError (Effect m) handle = Effect (fmap (flip catchError handle) m)+    catchError (Stateful s) handle = Stateful $ fmap (flip catchError handle) . s+    catchError (Alt p1 p2) handle = catchError p1 handle <|> catchError p2 handle+    catchError (Interleave p1 p2) handle = catchError p1 handle <|> catchError p2 handle+    catchError Empty _ = Empty+    catchError (Failure err) handle = handle err+    catchError (Axiom e) _ = (Axiom e)++instance (MonadReader r m) => MonadReader r (ProofStateT ext ext err s m) where+    ask = lift ask+    local f (Subgoal goal k) = Subgoal goal (local f . k)+    local f (Effect m) = Effect (local f m)+    local f (Stateful s) = Stateful (fmap (local f) . s)+    local f (Alt p1 p2) = Alt (local f p1) (local f p2)+    local f (Interleave p1 p2) = Interleave (local f p1) (local f p2)+    local _ Empty = Empty+    local _ (Failure err) = (Failure err)+    local _ (Axiom e) = (Axiom e)++instance (Monad m) => MonadState s (ProofStateT ext ext err s m) where+    state f = Stateful $ \s ->+      let (a, s') = f s+      in (s', pure a)++axiom :: ext -> ProofStateT ext' ext err s m jdg+axiom = Axiom++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+subgoals [] (Subgoal goal k) = applyCont k (pure goal)+subgoals (f:fs) (Subgoal goal k)  = applyCont (subgoals fs . k) (f goal)+subgoals fs (Effect m) = Effect (fmap (subgoals fs) m)+subgoals fs (Stateful s) = Stateful (fmap (subgoals fs) . s)+subgoals fs (Alt p1 p2) = Alt (subgoals fs p1) (subgoals fs p2)+subgoals fs (Interleave p1 p2) = Interleave (subgoals fs p1) (subgoals fs p2)+subgoals _ (Failure err) = Failure err+subgoals _ Empty = Empty+subgoals _ (Axiom ext) = Axiom ext++mapExtract :: (Functor m) => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext ext err s m jdg -> ProofStateT ext' ext' err s m jdg+mapExtract into out = \case+    Subgoal goal k -> Subgoal goal $ mapExtract into out . k . out+    Effect m -> Effect (fmap (mapExtract into out) m)+    Stateful s -> Stateful (fmap (mapExtract into out) . s)+    Alt t1 t2 -> Alt (mapExtract into out t1) (mapExtract into out t2)+    Interleave t1 t2 -> Interleave (mapExtract into out t1) (mapExtract into out t2)+    Empty -> Empty+    Failure err -> Failure err+    Axiom ext -> Axiom $ into ext++mapExtract' :: Functor m => (a -> b) -> ProofStateT ext' a err s m jdg -> ProofStateT ext' b err s m jdg+mapExtract' into = \case+    Subgoal goal k -> Subgoal goal $ mapExtract' into . k+    Effect m -> Effect (fmap (mapExtract' into) m)+    Stateful s -> Stateful (fmap (mapExtract' into) . s)+    Alt t1 t2 -> Alt (mapExtract' into t1) (mapExtract' into t2)+    Interleave t1 t2 -> Interleave (mapExtract' into t1) (mapExtract' into t2)+    Empty -> Empty+    Failure err -> Failure err+    Axiom ext -> Axiom $ into ext+

@@ -1,3 +1,4 @@+{-# LANGUAGE TupleSections #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-}@@ -18,129 +19,79 @@   , runTacticT   -- * Tactic Combinators   , (<@>)+  , (<%>)   , try   , many_   , choice   , progress+  , MonadLogic(..)   -- * Subgoal Manipulation   , goal   , focus-  , forSubgoals   -- * Tactic Creation   , MonadExtract(..)   , MonadRule(..)   , RuleT   , rule-  , MonadProvable(..)-  , ProvableT(..)-  , Provable-  , runProvable-  -- * Re-Exports-  , Alt(..)   ) where -import Data.Functor.Alt import Control.Applicative import Control.Monad.Except-import Control.Monad.Reader import Control.Monad.State.Strict-import Control.Monad.Trans-import Control.Monad.IO.Class-import Control.Monad.Morph--import Data.Bifunctor--import Pipes.Core-import Pipes.Lift (runStateP)+import Control.Monad.Logic  import Refinery.ProofState import Refinery.Tactic.Internal --- | 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.-(<@>) :: (MonadProvable jdg m) => TacticT jdg ext m () -> [TacticT jdg ext m ()] -> TacticT jdg ext m ()-t <@> ts = stateful t applyTac (ts ++ repeat (pure ()))-  where-    applyTac j = do-      tac <- gets head-      modify tail-      hoist lift $ asRule j tac+-- -- | 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+t <@> ts = tactic $ \j -> subgoals (fmap (\t' (_,j') -> proofState t' j') ts) (proofState t j) +infixr 3 <%>++(<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a+t1 <%> t2 = tactic $ \j -> Interleave (proofState t1 j) (proofState t2 j)++ -- | Tries to run a tactic, backtracking on failure-try :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()-try t = t <!> pure ()+try :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()+try t = t <|> pure ()  -- | Runs a tactic repeatedly until it fails-many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()+many_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m () many_ t = try (t >> many_ t)  -- | Get the current goal-goal :: (Monad m) => TacticT jdg ext m jdg+goal :: (Functor m) => TacticT jdg ext err s m jdg goal = TacticT $ get ---- | @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-choice :: (MonadProvable jdg m, MonadError err m) => err -> [TacticT jdg ext m a] -> TacticT jdg ext m a-choice err [] = throwError err-choice err (t:ts) = t <!> choice err ts+choice :: (Monad m) => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a+choice [] = empty+choice (t:ts) = t <%> choice ts --- | @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 :: (MonadProvable jdg m, MonadError err m) => (jdg -> jdg -> Bool) -> err ->  TacticT jdg ext m a -> TacticT jdg ext 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 progress eq err t = do   j <- goal   a <- t   j' <- goal   if j `eq` j' then pure a else throwError err --- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.-focus :: (MonadProvable jdg m, Monad m) => TacticT jdg ext m () -> Int -> TacticT jdg ext m () -> TacticT jdg ext m ()-focus t ix t' = stateful t applyTac 0-  where-    applyTac j = do-      n <- get-      put (n + 1)-      hoist lift $ asRule j (if n == ix then t' else pure ())---- | Applies @f@ to every subgoals resulting from the tactic @t@.-forSubgoals :: (Monad m) => TacticT jdg ext m a -> (jdg -> m b) -> TacticT jdg ext m a-forSubgoals t f = TacticT $ StateT $ \j -> ProofStateT $-   action >\\ (unProofStateT $ runStateT (unTacticT t) j)-  where-    action (a, j) = do-      lift $ f j-      request (a, j)---- | Runs a tactic, producing the extract, along with a list of unsolved subgoals.-runTacticT :: (MonadExtract ext m) => TacticT jdg ext m () -> jdg -> m (ext, [jdg])-runTacticT (TacticT t) j =-  fmap (second reverse) $ flip runStateT [] $ runEffect $ server +>> (hoist lift $ unProofStateT $ execStateT t j)-  where-    server :: (MonadExtract ext m) => jdg -> Server jdg ext (StateT [jdg] m) ext-    server j = do-      modify (j:)-      h <- hole-      respond h >>= server--class (Monad m) => MonadExtract ext m | m -> ext where-  -- | Generates a "hole" of type @ext@, which should represent-  -- an incomplete extract.-  hole :: m ext-  default hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext-  hole = lift hole--instance (MonadExtract ext m) => MonadExtract ext (Proxy a' a b' b m)-instance (MonadExtract ext m) => MonadExtract ext (StateT s m)-instance (MonadExtract ext m) => MonadExtract ext (ReaderT env m)-instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m)-instance (MonadExtract ext m) => MonadExtract ext (RuleT jdg ext m)+-- -- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.+focus :: (Functor m) => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()+focus t n t' = t <@> (replicate n (pure ()) ++ [t'] ++ repeat (pure ())) +-- | 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])]+runTacticT t j s = proofs s $ fmap snd $ proofState t j  -- | Turn an inference rule into a tactic.-rule :: (Monad m) => (jdg -> RuleT jdg ext m ext) -> TacticT jdg ext m ()-rule r = TacticT $ StateT $ \j -> ProofStateT $ (\j' -> request ((), j')) >\\ unRuleT (r j)+rule :: (Monad m) => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()+rule r = tactic $ \j -> fmap ((),) $ unRuleT (r j)+

@@ -1,14 +1,17 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE DefaultSignatures          #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DerivingStrategies         #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE FunctionalDependencies     #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase                 #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TupleSections              #-}+{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE UndecidableInstances       #-}+ ----------------------------------------------------------------------------- -- | -- Module      :  Refinery.Tactic.Internal@@ -22,34 +25,26 @@ -- change at any given time. module Refinery.Tactic.Internal   ( TacticT(..)+  , tactic+  , proofState   , mapTacticT-  , stateful-  , asRule   , MonadRule(..)   , RuleT(..)-  , mapRuleT-  , MonadProvable(..)-  , ProvableT(..)-  , Provable-  , runProvable   ) where -import Data.Functor.Alt+import GHC.Generics import Control.Applicative import Control.Monad.Identity import Control.Monad.Except import Control.Monad.Catch import Control.Monad.Reader import Control.Monad.State.Strict-import Control.Monad.Trans-import Control.Monad.IO.Class+import Control.Monad.Trans ()+import Control.Monad.IO.Class () import Control.Monad.Morph -import Data.Bifunctor--import Pipes.Core-import Pipes.Lift (evalStateP, runStateP)+import Data.Coerce  import Refinery.ProofState @@ -58,107 +53,120 @@ -- -- * @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 @'()'@-newtype TacticT jdg ext m a = TacticT { unTacticT :: StateT jdg (ProofStateT ext m) a }+-- * @err@ - The error type. We can use 'throwError' to abort the computation with a provided error+-- * @s@   - The state type.+-- * @m@   - The base monad.+-- * @a@   - The return value. This to make @'TacticT'@ a monad, and will always be @'()'@+newtype TacticT jdg ext err s m a = TacticT { unTacticT :: StateT jdg (ProofStateT ext ext err s m) a }   deriving ( Functor+           , Applicative+           , Alternative+           , Monad+           , MonadPlus            , MonadReader env            , MonadError err            , MonadIO            , MonadThrow            , MonadCatch+           , Generic            ) -instance (MonadProvable jdg m) => Applicative (TacticT jdg ext m) where-  pure a = TacticT $ StateT $ proving >=> \j -> pure (a, j)-  (<*>) = ap+instance (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) where+  show = show . flip runStateT mempty . unTacticT -instance (MonadProvable jdg m) => Monad (TacticT jdg ext m) where-  return = pure-  t >>= k = TacticT $ StateT $ proving >=> \j -> do-    (a, j') <- runStateT (unTacticT t) j-    runStateT (unTacticT $ k a) =<< proving j'+-- | Helper function for producing a tactic.+tactic :: (jdg -> ProofStateT ext ext err s m (a, jdg)) -> TacticT jdg ext err s m a+tactic t = TacticT $ StateT t +-- |  Helper function for deconstructing a tactic.+proofState :: TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m (a, jdg)+proofState t j = runStateT (unTacticT t) j+ -- | Map the unwrapped computation using the given function-mapTacticT :: (Monad m) => (m a -> m b) -> TacticT jdg ext m a -> TacticT jdg ext m b+mapTacticT :: (Monad m) => (m a -> m b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b mapTacticT f (TacticT m) = TacticT $ m >>= (lift . lift . f . return) -instance (MonadError err m) => Alt (TacticT jdg ext m) where-  (TacticT t1) <!> (TacticT t2) = TacticT $ t1 `catchError` (const t2)--instance MonadTrans (TacticT jdg ext) where+instance MonadTrans (TacticT jdg ext err s) where   lift m = TacticT $ lift $ lift m -instance (MonadProvable jdg m, MonadState s m) => MonadState s (TacticT jdg ext m) where-  get = lift get-  put = lift . put+instance (Monad m) => MonadState s (TacticT jdg ext err s m) where+    state f = tactic $ \j -> fmap (,j) $ state f --- | Helper function for making "stateful" tactics like "<@>"-stateful :: (Monad m) => TacticT jdg ext m a -> (jdg -> RuleT jdg ext (StateT s m) ext) -> s -> TacticT jdg ext m a-stateful (TacticT t) f s = TacticT $ StateT $ \j -> ProofStateT $-  evalStateP s $ action >\\ (hoist lift $ unProofStateT $ runStateT t j)-  where-    action (a, j) = (\j' -> request (a, j')) >\\ (unRuleT $ f j)+-- | A @'RuleT'@ is a monad transformer for creating inference rules.+newtype RuleT jdg ext err s m a = RuleT+  { unRuleT :: ProofStateT ext a err s m jdg+  }+  deriving stock Generic --- | Transforms a tactic into a rule. Useful for doing things with @'stateful'@.-asRule :: (Monad m) => jdg -> TacticT jdg ext m a -> RuleT jdg ext m ext-asRule j t = RuleT $ unProofStateT $ execStateT (unTacticT t) j+instance (Show jdg, Show err, Show a, Show (m (ProofStateT ext a err s m jdg))) => Show (RuleT jdg ext err s m a) where+  show = show . unRuleT --- | A @'RuleT'@ is a monad transformer for creating inference rules.-newtype RuleT jdg ext m a = RuleT { unRuleT :: Client jdg ext m a }-  deriving ( Functor-           , Applicative-           , Monad-           , MonadReader env-           , MonadState s-           , MonadError err-           , MonadIO-           , MonadThrow-           , MonadCatch-           , MonadTrans-           , MFunctor-           )+instance Functor m => Functor (RuleT jdg ext err s m) where+  fmap = coerce mapExtract' +instance Monad m => Applicative (RuleT jdg ext err s m) where+  pure = return+  (<*>) = ap --- | Map the unwrapped computation using the given function-mapRuleT :: (Monad m) => (m a -> m b) -> RuleT jdg ext m a -> RuleT jdg ext m b-mapRuleT f (RuleT m) = RuleT $ m >>= (lift . f . return)+instance Monad m => Monad (RuleT jdg ext err s m) where+  return = coerce . Axiom+  RuleT (Subgoal goal k)   >>= f = coerce $ Subgoal goal $ fmap (bindAlaCoerce f) k+  RuleT (Effect m)         >>= f = coerce $ Effect $ fmap (bindAlaCoerce f) m+  RuleT (Stateful s)       >>= f = coerce $ Stateful $ fmap (bindAlaCoerce f) . s+  RuleT (Alt p1 p2)        >>= f = coerce $ Alt (bindAlaCoerce f p1) (bindAlaCoerce f p2)+  RuleT (Interleave p1 p2) >>= f = coerce $ Interleave (bindAlaCoerce f p1) (bindAlaCoerce f p2)+  RuleT Empty              >>= _ = coerce $ Empty+  RuleT (Failure err)      >>= _ = coerce $ Failure err+  RuleT (Axiom e)          >>= f = f e +instance Monad m => MonadState s (RuleT jdg ext err s m) where+    state f = RuleT $ Stateful $ \s ->+        let (a, s') = f s+        in (s', Axiom a)++instance MonadReader r m => MonadReader r (RuleT jdg ext err s m) where+    ask = lift ask+    local f (RuleT (Subgoal goal k))   = coerce $ Subgoal goal (localAlaCoerce f . k)+    local f (RuleT (Effect m))         = coerce $ Effect (local f m)+    local f (RuleT (Stateful s))       = coerce $ Stateful (fmap (localAlaCoerce f) . s)+    local f (RuleT (Alt p1 p2))        = coerce $ Alt (localAlaCoerce f p1) (localAlaCoerce f p2)+    local f (RuleT (Interleave p1 p2)) = coerce $ Interleave (localAlaCoerce f p1) (localAlaCoerce f p2)+    local _ (RuleT Empty)              = coerce $ Empty+    local _ (RuleT (Failure err))      = coerce $ Failure err+    local _ (RuleT (Axiom e))          = coerce $ Axiom e++bindAlaCoerce+  :: (Monad m, Coercible c (m b), Coercible a1 (m a2)) =>+     (a2 -> m b) -> a1 -> c+bindAlaCoerce f = coerce . (f =<<) . coerce++localAlaCoerce+  :: (MonadReader r m) =>+     (r -> r) -> ProofStateT ext a err s m jdg -> ProofStateT ext a err s m jdg+localAlaCoerce f = coerce . local f . RuleT++instance MonadTrans (RuleT jdg ext err s) where+  lift = coerce . Effect . fmap Axiom++instance MFunctor (RuleT jdg ext err s) where+  hoist nat = hoist nat . coerce++instance MonadIO m => MonadIO (RuleT jdg ext err s m) where+  liftIO = lift . liftIO++instance Monad m => MonadError err (RuleT jdg ext err s m) where+  throwError = coerce . Failure+  catchError r h = coerce $ flip catchError h $ coerce r+ class (Monad m) => MonadRule jdg ext m | m -> jdg, m -> ext where   -- | Create a subgoal, and return the resulting extract.   subgoal :: jdg -> m ext   default subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext   subgoal = lift . subgoal -instance (Monad m) => MonadRule jdg ext (RuleT jdg ext m) where-  subgoal j = RuleT $ request j+instance (Monad m) => MonadRule jdg ext (RuleT jdg ext err s m) where+  subgoal j = RuleT $ Subgoal j Axiom  instance (MonadRule jdg ext m) => MonadRule jdg ext (ReaderT env m) instance (MonadRule jdg ext m) => MonadRule jdg ext (StateT env m) instance (MonadRule jdg ext m) => MonadRule jdg ext (ExceptT env m)-instance (MonadRule jdg ext m) => MonadRule jdg ext (ProvableT env m)--class (Monad m) => MonadProvable jdg m | m -> jdg where-  -- | Applies a transformation of goals at every step of the tactic.-  proving :: jdg -> m jdg-  default proving :: (MonadTrans t, MonadProvable jdg m1, m ~ t m1) => jdg -> m jdg-  proving = lift . proving--instance (MonadProvable jdg m) => MonadProvable jdg (ProofStateT ext m)-instance (MonadProvable jdg m) => MonadProvable jdg (ReaderT r m)-instance (MonadProvable jdg m) => MonadProvable jdg (StateT s m)-instance (MonadProvable jdg m) => MonadProvable jdg (ExceptT err m)-instance (Monad m) => MonadProvable jdg (ProvableT jdg m) where-  proving = pure---- | Helper newtype for when you don't have any need for the mechanisms of MonadProvable.-newtype ProvableT jdg m a = ProvableT { runProvableT :: m a }-  deriving (Functor, Applicative, Monad, MonadIO, MonadState s, MonadError err)--type Provable jdg a = ProvableT jdg Identity a--instance MonadTrans (ProvableT jdg) where-  lift = ProvableT--runProvable :: Provable jdg a -> a-runProvable = runIdentity . runProvableT

@@ -0,0 +1,41 @@+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}++module Checkers where++import Control.Monad.State.Class+import Test.QuickCheck hiding (Failure)+import Test.QuickCheck.Checkers++monadState+    :: forall m s a b+     . ( MonadState s m+       , EqProp (m s)+       , EqProp (m ())+       , Show s+       , Arbitrary s+       )+    => m (a, b)+    -> TestBatch+monadState _ =+  ( "MonadState laws"+  , [ ("get >> get", (get >> get) =-= get @s @m)+    , ("get >>= put", (get @s @m >>= put) =-= pure ())+    , ("put >> put", property $ do+        s1 <- arbitrary+        s2 <- arbitrary+        pure $+          counterexample (show s1) $+          counterexample (show s2) $+            (put @_ @m s1 >> put s2) =-= put s2+      )+    , ("put >> get", property $ do+        s <- arbitrary+        pure $+          counterexample (show s) $+            (put s >> get) =-= pure @m s+      )+    ]+  )+

@@ -1,2 +1,209 @@+{-# LANGUAGE DeriveAnyClass             #-}+{-# LANGUAGE DerivingStrategies         #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE LambdaCase                 #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE StandaloneDeriving         #-}+{-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE UndecidableInstances       #-}+{-# OPTIONS_GHC -Wredundant-constraints #-}+{-# OPTIONS_GHC -fno-warn-orphans       #-}++module Main where++import Control.Applicative+import Control.Monad+import Control.Monad.State.Strict (StateT (..))+import Control.Monad.State.Class+import Data.Function+import Data.Functor.Identity+import Data.Monoid (Sum (..))+import Refinery.ProofState+import Refinery.Tactic+import Refinery.Tactic.Internal+import Test.Hspec+import Test.QuickCheck hiding (Failure)+import Test.QuickCheck.Checkers+import Test.QuickCheck.Classes+import Checkers++testBatch :: TestBatch -> Spec+testBatch (batchName, tests) = describe ("laws for: " ++ batchName) $+  foldr (>>) (return ()) (map (uncurry it) tests)+++instance (MonadExtract ext m, EqProp (m [Either err (ext, [a])]), Arbitrary s)+      => EqProp (ProofStateT ext ext err s m a) where+  (=-=) a b = property $ do+    s <- arbitrary+    pure $ ((=-=) `on` proofs s) a b++instance ( Show jdg+         , MonadExtract ext m+         , Arbitrary jdg+         , EqProp (m [Either err (ext, [jdg])])+         , Show s+         , Arbitrary s+         )+      => EqProp (TacticT jdg ext err s m a) where+  (=-=) = (=-=) `on` runTacticT . (() <$)++instance ( Show jdg+         , Arbitrary jdg+         , EqProp (m [Either err (ext, [jdg])])+         , MonadExtract ext m+         , Show s+         , Arbitrary s+         )+      => EqProp (RuleT jdg ext err s m ext) where+  (=-=) = (=-=) `on` rule . const++instance MonadExtract Int Identity where+  hole = pure 0++instance ( CoArbitrary ext'+         , Arbitrary ext+         , Arbitrary err+         , Arbitrary a+         , Arbitrary (m (ProofStateT ext' ext err s m a))+         , CoArbitrary s+         , Arbitrary s+         )+      => Arbitrary (ProofStateT ext' ext err s m a) where+  arbitrary = getSize >>= \case+    n | n <= 1 -> oneof small+    _ -> oneof $+      [ Subgoal <$> decayArbitrary 2 <*> decayArbitrary 2+      , Effect  <$> arbitrary+      , Alt     <$> decayArbitrary 2 <*> decayArbitrary 2+      , Stateful <$> arbitrary+      ] ++ small+    where+      small =+        [ pure Empty+        , Failure <$> arbitrary+        , Axiom   <$> arbitrary+        ]+  shrink = genericShrink++instance (Arbitrary (m (a, s)), CoArbitrary s) => Arbitrary (StateT s m a) where+  arbitrary = StateT <$> arbitrary++instance ( CoArbitrary jdg+         , Arbitrary a+         , Arbitrary ext+         , Arbitrary err+         , CoArbitrary ext+         , Arbitrary jdg+         , Arbitrary (m (ProofStateT ext ext err s m (a, jdg)))+         , CoArbitrary s+         , Arbitrary s+         )+      => Arbitrary (TacticT jdg ext err s m a) where+  arbitrary = fmap (TacticT . StateT) arbitrary+  shrink = genericShrink++instance ( Arbitrary a+         , Arbitrary err+         , CoArbitrary ext+         , Arbitrary jdg+         , Arbitrary (m (ProofStateT ext a err s m jdg))+         , CoArbitrary s+         , Arbitrary s+         )+      => Arbitrary (RuleT jdg ext err s m a) where+  arbitrary = fmap RuleT arbitrary+  shrink = genericShrink++decayArbitrary :: Arbitrary a => Int -> Gen a+decayArbitrary n = scale (`div` n) arbitrary++type ProofStateTest = ProofStateT Int Int String Int Identity+type RuleTest = RuleT Int Int String Int Identity+type TacticTest = TacticT (Sum Int) Int String Int Identity+ main :: IO ()-main = putStrLn "Test suite not yet implemented"+main = hspec $ do+  describe "ProofStateT" $ do+    testBatch $ functor     (undefined :: ProofStateTest (Int, Int, Int))+    testBatch $ applicative (undefined :: ProofStateTest (Int, Int, Int))+    testBatch $ alternative (undefined :: ProofStateTest Int)+    testBatch $ monad       (undefined :: ProofStateTest (Int, Int, Int))+    testBatch $ monadPlus   (undefined :: ProofStateTest (Int, Int))+    testBatch $ monadState  (undefined :: ProofStateTest (Int, Int))+    it "distrib put over <|>" $ property $ distribPut (undefined :: ProofStateTest (Int))+  describe "RuleT" $ do+    testBatch $ functor     (undefined :: RuleTest (Int, Int, Int))+    testBatch $ applicative (undefined :: RuleTest (Int, Int, Int))+    testBatch $ monad       (undefined :: RuleTest (Int, Int, Int))+  describe "TacticT" $ do+    testBatch $ functor     (undefined :: TacticTest ((), (), ()))+    testBatch $ applicative (undefined :: TacticTest ((), (), ()))+    testBatch $ alternative (undefined :: TacticTest ())+    testBatch $ monad       (undefined :: TacticTest ((), (), ()))+    testBatch $ monadPlus   (undefined :: TacticTest ((), ()))+    testBatch $ monadState  (undefined :: TacticTest ((), ()))+    it "interleave - mzero" $ property $ interleaveMZero (undefined :: TacticTest Int)+    it "interleave - mplus" $ property $ interleaveMPlus (undefined :: TacticTest Int)+    it "distrib put over <|>" $ property $ distribPut (undefined :: TacticTest ())++leftAltBind+    :: forall m a b+    . (EqProp (m b), Monad m, Alternative m)+    => m a -> m a -> (a -> m b)+    -> Property+leftAltBind m1 m2 f =+  ((m1 <|> m2) >>= f) =-= ((m1 >>= f) <|> (m2 >>= f))++rightAltBind+    :: forall m a+    . (EqProp (m a), Monad m, Alternative m)+    => m () -> m a -> m a+    -> Property+rightAltBind m1 m2 m3 =+  (m1 >> (m2 <|> m3)) =-= ((m1 >> m2) <|> (m1 >> m3))++interleaveMZero+    :: forall m a jdg ext err s+     . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),+      Show jdg, Show s, Arbitrary jdg, Arbitrary s)+    => TacticT jdg ext err s m a  -- ^ proxy+    -> TacticT jdg ext err s m a+    -> Property+interleaveMZero _ m =+    (mzero <%> m) =-= m++interleaveMPlus+    :: forall m a jdg ext err s+     . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),+      Show jdg, Show s, Arbitrary jdg, Arbitrary s)+    => TacticT jdg ext err s m a  -- ^ proxy+    -> a+    -> TacticT jdg ext err s m a+    -> TacticT jdg ext err s m a+    -> Property+interleaveMPlus _ a m1 m2 =+    ((pure a <|> m1) <%> m2) =-= (pure a <|> (m2 <%> m1))++distribPut+    :: forall s m a+     . ( MonadState s m+       , Alternative m+       , EqProp (m a)+       , Arbitrary (m a)+       , Arbitrary s+       , Show s+       , Show (m a)+       )+    => m a -> Property+distribPut _ = property $ do+  s <- arbitrary @s+  m1 <- arbitrary @(m a)+  m2 <- arbitrary @(m a)+  pure $+    counterexample (show s) $+    counterexample (show m1) $+    counterexample (show m2) $+      (put s >> (m1 <|> m2)) =-= ((put s >> m1) <|> (put s >> m2))+