{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Refinery.Tactic.Internal
-- Copyright   :  (c) Reed Mullanix 2019
-- License     :  BSD-style
-- Maintainer  :  reedmullanix@gmail.com
--
--
-- = WARNING
-- This module is considered __internal__, and can
-- change at any given time.
module Refinery.Tactic.Internal
  ( TacticT(..)
  , tactic
  , proofState
  , proofState_
  , mapTacticT
  -- * Rules
  , RuleT(..)
  , subgoal
  , unsolvable
  )
where

import GHC.Generics
import Control.Applicative
import Control.Monad.Identity
import Control.Monad.Except
import Control.Monad.Catch
import Control.Monad.State.Strict
import Control.Monad.Trans ()
import Control.Monad.IO.Class ()
import Control.Monad.Morph

import Data.Coerce

import Refinery.ProofState

-- | A @'TacticT'@ is a monad transformer that performs proof refinement.
-- The type variables signifiy:
--
-- * @jdg@ - The goal type. This is the thing we are trying to construct a proof of.
-- * @ext@ - The extract type. This is what we will recieve after running the tactic.
-- * @err@ - The error type. We can use 'throwError' to abort the computation with a provided error
-- * @s@   - The state type.
-- * @m@   - The base monad.
-- * @a@   - The return value. This to make @'TacticT'@ a monad, and will always be @'Prelude.()'@
--
-- One of the most important things about this type is it's 'Monad' instance. @t1 >> t2@
-- Will execute @t1@ against the current goal, and then execute @t2@ on _all_ of the subgoals generated
-- by @t2@.
--
-- This Monad instance is lawful, and has been tested thouroughly, and a version of it has been formally verified in Agda.
-- _However_, just because it is correct doesn't mean that it lines up with your intuitions of how Monads behave!
-- In practice, it feels like a combination of the Non-Determinisitic Monads and some of the Time Travelling ones.
-- That doesn't mean that it's impossible to understand, just that it may push the boundaries of you intuitions.
newtype TacticT jdg ext err s m a = TacticT { TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT :: StateT jdg (ProofStateT ext ext err s m) a }
  deriving ( a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
(a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
(forall a b.
 (a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b)
-> (forall a b.
    a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a)
-> Functor (TacticT jdg ext err s m)
forall a b.
a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
forall a b.
(a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
forall jdg ext err s (m :: * -> *) a b.
Functor m =>
a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a b.
Functor m =>
(a -> b) -> TacticT jdg ext err s m a -> TacticT jdg 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 -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
$c<$ :: forall jdg ext err s (m :: * -> *) a b.
Functor m =>
a -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
fmap :: (a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
$cfmap :: forall jdg ext err s (m :: * -> *) a b.
Functor m =>
(a -> b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
Functor
           , Functor (TacticT jdg ext err s m)
a -> TacticT jdg ext err s m a
Functor (TacticT jdg ext err s m)
-> (forall a. a -> TacticT jdg ext err s m a)
-> (forall a b.
    TacticT jdg ext err s m (a -> b)
    -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b)
-> (forall a b c.
    (a -> b -> c)
    -> TacticT jdg ext err s m a
    -> TacticT jdg ext err s m b
    -> TacticT jdg ext err s m c)
-> (forall a b.
    TacticT jdg ext err s m a
    -> TacticT jdg ext err s m b -> TacticT jdg ext err s m b)
-> (forall a b.
    TacticT jdg ext err s m a
    -> TacticT jdg ext err s m b -> TacticT jdg ext err s m a)
-> Applicative (TacticT jdg ext err s m)
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
TacticT jdg ext err s m (a -> b)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
(a -> b -> c)
-> TacticT jdg ext err s m a
-> TacticT jdg ext err s m b
-> TacticT jdg ext err s m c
forall a. a -> TacticT jdg ext err s m a
forall a b.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
forall a b.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
forall a b.
TacticT jdg ext err s m (a -> b)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
forall a b c.
(a -> b -> c)
-> TacticT jdg ext err s m a
-> TacticT jdg ext err s m b
-> TacticT jdg ext err s m c
forall jdg ext err s (m :: * -> *).
Functor m =>
Functor (TacticT jdg ext err s m)
forall jdg ext err s (m :: * -> *) a.
Functor m =>
a -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m (a -> b)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
forall jdg ext err s (m :: * -> *) a b c.
Functor m =>
(a -> b -> c)
-> TacticT jdg ext err s m a
-> TacticT jdg ext err s m b
-> TacticT jdg ext err s m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
$c<* :: forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m a
*> :: TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
$c*> :: forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
liftA2 :: (a -> b -> c)
-> TacticT jdg ext err s m a
-> TacticT jdg ext err s m b
-> TacticT jdg ext err s m c
$cliftA2 :: forall jdg ext err s (m :: * -> *) a b c.
Functor m =>
(a -> b -> c)
-> TacticT jdg ext err s m a
-> TacticT jdg ext err s m b
-> TacticT jdg ext err s m c
<*> :: TacticT jdg ext err s m (a -> b)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
$c<*> :: forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m (a -> b)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
pure :: a -> TacticT jdg ext err s m a
$cpure :: forall jdg ext err s (m :: * -> *) a.
Functor m =>
a -> TacticT jdg ext err s m a
$cp1Applicative :: forall jdg ext err s (m :: * -> *).
Functor m =>
Functor (TacticT jdg ext err s m)
Applicative
           , Applicative (TacticT jdg ext err s m)
TacticT jdg ext err s m a
Applicative (TacticT jdg ext err s m)
-> (forall a. TacticT jdg ext err s m a)
-> (forall a.
    TacticT jdg ext err s m a
    -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a)
-> (forall a.
    TacticT jdg ext err s m a -> TacticT jdg ext err s m [a])
-> (forall a.
    TacticT jdg ext err s m a -> TacticT jdg ext err s m [a])
-> Alternative (TacticT jdg ext err s m)
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
forall a. TacticT jdg ext err s m a
forall a. TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
forall a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *).
Monad m =>
Applicative (TacticT jdg ext err s m)
forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
many :: TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
$cmany :: forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
some :: TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
$csome :: forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a -> TacticT jdg ext err s m [a]
<|> :: TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
$c<|> :: forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
empty :: TacticT jdg ext err s m a
$cempty :: forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
$cp1Alternative :: forall jdg ext err s (m :: * -> *).
Monad m =>
Applicative (TacticT jdg ext err s m)
Alternative
           , Applicative (TacticT jdg ext err s m)
a -> TacticT jdg ext err s m a
Applicative (TacticT jdg ext err s m)
-> (forall a b.
    TacticT jdg ext err s m a
    -> (a -> TacticT jdg ext err s m b) -> TacticT jdg ext err s m b)
-> (forall a b.
    TacticT jdg ext err s m a
    -> TacticT jdg ext err s m b -> TacticT jdg ext err s m b)
-> (forall a. a -> TacticT jdg ext err s m a)
-> Monad (TacticT jdg ext err s m)
TacticT jdg ext err s m a
-> (a -> TacticT jdg ext err s m b) -> TacticT jdg ext err s m b
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
forall a. a -> TacticT jdg ext err s m a
forall a b.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
forall a b.
TacticT jdg ext err s m a
-> (a -> TacticT jdg ext err s m b) -> TacticT jdg ext err s m b
forall jdg ext err s (m :: * -> *).
Functor m =>
Applicative (TacticT jdg ext err s m)
forall jdg ext err s (m :: * -> *) a.
Functor m =>
a -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> (a -> TacticT jdg ext err s m b) -> TacticT jdg ext err s m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> TacticT jdg ext err s m a
$creturn :: forall jdg ext err s (m :: * -> *) a.
Functor m =>
a -> TacticT jdg ext err s m a
>> :: TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
$c>> :: forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m b -> TacticT jdg ext err s m b
>>= :: TacticT jdg ext err s m a
-> (a -> TacticT jdg ext err s m b) -> TacticT jdg ext err s m b
$c>>= :: forall jdg ext err s (m :: * -> *) a b.
Functor m =>
TacticT jdg ext err s m a
-> (a -> TacticT jdg ext err s m b) -> TacticT jdg ext err s m b
$cp1Monad :: forall jdg ext err s (m :: * -> *).
Functor m =>
Applicative (TacticT jdg ext err s m)
Monad
           , Monad (TacticT jdg ext err s m)
Alternative (TacticT jdg ext err s m)
TacticT jdg ext err s m a
Alternative (TacticT jdg ext err s m)
-> Monad (TacticT jdg ext err s m)
-> (forall a. TacticT jdg ext err s m a)
-> (forall a.
    TacticT jdg ext err s m a
    -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a)
-> MonadPlus (TacticT jdg ext err s m)
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
forall a. TacticT jdg ext err s m a
forall a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *).
Monad m =>
Monad (TacticT jdg ext err s m)
forall jdg ext err s (m :: * -> *).
Monad m =>
Alternative (TacticT jdg ext err s m)
forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
mplus :: TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
$cmplus :: forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
mzero :: TacticT jdg ext err s m a
$cmzero :: forall jdg ext err s (m :: * -> *) a.
Monad m =>
TacticT jdg ext err s m a
$cp2MonadPlus :: forall jdg ext err s (m :: * -> *).
Monad m =>
Monad (TacticT jdg ext err s m)
$cp1MonadPlus :: forall jdg ext err s (m :: * -> *).
Monad m =>
Alternative (TacticT jdg ext err s m)
MonadPlus
           , Monad (TacticT jdg ext err s m)
Monad (TacticT jdg ext err s m)
-> (forall a. IO a -> TacticT jdg ext err s m a)
-> MonadIO (TacticT jdg ext err s m)
IO a -> TacticT jdg ext err s m a
forall a. IO a -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *).
MonadIO m =>
Monad (TacticT jdg ext err s m)
forall jdg ext err s (m :: * -> *) a.
MonadIO m =>
IO a -> TacticT jdg ext err s m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> TacticT jdg ext err s m a
$cliftIO :: forall jdg ext err s (m :: * -> *) a.
MonadIO m =>
IO a -> TacticT jdg ext err s m a
$cp1MonadIO :: forall jdg ext err s (m :: * -> *).
MonadIO m =>
Monad (TacticT jdg ext err s m)
MonadIO
           , Monad (TacticT jdg ext err s m)
e -> TacticT jdg ext err s m a
Monad (TacticT jdg ext err s m)
-> (forall e a. Exception e => e -> TacticT jdg ext err s m a)
-> MonadThrow (TacticT jdg ext err s m)
forall e a. Exception e => e -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *).
MonadThrow m =>
Monad (TacticT jdg ext err s m)
forall jdg ext err s (m :: * -> *) e a.
(MonadThrow m, Exception e) =>
e -> TacticT jdg ext err s m a
forall (m :: * -> *).
Monad m -> (forall e a. Exception e => e -> m a) -> MonadThrow m
throwM :: e -> TacticT jdg ext err s m a
$cthrowM :: forall jdg ext err s (m :: * -> *) e a.
(MonadThrow m, Exception e) =>
e -> TacticT jdg ext err s m a
$cp1MonadThrow :: forall jdg ext err s (m :: * -> *).
MonadThrow m =>
Monad (TacticT jdg ext err s m)
MonadThrow
           , (forall x.
 TacticT jdg ext err s m a -> Rep (TacticT jdg ext err s m a) x)
-> (forall x.
    Rep (TacticT jdg ext err s m a) x -> TacticT jdg ext err s m a)
-> Generic (TacticT jdg ext err s m a)
forall x.
Rep (TacticT jdg ext err s m a) x -> TacticT jdg ext err s m a
forall x.
TacticT jdg ext err s m a -> Rep (TacticT jdg ext err s m a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall jdg ext err s (m :: * -> *) a x.
Rep (TacticT jdg ext err s m a) x -> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a x.
TacticT jdg ext err s m a -> Rep (TacticT jdg ext err s m a) x
$cto :: forall jdg ext err s (m :: * -> *) a x.
Rep (TacticT jdg ext err s m a) x -> TacticT jdg ext err s m a
$cfrom :: forall jdg ext err s (m :: * -> *) a x.
TacticT jdg ext err s m a -> Rep (TacticT jdg ext err s m a) x
Generic
           )

instance (Monoid jdg, Show a, Show jdg, Show err, Show ext, Show (m (ProofStateT ext ext err s m (a, jdg)))) => Show (TacticT jdg ext err s m a) where
  show :: TacticT jdg ext err s m a -> String
show = ProofStateT ext ext err s m (a, jdg) -> String
forall a. Show a => a -> String
show (ProofStateT ext ext err s m (a, jdg) -> String)
-> (TacticT jdg ext err s m a
    -> ProofStateT ext ext err s m (a, jdg))
-> TacticT jdg ext err s m a
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT jdg (ProofStateT ext ext err s m) a
 -> jdg -> ProofStateT ext ext err s m (a, jdg))
-> jdg
-> StateT jdg (ProofStateT ext ext err s m) a
-> ProofStateT ext ext err s m (a, jdg)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT jdg (ProofStateT ext ext err s m) a
-> jdg -> ProofStateT ext ext err s m (a, jdg)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT jdg
forall a. Monoid a => a
mempty (StateT jdg (ProofStateT ext ext err s m) a
 -> ProofStateT ext ext err s m (a, jdg))
-> (TacticT jdg ext err s m a
    -> StateT jdg (ProofStateT ext ext err s m) a)
-> TacticT jdg ext err s m a
-> ProofStateT ext ext err s m (a, jdg)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT

-- | Helper function for producing a tactic.
tactic :: (jdg -> ProofStateT ext ext err s m (a, jdg)) -> TacticT jdg ext err s m a
tactic :: (jdg -> ProofStateT ext ext err s m (a, jdg))
-> TacticT jdg ext err s m a
tactic jdg -> ProofStateT ext ext err s m (a, jdg)
t = StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT jdg (ProofStateT ext ext err s m) a
 -> TacticT jdg ext err s m a)
-> StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
forall a b. (a -> b) -> a -> b
$ (jdg -> ProofStateT ext ext err s m (a, jdg))
-> StateT jdg (ProofStateT ext ext err s m) a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT jdg -> ProofStateT ext ext err s m (a, jdg)
t

-- | @proofState t j@ will deconstruct a tactic @t@ into a 'ProofStateT' by running it at @j@.
proofState :: TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m (a, jdg)
proofState :: TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, jdg)
proofState TacticT jdg ext err s m a
t jdg
j = StateT jdg (ProofStateT ext ext err s m) a
-> jdg -> ProofStateT ext ext err s m (a, jdg)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT TacticT jdg ext err s m a
t) jdg
j

