diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,10 +1,45 @@ # Changelog for refinery - -* 0.1.0.0 - Initial Release of the library +* 0.4.0.0 + - How failure is handled has been refined somewhat. Previously, if a + tactic failed, then the extraction process was terminated, and + `proofs` would return a `Left` describing the error. This design + worked, but led to some suboptimal error reporting. To fix this, + the `Failure` constructor from `ProofStateT` has been changed from + ``` + | Failure err + ``` + to + ``` + | Failure err (ext' -> ProofStateT ext' ext err s m goal) + ``` -## Unreleased changes + This allows us the option to continue the extraction process even + in the face of failure. This option is exercised in `partialProofs` + and `runPartialTacticT`. + - A bunch of helpful combinators have been added for extract + manipulation inside of tactics. + - `proofs` no longer returns a tuple, but rather a record type + ``` + data Proof s meta goal ext = Proof { pf_extract :: ext, pf_state :: s, pf_unsolvedGoals :: [(meta, goal)] } + ``` + - Added `handler`, and removed the `MonadError` instance for `TacticT`. + Now, instead of recovering from errors (which was fraught with subtle issues), + we allow the user to annotate errors instead. + - Added some useful tactic combinators: + - tweak + - peek + - poke + - inspect + - some_ + - Swapped the order of arguments to `mapExtract` to line up with `Profunctor` + - Reworked `MonadExtract` to support named holes. + - Added `reify` and `resume` combinators, which are used for inspecting the current proof state during tactic execution. +* 0.3.0.0 + - Reworked the core types of the library, which fixed a lot of the weird behavior + that users were experiencing. * 0.2.0.0 - Added Alternative/MonadPlus instances to ProofStateT, TacticT, RuleT + - Added Alternative/MonadPlus instances to ProofStateT, TacticT, RuleT +* 0.1.0.0 + - Initial Release of the library diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,8 +1,187 @@ -# refinery +# 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). +[![Hackage](http://img.shields.io/hackage/v/refinery.svg)](https://hackage.haskell.org/package/refinery) -## 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. +`refinery` provides a series of language-independent building blocks for creating automated, type directed program synthesis tools. +It is currently used to power the automatic code synthesis tool [Wingman For Haskell](https://haskellwingman.dev/). + +## Introduction +If you are already familiar with the idea of tactics, feel free to skip ahead to the [Usage](#Usage) section. + +What exactly do we do when we sit down and write a program? Sure, we may have lofty ideas about +what it may do in the end, but I'm talking about the actual process of writing a program. +For instance, take the following (rather silly) example: +```haskell +pairing :: (a -> b) -> (a -> c) -> a -> (b,c) +pairing = _ +``` + +The first thing we might do is look at the type, see that we are writing a function, and introduce the arguments. +```haskell +pairing :: (a -> b) -> (a -> c) -> a -> (b,c) +pairing f g a = _ +``` + +Then, we see that we are trying to make a pair type, so we will introduce a pair constructor. +```haskell +pairing :: (a -> b) -> (a -> c) -> a -> (b,c) +pairing f g a = (_, _) +``` +Then, we will see that we need to produce a `b` and a `c`, and we have two functions in scope that do that, so may as well +try them! +```haskell +pairing :: (a -> b) -> (a -> c) -> a -> (b,c) +pairing f g a = (f _, g _) +``` +Now, we need an `a`, and we have one in scope, so let's use that! +```haskell +pairing :: (a -> b) -> (a -> c) -> a -> (b,c) +pairing f g a = (f a, g a) +``` + +Now, this entire process of writing this function was entirely mechanical. We just looked at the type of the hole, +looked at what we had in scope, and applied some simple edits to get some more holes, and repeated. This feels +like we could automate this! + +Now, a "tactic" is exactly this. We can think of it morally as something like the following type: `(Type -> [Type], [Expr -> Expr])`. +In short, they break the hole down into a bunch of smaller holes, and combine expressions that fit into those holes into one big expression! +This library provides the means for creating simple tactics for _any_ language you can cook up, as well as "tactic combinators", which have +a similar flavor to parser combinators. Parser combinators let us compose small atomic parsers together to form larger ones, and Tactic +combinators let us compose together small tactics to create sophisticated tools for automatic program synthesis. + +## Usage +Let's walk through the usage of this library with a small example. The full source code of this example can be found in `tests/Spec/STLC.hs`. + +First, let's import the main module, along with some MTL stuff: +``` +import Data.List + +import Control.Monad.Identity +import Control.Monad.State + +import Refinery.Tactic +``` + + +Now let's define a teeny tiny simply typed lambda calculus: +```haskell +-- Expressions in simply typed lambda calculus, along with holes +data Term + = Var String + | Hole + | Lam String Term + | Pair Term Term + deriving (Show, Eq) + +-- Types in our version of simply typed lambda calculus +data Type + = TVar String + | Type :-> Type + | TPair Type Type + deriving (Show, Eq) +``` + +Now, we are going to need to define the idea of a "type in a context", commonly referred to as a "Judgement". +```haskell +newtype Judgement = [(String, Type)] :- Type + deriving (Show) +``` + +Now, a bit of boilerplate is required to tell `refinery` how to generate holes. +Most of the time, you will need to have a fresh source of variables for your holes, or you +may need to run effects when you generate them. However, in the name of simplicity, let's just use +`Identity` +```haskell +instance MonadExtract Term String Identity where + hole = pure Hole + unsolvableHole _ = pure Hole +``` + +Now for our first tactic: +```haskell +type T a = TacticT Judgement Term String Int Identity a + +-- Tactic for solving holes of type (a,b) +pair :: T () +pair = rule $ \goal -> + case goal of + (hys :- TPair a b) -> Pair <$> subgoal (hys :- a) <*> subgoal (hys :- b) + _ -> unsolvable "goal mismatch: Pair" +``` + +Now, there is a _lot_ going on here, so let's take it apart piece by piece: +To start, let's look at `TacticT`. The first type parameter is the "goal" type. +We can think of this as the thing that we are trying to "solve". For us, this +is `Judgement`, as we are going to need to know exactly what is in scope at a given point. + +The next type parameter is what the tactic is going to synthesize, commonly referred to as the +"extract". + +The next three type parameters are decidedly less exciting. They represent the type of errors, the +type of the state, and the base monad. We need to have a way of generating unique names, so let's +just use `Int` as our state to accomplish this. + + +That final type parameter is the type that the tactic during the course of execution. We will discuss this further in the future, +so if you are confused, feel free to ignore this type parameter for now. + +Next, we call `rule` to create a "basic" tactic, that lets us inspect the current goal, and create a bunch of subgoals via `subgoal`. +As we are trying to tell `refinery` how to synthesize pairs, we case on the type of the hole. If it is a pair type, we create two +new goals, one for each component of the tuple type, and then combine the solutions to those subgoals together with a pair constructor. +If the type does not match, then we throw an error via `unsolvable`. + + +Now, finally, we need a way of solving goals of the form `a -> b`. +``` +lam :: T () +lam = rule $ \case + (hys :- (a :-> b)) -> do + name <- gets show + modify (+ 1) + body <- subgoal $ ((name, a) : hys) :- b + pure $ Lam name body + _ -> unsolvable "goal mismatch: Lam" +``` +This is where the state comes in. We look up the current state, show it for use as a name, +and then increment it so that our names are unique. We then create a subgoal for `b`, +and add our new fresh name into scope, specifying that it has type `a`. +We then get the result of the subgoal and put it in a `Lam` constructor along with our fresh name. + +Finally, let's define a tactic for solving a goal by using something in scope. +```haskell +assumption :: T () +assumption = rule $ \ (hys :- a) -> + case find (\(_, ty) -> ty == a) hys of + Just (x, _) -> pure $ Var x + Nothing -> unsolvable "goal mismatch: Assumption" +``` + +Now, for something really exciting. Let's write a tactic that can synthesize expressions for this language. Now that we have our building blocks, this +is very easy! +```haskell +auto :: T () +auto = do + many_ lam + (pair >> auto) <|> assumption +``` +Before explaining how exactly this _works_, let's look at what it does! +```haskell +λ> solutions auto ([] :- (TVar "a" :-> TVar "b" :-> (TPair (TVar "a") (TVar "b")))) 0 +> [Lam "0" (Lam "1" (Pair (Var "0") (Var "1")))] +``` + +As we can see, it generated the right thing! Let's now step through _how_ exactly it did this. +To start, `many_` is a "tactic combinator". It takes a tactic as it's first argument, and +will run it repeatedly until it fails. This will result in a single subgoal that looks something like +```haskell +[("0", TVar "a"), ("1", TVar "b")] :- (TPair (TVar "a") (TVar "b")) +``` + +Now, for the magic. The bind for `TacticT` will run the second tactic on _every_ subgoal created by the first. +With this crucial piece of information, we can begin to see how `auto` works. Once `many_ lam` is executed, +we execute both `pair >> auto` and `assumption` against the subgoal generated, and collect all of the +solutions found by both branches together. `pair` will generate 2 subgoals, and then `>> auto` will apply +`auto` recursively to _both_ of those subgoals. + +## References +`refinery` is based roughly on [Algebraic Foundations of Proof Refinement](https://arxiv.org/abs/1703.05215) diff --git a/refinery.cabal b/refinery.cabal --- a/refinery.cabal +++ b/refinery.cabal @@ -1,13 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0. +-- This file has been generated from package.yaml by hpack version 0.34.3. -- -- see: https://github.com/sol/hpack --- --- hash: c5e5c657da3ec1e29d787f8c9eb17e054b2e5ad3a9e6420df6680e4cb31ca981 name: refinery -version: 0.3.0.0 +version: 0.4.0.0 synopsis: Toolkit for building proof automation systems description: Please see the README on GitHub at category: Language @@ -19,6 +17,10 @@ license: BSD3 license-file: LICENSE build-type: Simple +tested-with: + GHC ==8.6.5 + , GHC ==8.8.3 + , GHC ==8.10.4 extra-source-files: README.md ChangeLog.md @@ -40,7 +42,6 @@ build-depends: base >=4.7 && <5 , exceptions >=0.10 - , logict >=0.6 , mmorph >=1 , mtl >=2 default-language: Haskell2010 @@ -50,6 +51,8 @@ main-is: Spec.hs other-modules: Checkers + Spec.PropertyTests + Spec.STLC Paths_refinery hs-source-dirs: test @@ -60,7 +63,6 @@ , checkers , exceptions >=0.10 , hspec - , logict >=0.6 , mmorph >=1 , mtl >=2 , refinery diff --git a/src/Refinery/ProofState.hs b/src/Refinery/ProofState.hs --- a/src/Refinery/ProofState.hs +++ b/src/Refinery/ProofState.hs @@ -1,21 +1,25 @@ -{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} -{-# LANGUAGE TupleSections #-} {-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} ----------------------------------------------------------------------------- --- | +-- | The datatype that drives both Rules and Tactics +-- +-- If you just want to build tactics, you probably want to use 'Refinery.Tactic' instead. +-- However, if you need to get involved in the core of the library, this is the place to start. +-- -- Module : Refinery.ProofState -- Copyright : (c) Reed Mullanix 2019 -- License : BSD-style @@ -23,7 +27,21 @@ -- -- module Refinery.ProofState -where + ( ProofStateT(..) + -- * Proofstate Execution + , MonadExtract(..) + , Proof(..) + , PartialProof(..) + , proofs + , partialProofs + , subgoals + -- * Extract Manipulation + , mapExtract + -- * Speculative Execution + , MetaSubst(..) + , DependentMetaSubst(..) + , speculate + ) where import Control.Applicative import Control.Monad @@ -32,24 +50,50 @@ 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 Data.Either +import Data.Tuple (swap) import GHC.Generics +-- | The core data type of the library. +-- This represents a reified, in-progress proof strategy for a particular goal. +-- +-- NOTE: We need to split up the extract type into @ext'@ and @ext@, as +-- we want to be functorial (and monadic) in @ext@, but it shows up in both +-- co and contravariant positions. Splitting the type variable up into two solves this problem, +-- at the cost of looking ugly. data ProofStateT ext' ext err s m goal = Subgoal goal (ext' -> ProofStateT ext' ext err s m goal) + -- ^ Represents a subgoal, and a continuation that tells + -- us what to do with the resulting extract. | Effect (m (ProofStateT ext' ext err s m goal)) + -- ^ Run an effect. | Stateful (s -> (s, ProofStateT ext' ext err s m goal)) + -- ^ Run a stateful computation. We don't want to use 'StateT' here, as it + -- doesn't play nice with backtracking. | Alt (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal) + -- ^ Combine together the results of two @ProofState@s, preserving the order that they were synthesized in. | Interleave (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal) + -- ^ Similar to 'Alt', but will interleave the results, rather than just appending them. + -- This is useful if the first argument produces potentially infinite results. | Commit (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal) + -- ^ 'Commit' runs the first proofstate, and only runs the second if the first + -- does not produce any successful results. | Empty - | Failure err + -- ^ Silent failure. Always causes a backtrack, unlike 'Failure'. + | Failure err (ext' -> ProofStateT ext' ext err s m goal) + -- ^ This does double duty, depending on whether or not the user calls 'proofs' + -- or 'partialProofs'. In the first case, we ignore the continutation, backtrack, and + -- return an error in the result of 'proofs'. + -- In the second, we treat this as a sort of "unsolvable subgoal", and call the + -- continuation with a hole. + | Handle (ProofStateT ext' ext err s m goal) (err -> m err) + -- ^ An installed error handler. These allow us to add annotations to errors, + -- or run effects. | Axiom ext - deriving stock (Generic) + -- ^ Represents a simple extract. + deriving stock (Generic, Functor) 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 <> " )" @@ -59,20 +103,10 @@ 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 (Failure err _) = "(Failure " <> show err <> " )" + show (Handle p _) = "(Handle " <> show p <> " )" show (Axiom ext) = "(Axiom " <> show ext <> ")" -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 f (Commit p1 p2) = Commit (fmap f p1) (fmap f p2) - fmap _ Empty = Empty - fmap _ (Failure err) = Failure err - fmap _ (Axiom ext) = Axiom ext - instance Functor m => Applicative (ProofStateT ext ext err s m) where pure = return (<*>) = ap @@ -84,10 +118,13 @@ 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 nat (Failure err k) = Failure err $ fmap (hoist nat) k + hoist nat (Handle p h) = Handle (hoist nat p) (nat . h) hoist _ Empty = Empty hoist _ (Axiom ext) = Axiom ext +-- | Apply a continuation that creates new proof states from an extract +-- onto all of the 'Axiom' constructors of a 'ProofStateT'. applyCont :: (Functor m) => (ext -> ProofStateT ext' ext err s m a) @@ -100,20 +137,22 @@ 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 (Failure err k') = Failure err (applyCont k . k') +applyCont k (Handle p h) = Handle (applyCont k p) h applyCont k (Axiom ext) = k ext 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) - (Commit p1 p2) >>= f = Commit (p1 >>= f) (p2 >>= f) - (Failure err) >>= _ = Failure err - Empty >>= _ = Empty - (Axiom ext) >>= _ = Axiom ext + (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) + (Commit p1 p2) >>= f = Commit (p1 >>= f) (p2 >>= f) + (Failure err k) >>= f = Failure err (f <=< k) + (Handle p h) >>= f = Handle (p >>= f) h + Empty >>= _ = Empty + (Axiom ext) >>= _ = Axiom ext instance MonadTrans (ProofStateT ext ext err s) where lift m = Effect (fmap pure m) @@ -126,93 +165,165 @@ mzero = empty mplus = (<|>) -class (Monad m) => MonadExtract ext m | m -> ext where - -- | Generates a "hole" of type @ext@, which should represent +-- | 'MonadExtract' describes the effects required to generate named holes. +-- The @meta@ type parameter here is a so called "metavariable", which can be thought of as +-- a name for a hole. +class (Monad m) => MonadExtract meta ext err s m | m -> ext, m -> err, ext -> meta where + -- | Generates a named "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 + hole :: StateT s m (meta, ext) + default hole :: (MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => StateT s m (meta, ext) + hole = mapStateT lift hole -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) + -- | Generates an "unsolvable hole" of type @err@, which should represent + -- an incomplete extract that we have no hope of solving. + -- + -- These will get generated when you generate partial extracts via 'Refinery.Tactic.runPartialTacticT'. + unsolvableHole :: err -> StateT s m (meta, ext) + default unsolvableHole :: (MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => err -> StateT s m (meta, ext) + unsolvableHole = mapStateT lift . unsolvableHole -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 + +newHole :: MonadExtract meta ext err s m => s -> m (s, (meta, ext)) +newHole = fmap swap . runStateT hole + +newUnsolvableHole :: MonadExtract meta ext err s m => s -> err -> m (s, (meta, ext)) +newUnsolvableHole s err = fmap swap $ runStateT (unsolvableHole err) s + + +instance (MonadExtract meta ext err s m) => MonadExtract meta ext err s (ReaderT r m) +instance (MonadExtract meta ext err s m) => MonadExtract meta ext err s (StateT s m) +instance (MonadExtract meta ext err s m, Monoid w) => MonadExtract meta ext err s (LW.WriterT w m) +instance (MonadExtract meta ext err s m, Monoid w) => MonadExtract meta ext err s (SW.WriterT w m) +instance (MonadExtract meta ext err s m) => MonadExtract meta ext err s (ExceptT err m) + +-- | Represents a single result of the execution of some tactic. +data Proof s meta goal ext = Proof + { pf_extract :: ext + -- ^ The extract of the tactic. + , pf_state :: s + -- ^ The state at the end of tactic execution. + , pf_unsolvedGoals :: [(meta, goal)] + -- ^ All the goals that were still unsolved by the end of tactic execution. + } + deriving (Eq, Show, Generic) + +-- | Interleave two lists together. +-- @ +-- interleave [1,2,3,4] [5,6] +-- @ +-- > [1,5,2,6,3,4] +interleave :: [a] -> [a] -> [a] +interleave (x : xs) (y : ys) = x : y : (interleave xs ys) +interleave xs [] = xs +interleave [] ys = ys + +-- | Helper function for combining together two results from either 'proofs' or 'partialProofs'. +-- @prioritizing f as bs@ will use @f@ to combine together either two lists of failures or two lists of successes. +-- If we have one list of successes and one list of failures, we always take the successes. +-- +-- The logic behind this is that if either 'Alt' or 'Interleave' have successes, then the failures aren't particularly interesting. +prioritizing :: (forall a. [a] -> [a] -> [a]) + -> Either [b] [c] + -> Either [b] [c] + -> Either [b] [c] +prioritizing combine (Left a1) (Left a2) = Left $ a1 `combine` a2 +prioritizing _ (Left _) (Right b2) = Right b2 +prioritizing _ (Right b1) (Left _) = Right b1 +prioritizing combine (Right b1) (Right b2) = Right $ b1 `combine` b2 + +-- | Interpret a 'ProofStateT' into a list of (possibly incomplete) extracts. +-- This function will cause a proof to terminate when it encounters a 'Failure', and will return a 'Left'. +-- If you want to still recieve an extract even when you encounter a failure, you should use 'partialProofs'. +proofs :: forall ext err s m goal meta. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m goal -> m (Either [err] [(Proof s meta goal ext)]) +proofs s p = go s [] pure 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) = + go :: s -> [(meta, goal)] -> (err -> m err) -> ProofStateT ext ext err s m goal -> m (Either [err] [Proof s meta goal ext]) + go s goals _ (Subgoal goal k) = do + (s', (meta, h)) <- newHole s + -- Note [Handler Reset]: + -- We reset the handler stack to avoid the handlers leaking across subgoals. + -- This would happen when we had a handler that wasn't followed by an error call. + -- pair >> goal >>= \g -> (handler_ $ \_ -> traceM $ "Handling " <> show g) <|> failure "Error" + -- We would see the "Handling a" message when solving for b. + (go s' (goals ++ [(meta, goal)]) pure $ k h) + go s goals handlers (Effect m) = m >>= go s goals handlers + go s goals handlers (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 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 s goals (Axiom ext) = pure [Right (ext, s, goals)] + in go s' goals handlers p + go s goals handlers (Alt p1 p2) = + liftA2 (prioritizing (<>)) (go s goals handlers p1) (go s goals handlers p2) + go s goals handlers (Interleave p1 p2) = + liftA2 (prioritizing interleave) (go s goals handlers p1) (go s goals handlers p2) + go s goals handlers (Commit p1 p2) = go s goals handlers p1 >>= \case + Right solns | not (null solns) -> pure $ Right solns + solns -> (prioritizing (<>) solns) <$> go s goals handlers p2 + go _ _ _ Empty = pure $ Left [] + go _ _ handlers (Failure err _) = do + annErr <- handlers err + pure $ Left [annErr] + go s goals handlers (Handle p h) = + -- Note [Handler ordering]: + -- If we have multiple handlers in scope, then we want the handlers closer to the error site to + -- run /first/. This allows the handlers up the stack to add their annotations on top of the + -- ones lower down, which is the behavior that we desire. + -- IE: for @handler f >> handler g >> failure err@, @g@ ought to be run before @f@. + go s goals (h >=> handlers) p + go s goals _ (Axiom ext) = pure $ Right $ [Proof 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) -accumEither (Right b1) (Right b2) = Right (b1 <> b2) -accumEither Left{} x = x -accumEither x Left{} = x +-- | The result of executing 'partialProofs'. +data PartialProof s err meta goal ext + = PartialProof ext s [(meta, goal)] [(meta, err)] + -- ^ A so called "partial proof". These are proofs that encountered errors + -- during execution. + deriving (Eq, Show, Generic) +-- | Interpret a 'ProofStateT' into a list of (possibly incomplete) extracts. +-- This function will continue producing an extract when it encounters a 'Failure', leaving +-- a hole in the extract in it's place. If you want the extraction to terminate when you encounter an error, +-- you should use 'proofs'. +partialProofs :: forall meta ext err s m goal. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m goal -> m (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]) +partialProofs s pf = go s [] [] pure pf + where + go :: s -> [(meta, goal)] -> [(meta, err)] -> (err -> m err) -> ProofStateT ext ext err s m goal -> m (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]) + go s goals errs _ (Subgoal goal k) = do + (s', (meta, h)) <- newHole s + -- See Note [Handler Reset] + go s' (goals ++ [(meta, goal)]) errs pure $ k h + go s goals errs handlers (Effect m) = m >>= go s goals errs handlers + go s goals errs handlers (Stateful f) = + let (s', p) = f s + in go s' goals errs handlers p + go s goals errs handlers (Alt p1 p2) = liftA2 (prioritizing (<>)) (go s goals errs handlers p1) (go s goals errs handlers p2) + go s goals errs handlers (Interleave p1 p2) = liftA2 (prioritizing interleave) (go s goals errs handlers p1) (go s goals errs handlers p2) + go s goals errs handlers (Commit p1 p2) = go s goals errs handlers p1 >>= \case + Right solns | not (null solns) -> pure $ Right solns + solns -> (prioritizing (<>) solns) <$> go s goals errs handlers p2 + go _ _ _ _ Empty = pure $ Left [] + go s goals errs handlers (Failure err k) = do + annErr <- handlers err + (s', (meta, h)) <- newUnsolvableHole s annErr + go s' goals (errs ++ [(meta, annErr)]) handlers $ k h + go s goals errs handlers (Handle p h) = + -- See Note [Handler ordering] + go s goals errs (h >=> handlers) p + go s goals [] _ (Axiom ext) = pure $ Right [Proof ext s goals] + go s goals errs _ (Axiom ext) = pure $ Left [PartialProof ext s goals errs] + 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 (Commit p1 p2) handle = Commit (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 = 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) - -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 f (Commit p1 p2) = Commit (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 fs p@ will apply a list of functions producing a new 'ProofStateT' to each of the subgoals of @p@ in order. +-- If the list of functions is longer than the number of subgoals, then the extra functions are ignored. +-- If the list of functions is shorter, then we simply apply @pure@ to all of the remaining subgoals. 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) @@ -221,30 +332,74 @@ 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 fs (Failure err k) = Failure err (subgoals fs . k) +subgoals fs (Handle p h) = Handle (subgoals fs p) h 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) - Commit t1 t2 -> Commit (mapExtract into out t1) (mapExtract into out t2) - Empty -> Empty - Failure err -> Failure err - Axiom ext -> Axiom $ into ext +-- | @mapExtract f g p@ allows yout to modify the extract type of a ProofState. +-- This witness the @Profunctor@ instance of 'ProofStateT', which we can't write without a newtype due to +-- the position of the type variables +mapExtract :: (Functor m) => (a -> ext') -> (ext -> b) -> ProofStateT ext' ext err s m jdg -> ProofStateT a b err s m jdg +mapExtract into out (Subgoal goal k) = Subgoal goal (mapExtract into out . k . into) +mapExtract into out (Effect m) = Effect (fmap (mapExtract into out) m) +mapExtract into out (Stateful s) = Stateful (fmap (mapExtract into out) . s) +mapExtract into out (Alt p1 p2) = Alt (mapExtract into out p1) (mapExtract into out p2) +mapExtract into out (Interleave p1 p2) = Interleave (mapExtract into out p1) (mapExtract into out p2) +mapExtract into out (Commit p1 p2) = Commit (mapExtract into out p1) (mapExtract into out p2) +mapExtract _ _ Empty = Empty +mapExtract into out (Failure err k) = Failure err (mapExtract into out . k . into) +mapExtract into out (Handle p h) = Handle (mapExtract into out p) h +mapExtract _ out (Axiom ext) = Axiom (out 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) - Commit t1 t2 -> Commit (mapExtract' into t1) (mapExtract' into t2) - Empty -> Empty - Failure err -> Failure err - Axiom ext -> Axiom $ into ext +-- | 'MetaSubst' captures the notion of substituting metavariables of type @meta@ into an extract of type @ext@. +-- Note that these substitutions should most likely _not_ be capture avoiding. +class MetaSubst meta ext | ext -> meta where + -- | @substMeta meta e1 e2@ will substitute all occurances of @meta@ in @e2@ with @e1@. + substMeta :: meta -> ext -> ext -> ext + +-- | 'DependentMetaSubst' captures the notion of substituting metavariables of type @meta@ into judgements of type @jdg@. +-- This really only matters when you are dealing with dependent types, specifically existentials. +-- For instance, consider the goal +-- Σ (x : A) (B x) +-- The type of the second goal we would produce here _depends_ on the solution to the first goal, +-- so we need to know how to substitute holes in judgements in order to properly implement 'Refinery.Tactic.resume'. +class MetaSubst meta ext => DependentMetaSubst meta jdg ext where + -- | @dependentSubst meta e j@ will substitute all occurances of @meta@ in @j@ with @e@. + -- This method only really makes sense if you have goals that depend on earlier extracts. + -- If this isn't the case, don't implement this. + dependentSubst :: meta -> ext -> jdg -> jdg + +-- | @speculate s p@ will record the current state of the proof as part of the extraction process. +-- In doing so, this will also remove any subgoal constructors by filling them with holes. +speculate :: forall meta ext err s m jdg x. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m jdg -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x +speculate s = go s [] pure + where + go :: s -> [(meta, jdg)] -> (err -> m err) -> ProofStateT ext ext err s m jdg -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x + go s goals _ (Subgoal goal k) = Effect $ do + (s', (meta, h)) <- newHole s + -- See Note [Handler Reset] + pure $ go s' (goals ++ [(meta, goal)]) pure (k h) + go s goals handler (Effect m) = Effect (fmap (go s goals handler) m) + go s goals handler (Stateful st) = + let (s', p) = st s + in go s' goals handler p + go s goals handler (Alt p1 p2) = Alt (go s goals handler p1) (go s goals handler p2) + go s goals handler (Interleave p1 p2) = Interleave (go s goals handler p1) (go s goals handler p2) + go s goals handler (Commit p1 p2) = Commit (go s goals handler p1) (go s goals handler p2) + go _ _ _ Empty = Empty + go _ _ handler (Failure err _) = Effect $ do + annErr <- handler err + pure $ Axiom $ Left annErr + go s goals handler (Handle p h) = + -- Note [Speculation + Handler]: + -- When speculating, we want to _keep_ any handlers in place, as well as using them to annotate any errors. + -- For instance, consider: + -- reify (handler_ h >> failure "Error 1") $ \_ -> failure "Error 2" + -- + -- We want the handler installed as a part of the reify to be executed when the failure happens + -- in the tactic we are reifing, _and_ also when the subsequent failure happens. + -- + -- See Note [Handler Ordering] as well for more details on the @h >=> handler@ bit. + Handle (go s goals (h >=> handler) p) h + go s goals _ (Axiom ext) = Axiom $ Right (Proof ext s goals) diff --git a/src/Refinery/Tactic.hs b/src/Refinery/Tactic.hs --- a/src/Refinery/Tactic.hs +++ b/src/Refinery/Tactic.hs @@ -1,16 +1,19 @@ -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- --- | +-- | Tactics and Tactic Combinators +-- +-- This module contains everything you need to start defining tactics +-- and tactic combinators. -- Module : Refinery.Tactic -- Copyright : (c) Reed Mullanix 2019 -- License : BSD-style @@ -18,31 +21,53 @@ module Refinery.Tactic ( TacticT , runTacticT + , runPartialTacticT + , evalTacticT + , Proof(..) + , PartialProof(..) -- * Tactic Combinators , (<@>) , (<%>) - , commit , try + , commit , many_ + , some_ , choice , progress - , gather - , pruning , ensure + -- * Errors and Error Handling + , failure + , handler + , handler_ + -- * Extract Manipulation + , tweak -- * Subgoal Manipulation , goal + , inspect , focus -- * Tactic Creation , MonadExtract(..) - , MonadRule(..) , RuleT , rule + , rule_ + , subgoal + , unsolvable + -- * Introspection + , MetaSubst(..) + , DependentMetaSubst(..) + , reify + , resume + , resume' + , pruning + , peek + , attempt ) where import Control.Applicative -import Control.Monad.Except -import Control.Monad.State.Strict +import Control.Monad.State.Class +import Data.Bifunctor + import Refinery.ProofState import Refinery.Tactic.Internal @@ -62,28 +87,71 @@ (<%>) :: 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 () try t = t <|> pure () --- | Runs a tactic repeatedly until it fails +-- | @commit t1 t2@ will run @t1@, and then run @t2@ only if @t1@ (and all subsequent tactics) failed to produce any successes. +-- +-- NOTE: @commit@ does have some sneaky semantics that you have to be aware of. Specifically, it interacts a bit +-- surprisingly with '>>='. Namely, the following algebraic law holds +-- @ +-- commit t1 t2 >>= f = commit (t1 >>= f) (t2 >>= f) +-- @ +-- For instance, if you have something like @commit t1 t2 >>= somethingThatMayFail@, then this +-- law implies that this is the same as @commit (t1 >>= somethingThatMayFail) (t2 >>= somethingThatMayFail)@, +-- which means that we might execute @t2@ _even if_ @t1@ seemingly succeeds. +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) + +-- | Runs a tactic 0 or more times until it fails. +-- Note that 'many_' is almost always the right choice over 'many'. +-- Due to the semantics of 'Alternative', 'many' will create a bunch +-- of partially solved goals along the way, one for each iteration. many_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m () many_ t = try (t >> many_ t) +-- | Runs a tactic 1 or more times until it fails. +-- Note that 'some_' is almost always the right choice over 'some'. +-- Due to the semantics of 'Alternative', 'some' will create a bunch +-- of partially solved goals along the way, one for each iteration. +some_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m () +some_ t = t >> many_ t + -- | Get the current goal goal :: (Functor m) => TacticT jdg ext err s m jdg -goal = TacticT $ get +goal = TacticT get +-- | Inspect the current goal. +inspect :: (Functor m) => (jdg -> a) -> TacticT jdg ext err s m a +inspect f = TacticT $ gets f + -- | @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 +choice = foldr (<%>) empty +-- | @failure err@ will create an unsolvable hole that will be ignored by subsequent tactics. +failure :: err -> TacticT jdg ext err s m a +failure err = tactic $ \_ -> Failure err Axiom + +-- | @handler f@ will install an "error handler". These let you add more context to errors, and +-- potentially run effects. For instance, you may want to take note that a particular situation is +-- unsolvable, and that we shouldn't attempt to run this series of tactics against a given goal again. +-- +-- Note that handlers further down the stack get run before those higher up the stack. +-- For instance, consider the following example: +-- @ +-- handler f >> handler g >> failure err +-- @ +-- Here, @g@ will get run before @f@. +handler :: (err -> m err) -> TacticT jdg ext err s m () +handler h = tactic $ \j -> Handle (Subgoal ((), j) Axiom) h + +-- | A variant of 'handler' that doesn't modify the error at all, and solely exists to run effects. +handler_ :: (Functor m) => (err -> m ()) -> TacticT jdg ext err s m () +handler_ h = handler (\err -> err <$ h 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@. @@ -92,27 +160,9 @@ j <- goal a <- t j' <- goal - if j `eq` j' then pure a else throwError err - --- | @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 + if j `eq` j' then pure a else failure err --- | @filterT p f t@ runs the tactic @t@, and applies a predicate to the state after the execution of @t@. We also run +-- | @ensure 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 @@ -125,18 +175,97 @@ s <- get modify f case p s of - Just err -> throwError err + Just err -> unsolvable 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 ())) +-- | @tweak f t@ lets us modify the extract produced by the tactic @t@. +tweak :: (Functor m) => (ext -> ext) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m () +tweak f t = tactic $ \j -> mapExtract id f $ proofState t j + -- | 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])] +-- Note that this function will backtrack on errors. If you want a version that provides partial proofs, +-- use 'runPartialTacticT' +runTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m (Either [err] [(Proof s meta jdg ext)]) runTacticT t j s = proofs s $ fmap snd $ proofState t j --- | Turn an inference rule into a tactic. +-- | Run a tactic, and get just the list of extracts, ignoring any other information. +evalTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m [ext] +evalTacticT t j s = either (const []) (map pf_extract) <$> runTacticT t j s + +-- | Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals. +-- Note that this function will produce a so called "Partial Proof". This means that we no longer backtrack on errors, +-- but rather leave an unsolved hole, and continue synthesizing a extract. +-- If you want a version that backgracks on errors, see 'runTacticT'. +-- +-- Note that this version is inherently slower than 'runTacticT', as it needs to continue producing extracts. +runPartialTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m (Either [PartialProof s err meta jdg ext] [(Proof s meta jdg ext)]) +runPartialTacticT t j s = partialProofs s $ fmap snd $ proofState t j + +-- | Turn an inference rule that examines the current goal into a tactic. 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) +-- | Turn an inference rule into a tactic. +rule_ :: (Monad m) => RuleT jdg ext err s m ext -> TacticT jdg ext err s m () +rule_ r = tactic $ \_ -> fmap ((),) $ unRuleT r + +introspect :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m a -> (err -> TacticT jdg ext err s m ()) -> (Proof s meta jdg ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m () +introspect t handle f = rule $ \j -> do + s <- get + (RuleT $ speculate s $ proofState_ t j) >>= \case + Left err -> RuleT $ proofState_ (handle err) j + Right pf -> RuleT $ proofState_ (f pf) j + +-- | @reify t f@ will execute the tactic @t@, and resolve all of it's subgoals by filling them with holes. +-- The resulting subgoals and partial extract are then passed to @f@. +reify :: forall meta jdg ext err s m . (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> (Proof s meta jdg ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m () +reify t f = introspect t failure f + +-- | @resume goals partial@ allows for resumption of execution after a call to 'reify'. +-- If your language doesn't support dependent subgoals, consider using @resume'@ instead. +resume :: forall meta jdg ext err s m. (DependentMetaSubst meta jdg ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m () +resume (Proof partialExt s goals) = rule $ \_ -> do + put s + solns <- dependentSubgoals goals + pure $ foldr (\(meta, soln) ext -> substMeta meta soln ext) partialExt solns + where + dependentSubgoals :: [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)] + dependentSubgoals [] = pure [] + dependentSubgoals ((meta, g) : gs) = do + soln <- subgoal g + solns <- dependentSubgoals $ fmap (second (dependentSubst meta soln)) gs + pure ((meta, soln) : solns) + +-- | A version of @resume@ that doesn't perform substitution into the goal types. +-- This only makes sense if your language doesn't support dependent subgoals. +-- If it does, use @resume@ instead, as this will leave the dependent subgoals with holes in them. +resume' :: forall meta jdg ext err s m. (MetaSubst meta ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m () +resume' (Proof partialExt s goals) = rule $ \_ -> do + put s + solns <- traverse (\(meta, g) -> (meta, ) <$> subgoal g) goals + pure $ foldr (\(meta, soln) ext -> substMeta meta soln ext) partialExt solns + +-- | @pruning t p@ will execute @t@, and then apply @p@ to any subgoals it generates. If this predicate returns an error, we terminate the execution. +-- Otherwise, we resume execution via 'resume''. +pruning :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m () +pruning t p = reify t $ \pf -> case (p $ fmap snd $ pf_unsolvedGoals pf) of + Just err -> failure err + Nothing -> resume' pf + +-- | @peek t p@ will execute @t@, and then apply @p@ to the extract it produces. If this predicate returns an error, we terminate the execution. +-- Otherwise, we resume execution via 'resume''. +-- +-- Note that the extract produced may contain holes, as it is the extract produced by running _just_ @t@ against the current goal. +peek :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> (ext -> Maybe err) -> TacticT jdg ext err s m () +peek t p = reify t $ \pf -> case (p $ pf_extract pf) of + Just err -> failure err + Nothing -> resume' pf + +-- | @attempt t1 t2@ will partially execute @t1@, inspect it's result, and only run @t2@ if it fails. +-- If @t1@ succeeded, we will 'resume'' execution of it. +attempt :: (MonadExtract meta ext err s m, MetaSubst meta ext) => TacticT jdg ext err s m () -> TacticT jdg ext err s m () -> TacticT jdg ext err s m () +attempt t1 t2 = introspect t1 (\_ -> t2) resume' diff --git a/src/Refinery/Tactic/Internal.hs b/src/Refinery/Tactic/Internal.hs --- a/src/Refinery/Tactic/Internal.hs +++ b/src/Refinery/Tactic/Internal.hs @@ -27,9 +27,12 @@ ( TacticT(..) , tactic , proofState + , proofState_ , mapTacticT - , MonadRule(..) + -- * Rules , RuleT(..) + , subgoal + , unsolvable ) where @@ -38,7 +41,6 @@ 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 () @@ -56,18 +58,24 @@ -- * @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 @'()'@ +-- * @a@ - The return value. This to make @'TacticT'@ a monad, and will always be @'Prelude.()'@ +-- +-- One of the most important things about this type is it's 'Monad' instance. @t1 >> t2@ +-- Will execute @t1@ against the current goal, and then execute @t2@ on _all_ of the subgoals generated +-- by @t2@. +-- +-- This Monad instance is lawful, and has been tested thouroughly, and a version of it has been formally verified in Agda. +-- _However_, just because it is correct doesn't mean that it lines up with your intuitions of how Monads behave! +-- In practice, it feels like a combination of the Non-Determinisitic Monads and some of the Time Travelling ones. +-- That doesn't mean that it's impossible to understand, just that it may push the boundaries of you intuitions. 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 ) @@ -78,10 +86,14 @@ 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 t j@ will deconstruct a tactic @t@ into a 'ProofStateT' by running it at @j@. proofState :: TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m (a, jdg) proofState t j = runStateT (unTacticT t) j +-- | Like 'proofState', but we discard the return value of @t@. +proofState_ :: (Functor m) => TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg +proofState_ t j = execStateT (unTacticT t) j + -- | 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 mapTacticT f (TacticT m) = TacticT $ m >>= (lift . lift . f . return) @@ -106,12 +118,16 @@ show = show . unRuleT instance Functor m => Functor (RuleT jdg ext err s m) where - fmap = coerce mapExtract' + fmap f = coerce (mapExtract id f) instance Monad m => Applicative (RuleT jdg ext err s m) where pure = return (<*>) = ap +instance Monad m => Alternative (RuleT jdg ext err s m) where + empty = coerce Empty + (<|>) = coerce Alt + 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 @@ -119,9 +135,10 @@ 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 (Commit p1 p2) >>= f = coerce $ Commit (bindAlaCoerce f p1) (bindAlaCoerce f p2) RuleT Empty >>= _ = coerce $ Empty - RuleT (Failure err) >>= _ = coerce $ Failure err + RuleT (Failure err k) >>= f = coerce $ Failure err $ fmap (bindAlaCoerce f) k + RuleT (Handle p h) >>= f = coerce $ Handle (bindAlaCoerce f p) h RuleT (Axiom e) >>= f = f e instance Monad m => MonadState s (RuleT jdg ext err s m) where @@ -129,28 +146,11 @@ 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 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 - 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 @@ -160,19 +160,11 @@ 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 err s m) where - subgoal j = RuleT $ Subgoal j Axiom +-- | Create a subgoal, and return the resulting extract. +subgoal :: jdg -> RuleT jdg ext err s m ext +subgoal jdg = RuleT $ Subgoal jdg 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) +-- | Create an "unsolvable" hole. These holes are ignored by subsequent tactics, +-- but do not cause a backtracking failure. +unsolvable :: err -> RuleT jdg ext err s m ext +unsolvable err = RuleT $ Failure err Axiom diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,244 +1,11 @@ -{-# 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 Control.Monad.Error.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, s, [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, s, [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, s, [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 +import Spec.PropertyTests +import Spec.STLC main :: IO () 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 ()) - 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 - . (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, 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 -interleaveMZero _ m = - (mzero <%> m) =-= m - -interleaveMPlus - :: 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 - -> 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)) - -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 + propertyTests + stlcTests diff --git a/test/Spec/PropertyTests.hs b/test/Spec/PropertyTests.hs new file mode 100644 --- /dev/null +++ b/test/Spec/PropertyTests.hs @@ -0,0 +1,243 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wredundant-constraints #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Spec.PropertyTests 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 +import Data.Foldable + +testBatch :: TestBatch -> Spec +testBatch (batchName, tests) = describe ("laws for: " ++ batchName) $ + traverse_ (uncurry it) tests + + +instance (EqProp ext, EqProp meta, EqProp s, EqProp jdg) => EqProp (Proof s meta jdg ext) where + +instance (MonadExtract meta ext err s m, EqProp (m (Either [err] [Proof s meta a ext])), Arbitrary s) + => EqProp (ProofStateT ext ext err s m a) where + (=-=) a b = property $ do + s <- arbitrary + pure $ ((=-=) `on` proofs s) a b + +instance ( MonadExtract meta ext err s m + , Arbitrary jdg + , EqProp (m (Either [err] [Proof s meta jdg ext])) + , Show s + , Arbitrary s + , Show jdg + ) + => EqProp (TacticT jdg ext err s m a) where + (=-=) = (=-=) `on` runTacticT . (() <$) + +instance ( Arbitrary jdg + , EqProp (m (Either [err] [Proof s meta jdg ext])) + , MonadExtract meta ext err s m + , Arbitrary s + , Show s , Show jdg + ) + => EqProp (RuleT jdg ext err s m ext) where + (=-=) = (=-=) `on` rule . const + +instance MonadExtract Int Int String Int Identity where + hole = do + i <- get + modify (+1) + pure (i, 0) + unsolvableHole _ = do + i <- get + modify (+1) + pure (i, 0) + +instance ( CoArbitrary ext' + , Arbitrary ext + , CoArbitrary err + , Arbitrary err + , Arbitrary a + , Arbitrary (m (ProofStateT ext' ext err s m a)) + , Arbitrary (m err) + , 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 + , Interleave <$> decayArbitrary 2 <*> decayArbitrary 2 + , Alt <$> decayArbitrary 2 <*> decayArbitrary 2 + , Stateful <$> arbitrary + , Failure <$> arbitrary <*> decayArbitrary 2 + , Handle <$> decayArbitrary 2 <*> arbitrary + ] ++ small + where + small = + [ pure Empty + , 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 + , CoArbitrary err + , Arbitrary err + , CoArbitrary ext + , Arbitrary jdg + , Arbitrary (m (ProofStateT ext ext err s m (a, jdg))) + , Arbitrary (m err) + , CoArbitrary s + , Arbitrary s + ) + => Arbitrary (TacticT jdg ext err s m a) where + arbitrary = fmap (TacticT . StateT) arbitrary + shrink = genericShrink + +instance ( Arbitrary a + , CoArbitrary err + , Arbitrary err + , CoArbitrary ext + , Arbitrary jdg + , Arbitrary (m (ProofStateT ext a err s m jdg)) + , Arbitrary (m err) + , 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 + +propertyTests :: Spec +propertyTests = 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 $ alternative (undefined :: RuleTest 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 ()) + -- it "constant peek" $ property $ peekConst (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 meta jdg ext err s + . (MonadExtract meta ext err s m + , EqProp (m (Either [err] [Proof s meta jdg ext])) + , Show s , Show jdg + , 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 meta jdg ext err s + . (MonadExtract meta ext err s m + , EqProp (m (Either [err] [Proof s meta jdg ext])) + , Show s , Show jdg + , 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)) + +-- peekConst +-- :: forall m jdg ext err s +-- . (MonadExtract ext err m +-- , EqProp (m [Either err (Proof s jdg ext)]) +-- , Show s , Show jdg +-- , Arbitrary jdg, Arbitrary s) +-- => TacticT jdg ext err s m () -- ^ proxy +-- -> TacticT jdg ext err s m () +-- -> TacticT jdg ext err s m () +-- -> Property +-- peekConst _ t t' = +-- peek t (const t') =-= (t' >> t) diff --git a/test/Spec/STLC.hs b/test/Spec/STLC.hs new file mode 100644 --- /dev/null +++ b/test/Spec/STLC.hs @@ -0,0 +1,147 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +module Spec.STLC where + +import Data.List +import Data.String (IsString(..)) + +import Control.Applicative +import Control.Monad.Identity +import Control.Monad.State + +import Refinery.ProofState +import Refinery.Tactic + +import Test.Hspec + +-- Just a very simple version of Simply Typed Lambda Calculus, +-- augmented with 'Hole' so that we can have +-- incomplete extracts. +data Term + = Var String + | Hole Int + | Lam String Term + | Pair Term Term + deriving (Show, Eq) + + +-- The type part of simply typed lambda calculus +data Type + = TVar String + | Type :-> Type + | TPair Type Type + deriving (Show, Eq) + +data TacticState = TacticState { name :: Int, meta :: Int } + deriving Show + +fresh :: MonadState TacticState m => m String +fresh = do + nm <- gets (show . name) + modify (\s -> s { name = name s + 1 }) + pure nm + +infixr 4 :-> + +instance IsString Type where + fromString = TVar + +-- A judgement is just a context, along with a goal +data Judgement = [(String, Type)] :- Type + deriving (Show, Eq) + +instance MonadExtract Int Term String TacticState Identity where + hole = do + m <- gets meta + modify $ \ts -> ts { meta = m + 1} + pure (m, Hole m) + unsolvableHole _ = do + m <- gets meta + modify $ \ts -> ts { meta = m + 1} + pure (m, Hole m) + +instance MetaSubst Int Term where + substMeta _ _ (Var s) = Var s + substMeta i t1 (Hole i') = if i == i' then t1 else (Hole i') + substMeta i t1 (Lam s body) = Lam s (substMeta i t1 body) + substMeta i t1 (Pair l r) = Pair (substMeta i t1 l) (substMeta i t1 r) + +type T a = TacticT Judgement Term String TacticState Identity a + +pair :: T () +pair = rule $ \case + (hys :- TPair a b) -> Pair <$> subgoal (hys :- a) <*> subgoal (hys :- b) + _ -> unsolvable "goal mismatch: Pair" + +lam :: T () +lam = rule $ \case + (hys :- (a :-> b)) -> do + nm <- fresh + body <- subgoal $ ((nm, a) : hys) :- b + pure $ Lam nm body + _ -> unsolvable "goal mismatch: Lam" + +assumption :: T () +assumption = rule $ \ (hys :- a) -> + case find (\(_, ty) -> ty == a) hys of + Just (x, _) -> pure $ Var x + Nothing -> unsolvable "goal mismatch: Assumption" + +auto :: T () +auto = do + many_ lam + choice [ pair >> auto + , assumption + ] + +refine :: T () +refine = do + many_ lam + try pair + +testHandlers :: T () +testHandlers = do + handler (\err -> pure $ err ++ " Third") + handler (\err -> pure $ err ++ " Second") + failure "First" + +testHandlerAlt :: T () +testHandlerAlt = do + handler (\err -> pure $ err ++ " Handled") + (failure "Error1") <|> (failure "Error2") + +testReify :: T () +testReify = do + lam + lam + reify pair $ \ (Proof _ _ goals) -> failure $ "Generated " <> show (length goals) <> " subgoals" + +testAttempt :: T () +testAttempt = do + lam + attempt lam (failure "Attempt Test Failed") + failure $ "Attempt Test Succeeds" + +jdg :: Judgement +jdg = ([] :- ("a" :-> "b" :-> (TPair "a" "b"))) + +evalT :: T () -> Judgement -> Either [String] [Term] +evalT t j = fmap (fmap pf_extract) $ runIdentity $ runTacticT t j (TacticState 0 0) + +stlcTests :: Spec +stlcTests = do + describe "Simply Typed Lambda Calculus" $ do + it "auto synthesize a solution" $ (evalT auto jdg) `shouldBe` (Right [(Lam "0" $ Lam "1" $ Pair (Var "0") (Var "1"))]) + it "handler ordering is correct" $ (evalT testHandlers jdg) `shouldBe` (Left ["First Second Third"]) + it "handler works through alt" $ (evalT testHandlerAlt jdg) `shouldBe` (Left ["Error1 Handled","Error2 Handled"]) + it "reify gets the right subgoals" $ (evalT testReify jdg) `shouldBe` (Left ["Generated 2 subgoals"]) + it "attempt properly handles errors" $ (evalT testAttempt jdg) `shouldBe` (Left ["Attempt Test Succeeds"])