{-# LANGUAGE RankNTypes #-}

------------------------------------------------------------------------------
-- | Things that belong in the future release of refinery v5.
module Refinery.Future
  ( runStreamingTacticT
  , hoistListT
  , consume
  ) where

import Control.Applicative
import Control.Monad (ap, (>=>))
import Control.Monad.State.Lazy (runStateT)
import Control.Monad.Trans
import Data.Either (isRight)
import Data.Functor ((<&>))
import Data.Tuple (swap)
import Refinery.ProofState
import Refinery.Tactic.Internal



hoistElem :: Functor m => (forall x. m x -> n x) -> Elem m a -> Elem n a
hoistElem :: (forall x. m x -> n x) -> Elem m a -> Elem n a
hoistElem forall x. m x -> n x
_ Elem m a
Done = Elem n a
forall (m :: * -> *) a. Elem m a
Done
hoistElem forall x. m x -> n x
f (Next a
a ListT m a
lt) = a -> ListT n a -> Elem n a
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next a
a (ListT n a -> Elem n a) -> ListT n a -> Elem n a
forall a b. (a -> b) -> a -> b
$ (forall x. m x -> n x) -> ListT m a -> ListT n a
forall (m :: * -> *) (n :: * -> *) a.
Functor m =>
(forall x. m x -> n x) -> ListT m a -> ListT n a
hoistListT forall x. m x -> n x
f ListT m a
lt


hoistListT :: Functor m => (forall x. m x -> n x) -> ListT m a -> ListT n a
hoistListT :: (forall x. m x -> n x) -> ListT m a -> ListT n a
hoistListT forall x. m x -> n x
f ListT m a
t = n (Elem n a) -> ListT n a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (n (Elem n a) -> ListT n a) -> n (Elem n a) -> ListT n a
forall a b. (a -> b) -> a -> b
$ m (Elem n a) -> n (Elem n a)
forall x. m x -> n x
f (m (Elem n a) -> n (Elem n a)) -> m (Elem n a) -> n (Elem n a)
forall a b. (a -> b) -> a -> b
$ (Elem m a -> Elem n a) -> m (Elem m a) -> m (Elem n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall x. m x -> n x) -> Elem m a -> Elem n a
forall (m :: * -> *) (n :: * -> *) a.
Functor m =>
(forall x. m x -> n x) -> Elem m a -> Elem n a
hoistElem forall x. m x -> n x
f) (m (Elem m a) -> m (Elem n a)) -> m (Elem m a) -> m (Elem n a)
forall a b. (a -> b) -> a -> b
$ ListT m a -> m (Elem m a)
forall (m :: * -> *) a. ListT m a -> m (Elem m a)
unListT ListT m a
t


consume :: Monad m => ListT m a -> (a -> m ()) -> m ()
consume :: ListT m a -> (a -> m ()) -> m ()
consume ListT m a
lt a -> m ()
f = ListT m a -> m (Elem m a)
forall (m :: * -> *) a. ListT m a -> m (Elem m a)
unListT ListT m a
lt m (Elem m a) -> (Elem m a -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Elem m a
Done -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Next a
a ListT m a
lt' -> a -> m ()
f a
a m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ListT m a -> (a -> m ()) -> m ()
forall (m :: * -> *) a. Monad m => ListT m a -> (a -> m ()) -> m ()
consume ListT m a
lt' a -> m ()
f


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

runStreamingTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> ListT m (Either err (Proof s meta jdg ext))
runStreamingTacticT :: TacticT jdg ext err s m ()
-> jdg -> s -> ListT m (Either err (Proof s meta jdg ext))
runStreamingTacticT TacticT jdg ext err s m ()
t jdg
j s
s = s
-> ProofStateT ext ext err s m jdg
-> ListT m (Either err (Proof s meta jdg ext))
forall ext err s (m :: * -> *) goal meta.
MonadExtract meta ext err s m =>
s
-> ProofStateT ext ext err s m goal
-> ListT m (Either err (Proof s meta goal ext))
streamProofs s
s (ProofStateT ext ext err s m jdg
 -> ListT m (Either err (Proof s meta jdg ext)))
-> ProofStateT ext ext err s m jdg
-> ListT m (Either err (Proof s meta jdg ext))
forall a b. (a -> b) -> a -> b
$ (((), jdg) -> jdg)
-> ProofStateT ext ext err s m ((), jdg)
-> ProofStateT ext ext err s m jdg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), jdg) -> jdg
forall a b. (a, b) -> b
snd (ProofStateT ext ext err s m ((), jdg)
 -> ProofStateT ext ext err s m jdg)