-- | Like 'proofState', but we discard the return value of @t@.
proofState_ :: (Functor m) => TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg
proofState_ :: TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg
proofState_ TacticT jdg ext err s m a
t jdg
j = StateT jdg (ProofStateT ext ext err s m) a
-> jdg -> ProofStateT ext ext err s m jdg
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT TacticT jdg ext err s m a
t) jdg
j

-- | Map the unwrapped computation using the given function
mapTacticT :: (Monad m) => (m a -> m b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
mapTacticT :: (m a -> m b)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
mapTacticT m a -> m b
f (TacticT StateT jdg (ProofStateT ext ext err s m) a
m) = StateT jdg (ProofStateT ext ext err s m) b
-> TacticT jdg ext err s m b
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT jdg (ProofStateT ext ext err s m) b
 -> TacticT jdg ext err s m b)
-> StateT jdg (ProofStateT ext ext err s m) b
-> TacticT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ StateT jdg (ProofStateT ext ext err s m) a
m StateT jdg (ProofStateT ext ext err s m) a
-> (a -> StateT jdg (ProofStateT ext ext err s m) b)
-> StateT jdg (ProofStateT ext ext err s m) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ProofStateT ext ext err s m b
-> StateT jdg (ProofStateT ext ext err s m) b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProofStateT ext ext err s m b
 -> StateT jdg (ProofStateT ext ext err s m) b)
