refinery 0.2.0.0 → 0.3.0.0
raw patch · 6 files changed
+129/−27 lines, 6 files
Files
- refinery.cabal +2/−2
- src/Refinery/ProofState.hs +23/−7
- src/Refinery/Tactic.hs +57/−12
- src/Refinery/Tactic/Internal.hs +6/−0
- test/Checkers.hs +1/−1
- test/Spec.hs +40/−5
refinery.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 47bfe1a8a6266a80890a145e94605cb2fc4b85749382b27f0f5ed1db65241473+-- hash: c5e5c657da3ec1e29d787f8c9eb17e054b2e5ad3a9e6420df6680e4cb31ca981 name: refinery-version: 0.2.0.0+version: 0.3.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
src/Refinery/ProofState.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} {-# LANGUAGE TupleSections #-}@@ -34,6 +35,7 @@ import Control.Monad.Logic import Control.Monad.Morph import Control.Monad.Reader+import Data.Either import GHC.Generics @@ -43,6 +45,7 @@ | 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)+ | Commit (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal) | Empty | Failure err | Axiom ext@@ -54,6 +57,7 @@ show (Stateful _) = "(Stateful <s>)" show (Alt p1 p2) = "(Alt " <> show p1 <> " " <> show p2 <> ")" show (Interleave p1 p2) = "(Interleave " <> show p1 <> " " <> show p2 <> ")"+ show (Commit p1 p2) = "(Commit " <> show p1 <> " " <> show p2 <> ")" show Empty = "Empty" show (Failure err) = "(Failure " <> show err <> ")" show (Axiom ext) = "(Axiom " <> show ext <> ")"@@ -64,6 +68,7 @@ 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 f (Commit p1 p2) = Commit (fmap f p1) (fmap f p2) fmap _ Empty = Empty fmap _ (Failure err) = Failure err fmap _ (Axiom ext) = Axiom ext@@ -78,20 +83,22 @@ 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 nat (Commit p1 p2) = Commit (hoist nat p1) (hoist nat p2) hoist _ (Failure err) = Failure err hoist _ Empty = Empty hoist _ (Axiom ext) = Axiom ext 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+ => (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 k (Commit p1 p2) = Commit (applyCont k p1) (applyCont k p2) applyCont _ Empty = Empty applyCont _ (Failure err) = (Failure err) applyCont k (Axiom ext) = k ext@@ -103,6 +110,7 @@ (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)+ (Commit p1 p2) >>= f = Commit (p1 >>= f) (p2 >>= f) (Failure err) >>= _ = Failure err Empty >>= _ = Empty (Axiom ext) >>= _ = Axiom ext@@ -131,7 +139,7 @@ instance (MonadExtract ext m, Monoid w) => MonadExtract ext (SW.WriterT w m) instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m) -proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, [goal])]+proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, s, [goal])] proofs s p = go s [] p where go s goals (Subgoal goal k) = do@@ -143,9 +151,12 @@ 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 s goals (Commit p1 p2) = go s goals p1 >>= \case+ (rights -> []) -> go s goals p2+ solns -> pure solns go _ _ Empty = pure [] go _ _ (Failure err) = pure [throwError err]- go _ goals (Axiom ext) = pure [Right (ext, goals)]+ go s goals (Axiom ext) = pure [Right (ext, s, goals)] accumEither :: (Semigroup a, Semigroup b) => Either a b -> Either a b -> Either a b accumEither (Left a1) (Left a2) = Left (a1 <> a2)@@ -165,6 +176,7 @@ 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 (Commit p1 p2) handle = Commit (catch p1 handle) (catch p2 handle) catch Empty _ = Empty catch (Failure err) _ = Failure err catch (Axiom e) _ = (Axiom e)@@ -175,7 +187,8 @@ 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 (Interleave p1 p2) handle = Interleave (catchError p1 handle) (catchError p2 handle)+ catchError (Commit p1 p2) handle = catchError p1 handle <|> catchError p2 handle catchError Empty _ = Empty catchError (Failure err) handle = handle err catchError (Axiom e) _ = (Axiom e)@@ -187,6 +200,7 @@ 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 f (Commit p1 p2) = Commit (local f p1) (local f p2) local _ Empty = Empty local _ (Failure err) = (Failure err) local _ (Axiom e) = (Axiom e)@@ -206,6 +220,7 @@ 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 fs (Commit p1 p2) = Commit (subgoals fs p1) (subgoals fs p2) subgoals _ (Failure err) = Failure err subgoals _ Empty = Empty subgoals _ (Axiom ext) = Axiom ext@@ -217,6 +232,7 @@ 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)+ Commit t1 t2 -> Commit (mapExtract into out t1) (mapExtract into out t2) Empty -> Empty Failure err -> Failure err Axiom ext -> Axiom $ into ext@@ -228,7 +244,7 @@ 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)+ Commit t1 t2 -> Commit (mapExtract' into t1) (mapExtract' into t2) Empty -> Empty Failure err -> Failure err Axiom ext -> Axiom $ into ext-
src/Refinery/Tactic.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} -----------------------------------------------------------------------------@@ -20,11 +21,14 @@ -- * Tactic Combinators , (<@>) , (<%>)+ , commit , try , many_ , choice , progress- , MonadLogic(..)+ , gather+ , pruning+ , ensure -- * Subgoal Manipulation , goal , focus@@ -38,24 +42,29 @@ import Control.Applicative import Control.Monad.Except import Control.Monad.State.Strict-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.+-- | 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 <%> +-- | @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 t1 <%> t2 = tactic $ \j -> Interleave (proofState t1 j) (proofState t2 j) +-- | @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+commit t1 t2 = tactic $ \j -> Commit (proofState t1 j) (proofState t2 j) -- | Tries to run a tactic, backtracking on failure try :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()@@ -69,13 +78,15 @@ goal :: (Functor m) => TacticT jdg ext err s m jdg goal = TacticT $ get +-- | @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 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 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@@ -83,12 +94,46 @@ 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.+-- | @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+gather t f = tactic $ \j -> do+ s <- get+ results <- lift $ proofs s $ proofState t j+ msum $ flip fmap results $ \case+ Left err -> throwError err+ Right (_, _, jdgs) -> proofState (f jdgs) j++-- | @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 ()+pruning t p = gather t $ maybe t throwError . p . fmap snd++-- | @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 ()+ensure p f t = check >> t+ where+ -- NOTE It may seem backwards to run check _before_ t, but we+ -- need to do the predicate check after the subgoal has been resolved,+ -- and not on every generated subgoal.+ check = rule $ \j -> do+ e <- subgoal j+ s <- get+ modify f+ case p s of+ Just err -> throwError err+ Nothing -> pure e++-- | 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 :: (MonadExtract ext m) => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, s, [jdg])] runTacticT t j s = proofs s $ fmap snd $ proofState t j -- | Turn an inference rule into a tactic.
src/Refinery/Tactic/Internal.hs view
@@ -86,9 +86,13 @@ 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 MFunctor (TacticT jdg ext err s) where+ hoist f = TacticT . (hoist (hoist f)) . unTacticT+ instance MonadTrans (TacticT jdg ext err s) where lift m = TacticT $ lift $ lift m + instance (Monad m) => MonadState s (TacticT jdg ext err s m) where state f = tactic $ \j -> fmap (,j) $ state f @@ -115,6 +119,7 @@ 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 (Commit p1 p2) >>= f = coerce $ Commit (bindAlaCoerce f p1) (bindAlaCoerce f p2) RuleT Empty >>= _ = coerce $ Empty RuleT (Failure err) >>= _ = coerce $ Failure err RuleT (Axiom e) >>= f = f e@@ -131,6 +136,7 @@ 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 f (RuleT (Commit p1 p2)) = coerce $ Commit (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
test/Checkers.hs view
@@ -34,7 +34,7 @@ s <- arbitrary pure $ counterexample (show s) $- (put s >> get) =-= pure @m s+ (put s >> get) =-= (put s >> pure @m s) ) ] )
test/Spec.hs view
@@ -16,6 +16,7 @@ import Control.Monad import Control.Monad.State.Strict (StateT (..)) import Control.Monad.State.Class+import Control.Monad.Error.Class import Data.Function import Data.Functor.Identity import Data.Monoid (Sum (..))@@ -33,7 +34,7 @@ foldr (>>) (return ()) (map (uncurry it) tests) -instance (MonadExtract ext m, EqProp (m [Either err (ext, [a])]), Arbitrary s)+instance (MonadExtract ext m, EqProp (m [Either err (ext, s, [a])]), Arbitrary s) => EqProp (ProofStateT ext ext err s m a) where (=-=) a b = property $ do s <- arbitrary@@ -42,7 +43,7 @@ instance ( Show jdg , MonadExtract ext m , Arbitrary jdg- , EqProp (m [Either err (ext, [jdg])])+ , EqProp (m [Either err (ext, s, [jdg])]) , Show s , Arbitrary s )@@ -51,7 +52,7 @@ instance ( Show jdg , Arbitrary jdg- , EqProp (m [Either err (ext, [jdg])])+ , EqProp (m [Either err (ext, s, [jdg])]) , MonadExtract ext m , Show s , Arbitrary s@@ -147,6 +148,9 @@ it "interleave - mzero" $ property $ interleaveMZero (undefined :: TacticTest Int) it "interleave - mplus" $ property $ interleaveMPlus (undefined :: TacticTest Int) it "distrib put over <|>" $ property $ distribPut (undefined :: TacticTest ())+ it "pure absorption on commit" $ property $ absorptionPureCommit (undefined :: TacticTest Int)+ it "empty identity on commit" $ property $ emptyIdentityCommit (undefined :: TacticTest Int)+ it "failure identity on commit" $ property $ emptyIdentityCommit (undefined :: TacticTest Int) leftAltBind :: forall m a b@@ -166,7 +170,7 @@ interleaveMZero :: forall m a jdg ext err s- . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),+ . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]), Show jdg, Show s, Arbitrary jdg, Arbitrary s) => TacticT jdg ext err s m a -- ^ proxy -> TacticT jdg ext err s m a@@ -176,7 +180,7 @@ interleaveMPlus :: forall m a jdg ext err s- . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),+ . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]), Show jdg, Show s, Arbitrary jdg, Arbitrary s) => TacticT jdg ext err s m a -- ^ proxy -> a@@ -207,3 +211,34 @@ counterexample (show m2) $ (put s >> (m1 <|> m2)) =-= ((put s >> m1) <|> (put s >> m2)) +absorptionPureCommit+ :: forall m a jdg ext err s+ . (MonadExtract ext m, EqProp (m [Either err (ext, s, [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+ -> Property+absorptionPureCommit _ a t =+ (commit (pure a) t) =-= pure a++emptyIdentityCommit+ :: forall m a jdg ext err s+ . (MonadExtract ext m, EqProp (m [Either err (ext, s, [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+emptyIdentityCommit _ t =+ (commit empty t) =-= t++failureIdentityCommit+ :: forall m a jdg ext err s+ . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]),+ Show jdg, Show s, Arbitrary jdg, Arbitrary s)+ => TacticT jdg ext err s m a -- ^ proxy+ -> err+ -> TacticT jdg ext err s m a+ -> Property+failureIdentityCommit _ e t =+ (commit (throwError e) t) =-= t