-> ProofStateT ext ext err s m ((), jdg)
-> ProofStateT ext ext err s m jdg
forall a b. (a -> b) -> a -> b
$ TacticT jdg ext err s m ()
-> jdg -> ProofStateT ext ext err s m ((), jdg)
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, jdg)
proofState TacticT jdg ext err s m ()
t jdg
j

data Elem m a
    = Done
    | Next a (ListT m a)
    deriving stock a -> Elem m b -> Elem m a
(a -> b) -> Elem m a -> Elem m b
(forall a b. (a -> b) -> Elem m a -> Elem m b)
-> (forall a b. a -> Elem m b -> Elem m a) -> Functor (Elem m)
forall a b. a -> Elem m b -> Elem m a
forall a b. (a -> b) -> Elem m a -> Elem m b
forall (m :: * -> *) a b. Functor m => a -> Elem m b -> Elem m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> Elem m a -> Elem m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Elem m b -> Elem m a
$c<$ :: forall (m :: * -> *) a b. Functor m => a -> Elem m b -> Elem m a
fmap :: (a -> b) -> Elem m a -> Elem m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> Elem m a -> Elem m b
Functor


point :: Applicative m => a -> Elem m a
point :: a -> Elem m a
point a
a = a -> ListT m a -> Elem m a
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next a
a (ListT m a -> Elem m a) -> ListT m a -> Elem m a
forall a b. (a -> b) -> a -> b
$ m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m a) -> ListT m a) -> m (Elem m a) -> ListT m a
forall a b. (a -> b) -> a -> b
$ Elem m a -> m (Elem m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elem m a
forall (m :: * -> *) a. Elem m a
Done

newtype ListT m a = ListT { ListT m a -> m (Elem m a)
unListT :: m (Elem m a) }

cons :: (Applicative m) => a -> ListT m a -> ListT m a
cons :: a -> ListT m a -> ListT m a
cons a
x ListT m a
xs = m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m a) -> ListT m a) -> m (Elem m a) -> ListT m a
forall a b. (a -> b) -> a -> b
$ Elem m a -> m (Elem m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elem m a -> m (Elem m a)) -> Elem m a -> m (Elem m a)
forall a b. (a -> b) -> a -> b
$ a -> ListT m a -> Elem m a
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next a
x ListT m a
xs

instance Functor m => Functor (ListT m) where
    fmap :: (a -> b) -> ListT m a -> ListT m b
fmap a -> b
f (ListT m (Elem m a)
xs) = m (Elem m b) -> ListT m b
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m b) -> ListT m b) -> m (Elem m b) -> ListT m b
forall a b. (a -> b) -> a -> b
$ m (Elem m a)
xs m (Elem m a) -> (Elem m a -> Elem m b) -> m (Elem m b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
        Elem m a
Done -> Elem m b
forall (m :: * -> *) a. Elem m a
Done
        Next a
a ListT m a
xs -> b -> ListT m b -> Elem m b
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next (a -> b
f a
a) ((a -> b) -> ListT m a -> ListT m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ListT m a
xs)

instance (Monad m) => Applicative (ListT m) where
    pure :: a -> ListT m a
pure = a -> ListT m a
forall (m :: * -> *) a. Monad m => a -> m a
return
    <*> :: ListT m (a -> b) -> ListT m a -> ListT m b
(<*>) = ListT m (a -> b) -> ListT m a -> ListT m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (Monad m) => Alternative (ListT m) where
    empty :: ListT m a
empty = m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m a) -> ListT m a) -> m (Elem m a) -> ListT m a
forall a b. (a -> b) -> a -> b
$ Elem m a -> m (Elem m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elem m a
forall (m :: * -> *) a. Elem m a
Done
    (ListT m (Elem m a)
xs) <|> :: ListT m a -> ListT m a -> ListT m a
<|> (ListT m (Elem m a)
ys) =
        m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m a) -> ListT m a) -> m (Elem m a) -> ListT m a