-> (a -> ProofStateT ext ext err s m b)
-> a
-> StateT jdg (ProofStateT ext ext err s m) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m b -> ProofStateT ext ext err s m b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m b -> ProofStateT ext ext err s m b)
-> (a -> m b) -> a -> ProofStateT ext ext err s m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m b
f (m a -> m b) -> (a -> m a) -> a -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return)

instance MFunctor (TacticT jdg ext err s) where
  hoist :: (forall a. m a -> n a)
-> TacticT jdg ext err s m b -> TacticT jdg ext err s n b
hoist forall a. m a -> n a
f = StateT jdg (ProofStateT ext ext err s n) b
-> TacticT jdg ext err s n b
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT jdg (ProofStateT ext ext err s n) b
 -> TacticT jdg ext err s n b)
-> (TacticT jdg ext err s m b
    -> StateT jdg (ProofStateT ext ext err s n) b)
-> TacticT jdg ext err s m b
-> TacticT jdg ext err s n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((forall a.
 ProofStateT ext ext err s m a -> ProofStateT ext ext err s n a)
-> StateT jdg (ProofStateT ext ext err s m) b
-> StateT jdg (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)
-> ProofStateT ext ext err s m a -> ProofStateT ext ext err s n a
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
f)) (StateT jdg (ProofStateT ext ext err s m) b
 -> StateT jdg (ProofStateT ext ext err s n) b)
