{-# OPTIONS_GHC -Wno-name-shadowing #-}

{-# LANGUAGE DefaultSignatures      #-}
{-# LANGUAGE DeriveFunctor          #-}
{-# LANGUAGE DeriveGeneric          #-}
{-# LANGUAGE DerivingStrategies     #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# 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
-- Maintainer  :  reedmullanix@gmail.com
--
--
module Refinery.ProofState
  ( ProofStateT(..)
  -- * Proofstate Execution
  , MonadExtract(..)
  , Proof(..)
  , PartialProof(..)
  , proofs
  , partialProofs
  , subgoals
  -- * Extract Manipulation
  , mapExtract
  -- * Speculative Execution
  , MetaSubst(..)
  , DependentMetaSubst(..)
  , speculate
  ) where

import           Control.Applicative
import           Control.Monad
import           Control.Monad.Catch hiding (handle)
import           Control.Monad.Except
import qualified Control.Monad.Writer.Lazy as LW
import qualified Control.Monad.Writer.Strict as SW
import           Control.Monad.State
import           Control.Monad.Morph
import           Control.Monad.Reader
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
    -- ^ 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
    -- ^ Represents a simple extract.
    deriving stock ((forall x.
 ProofStateT ext' ext err s m goal
 -> Rep (ProofStateT ext' ext err s m goal) x)
-> (forall x.
    Rep (ProofStateT ext' ext err s m goal) x
    -> ProofStateT ext' ext err s m goal)
-> Generic (ProofStateT ext' ext err s m goal)
forall x.
Rep (ProofStateT ext' ext err s m goal) x
-> ProofStateT ext' ext err s m goal
forall x.
ProofStateT ext' ext err s m goal
-> Rep (ProofStateT ext' ext err s m goal) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ext' ext err s (m :: * -> *) goal x.
Rep (ProofStateT ext' ext err s m goal) x
-> ProofStateT ext' ext err s m goal
forall ext' ext err s (m :: * -> *) goal x.
ProofStateT ext' ext err s m goal
-> Rep (ProofStateT ext' ext err s m goal) x
$cto :: forall ext' ext err s (m :: * -> *) goal x.
Rep (ProofStateT ext' ext err s m goal) x
-> ProofStateT ext' ext err s m goal
$cfrom :: forall ext' ext err s (m :: * -> *) goal x.
ProofStateT ext' ext err s m goal
-> Rep (ProofStateT ext' ext err s m goal) x
Generic, a
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s m a
(a -> b)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m b
(forall a b.
 (a -> b)
 -> ProofStateT ext' ext err s m a
 -> ProofStateT ext' ext err s m b)
-> (forall a b.
    a
    -> ProofStateT ext' ext err s m b
    -> ProofStateT ext' ext err s m a)
-> Functor (ProofStateT ext' ext err s m)
forall a b.
a
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s m a
forall a b.
(a -> b)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m b
forall ext' ext err s (m :: * -> *) a b.
Functor m =>
a
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) a b.
Functor m =>
(a -> b)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s m a
$c<$ :: forall ext' ext err s (m :: * -> *) a b.
Functor m =>
a
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s m a
fmap :: (a -> b)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m b
$cfmap :: forall ext' ext err s (m :: * -> *) a b.
Functor m =>
(a -> b)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m b
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 :: ProofStateT ext' ext err s m goal -> String
show (Subgoal goal
goal ext' -> ProofStateT ext' ext err s m goal
_) = String
"(Subgoal " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> goal -> String
forall a. Show a => a -> String
show goal
goal String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" <k>)"
  show (Effect m (ProofStateT ext' ext err s m goal)
m) = String
"(Effect " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> m (ProofStateT ext' ext err s m goal) -> String
forall a. Show a => a -> String
show m (ProofStateT ext' ext err s m goal)
m String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (Stateful s -> (s, ProofStateT ext' ext err s m goal)
_) = String
"(Stateful <s>)"
  show (Alt ProofStateT ext' ext err s m goal
p1 ProofStateT ext' ext err s m goal
p2) = String
"(Alt " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofStateT ext' ext err s m goal -> String
forall a. Show a => a -> String
show ProofStateT ext' ext err s m goal
p1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofStateT ext' ext err s m goal -> String
forall a. Show a => a -> String
show ProofStateT ext' ext err s m goal
p2 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (Interleave ProofStateT ext' ext err s m goal
p1 ProofStateT ext' ext err s m goal
p2) = String
"(Interleave " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofStateT ext' ext err s m goal -> String
forall a. Show a => a -> String
show ProofStateT ext' ext err s m goal
p1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofStateT ext' ext err s m goal -> String
forall a. Show a => a -> String
show ProofStateT ext' ext err s m goal
p2 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (Commit ProofStateT ext' ext err s m goal
p1 ProofStateT ext' ext err s m goal
p2) = String
"(Commit " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofStateT ext' ext err s m goal -> String
forall a. Show a => a -> String
show ProofStateT ext' ext err s m goal
p1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofStateT ext' ext err s m goal -> String
forall a. Show a => a -> String
show ProofStateT ext' ext err s m goal
p2 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show ProofStateT ext' ext err s m goal
Empty = String
"Empty"
  show (Failure err
err ext' -> ProofStateT ext' ext err s m goal
_) = String
"(Failure " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> err -> String
forall a. Show a => a -> String
show err
err String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" <k>)"
  show (Handle ProofStateT ext' ext err s m goal
p err -> m err
_) = String
"(Handle " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofStateT ext' ext err s m goal -> String
forall a. Show a => a -> String
show ProofStateT ext' ext err s m goal
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" <h>)"
  show (Axiom ext
ext) = String
"(Axiom " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ext -> String
forall a. Show a => a -> String
show ext
ext String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"

instance Functor m => Applicative (ProofStateT ext ext err s m) where
    pure :: a -> ProofStateT ext ext err s m a
pure = a -> ProofStateT ext ext err s m a
forall (m :: * -> *) a. Monad m => a -> m a
return
    <*> :: ProofStateT ext ext err s m (a -> b)
-> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b
(<*>) = ProofStateT ext ext err s m (a -> b)
-> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance MFunctor (ProofStateT ext' ext err s) where
  hoist :: (forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
hoist forall a. m a -> n a
nat (Subgoal b
a ext' -> ProofStateT ext' ext err s m b
k) = b
-> (ext' -> ProofStateT ext' ext err s n b)
-> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
goal
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Subgoal b
a ((ext' -> ProofStateT ext' ext err s n b)
 -> ProofStateT ext' ext err s n b)
-> (ext' -> ProofStateT ext' ext err s n b)
-> ProofStateT ext' ext err s n b
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b)
-> (ext' -> ProofStateT ext' ext err s m b)
-> ext'
-> ProofStateT ext' ext err s n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat) ext' -> ProofStateT ext' ext err s m b
k
  hoist forall a. m a -> n a
nat (Effect m (ProofStateT ext' ext err s m b)
m)    = n (ProofStateT ext' ext err s n b)
-> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect (n (ProofStateT ext' ext err s n b)
 -> ProofStateT ext' ext err s n b)
-> n (ProofStateT ext' ext err s n b)
-> ProofStateT ext' ext err s n b
forall a b. (a -> b) -> a -> b
$ m (ProofStateT ext' ext err s n b)
-> n (ProofStateT ext' ext err s n b)
forall a. m a -> n a
nat (m (ProofStateT ext' ext err s n b)
 -> n (ProofStateT ext' ext err s n b))
-> m (ProofStateT ext' ext err s n b)
-> n (ProofStateT ext' ext err s n b)
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b)
-> m (ProofStateT ext' ext err s m b)
-> m (ProofStateT ext' ext err s n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat) m (ProofStateT ext' ext err s m b)
m
  hoist forall a. m a -> n a
nat (Stateful s -> (s, ProofStateT ext' ext err s m b)
f)    = (s -> (s, ProofStateT ext' ext err s n b))
-> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
(s -> (s, ProofStateT ext' ext err s m goal))
-> ProofStateT ext' ext err s m goal
Stateful ((s -> (s, ProofStateT ext' ext err s n b))
 -> ProofStateT ext' ext err s n b)
-> (s -> (s, ProofStateT ext' ext err s n b))
-> ProofStateT ext' ext err s n b
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b)
-> (s, ProofStateT ext' ext err s m b)
-> (s, ProofStateT ext' ext err s n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat) ((s, ProofStateT ext' ext err s m b)
 -> (s, ProofStateT ext' ext err s n b))
-> (s -> (s, ProofStateT ext' ext err s m b))
-> s
-> (s, ProofStateT ext' ext err s n b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (s, ProofStateT ext' ext err s m b)
f
  hoist forall a. m a -> n a
nat (Alt ProofStateT ext' ext err s m b
p1 ProofStateT ext' ext err s m b
p2)   = ProofStateT ext' ext err s n b
-> ProofStateT ext' ext err s n b -> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Alt ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat ProofStateT ext' ext err s m b
p1) ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat ProofStateT ext' ext err s m b
p2)
  hoist forall a. m a -> n a
nat (Interleave ProofStateT ext' ext err s m b
p1 ProofStateT ext' ext err s m b
p2)   = ProofStateT ext' ext err s n b
-> ProofStateT ext' ext err s n b -> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Interleave ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat ProofStateT ext' ext err s m b
p1) ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat ProofStateT ext' ext err s m b
p2)
  hoist forall a. m a -> n a
nat (Commit ProofStateT ext' ext err s m b
p1 ProofStateT ext' ext err s m b
p2)   = ProofStateT ext' ext err s n b
-> ProofStateT ext' ext err s n b -> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Commit ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat ProofStateT ext' ext err s m b
p1) ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat ProofStateT ext' ext err s m b
p2)
  hoist forall a. m a -> n a
nat (Failure err
err ext' -> ProofStateT ext' ext err s m b
k) = err
-> (ext' -> ProofStateT ext' ext err s n b)
-> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
err
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Failure err
err ((ext' -> ProofStateT ext' ext err s n b)
 -> ProofStateT ext' ext err s n b)
-> (ext' -> ProofStateT ext' ext err s n b)
-> ProofStateT ext' ext err s n b
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b)
-> (ext' -> ProofStateT ext' ext err s m b)
-> ext'
-> ProofStateT ext' ext err s n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat) ext' -> ProofStateT ext' ext err s m b
k
  hoist forall a. m a -> n a
nat (Handle ProofStateT ext' ext err s m b
p err -> m err
h) = ProofStateT ext' ext err s n b
-> (err -> n err) -> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> (err -> m err) -> ProofStateT ext' ext err s m goal
Handle ((forall a. m a -> n a)
-> ProofStateT ext' ext err s m b -> ProofStateT ext' ext err s n b
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. m a -> n a
nat ProofStateT ext' ext err s m b
p) (m err -> n err
forall a. m a -> n a
nat (m err -> n err) -> (err -> m err) -> err -> n err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. err -> m err
h)
  hoist forall a. m a -> n a
_ ProofStateT ext' ext err s m b
Empty         = ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
  hoist forall a. m a -> n a
_ (Axiom ext
ext)   = ext -> ProofStateT ext' ext err s n b
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom ext
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)
    -> ProofStateT ext' ext err s m a
    -> ProofStateT ext' ext err s m a
applyCont :: (ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k (Subgoal a
goal ext' -> ProofStateT ext' ext err s m a
k') = a
-> (ext' -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
goal
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Subgoal a
goal ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k (ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a)
-> (ext' -> ProofStateT ext' ext err s m a)
-> ext'
-> ProofStateT ext' ext err s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ext' -> ProofStateT ext' ext err s m a
k')
applyCont ext -> ProofStateT ext' ext err s m a
k (Effect m (ProofStateT ext' ext err s m a)
m) = m (ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect ((ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a)
-> m (ProofStateT ext' ext err s m a)
-> m (ProofStateT ext' ext err s m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k) m (ProofStateT ext' ext err s m a)
m)
applyCont ext -> ProofStateT ext' ext err s m a
k (Stateful s -> (s, ProofStateT ext' ext err s m a)
s) = (s -> (s, ProofStateT ext' ext err s m a))
-> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
(s -> (s, ProofStateT ext' ext err s m goal))
-> ProofStateT ext' ext err s m goal
Stateful ((s -> (s, ProofStateT ext' ext err s m a))
 -> ProofStateT ext' ext err s m a)
-> (s -> (s, ProofStateT ext' ext err s m a))
-> ProofStateT ext' ext err s m a
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a)
-> (s, ProofStateT ext' ext err s m a)
-> (s, ProofStateT ext' ext err s m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k) ((s, ProofStateT ext' ext err s m a)
 -> (s, ProofStateT ext' ext err s m a))
-> (s -> (s, ProofStateT ext' ext err s m a))
-> s
-> (s, ProofStateT ext' ext err s m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (s, ProofStateT ext' ext err s m a)
s
applyCont ext -> ProofStateT ext' ext err s m a
k (Alt ProofStateT ext' ext err s m a
p1 ProofStateT ext' ext err s m a
p2) = ProofStateT ext' ext err s m a
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Alt ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k ProofStateT ext' ext err s m a
p1) ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k ProofStateT ext' ext err s m a
p2)
applyCont ext -> ProofStateT ext' ext err s m a
k (Interleave ProofStateT ext' ext err s m a
p1 ProofStateT ext' ext err s m a
p2) = ProofStateT ext' ext err s m a
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Interleave ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k ProofStateT ext' ext err s m a
p1) ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k ProofStateT ext' ext err s m a
p2)
applyCont ext -> ProofStateT ext' ext err s m a
k (Commit ProofStateT ext' ext err s m a
p1 ProofStateT ext' ext err s m a
p2) = ProofStateT ext' ext err s m a
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Commit ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k ProofStateT ext' ext err s m a
p1) ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k ProofStateT ext' ext err s m a
p2)
applyCont ext -> ProofStateT ext' ext err s m a
_ ProofStateT ext' ext err s m a
Empty = ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
applyCont ext -> ProofStateT ext' ext err s m a
k (Failure err
err ext' -> ProofStateT ext' ext err s m a
k') = err
-> (ext' -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
err
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Failure err
err ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k (ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a)
-> (ext' -> ProofStateT ext' ext err s m a)
-> ext'
-> ProofStateT ext' ext err s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ext' -> ProofStateT ext' ext err s m a
k')
applyCont ext -> ProofStateT ext' ext err s m a
k (Handle ProofStateT ext' ext err s m a
p err -> m err
h) = ProofStateT ext' ext err s m a
-> (err -> m err) -> ProofStateT ext' ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> (err -> m err) -> ProofStateT ext' ext err s m goal
Handle ((ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext' ext err s m a
k ProofStateT ext' ext err s m a
p) err -> m err
h
applyCont ext -> ProofStateT ext' ext err s m a
k (Axiom ext
ext) = ext -> ProofStateT ext' ext err s m a
k ext
ext

instance Functor m => Monad (ProofStateT ext ext err s m) where
    return :: a -> ProofStateT ext ext err s m a
return a
goal = a
-> (ext -> ProofStateT ext ext err s m a)
-> ProofStateT ext ext err s m a
forall ext' ext err s (m :: * -> *) goal.
goal
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Subgoal a
goal ext -> ProofStateT ext ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom
    (Subgoal a
a ext -> ProofStateT ext ext err s m a
k)      >>= :: ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
>>= a -> ProofStateT ext ext err s m b
f = (ext -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m b
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont (a -> ProofStateT ext ext err s m b
f (a -> ProofStateT ext ext err s m b)
-> (ext -> ProofStateT ext ext err s m a)
-> ext
-> ProofStateT ext ext err s m b
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ext -> ProofStateT ext ext err s m a
k) (a -> ProofStateT ext ext err s m b
f a
a)
    (Effect m (ProofStateT ext ext err s m a)
m)         >>= a -> ProofStateT ext ext err s m b
f = m (ProofStateT ext ext err s m b) -> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect ((ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b)
-> m (ProofStateT ext ext err s m a)
-> m (ProofStateT ext ext err s m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f) m (ProofStateT ext ext err s m a)
m)
    (Stateful s -> (s, ProofStateT ext ext err s m a)
s)       >>= a -> ProofStateT ext ext err s m b
f = (s -> (s, ProofStateT ext ext err s m b))
-> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
(s -> (s, ProofStateT ext' ext err s m goal))
-> ProofStateT ext' ext err s m goal
Stateful ((s -> (s, ProofStateT ext ext err s m b))
 -> ProofStateT ext ext err s m b)
-> (s -> (s, ProofStateT ext ext err s m b))
-> ProofStateT ext ext err s m b
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext ext err s m a -> ProofStateT ext ext err s m b)
-> (s, ProofStateT ext ext err s m a)
-> (s, ProofStateT ext ext err s m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f) ((s, ProofStateT ext ext err s m a)
 -> (s, ProofStateT ext ext err s m b))
-> (s -> (s, ProofStateT ext ext err s m a))
-> s
-> (s, ProofStateT ext ext err s m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (s, ProofStateT ext ext err s m a)
s
    (Alt ProofStateT ext ext err s m a
p1 ProofStateT ext ext err s m a
p2)        >>= a -> ProofStateT ext ext err s m b
f = ProofStateT ext ext err s m b
-> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Alt (ProofStateT ext ext err s m a
p1 ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f) (ProofStateT ext ext err s m a
p2 ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f)
    (Interleave ProofStateT ext ext err s m a
p1 ProofStateT ext ext err s m a
p2) >>= a -> ProofStateT ext ext err s m b
f = ProofStateT ext ext err s m b
-> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Interleave (ProofStateT ext ext err s m a
p1 ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f) (ProofStateT ext ext err s m a
p2 ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f)
    (Commit ProofStateT ext ext err s m a
p1 ProofStateT ext ext err s m a
p2)     >>= a -> ProofStateT ext ext err s m b
f = ProofStateT ext ext err s m b
-> ProofStateT ext ext err s m b -> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Commit (ProofStateT ext ext err s m a
p1 ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f) (ProofStateT ext ext err s m a
p2 ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f)
    (Failure err
err ext -> ProofStateT ext ext err s m a
k)    >>= a -> ProofStateT ext ext err s m b
f = err
-> (ext -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
err
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Failure err
err (a -> ProofStateT ext ext err s m b
f (a -> ProofStateT ext ext err s m b)
-> (ext -> ProofStateT ext ext err s m a)
-> ext
-> ProofStateT ext ext err s m b
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ext -> ProofStateT ext ext err s m a
k)
    (Handle ProofStateT ext ext err s m a
p err -> m err
h)       >>= a -> ProofStateT ext ext err s m b
f = ProofStateT ext ext err s m b
-> (err -> m err) -> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> (err -> m err) -> ProofStateT ext' ext err s m goal
Handle (ProofStateT ext ext err s m a
p ProofStateT ext ext err s m a
-> (a -> ProofStateT ext ext err s m b)
-> ProofStateT ext ext err s m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofStateT ext ext err s m b
f) err -> m err
h
    ProofStateT ext ext err s m a
Empty              >>= a -> ProofStateT ext ext err s m b
_ = ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
    (Axiom ext
ext)        >>= a -> ProofStateT ext ext err s m b
_ = ext -> ProofStateT ext ext err s m b
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom ext
ext

instance MonadTrans (ProofStateT ext ext err s) where
    lift :: m a -> ProofStateT ext ext err s m a
lift m a
m = m (ProofStateT ext ext err s m a) -> ProofStateT ext ext err s m a
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect ((a -> ProofStateT ext ext err s m a)
-> m a -> m (ProofStateT ext ext err s m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> ProofStateT ext ext err s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure m a
m)

instance (Monad m) => Alternative (ProofStateT ext ext err s m) where
    empty :: ProofStateT ext ext err s m a
empty = ProofStateT ext ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
    <|> :: ProofStateT ext ext err s m a
-> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a
(<|>) = ProofStateT ext ext err s m a
-> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Alt

instance (Monad m) => MonadPlus (ProofStateT ext ext err s m) where
    mzero :: ProofStateT ext ext err s m a
mzero = ProofStateT ext ext err s m a
forall (f :: * -> *) a. Alternative f => f a
empty
    mplus :: ProofStateT ext ext err s m a
-> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a
mplus = ProofStateT ext ext err s m a
-> ProofStateT ext ext err s m a -> ProofStateT ext ext err s m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)

-- | '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 :: StateT s m (meta, ext)
  default hole :: (MonadTrans t, MonadExtract meta ext err s m1, m ~ t m1) => StateT s m (meta, ext)
  hole = (m1 ((meta, ext), s) -> t m1 ((meta, ext), s))
-> StateT s m1 (meta, ext) -> StateT s (t m1) (meta, ext)
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
mapStateT m1 ((meta, ext), s) -> t m1 ((meta, ext), s)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift StateT s m1 (meta, ext)
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
StateT s m (meta, ext)
hole

  -- | 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 = (m1 ((meta, ext), s) -> t m1 ((meta, ext), s))
-> StateT s m1 (meta, ext) -> StateT s (t m1) (meta, ext)
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
mapStateT m1 ((meta, ext), s) -> t m1 ((meta, ext), s)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT s m1 (meta, ext) -> StateT s (t m1) (meta, ext))
-> (err -> StateT s m1 (meta, ext))
-> err
-> StateT s (t m1) (meta, ext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. err -> StateT s m1 (meta, ext)
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
err -> StateT s m (meta, ext)
unsolvableHole


newHole :: MonadExtract meta ext err s m => s -> m (s, (meta, ext))
newHole :: s -> m (s, (meta, ext))
newHole = (((meta, ext), s) -> (s, (meta, ext)))
-> m ((meta, ext), s) -> m (s, (meta, ext))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((meta, ext), s) -> (s, (meta, ext))
forall a b. (a, b) -> (b, a)
swap (m ((meta, ext), s) -> m (s, (meta, ext)))
-> (s -> m ((meta, ext), s)) -> s -> m (s, (meta, ext))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT s m (meta, ext) -> s -> m ((meta, ext), s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT s m (meta, ext)
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
StateT s m (meta, ext)
hole

newUnsolvableHole :: MonadExtract meta ext err s m => s -> err -> m (s, (meta, ext))
newUnsolvableHole :: s -> err -> m (s, (meta, ext))
newUnsolvableHole s
s err
err = (((meta, ext), s) -> (s, (meta, ext)))
-> m ((meta, ext), s) -> m (s, (meta, ext))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((meta, ext), s) -> (s, (meta, ext))
forall a b. (a, b) -> (b, a)
swap (m ((meta, ext), s) -> m (s, (meta, ext)))
-> m ((meta, ext), s) -> m (s, (meta, ext))
forall a b. (a -> b) -> a -> b
$ StateT s m (meta, ext) -> s -> m ((meta, ext), s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (err -> StateT s m (meta, ext)
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
err -> StateT s m (meta, ext)
unsolvableHole err
err) s
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
    { Proof s meta goal ext -> ext
pf_extract :: ext
    -- ^ The extract of the tactic.
    , Proof s meta goal ext -> s
pf_state :: s
    -- ^ The state at the end of tactic execution.
    , Proof s meta goal ext -> [(meta, goal)]
pf_unsolvedGoals :: [(meta, goal)]
    -- ^ All the goals that were still unsolved by the end of tactic execution.
    }
    deriving (Proof s meta goal ext -> Proof s meta goal ext -> Bool
(Proof s meta goal ext -> Proof s meta goal ext -> Bool)
-> (Proof s meta goal ext -> Proof s meta goal ext -> Bool)
-> Eq (Proof s meta goal ext)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s meta goal ext.
(Eq ext, Eq s, Eq meta, Eq goal) =>
Proof s meta goal ext -> Proof s meta goal ext -> Bool
/= :: Proof s meta goal ext -> Proof s meta goal ext -> Bool
$c/= :: forall s meta goal ext.
(Eq ext, Eq s, Eq meta, Eq goal) =>
Proof s meta goal ext -> Proof s meta goal ext -> Bool
== :: Proof s meta goal ext -> Proof s meta goal ext -> Bool
$c== :: forall s meta goal ext.
(Eq ext, Eq s, Eq meta, Eq goal) =>
Proof s meta goal ext -> Proof s meta goal ext -> Bool
Eq, Int -> Proof s meta goal ext -> ShowS
[Proof s meta goal ext] -> ShowS
Proof s meta goal ext -> String
(Int -> Proof s meta goal ext -> ShowS)
-> (Proof s meta goal ext -> String)
-> ([Proof s meta goal ext] -> ShowS)
-> Show (Proof s meta goal ext)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s meta goal ext.
(Show ext, Show s, Show meta, Show goal) =>
Int -> Proof s meta goal ext -> ShowS
forall s meta goal ext.
(Show ext, Show s, Show meta, Show goal) =>
[Proof s meta goal ext] -> ShowS
forall s meta goal ext.
(Show ext, Show s, Show meta, Show goal) =>
Proof s meta goal ext -> String
showList :: [Proof s meta goal ext] -> ShowS
$cshowList :: forall s meta goal ext.
(Show ext, Show s, Show meta, Show goal) =>
[Proof s meta goal ext] -> ShowS
show :: Proof s meta goal ext -> String
$cshow :: forall s meta goal ext.
(Show ext, Show s, Show meta, Show goal) =>
Proof s meta goal ext -> String
showsPrec :: Int -> Proof s meta goal ext -> ShowS
$cshowsPrec :: forall s meta goal ext.
(Show ext, Show s, Show meta, Show goal) =>
Int -> Proof s meta goal ext -> ShowS
Show, (forall x. Proof s meta goal ext -> Rep (Proof s meta goal ext) x)
-> (forall x.
    Rep (Proof s meta goal ext) x -> Proof s meta goal ext)
-> Generic (Proof s meta goal ext)
forall x. Rep (Proof s meta goal ext) x -> Proof s meta goal ext
forall x. Proof s meta goal ext -> Rep (Proof s meta goal ext) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s meta goal ext x.
Rep (Proof s meta goal ext) x -> Proof s meta goal ext
forall s meta goal ext x.
Proof s meta goal ext -> Rep (Proof s meta goal ext) x
$cto :: forall s meta goal ext x.
Rep (Proof s meta goal ext) x -> Proof s meta goal ext
$cfrom :: forall s meta goal ext x.
Proof s meta goal ext -> Rep (Proof s meta goal ext) x
Generic)

-- | Interleave two lists together.
-- @
--     interleave [1,2,3,4] [5,6]
-- @
-- > [1,5,2,6,3,4]
interleave :: [a] -> [a] -> [a]
interleave :: [a] -> [a] -> [a]
interleave (a
x : [a]
xs) (a
y : [a]
ys) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: ([a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
interleave [a]
xs [a]
ys)
interleave [a]
xs [] = [a]
xs
interleave [] [a]
ys = [a]
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 :: (forall a. [a] -> [a] -> [a])
-> Either [b] [c] -> Either [b] [c] -> Either [b] [c]
prioritizing forall a. [a] -> [a] -> [a]
combine (Left [b]
a1) (Left [b]
a2)   = [b] -> Either [b] [c]
forall a b. a -> Either a b
Left ([b] -> Either [b] [c]) -> [b] -> Either [b] [c]
forall a b. (a -> b) -> a -> b
$ [b]
a1 [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
`combine` [b]
a2
prioritizing forall a. [a] -> [a] -> [a]
_ (Left [b]
_) (Right [c]
b2)         = [c] -> Either [b] [c]
forall a b. b -> Either a b
Right [c]
b2
prioritizing forall a. [a] -> [a] -> [a]
_ (Right [c]
b1) (Left [b]
_)         = [c] -> Either [b] [c]
forall a b. b -> Either a b
Right [c]
b1
prioritizing forall a. [a] -> [a] -> [a]
combine (Right [c]
b1) (Right [c]
b2) = [c] -> Either [b] [c]
forall a b. b -> Either a b
Right ([c] -> Either [b] [c]) -> [c] -> Either [b] [c]
forall a b. (a -> b) -> a -> b
$ [c]
b1 [c] -> [c] -> [c]
forall a. [a] -> [a] -> [a]
`combine` [c]
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
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
proofs s
s ProofStateT ext ext err s m goal
p = s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [] err -> m err
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProofStateT ext ext err s m goal
p
    where
      go :: s -> [(meta, goal)] -> (err -> m err) -> ProofStateT ext ext err s m goal -> m (Either [err] [Proof s meta goal ext])
      go :: s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
_ (Subgoal goal
goal ext -> ProofStateT ext ext err s m goal
k) = do
         (s
s', (meta
meta, ext
h)) <- s -> m (s, (meta, ext))
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
s -> m (s, (meta, ext))
newHole s
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.
         (s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s' ([(meta, goal)]
goals [(meta, goal)] -> [(meta, goal)] -> [(meta, goal)]
forall a. [a] -> [a] -> [a]
++ [(meta
meta, goal
goal)]) err -> m err
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProofStateT ext ext err s m goal
 -> m (Either [err] [Proof s meta goal ext]))
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ ext -> ProofStateT ext ext err s m goal
k ext
h)
      go s
s [(meta, goal)]
goals err -> m err
handlers (Effect m (ProofStateT ext ext err s m goal)
m) = m (ProofStateT ext ext err s m goal)
m m (ProofStateT ext ext err s m goal)
-> (ProofStateT ext ext err s m goal
    -> m (Either [err] [Proof s meta goal ext]))
-> m (Either [err] [Proof s meta goal ext])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
handlers
      go s
s [(meta, goal)]
goals err -> m err
handlers (Stateful s -> (s, ProofStateT ext ext err s m goal)
f) =
          let (s
s', ProofStateT ext ext err s m goal
p) = s -> (s, ProofStateT ext ext err s m goal)
f s
s
          in s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s' [(meta, goal)]
goals err -> m err
handlers ProofStateT ext ext err s m goal
p
      go s
s [(meta, goal)]
goals err -> m err
handlers (Alt ProofStateT ext ext err s m goal
p1 ProofStateT ext ext err s m goal
p2) =
          (Either [err] [Proof s meta goal ext]
 -> Either [err] [Proof s meta goal ext]
 -> Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ((forall a. [a] -> [a] -> [a])
-> Either [err] [Proof s meta goal ext]
-> Either [err] [Proof s meta goal ext]
-> Either [err] [Proof s meta goal ext]
forall b c.
(forall a. [a] -> [a] -> [a])
-> Either [b] [c] -> Either [b] [c] -> Either [b] [c]
prioritizing forall a. Semigroup a => a -> a -> a
forall a. [a] -> [a] -> [a]
(<>)) (s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
handlers ProofStateT ext ext err s m goal
p1) (s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
handlers ProofStateT ext ext err s m goal
p2)
      go s
s [(meta, goal)]
goals err -> m err
handlers (Interleave ProofStateT ext ext err s m goal
p1 ProofStateT ext ext err s m goal
p2) =
          (Either [err] [Proof s meta goal ext]
 -> Either [err] [Proof s meta goal ext]
 -> Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ((forall a. [a] -> [a] -> [a])
-> Either [err] [Proof s meta goal ext]
-> Either [err] [Proof s meta goal ext]
-> Either [err] [Proof s meta goal ext]
forall b c.
(forall a. [a] -> [a] -> [a])
-> Either [b] [c] -> Either [b] [c] -> Either [b] [c]
prioritizing forall a. [a] -> [a] -> [a]
interleave) (s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
handlers ProofStateT ext ext err s m goal
p1) (s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
handlers ProofStateT ext ext err s m goal
p2)
      go s
s [(meta, goal)]
goals err -> m err
handlers (Commit ProofStateT ext ext err s m goal
p1 ProofStateT ext ext err s m goal
p2) = s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
handlers ProofStateT ext ext err s m goal
p1 m (Either [err] [Proof s meta goal ext])
-> (Either [err] [Proof s meta goal ext]
    -> m (Either [err] [Proof s meta goal ext]))
-> m (Either [err] [Proof s meta goal ext])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Right [Proof s meta goal ext]
solns | Bool -> Bool
not ([Proof s meta goal ext] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Proof s meta goal ext]
solns) -> Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [err] [Proof s meta goal ext]
 -> m (Either [err] [Proof s meta goal ext]))
-> Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [Proof s meta goal ext] -> Either [err] [Proof s meta goal ext]
forall a b. b -> Either a b
Right [Proof s meta goal ext]
solns
          Either [err] [Proof s meta goal ext]
solns                          -> ((forall a. [a] -> [a] -> [a])
-> Either [err] [Proof s meta goal ext]
-> Either [err] [Proof s meta goal ext]
-> Either [err] [Proof s meta goal ext]
forall b c.
(forall a. [a] -> [a] -> [a])
-> Either [b] [c] -> Either [b] [c] -> Either [b] [c]
prioritizing forall a. Semigroup a => a -> a -> a
forall a. [a] -> [a] -> [a]
(<>) Either [err] [Proof s meta goal ext]
solns) (Either [err] [Proof s meta goal ext]
 -> Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
-> m (Either [err] [Proof s meta goal ext])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals err -> m err
handlers ProofStateT ext ext err s m goal
p2
      go s
_ [(meta, goal)]
_ err -> m err
_ ProofStateT ext ext err s m goal
Empty = Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [err] [Proof s meta goal ext]
 -> m (Either [err] [Proof s meta goal ext]))
-> Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [err] -> Either [err] [Proof s meta goal ext]
forall a b. a -> Either a b
Left []
      go s
_ [(meta, goal)]
_ err -> m err
handlers (Failure err
err ext -> ProofStateT ext ext err s m goal
_) = do
          err
annErr <- err -> m err
handlers err
err
          Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [err] [Proof s meta goal ext]
 -> m (Either [err] [Proof s meta goal ext]))
-> Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [err] -> Either [err] [Proof s meta goal ext]
forall a b. a -> Either a b
Left [err
annErr]
      go s
s [(meta, goal)]
goals err -> m err
handlers (Handle ProofStateT ext ext err s m goal
p err -> m err
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@.
          s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Either [err] [Proof s meta goal ext])
go s
s [(meta, goal)]
goals (err -> m err
h (err -> m err) -> (err -> m err) -> err -> m err
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> err -> m err
handlers) ProofStateT ext ext err s m goal
p
      go s
s [(meta, goal)]
goals err -> m err
_ (Axiom ext
ext) = Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [err] [Proof s meta goal ext]
 -> m (Either [err] [Proof s meta goal ext]))
-> Either [err] [Proof s meta goal ext]
-> m (Either [err] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [Proof s meta goal ext] -> Either [err] [Proof s meta goal ext]
forall a b. b -> Either a b
Right ([Proof s meta goal ext] -> Either [err] [Proof s meta goal ext])
-> [Proof s meta goal ext] -> Either [err] [Proof s meta goal ext]
forall a b. (a -> b) -> a -> b
$ [ext -> s -> [(meta, goal)] -> Proof s meta goal ext
forall s meta goal ext.
ext -> s -> [(meta, goal)] -> Proof s meta goal ext
Proof ext
ext s
s [(meta, goal)]
goals]

-- | 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 (PartialProof s err meta goal ext
-> PartialProof s err meta goal ext -> Bool
(PartialProof s err meta goal ext
 -> PartialProof s err meta goal ext -> Bool)
-> (PartialProof s err meta goal ext
    -> PartialProof s err meta goal ext -> Bool)
-> Eq (PartialProof s err meta goal ext)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s err meta goal ext.
(Eq ext, Eq s, Eq meta, Eq goal, Eq err) =>
PartialProof s err meta goal ext
-> PartialProof s err meta goal ext -> Bool
/= :: PartialProof s err meta goal ext
-> PartialProof s err meta goal ext -> Bool
$c/= :: forall s err meta goal ext.
(Eq ext, Eq s, Eq meta, Eq goal, Eq err) =>
PartialProof s err meta goal ext
-> PartialProof s err meta goal ext -> Bool
== :: PartialProof s err meta goal ext
-> PartialProof s err meta goal ext -> Bool
$c== :: forall s err meta goal ext.
(Eq ext, Eq s, Eq meta, Eq goal, Eq err) =>
PartialProof s err meta goal ext
-> PartialProof s err meta goal ext -> Bool
Eq, Int -> PartialProof s err meta goal ext -> ShowS
[PartialProof s err meta goal ext] -> ShowS
PartialProof s err meta goal ext -> String
(Int -> PartialProof s err meta goal ext -> ShowS)
-> (PartialProof s err meta goal ext -> String)
-> ([PartialProof s err meta goal ext] -> ShowS)
-> Show (PartialProof s err meta goal ext)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s err meta goal ext.
(Show ext, Show s, Show meta, Show goal, Show err) =>
Int -> PartialProof s err meta goal ext -> ShowS
forall s err meta goal ext.
(Show ext, Show s, Show meta, Show goal, Show err) =>
[PartialProof s err meta goal ext] -> ShowS
forall s err meta goal ext.
(Show ext, Show s, Show meta, Show goal, Show err) =>
PartialProof s err meta goal ext -> String
showList :: [PartialProof s err meta goal ext] -> ShowS
$cshowList :: forall s err meta goal ext.
(Show ext, Show s, Show meta, Show goal, Show err) =>
[PartialProof s err meta goal ext] -> ShowS
show :: PartialProof s err meta goal ext -> String
$cshow :: forall s err meta goal ext.
(Show ext, Show s, Show meta, Show goal, Show err) =>
PartialProof s err meta goal ext -> String
showsPrec :: Int -> PartialProof s err meta goal ext -> ShowS
$cshowsPrec :: forall s err meta goal ext.
(Show ext, Show s, Show meta, Show goal, Show err) =>
Int -> PartialProof s err meta goal ext -> ShowS
Show, (forall x.
 PartialProof s err meta goal ext
 -> Rep (PartialProof s err meta goal ext) x)
-> (forall x.
    Rep (PartialProof s err meta goal ext) x
    -> PartialProof s err meta goal ext)
-> Generic (PartialProof s err meta goal ext)
forall x.
Rep (PartialProof s err meta goal ext) x
-> PartialProof s err meta goal ext
forall x.
PartialProof s err meta goal ext
-> Rep (PartialProof s err meta goal ext) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s err meta goal ext x.
Rep (PartialProof s err meta goal ext) x
-> PartialProof s err meta goal ext
forall s err meta goal ext x.
PartialProof s err meta goal ext
-> Rep (PartialProof s err meta goal ext) x
$cto :: forall s err meta goal ext x.
Rep (PartialProof s err meta goal ext) x
-> PartialProof s err meta goal ext
$cfrom :: forall s err meta goal ext x.
PartialProof s err meta goal ext
-> Rep (PartialProof s err meta goal ext) x
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
-> ProofStateT ext ext err s m goal
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
partialProofs s
s ProofStateT ext ext err s m goal
pf = 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
s [] [] err -> m err
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProofStateT ext ext err s m goal
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
-> [(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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
_ (Subgoal goal
goal ext -> ProofStateT ext ext err s m goal
k) = do
         (s
s', (meta
meta, ext
h)) <- s -> m (s, (meta, ext))
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
s -> m (s, (meta, ext))
newHole s
s
         -- See Note [Handler Reset]
         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
s' ([(meta, goal)]
goals [(meta, goal)] -> [(meta, goal)] -> [(meta, goal)]
forall a. [a] -> [a] -> [a]
++ [(meta
meta, goal
goal)]) [(meta, err)]
errs err -> m err
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProofStateT ext ext err s m goal
 -> m (Either
         [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> ProofStateT ext ext err s m goal
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ ext -> ProofStateT ext ext err s m goal
k ext
h
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers (Effect m (ProofStateT ext ext err s m goal)
m) = m (ProofStateT ext ext err s m goal)
m m (ProofStateT ext ext err s m goal)
-> (ProofStateT ext ext err s m goal
    -> m (Either
            [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers (Stateful s -> (s, ProofStateT ext ext err s m goal)
f) =
          let (s
s', ProofStateT ext ext err s m goal
p) = s -> (s, ProofStateT ext ext err s m goal)
f s
s
          in 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
s' [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers ProofStateT ext ext err s m goal
p
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers (Alt ProofStateT ext ext err s m goal
p1 ProofStateT ext ext err s m goal
p2) = (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> Either
      [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> Either
      [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ((forall a. [a] -> [a] -> [a])
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
forall b c.
(forall a. [a] -> [a] -> [a])
-> Either [b] [c] -> Either [b] [c] -> Either [b] [c]
prioritizing forall a. Semigroup a => a -> a -> a
forall a. [a] -> [a] -> [a]
(<>)) (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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers ProofStateT ext ext err s m goal
p1) (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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers ProofStateT ext ext err s m goal
p2)
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers (Interleave ProofStateT ext ext err s m goal
p1 ProofStateT ext ext err s m goal
p2) = (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> Either
      [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> Either
      [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ((forall a. [a] -> [a] -> [a])
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
forall b c.
(forall a. [a] -> [a] -> [a])
-> Either [b] [c] -> Either [b] [c] -> Either [b] [c]
prioritizing forall a. [a] -> [a] -> [a]
interleave) (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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers ProofStateT ext ext err s m goal
p1) (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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers ProofStateT ext ext err s m goal
p2)
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers (Commit ProofStateT ext ext err s m goal
p1 ProofStateT ext ext err s m goal
p2) = 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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers ProofStateT ext ext err s m goal
p1 m (Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> (Either
      [PartialProof s err meta goal ext] [Proof s meta goal ext]
    -> m (Either
            [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Right [Proof s meta goal ext]
solns | Bool -> Bool
not ([Proof s meta goal ext] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Proof s meta goal ext]
solns) -> Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> m (Either
         [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
forall a b. b -> Either a b
Right [Proof s meta goal ext]
solns
          Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
solns                          -> ((forall a. [a] -> [a] -> [a])
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
forall b c.
(forall a. [a] -> [a] -> [a])
-> Either [b] [c] -> Either [b] [c] -> Either [b] [c]
prioritizing forall a. Semigroup a => a -> a -> a
forall a. [a] -> [a] -> [a]
(<>) Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
solns) (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> Either
      [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers ProofStateT ext ext err s m goal
p2
      go s
_ [(meta, goal)]
_ [(meta, err)]
_ err -> m err
_ ProofStateT ext ext err s m goal
Empty = Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> m (Either
         [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [PartialProof s err meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
forall a b. a -> Either a b
Left []
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers (Failure err
err ext -> ProofStateT ext ext err s m goal
k) = do
          err
annErr <- err -> m err
handlers err
err
          (s
s', (meta
meta, ext
h)) <- s -> err -> m (s, (meta, ext))
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
s -> err -> m (s, (meta, ext))
newUnsolvableHole s
s err
annErr
          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
s' [(meta, goal)]
goals ([(meta, err)]
errs [(meta, err)] -> [(meta, err)] -> [(meta, err)]
forall a. [a] -> [a] -> [a]
++ [(meta
meta, err
annErr)]) err -> m err
handlers (ProofStateT ext ext err s m goal
 -> m (Either
         [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> ProofStateT ext ext err s m goal
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ ext -> ProofStateT ext ext err s m goal
k ext
h
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
handlers (Handle ProofStateT ext ext err s m goal
p err -> m err
h) =
          -- See Note [Handler ordering]
          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
s [(meta, goal)]
goals [(meta, err)]
errs (err -> m err
h (err -> m err) -> (err -> m err) -> err -> m err
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> err -> m err
handlers) ProofStateT ext ext err s m goal
p
      go s
s [(meta, goal)]
goals [] err -> m err
_ (Axiom ext
ext) = Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> m (Either
         [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [Proof s meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
forall a b. b -> Either a b
Right [ext -> s -> [(meta, goal)] -> Proof s meta goal ext
forall s meta goal ext.
ext -> s -> [(meta, goal)] -> Proof s meta goal ext
Proof ext
ext s
s [(meta, goal)]
goals]
      go s
s [(meta, goal)]
goals [(meta, err)]
errs err -> m err
_ (Axiom ext
ext) = Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [PartialProof s err meta goal ext] [Proof s meta goal ext]
 -> m (Either
         [PartialProof s err meta goal ext] [Proof s meta goal ext]))
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
-> m (Either
        [PartialProof s err meta goal ext] [Proof s meta goal ext])
forall a b. (a -> b) -> a -> b
$ [PartialProof s err meta goal ext]
-> Either
     [PartialProof s err meta goal ext] [Proof s meta goal ext]
forall a b. a -> Either a b
Left [ext
-> s
-> [(meta, goal)]
-> [(meta, err)]
-> PartialProof s err meta goal ext
forall s err meta goal ext.
ext
-> s
-> [(meta, goal)]
-> [(meta, err)]
-> PartialProof s err meta goal ext
PartialProof ext
ext s
s [(meta, goal)]
goals [(meta, err)]
errs]

instance (MonadIO m) => MonadIO (ProofStateT ext ext err s m) where
  liftIO :: IO a -> ProofStateT ext ext err s m a
liftIO = m a -> ProofStateT ext ext err s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ProofStateT ext ext err s m a)
-> (IO a -> m a) -> IO a -> ProofStateT ext ext err s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

instance (MonadThrow m) => MonadThrow (ProofStateT ext ext err s m) where
  throwM :: e -> ProofStateT ext ext err s m a
throwM = m a -> ProofStateT ext ext err s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ProofStateT ext ext err s m a)
-> (e -> m a) -> e -> ProofStateT ext ext err s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM

instance (Monad m) => MonadState s (ProofStateT ext ext err s m) where
    state :: (s -> (a, s)) -> ProofStateT ext ext err s m a
state s -> (a, s)
f = (s -> (s, ProofStateT ext ext err s m a))
-> ProofStateT ext ext err s m a
forall ext' ext err s (m :: * -> *) goal.
(s -> (s, ProofStateT ext' ext err s m goal))
-> ProofStateT ext' ext err s m goal
Stateful ((s -> (s, ProofStateT ext ext err s m a))
 -> ProofStateT ext ext err s m a)
-> (s -> (s, ProofStateT ext ext err s m a))
-> ProofStateT ext ext err s m a
forall a b. (a -> b) -> a -> b
$ \s
s ->
      let (a
a, s
s') = s -> (a, s)
f s
s
      in (s
s', a -> ProofStateT ext ext err s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)

-- | @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 :: [jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
subgoals [] (Subgoal jdg
goal ext -> ProofStateT ext ext err s m jdg
k) = (ext -> ProofStateT ext ext err s m jdg)
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ext -> ProofStateT ext ext err s m jdg
k (jdg -> ProofStateT ext ext err s m jdg
forall (f :: * -> *) a. Applicative f => a -> f a
pure jdg
goal)
subgoals (jdg -> ProofStateT ext ext err s m jdg
f:[jdg -> ProofStateT ext ext err s m jdg]
fs) (Subgoal jdg
goal ext -> ProofStateT ext ext err s m jdg
k)  = (ext -> ProofStateT ext ext err s m jdg)
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) ext ext' err s a.
Functor m =>
(ext -> ProofStateT ext' ext err s m a)
-> ProofStateT ext' ext err s m a -> ProofStateT ext' ext err s m a
applyCont ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs (ProofStateT ext ext err s m jdg
 -> ProofStateT ext ext err s m jdg)
-> (ext -> ProofStateT ext ext err s m jdg)
-> ext
-> ProofStateT ext ext err s m jdg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ext -> ProofStateT ext ext err s m jdg
k) (jdg -> ProofStateT ext ext err s m jdg
f jdg
goal)
subgoals [jdg -> ProofStateT ext ext err s m jdg]
fs (Effect m (ProofStateT ext ext err s m jdg)
m) = m (ProofStateT ext ext err s m jdg)
-> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect ((ProofStateT ext ext err s m jdg
 -> ProofStateT ext ext err s m jdg)
-> m (ProofStateT ext ext err s m jdg)
-> m (ProofStateT ext ext err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs) m (ProofStateT ext ext err s m jdg)
m)
subgoals [jdg -> ProofStateT ext ext err s m jdg]
fs (Stateful s -> (s, ProofStateT ext ext err s m jdg)
s) = (s -> (s, ProofStateT ext ext err s m jdg))
-> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
(s -> (s, ProofStateT ext' ext err s m goal))
-> ProofStateT ext' ext err s m goal
Stateful ((ProofStateT ext ext err s m jdg
 -> ProofStateT ext ext err s m jdg)
-> (s, ProofStateT ext ext err s m jdg)
-> (s, ProofStateT ext ext err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs) ((s, ProofStateT ext ext err s m jdg)
 -> (s, ProofStateT ext ext err s m jdg))
-> (s -> (s, ProofStateT ext ext err s m jdg))
-> s
-> (s, ProofStateT ext ext err s m jdg)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (s, ProofStateT ext ext err s m jdg)
s)
subgoals [jdg -> ProofStateT ext ext err s m jdg]
fs (Alt ProofStateT ext ext err s m jdg
p1 ProofStateT ext ext err s m jdg
p2) = ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Alt ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs ProofStateT ext ext err s m jdg
p1) ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs ProofStateT ext ext err s m jdg
p2)
subgoals [jdg -> ProofStateT ext ext err s m jdg]
fs (Interleave ProofStateT ext ext err s m jdg
p1 ProofStateT ext ext err s m jdg
p2) = ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Interleave ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs ProofStateT ext ext err s m jdg
p1) ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs ProofStateT ext ext err s m jdg
p2)
subgoals [jdg -> ProofStateT ext ext err s m jdg]
fs (Commit ProofStateT ext ext err s m jdg
p1 ProofStateT ext ext err s m jdg
p2) = ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Commit ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs ProofStateT ext ext err s m jdg
p1) ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs ProofStateT ext ext err s m jdg
p2)
subgoals [jdg -> ProofStateT ext ext err s m jdg]
fs (Failure err
err ext -> ProofStateT ext ext err s m jdg
k) = err
-> (ext -> ProofStateT ext ext err s m jdg)
-> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
err
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Failure err
err ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs (ProofStateT ext ext err s m jdg
 -> ProofStateT ext ext err s m jdg)
-> (ext -> ProofStateT ext ext err s m jdg)
-> ext
-> ProofStateT ext ext err s m jdg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ext -> ProofStateT ext ext err s m jdg
k)
subgoals [jdg -> ProofStateT ext ext err s m jdg]
fs (Handle ProofStateT ext ext err s m jdg
p err -> m err
h) = ProofStateT ext ext err s m jdg
-> (err -> m err) -> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> (err -> m err) -> ProofStateT ext' ext err s m goal
Handle ([jdg -> ProofStateT ext ext err s m jdg]
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s.
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 [jdg -> ProofStateT ext ext err s m jdg]
fs ProofStateT ext ext err s m jdg
p) err -> m err
h
subgoals [jdg -> ProofStateT ext ext err s m jdg]
_ ProofStateT ext ext err s m jdg
Empty = ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
subgoals [jdg -> ProofStateT ext ext err s m jdg]
_ (Axiom ext
ext) = ext -> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom ext
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 :: (a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out (Subgoal jdg
goal ext' -> ProofStateT ext' ext err s m jdg
k) = jdg
-> (a -> ProofStateT a b err s m jdg)
-> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
goal
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Subgoal jdg
goal ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out (ProofStateT ext' ext err s m jdg -> ProofStateT a b err s m jdg)
-> (a -> ProofStateT ext' ext err s m jdg)
-> a
-> ProofStateT a b err s m jdg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ext' -> ProofStateT ext' ext err s m jdg
k (ext' -> ProofStateT ext' ext err s m jdg)
-> (a -> ext') -> a -> ProofStateT ext' ext err s m jdg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ext'
into)
mapExtract a -> ext'
into ext -> b
out (Effect m (ProofStateT ext' ext err s m jdg)
m) = m (ProofStateT a b err s m jdg) -> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect ((ProofStateT ext' ext err s m jdg -> ProofStateT a b err s m jdg)
-> m (ProofStateT ext' ext err s m jdg)
-> m (ProofStateT a b err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out) m (ProofStateT ext' ext err s m jdg)
m)
mapExtract a -> ext'
into ext -> b
out (Stateful s -> (s, ProofStateT ext' ext err s m jdg)
s) = (s -> (s, ProofStateT a b err s m jdg))
-> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
(s -> (s, ProofStateT ext' ext err s m goal))
-> ProofStateT ext' ext err s m goal
Stateful ((ProofStateT ext' ext err s m jdg -> ProofStateT a b err s m jdg)
-> (s, ProofStateT ext' ext err s m jdg)
-> (s, ProofStateT a b err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out) ((s, ProofStateT ext' ext err s m jdg)
 -> (s, ProofStateT a b err s m jdg))
-> (s -> (s, ProofStateT ext' ext err s m jdg))
-> s
-> (s, ProofStateT a b err s m jdg)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (s, ProofStateT ext' ext err s m jdg)
s)
mapExtract a -> ext'
into ext -> b
out (Alt ProofStateT ext' ext err s m jdg
p1 ProofStateT ext' ext err s m jdg
p2) = ProofStateT a b err s m jdg
-> ProofStateT a b err s m jdg -> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Alt ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out ProofStateT ext' ext err s m jdg
p1) ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out ProofStateT ext' ext err s m jdg
p2)
mapExtract a -> ext'
into ext -> b
out (Interleave ProofStateT ext' ext err s m jdg
p1 ProofStateT ext' ext err s m jdg
p2) = ProofStateT a b err s m jdg
-> ProofStateT a b err s m jdg -> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Interleave ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out ProofStateT ext' ext err s m jdg
p1) ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out ProofStateT ext' ext err s m jdg
p2)
mapExtract a -> ext'
into ext -> b
out (Commit ProofStateT ext' ext err s m jdg
p1 ProofStateT ext' ext err s m jdg
p2) = ProofStateT a b err s m jdg
-> ProofStateT a b err s m jdg -> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Commit ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out ProofStateT ext' ext err s m jdg
p1) ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out ProofStateT ext' ext err s m jdg
p2)
mapExtract a -> ext'
_ ext -> b
_ ProofStateT ext' ext err s m jdg
Empty = ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
mapExtract a -> ext'
into ext -> b
out (Failure err
err ext' -> ProofStateT ext' ext err s m jdg
k) = err
-> (a -> ProofStateT a b err s m jdg)
-> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
err
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Failure err
err ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out (ProofStateT ext' ext err s m jdg -> ProofStateT a b err s m jdg)
-> (a -> ProofStateT ext' ext err s m jdg)
-> a
-> ProofStateT a b err s m jdg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ext' -> ProofStateT ext' ext err s m jdg
k (ext' -> ProofStateT ext' ext err s m jdg)
-> (a -> ext') -> a -> ProofStateT ext' ext err s m jdg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ext'
into)
mapExtract a -> ext'
into ext -> b
out (Handle ProofStateT ext' ext err s m jdg
p err -> m err
h) = ProofStateT a b err s m jdg
-> (err -> m err) -> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> (err -> m err) -> ProofStateT ext' ext err s m goal
Handle ((a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract a -> ext'
into ext -> b
out ProofStateT ext' ext err s m jdg
p) err -> m err
h
mapExtract a -> ext'
_ ext -> b
out (Axiom ext
ext) = b -> ProofStateT a b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom (ext -> b
out ext
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
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
speculate s
s = 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
s [] err -> m err
forall (f :: * -> *) a. Applicative f => a -> f a
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
-> [(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
s [(meta, jdg)]
goals err -> m err
_ (Subgoal jdg
goal ext -> ProofStateT ext ext err s m jdg
k) = m (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect (m (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
 -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> m (ProofStateT
        ext (Either err (Proof s meta jdg ext)) err s m x)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall a b. (a -> b) -> a -> b
$ do
          (s
s', (meta
meta, ext
h)) <- s -> m (s, (meta, ext))
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
s -> m (s, (meta, ext))
newHole s
s
          -- See Note [Handler Reset]
          ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> m (ProofStateT
        ext (Either err (Proof s meta jdg ext)) err s m x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
 -> m (ProofStateT
         ext (Either err (Proof s meta jdg ext)) err s m x))
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> m (ProofStateT
        ext (Either err (Proof s meta jdg ext)) err s m x)
forall a b. (a -> b) -> a -> b
$ 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
s' ([(meta, jdg)]
goals [(meta, jdg)] -> [(meta, jdg)] -> [(meta, jdg)]
forall a. [a] -> [a] -> [a]
++ [(meta
meta, jdg
goal)]) err -> m err
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ext -> ProofStateT ext ext err s m jdg
k ext
h)
      go s
s [(meta, jdg)]
goals err -> m err
handler (Effect m (ProofStateT ext ext err s m jdg)
m) = m (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect ((ProofStateT ext ext err s m jdg
 -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> m (ProofStateT ext ext err s m jdg)
-> m (ProofStateT
        ext (Either err (Proof s meta jdg ext)) err s m x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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
s [(meta, jdg)]
goals err -> m err
handler) m (ProofStateT ext ext err s m jdg)
m)
      go s
s [(meta, jdg)]
goals err -> m err
handler (Stateful s -> (s, ProofStateT ext ext err s m jdg)
st) =
          let (s
s', ProofStateT ext ext err s m jdg
p) = s -> (s, ProofStateT ext ext err s m jdg)
st s
s
          in 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
s' [(meta, jdg)]
goals err -> m err
handler ProofStateT ext ext err s m jdg
p
      go s
s [(meta, jdg)]
goals err -> m err
handler (Alt ProofStateT ext ext err s m jdg
p1 ProofStateT ext ext err s m jdg
p2) = ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Alt (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
s [(meta, jdg)]
goals err -> m err
handler ProofStateT ext ext err s m jdg
p1) (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
s [(meta, jdg)]
goals err -> m err
handler ProofStateT ext ext err s m jdg
p2)
      go s
s [(meta, jdg)]
goals err -> m err
handler (Interleave ProofStateT ext ext err s m jdg
p1 ProofStateT ext ext err s m jdg
p2) = ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Interleave (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
s [(meta, jdg)]
goals err -> m err
handler ProofStateT ext ext err s m jdg
p1) (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
s [(meta, jdg)]
goals err -> m err
handler ProofStateT ext ext err s m jdg
p2)
      go s
s [(meta, jdg)]
goals err -> m err
handler (Commit ProofStateT ext ext err s m jdg
p1 ProofStateT ext ext err s m jdg
p2) = ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
-> ProofStateT ext' ext err s m goal
Commit (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
s [(meta, jdg)]
goals err -> m err
handler ProofStateT ext ext err s m jdg
p1) (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
s [(meta, jdg)]
goals err -> m err
handler ProofStateT ext ext err s m jdg
p2)
      go s
_ [(meta, jdg)]
_     err -> m err
_       ProofStateT ext ext err s m jdg
Empty = ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
      go s
_ [(meta, jdg)]
_     err -> m err
handler (Failure err
err ext -> ProofStateT ext ext err s m jdg
_) = m (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect (m (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
 -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> m (ProofStateT
        ext (Either err (Proof s meta jdg ext)) err s m x)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall a b. (a -> b) -> a -> b
$ do
          err
annErr <- err -> m err
handler err
err
          ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> m (ProofStateT
        ext (Either err (Proof s meta jdg ext)) err s m x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
 -> m (ProofStateT
         ext (Either err (Proof s meta jdg ext)) err s m x))
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> m (ProofStateT
        ext (Either err (Proof s meta jdg ext)) err s m x)
forall a b. (a -> b) -> a -> b
$ Either err (Proof s meta jdg ext)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom (Either err (Proof s meta jdg ext)
 -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> Either err (Proof s meta jdg ext)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall a b. (a -> b) -> a -> b
$ err -> Either err (Proof s meta jdg ext)
forall a b. a -> Either a b
Left err
annErr
      go s
s [(meta, jdg)]
goals err -> m err
handler (Handle ProofStateT ext ext err s m jdg
p err -> m err
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.
          ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
-> (err -> m err)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
-> (err -> m err) -> ProofStateT ext' ext err s m goal
Handle (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
s [(meta, jdg)]
goals (err -> m err
h (err -> m err) -> (err -> m err) -> err -> m err
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> err -> m err
handler) ProofStateT ext ext err s m jdg
p) err -> m err
h
      go s
s [(meta, jdg)]
goals err -> m err
_       (Axiom ext
ext) = Either err (Proof s meta jdg ext)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom (Either err (Proof s meta jdg ext)
 -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x)
-> Either err (Proof s meta jdg ext)
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m x
forall a b. (a -> b) -> a -> b
$ Proof s meta jdg ext -> Either err (Proof s meta jdg ext)
forall a b. b -> Either a b
Right (ext -> s -> [(meta, jdg)] -> Proof s meta jdg ext
forall s meta goal ext.
ext -> s -> [(meta, goal)] -> Proof s meta goal ext
Proof ext
ext s
s [(meta, jdg)]
goals)