refinery (empty) → 0.1.0.0

raw patch · 9 files changed

+492/−0 lines, 9 filesdep +basedep +containersdep +exceptionssetup-changed

Dependencies added: base, containers, exceptions, mmorph, mtl, pipes, refinery, semigroupoids

Files

ChangeLog.md +3/−0
LICENSE +29/−0
README.md +8/−0
Setup.hs +2/−0
refinery.cabal +66/−0
src/Refinery/ProofState.hs +72/−0
src/Refinery/Tactic.hs +146/−0
src/Refinery/Tactic/Internal.hs +164/−0
test/Spec.hs +2/−0

+ ChangeLog.md view

@@ -0,0 +1,3 @@+# Changelog for refinery++## Unreleased changes

+ LICENSE view

@@ -0,0 +1,29 @@+BSD 3-Clause License++Copyright (c) 2018, Reed Mullanix+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++* Redistributions of source code must retain the above copyright notice, this+  list of conditions and the following disclaimer.++* Redistributions in binary form must reproduce the above copyright notice,+  this list of conditions and the following disclaimer in the documentation+  and/or other materials provided with the distribution.++* Neither the name of the copyright holder nor the names of its+  contributors may be used to endorse or promote products derived from+  this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,8 @@+# refinery++`refinery` is a toolkit for building proof refinement/proof automation systems, based roughly on the [+Algebraic Foundations of Proof Refinement](https://arxiv.org/abs/1703.05215).++## Overview+The main datatype of the library is `TacticT goal extract m a`, which is a monad transformer that behaves as a tactic.+When creating your domain-specific tactics, you should use `RuleT` and `rule` to implement them.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ refinery.cabal view

@@ -0,0 +1,66 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.1.+--+-- see: https://github.com/sol/hpack+--+-- hash: f61ff60d97eac2723f257e2cb25ede1205a5cb260049a1708c66c7ab0d4669f8++name:           refinery+version:        0.1.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+homepage:       https://github.com/totbwf/refinery#readme+bug-reports:    https://github.com/totbwf/refinery/issues+author:         Reed Mullanix+maintainer:     reedmullanix@gmail.com+copyright:      2019 Reed Mullanix+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/totbwf/refinery++library+  exposed-modules:+      Refinery.ProofState+      Refinery.Tactic+      Refinery.Tactic.Internal+  other-modules:+      Paths_refinery+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , containers >=0.5+    , exceptions >=0.10+    , 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:+      Paths_refinery+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , containers >=0.5+    , exceptions >=0.10+    , mmorph >=1+    , mtl >=2+    , pipes >=4+    , refinery+    , semigroupoids >=5+  default-language: Haskell2010

+ src/Refinery/ProofState.hs view

@@ -0,0 +1,72 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Refinery.ProofState+-- Copyright   :  (c) Reed Mullanix 2019+-- License     :  BSD-style+-- Maintainer  :  reedmullanix@gmail.com+--+--+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 Pipes.Core++newtype ProofStateT ext m jdg = ProofStateT { unProofStateT :: Client jdg ext m ext }++instance (Monad m) => Functor (ProofStateT ext m) where+  fmap f (ProofStateT p) = ProofStateT $ (request . f) >\\ p++instance (Monad m) => Applicative (ProofStateT ext m) where+  pure a = ProofStateT $ request a+  (ProofStateT pf) <*> (ProofStateT pa) = ProofStateT $ (\f -> (request . f) >\\ pa) >\\ pf++instance (Monad m) => Monad (ProofStateT ext m) where+  return = pure+  (ProofStateT p) >>= k = ProofStateT $ (unProofStateT . k) >\\ p++instance MonadTrans (ProofStateT ext) where+  lift m = ProofStateT $ request =<< (lift m)++instance (MonadIO m) => MonadIO (ProofStateT ext m) where+  liftIO m = ProofStateT $ request =<< (liftIO m)++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 (MonadThrow m) => MonadThrow (ProofStateT ext m) where+  throwM e = ProofStateT $ lift $ throwM e++instance (MonadCatch m) => MonadCatch (ProofStateT ext m) where+  catch (ProofStateT m) h = ProofStateT $ catch m (unProofStateT . h)++instance (MonadReader env m) => MonadReader env (ProofStateT ext m) where+  ask = lift ask+  local f (ProofStateT m) = ProofStateT $ local f m++instance (MonadState s m) => MonadState s (ProofStateT ext m) where+  get = lift get+  put = lift . put++axiom :: (Monad m) => ext -> ProofStateT ext m jdg+axiom e = ProofStateT $ return e++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))

+ src/Refinery/Tactic.hs view

@@ -0,0 +1,146 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Refinery.Tactic+-- Copyright   :  (c) Reed Mullanix 2019+-- License     :  BSD-style+-- Maintainer  :  reedmullanix@gmail.com+module Refinery.Tactic+  ( TacticT+  , runTacticT+  -- * Tactic Combinators+  , (<@>)+  , try+  , many_+  , choice+  , progress+  -- * 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 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++-- | 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 ()++-- | Runs a tactic repeatedly until it fails+many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()+many_ t = try (t >> many_ t)++-- | Get the current goal+goal :: (Monad m) => TacticT jdg ext 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++-- | @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 = 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)+++-- | 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)

+ src/Refinery/Tactic/Internal.hs view

@@ -0,0 +1,164 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE TypeFamilies #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Refinery.Tactic.Internal+-- Copyright   :  (c) Reed Mullanix 2019+-- License     :  BSD-style+-- Maintainer  :  reedmullanix@gmail.com+--+--+-- = WARNING+-- This module is considered __internal__, and can+-- change at any given time.+module Refinery.Tactic.Internal+  ( TacticT(..)+  , mapTacticT+  , stateful+  , asRule+  , MonadRule(..)+  , RuleT(..)+  , mapRuleT+  , MonadProvable(..)+  , ProvableT(..)+  , Provable+  , runProvable+  )+where++import Data.Functor.Alt+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.Morph++import Data.Bifunctor++import Pipes.Core+import Pipes.Lift (evalStateP, runStateP)++import Refinery.ProofState++-- | A @'TacticT'@ is a monad transformer that performs proof refinement.+-- The type variables signifiy:+--+-- * @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 }+  deriving ( Functor+           , MonadReader env+           , MonadError err+           , MonadIO+           , MonadThrow+           , MonadCatch+           )++instance (MonadProvable jdg m) => Applicative (TacticT jdg ext m) where+  pure a = TacticT $ StateT $ proving >=> \j -> pure (a, j)+  (<*>) = ap++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'++-- | 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 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+  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++-- | 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)++-- | 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++-- | 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+           )+++-- | 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)++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 (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

+ test/Spec.hs view

@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"