-> (TacticT jdg ext err s m b
    -> StateT jdg (ProofStateT ext ext err s m) b)
-> TacticT jdg ext err s m b
-> StateT jdg (ProofStateT ext ext err s n) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticT jdg ext err s m b
-> StateT jdg (ProofStateT ext ext err s m) b
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT

instance MonadTrans (TacticT jdg ext err s) where
  lift :: m a -> TacticT jdg ext err s m a
lift m a
m = StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT jdg (ProofStateT ext ext err s m) a
 -> TacticT jdg ext err s m a)
-> StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
forall a b. (a -> b) -> a -> b
$ ProofStateT ext ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProofStateT ext ext err s m a
 -> StateT jdg (ProofStateT ext ext err s m) a)
-> ProofStateT ext ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
forall a b. (a -> b) -> a -> b
$ 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
m


instance (Monad m) => MonadState s (TacticT jdg ext err s m) where
    state :: (s -> (a, s)) -> TacticT jdg ext err s m a
state s -> (a, s)
f = (jdg -> ProofStateT ext ext err s m (a, jdg))
-> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
(jdg -> ProofStateT ext ext err s m (a, jdg))
-> TacticT jdg ext err s m a
tactic ((jdg -> ProofStateT ext ext err s m (a, jdg))
 -> TacticT jdg ext err s m a)
