refinery 0.3.0.0 → 0.4.0.0

raw patch · 9 files changed

+1118/−469 lines, 9 filesdep −logictPVP ok

version bump matches the API change (PVP)

Dependencies removed: logict

API changes (from Hackage documentation)

Files

• ChangeLog.md +40/−5
• README.md +185/−6
• refinery.cabal +8/−6
• src/Refinery/ProofState.hs +280/−125
• src/Refinery/Tactic.hs +177/−48
• src/Refinery/Tactic/Internal.hs +34/−42
• test/Spec.hs +4/−237
• test/Spec/PropertyTests.hs +243/−0
• test/Spec/STLC.hs +147/−0

@@ -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

@@ -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.++<!-- FIXME: Better explanation -->+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)

@@ -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 <https://github.com/githubuser/refinery#readme> 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

@@ -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 <> " <k>)"@@ -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 <> " <k>)"+  show (Handle p _) = "(Handle " <> show p <> " <h>)"   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)

@@ -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'

@@ -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

@@ -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

@@ -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)

@@ -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"])