forall a b. (a -> b) -> a -> b
$ m (Elem m a)
xs m (Elem m a) -> (Elem m a -> m (Elem m a)) -> m (Elem m a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Elem m a
Done -> m (Elem m a)
ys
          Next a
x ListT m a
xs -> Elem m a -> m (Elem m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> ListT m a -> Elem m a
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next a
x (ListT m a
xs ListT m a -> ListT m a -> ListT m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT m (Elem m a)
ys))

instance (Monad m) => Monad (ListT m) where
    return :: a -> ListT m a
return a
a = a -> ListT m a -> ListT m a
forall (m :: * -> *) a.
Applicative m =>
a -> ListT m a -> ListT m a
cons a
a ListT m a
forall (f :: * -> *) a. Alternative f => f a
empty
    (ListT m (Elem m a)
xs) >>= :: ListT m a -> (a -> ListT m b) -> ListT m b
>>= a -> ListT m b
k =
        m (Elem m b) -> ListT m b
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m b) -> ListT m b) -> m (Elem m b) -> ListT m b
forall a b. (a -> b) -> a -> b
$ m (Elem m a)
xs m (Elem m a) -> (Elem m a -> m (Elem m b)) -> m (Elem m b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Elem m a
Done -> Elem m b -> m (Elem m b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elem m b
forall (m :: * -> *) a. Elem m a
Done
          Next a
x ListT m a
xs -> ListT m b -> m (Elem m b)
forall (m :: * -> *) a. ListT m a -> m (Elem m a)
unListT (ListT m b -> m (Elem m b)) -> ListT m b -> m (Elem m b)
forall a b. (a -> b) -> a -> b
$ a -> ListT m b
k a
x ListT m b -> ListT m b -> ListT m b
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ListT m a
xs ListT m a -> (a -> ListT m b) -> ListT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ListT m b
k)


instance MonadTrans ListT where
    lift :: m a -> ListT m a
lift m a
m = m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m a) -> ListT m a) -> m (Elem m a) -> ListT m a
forall a b. (a -> b) -> a -> b
$ (a -> Elem m a) -> m a -> m (Elem m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
x -> a -> ListT m a -> Elem m a
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next a
x ListT m a
forall (f :: * -> *) a. Alternative f => f a
empty) m a
m


interleaveT :: (Monad m) => Elem m a -> Elem m a -> Elem m a
interleaveT :: Elem m a -> Elem m a -> Elem m a
interleaveT Elem m a
xs Elem m a
ys =
    case Elem m a
xs of
      Elem m a
Done -> Elem m a
ys
      Next a
x ListT m a
xs -> a -> ListT m a -> Elem m a
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next a
x (ListT m a -> Elem m a) -> ListT m a -> Elem m a
forall a b. (a -> b) -> a -> b
$ m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m a) -> ListT m a) -> m (Elem m a) -> ListT m a
forall a b. (a -> b) -> a -> b
$ (Elem m a -> Elem m a) -> m (Elem m a) -> m (Elem m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Elem m a -> Elem m a -> Elem m a
forall (m :: * -> *) a. Monad m => Elem m a -> Elem m a -> Elem m a
interleaveT Elem m a
ys) (m (Elem m a) -> m (Elem m a)) -> m (Elem m a) -> m (Elem m a)
forall a b. (a -> b) -> a -> b
$ ListT m a -> m (Elem m a)
forall (m :: * -> *) a. ListT m a -> m (Elem m a)
unListT ListT m a
xs

--         ys <&> \case
--           Done -> Next x xs
--           Next y ys -> Next x (cons y (interleaveT xs ys))

force :: (Monad m) => Elem m a -> m [a]
force :: Elem m a -> m [a]
force = \case
    Elem m a
Done -> [a] -> m [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    Next a
x ListT m a
xs' -> (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ListT m a -> m (Elem m a)
forall (m :: * -> *) a. ListT m a -> m (Elem m a)
unListT ListT m a
xs' m (Elem m a) -> (Elem m a -> m [a]) -> m [a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Elem m a -> m [a]
forall (m :: * -> *) a. Monad m => Elem m a -> m [a]
force)

ofList :: Monad m => [a] -> Elem m a
ofList :: [a] -> Elem m a
ofList [] = Elem m a
forall (m :: * -> *) a. Elem m a
Done
ofList (a
x:[a]
xs) = a -> ListT m a -> Elem m a
forall (m :: * -> *) a. a -> ListT m a -> Elem m a
Next a
x (ListT m a -> Elem m a) -> ListT m a -> Elem m a
forall a b. (a -> b) -> a -> b
$ m (Elem m a) -> ListT m a
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m a) -> ListT m a) -> m (Elem m a) -> ListT m a
forall a b. (a -> b) -> a -> b
$ Elem m a -> m (Elem m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elem m a -> m (Elem m a)) -> Elem m a -> m (Elem m a)
forall a b. (a -> b) -> a -> b
$ [a] -> Elem m a
forall (m :: * -> *) a. Monad m => [a] -> Elem m a
ofList [a]
xs

streamProofs :: forall ext err s m goal meta. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m goal -> ListT m (Either err (Proof s meta goal ext))
streamProofs :: s
-> ProofStateT ext ext err s m goal
-> ListT m (Either err (Proof s meta goal ext))
streamProofs s
s ProofStateT ext ext err s m goal
p = m (Elem m (Either err (Proof s meta goal ext)))
-> ListT m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (m (Elem m (Either err (Proof s meta goal ext)))
 -> ListT m (Either err (Proof s meta goal ext)))