-> (jdg -> ProofStateT ext ext err s m (a, jdg))
-> TacticT jdg ext err s m a
forall a b. (a -> b) -> a -> b
$ \jdg
j -> (a -> (a, jdg))
-> ProofStateT ext ext err s m a
-> ProofStateT ext ext err s m (a, jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,jdg
j) (ProofStateT ext ext err s m a
 -> ProofStateT ext ext err s m (a, jdg))
-> ProofStateT ext ext err s m a
-> ProofStateT ext ext err s m (a, jdg)
forall a b. (a -> b) -> a -> b
$ (s -> (a, s)) -> ProofStateT ext ext err s m a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state s -> (a, s)
f

-- | A @'RuleT'@ is a monad transformer for creating inference rules.
newtype RuleT jdg ext err s m a = RuleT
  { RuleT jdg ext err s m a -> ProofStateT ext a err s m jdg
unRuleT :: ProofStateT ext a err s m jdg
  }
  deriving stock (forall x.
 RuleT jdg ext err s m a -> Rep (RuleT jdg ext err s m a) x)
-> (forall x.
    Rep (RuleT jdg ext err s m a) x -> RuleT jdg ext err s m a)
-> Generic (RuleT jdg ext err s m a)
forall x.
Rep (RuleT jdg ext err s m a) x -> RuleT jdg ext err s m a
forall x.
RuleT jdg ext err s m a -> Rep (RuleT jdg ext err s m a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall jdg ext err s (m :: * -> *) a x.
Rep (RuleT jdg ext err s m a) x -> RuleT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a x.
RuleT jdg ext err s m a -> Rep (RuleT jdg ext err s m a) x
$cto :: forall jdg ext err s (m :: * -> *) a x.
Rep (RuleT jdg ext err s m a) x -> RuleT jdg ext err s m a
$cfrom :: forall jdg ext err s (m :: * -> *) a x.
RuleT jdg ext err s m a -> Rep (RuleT jdg ext err s m a) x
Generic

instance (Show jdg, Show err, Show a, Show (m (ProofStateT ext a err s m jdg))) => Show (RuleT jdg ext err s m a) where
  show :: RuleT jdg ext err s m a -> String
show = ProofStateT ext a err s m jdg -> String
forall a. Show a => a -> String
show (ProofStateT ext a err s m jdg -> String)
-> (RuleT jdg ext err s m a -> ProofStateT ext a err s m jdg)
-> RuleT jdg ext err s m a
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RuleT jdg ext err s m a -> ProofStateT ext a err s m jdg
forall jdg ext err s (m :: * -> *) a.
RuleT jdg ext err s m a -> ProofStateT ext a err s m jdg
unRuleT

instance Functor m => Functor (RuleT jdg ext err s m) where
  fmap :: (a -> b) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m b
fmap a -> b
f = (ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg)
-> RuleT jdg ext err s m a -> RuleT jdg ext err s m b
coerce ((ext -> ext)
-> (a -> b)
-> ProofStateT ext a err s m jdg
-> ProofStateT ext 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 ext -> ext
forall a. a -> a
id a -> b
f)

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

instance Monad m => Alternative (RuleT jdg ext err s m) where
    empty :: RuleT jdg ext err s m a
empty = ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
coerce ProofStateT ext a err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
    <|> :: RuleT jdg ext err s m a
-> RuleT jdg ext err s m a -> RuleT jdg ext err s m a
(<|>) = (ProofStateT ext a err s m jdg
 -> ProofStateT ext a err s m jdg -> ProofStateT ext a err s m jdg)
-> RuleT jdg ext err s m a
-> RuleT jdg ext err s m a
-> RuleT jdg ext err s m a
coerce ProofStateT ext a err s m jdg
-> ProofStateT ext a err s m jdg -> ProofStateT ext a 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

instance Monad m => Monad (RuleT jdg ext err s m) where
  return :: a -> RuleT jdg ext err s m a
return = ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
coerce (ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a)
-> (a -> ProofStateT ext a err s m jdg)
-> a
-> RuleT jdg ext err s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ProofStateT ext a err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom
  RuleT (Subgoal jdg
goal ext -> ProofStateT ext a err s m jdg
k)   >>= :: RuleT jdg ext err s m a
-> (a -> RuleT jdg ext err s m b) -> RuleT jdg ext err s m b
>>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ jdg
-> (ext -> ProofStateT ext b err s m jdg)
-> ProofStateT ext 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 ((ext -> ProofStateT ext b err s m jdg)
 -> ProofStateT ext b err s m jdg)
-> (ext -> ProofStateT ext b err s m jdg)
-> ProofStateT ext b err s m jdg
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg)
-> (ext -> ProofStateT ext a err s m jdg)
-> ext
-> ProofStateT ext b err s m jdg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f) ext -> ProofStateT ext a err s m jdg
k
  RuleT (Effect m (ProofStateT ext a err s m jdg)
m)         >>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ m (ProofStateT ext b err s m jdg) -> ProofStateT ext 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 (m (ProofStateT ext b err s m jdg)
 -> ProofStateT ext b err s m jdg)
-> m (ProofStateT ext b err s m jdg)
-> ProofStateT ext b err s m jdg
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg)
-> m (ProofStateT ext a err s m jdg)
-> m (ProofStateT ext b err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f) m (ProofStateT ext a err s m jdg)
m
  RuleT (Stateful s -> (s, ProofStateT ext a err s m jdg)
s)       >>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ (s -> (s, ProofStateT ext b err s m jdg))
-> ProofStateT ext 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 ((s -> (s, ProofStateT ext b err s m jdg))
 -> ProofStateT ext b err s m jdg)
-> (s -> (s, ProofStateT ext b err s m jdg))
-> ProofStateT ext b err s m jdg
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg)
-> (s, ProofStateT ext a err s m jdg)
-> (s, ProofStateT ext b err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f) ((s, ProofStateT ext a err s m jdg)
 -> (s, ProofStateT ext b err s m jdg))
-> (s -> (s, ProofStateT ext a err s m jdg))
-> s
-> (s, ProofStateT ext b err s m jdg)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (s, ProofStateT ext a err s m jdg)
s
  RuleT (Alt ProofStateT ext a err s m jdg
p1 ProofStateT ext a err s m jdg
p2)        >>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ ProofStateT ext b err s m jdg
-> ProofStateT ext b err s m jdg -> ProofStateT ext 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 -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f ProofStateT ext a err s m jdg
p1) ((a -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f ProofStateT ext a err s m jdg
p2)
  RuleT (Interleave ProofStateT ext a err s m jdg
p1 ProofStateT ext a err s m jdg
p2) >>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ ProofStateT ext b err s m jdg
-> ProofStateT ext b err s m jdg -> ProofStateT ext 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 -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f ProofStateT ext a err s m jdg
p1) ((a -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f ProofStateT ext a err s m jdg
p2)
  RuleT (Commit ProofStateT ext a err s m jdg
p1 ProofStateT ext a err s m jdg
p2)     >>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ ProofStateT ext b err s m jdg
-> ProofStateT ext b err s m jdg -> ProofStateT ext 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 -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f ProofStateT ext a err s m jdg
p1) ((a -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f ProofStateT ext a err s m jdg
p2)
  RuleT ProofStateT ext a err s m jdg
Empty              >>= a -> RuleT jdg ext err s m b
_ = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ ProofStateT ext b err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
  RuleT (Failure err
err ext -> ProofStateT ext a err s m jdg
k)    >>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ err
-> (ext -> ProofStateT ext b err s m jdg)
-> ProofStateT ext 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 ((ext -> ProofStateT ext b err s m jdg)
 -> ProofStateT ext b err s m jdg)
-> (ext -> ProofStateT ext b err s m jdg)
-> ProofStateT ext b err s m jdg
forall a b. (a -> b) -> a -> b
$ (ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg)
-> (ext -> ProofStateT ext a err s m jdg)
-> ext
-> ProofStateT ext b err s m jdg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f) ext -> ProofStateT ext a err s m jdg
k
  RuleT (Handle ProofStateT ext a err s m jdg
p err -> m err
h)       >>= a -> RuleT jdg ext err s m b
f = ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
coerce (ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b)
-> ProofStateT ext b err s m jdg -> RuleT jdg ext err s m b
forall a b. (a -> b) -> a -> b
$ ProofStateT ext b err s m jdg
-> (err -> m err) -> ProofStateT ext 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 -> RuleT jdg ext err s m b)
-> ProofStateT ext a err s m jdg -> ProofStateT ext b err s m jdg
forall (m :: * -> *) c b a1 a2.
(Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
(a2 -> m b) -> a1 -> c
bindAlaCoerce a -> RuleT jdg ext err s m b
f ProofStateT ext a err s m jdg
p) err -> m err
h
  RuleT (Axiom a
e)          >>= a -> RuleT jdg ext err s m b
f = a -> RuleT jdg ext err s m b
f a
e