-> m (Elem m (Either err (Proof s meta goal ext)))
-> ListT m (Either err (Proof s meta goal ext))
forall a b. (a -> b) -> a -> b
$ s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Elem 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 (Elem m (Either err (Proof s meta goal ext)))
      go :: s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Elem 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 (Elem 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 (Elem m (Either err (Proof s meta goal ext))))
-> ProofStateT ext ext err s m goal
-> m (Elem 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 (Elem m (Either err (Proof s meta goal ext))))
-> m (Elem 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 (Elem 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 (Elem 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) =
          ListT m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall (m :: * -> *) a. ListT m a -> m (Elem m a)
unListT (ListT m (Either err (Proof s meta goal ext))
 -> m (Elem m (Either err (Proof s meta goal ext))))
-> ListT m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall a b. (a -> b) -> a -> b
$ m (Elem m (Either err (Proof s meta goal ext)))
-> ListT m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Elem 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) ListT m (Either err (Proof s meta goal ext))
-> ListT m (Either err (Proof s meta goal ext))
-> ListT m (Either err (Proof s meta goal ext))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m (Elem m (Either err (Proof s meta goal ext)))
-> ListT m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. m (Elem m a) -> ListT m a
ListT (s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Elem 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) =
          Elem m (Either err (Proof s meta goal ext))
-> Elem m (Either err (Proof s meta goal ext))
-> Elem m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. Monad m => Elem m a -> Elem m a -> Elem m a
interleaveT (Elem m (Either err (Proof s meta goal ext))
 -> Elem m (Either err (Proof s meta goal ext))
 -> Elem m (Either err (Proof s meta goal ext)))
-> m (Elem m (Either err (Proof s meta goal ext)))
-> m (Elem m (Either err (Proof s meta goal ext))
      -> Elem 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 (Elem 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 (Elem m (Either err (Proof s meta goal ext))
   -> Elem m (Either err (Proof s meta goal ext)))
-> m (Elem m (Either err (Proof s meta goal ext)))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Elem 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) = do
          [Either err (Proof s meta goal ext)]
solns <- Elem m (Either err (Proof s meta goal ext))
-> m [Either err (Proof s meta goal ext)]
forall (m :: * -> *) a. Monad m => Elem m a -> m [a]
force (Elem m (Either err (Proof s meta goal ext))
 -> m [Either err (Proof s meta goal ext)])
-> m (Elem m (Either err (Proof s meta goal ext)))
-> m [Either err (Proof s meta goal ext)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Elem 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
          if (Either err (Proof s meta goal ext) -> Bool)
-> [Either err (Proof s meta goal ext)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Either err (Proof s meta goal ext) -> Bool
forall a b. Either a b -> Bool
isRight [Either err (Proof s meta goal ext)]
solns then Elem m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elem m (Either err (Proof s meta goal ext))
 -> m (Elem m (Either err (Proof s meta goal ext))))
-> Elem m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall a b. (a -> b) -> a -> b
$ [Either err (Proof s meta goal ext)]
-> Elem m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. Monad m => [a] -> Elem m a
ofList [Either err (Proof s meta goal ext)]
solns else s
-> [(meta, goal)]
-> (err -> m err)
-> ProofStateT ext ext err s m goal
-> m (Elem 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 = Elem m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elem m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. Elem m a
Done
      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
          Elem m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elem m (Either err (Proof s meta goal ext))
 -> m (Elem m (Either err (Proof s meta goal ext))))
-> Elem m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall a b. (a -> b) -> a -> b
$ Either err (Proof s meta goal ext)
-> Elem m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. Applicative m => a -> Elem m a
point (Either err (Proof s meta goal ext)
 -> Elem m (Either err (Proof s meta goal ext)))
-> Either err (Proof s meta goal ext)
-> Elem 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 (Elem 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) = Elem m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elem m (Either err (Proof s meta goal ext))
 -> m (Elem m (Either err (Proof s meta goal ext))))
-> Elem m (Either err (Proof s meta goal ext))
-> m (Elem m (Either err (Proof s meta goal ext)))
forall a b. (a -> b) -> a -> b
$ Either err (Proof s meta goal ext)
-> Elem m (Either err (Proof s meta goal ext))
forall (m :: * -> *) a. Applicative m => a -> Elem m a
point (Either err (Proof s meta goal ext)
 -> Elem m (Either err (Proof s meta goal ext)))
-> Either err (Proof s meta goal ext)
-> Elem 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 (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)