instance Monad m => MonadState s (RuleT jdg ext err s m) where
    state :: (s -> (a, s)) -> RuleT jdg ext err s m a
state s -> (a, s)
f = ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a)
-> ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
forall a b. (a -> b) -> a -> b
$ (s -> (s, ProofStateT ext a err s m jdg))
-> ProofStateT ext a 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 ((s -> (s, ProofStateT ext a err s m jdg))
 -> ProofStateT ext a err s m jdg)
-> (s -> (s, ProofStateT ext a err s m jdg))
-> ProofStateT ext a err s m jdg
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 a err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom a
a)

bindAlaCoerce
  :: (Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
     (a2 -> m b) -> a1 -> c
bindAlaCoerce :: (a2 -> m b) -> a1 -> c
bindAlaCoerce a2 -> m b
f = m b -> c
coerce (m b -> c) -> (a1 -> m b) -> a1 -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a2 -> m b
f (a2 -> m b) -> m a2 -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (m a2 -> m b) -> (a1 -> m a2) -> a1 -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a1 -> m a2
coerce

instance MonadTrans (RuleT jdg ext err s) where
  lift :: m a -> RuleT jdg ext err s m a
lift = ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
coerce (ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a)
-> (m a -> ProofStateT ext a err s m jdg)
-> m a
-> RuleT jdg ext err s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (ProofStateT ext a err s m jdg) -> ProofStateT ext a 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 (m (ProofStateT ext a err s m jdg)
 -> ProofStateT ext a err s m jdg)
-> (m a -> m (ProofStateT ext a err s m jdg))
-> m a
-> ProofStateT ext a err s m jdg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> ProofStateT ext a err s m jdg)
-> m a -> m (ProofStateT ext a err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> ProofStateT ext a err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom

instance MFunctor (RuleT jdg ext err s) where
  hoist :: (forall a. m a -> n a)
-> RuleT jdg ext err s m b -> RuleT jdg ext err s n b
hoist forall a. m a -> n a
nat = (forall a. m a -> n a)
-> RuleT jdg ext err s m b -> RuleT jdg 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 (RuleT jdg ext err s m b -> RuleT jdg ext err s n b)
-> (RuleT jdg ext err s m b -> RuleT jdg ext err s m b)
-> RuleT jdg ext err s m b
-> RuleT jdg ext err s n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RuleT jdg ext err s m b -> RuleT jdg ext err s m b
coerce

instance MonadIO m => MonadIO (RuleT jdg ext err s m) where
  liftIO :: IO a -> RuleT jdg ext err s m a
liftIO = m a -> RuleT jdg ext err s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> RuleT jdg ext err s m a)
-> (IO a -> m a) -> IO a -> RuleT jdg 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

-- | Create a subgoal, and return the resulting extract.
subgoal :: jdg -> RuleT jdg ext err s m ext
subgoal :: jdg -> RuleT jdg ext err s m ext
subgoal jdg
jdg = ProofStateT ext ext err s m jdg -> RuleT jdg ext err s m ext
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT ext ext err s m jdg -> RuleT jdg ext err s m ext)
-> ProofStateT ext ext err s m jdg -> RuleT jdg ext err s m ext
forall a b. (a -> b) -> a -> b
$ jdg
-> (ext -> ProofStateT ext ext err s m jdg)
-> ProofStateT ext ext 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
jdg ext -> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom

-- | Create an "unsolvable" hole. These holes are ignored by subsequent tactics,
-- but do not cause a backtracking failure.
unsolvable :: err -> RuleT jdg ext err s m ext
unsolvable :: err -> RuleT jdg ext err s m ext
unsolvable err
err = ProofStateT ext ext err s m jdg -> RuleT jdg ext err s m ext
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT ext ext err s m jdg -> RuleT jdg ext err s m ext)
-> ProofStateT ext ext err s m jdg -> RuleT jdg ext err s m ext
forall a b. (a -> b) -> a -> b
$ 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 ext -> ProofStateT ext ext err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom