{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
-----------------------------------------------------------------------------
-- | Tactics and Tactic Combinators
--
-- This module contains everything you need to start defining tactics
-- and tactic combinators.
-- Module      :  Refinery.Tactic
-- Copyright   :  (c) Reed Mullanix 2019
-- License     :  BSD-style
-- Maintainer  :  reedmullanix@gmail.com
module Refinery.Tactic
  ( TacticT
  , runTacticT
  , runPartialTacticT
  , evalTacticT
  , Proof(..)
  , PartialProof(..)
  -- * Tactic Combinators
  , (<@>)
  , (<%>)
  , try
  , commit
  , many_
  , some_
  , choice
  , progress
  , ensure
  -- * Errors and Error Handling
  , failure
  , handler
  , handler_
  -- * Extract Manipulation
  , tweak
  -- * Subgoal Manipulation
  , goal
  , inspect
  , focus
  -- * Tactic Creation
  , MonadExtract(..)
  , RuleT
  , rule
  , rule_
  , subgoal
  , unsolvable
  -- * Introspection
  , MetaSubst(..)
  , DependentMetaSubst(..)
  , reify
  , resume
  , resume'
  , pruning
  , peek
  , attempt
  ) where

import Control.Applicative
import Control.Monad.State.Class

import Data.Bifunctor

import Refinery.ProofState
import Refinery.Tactic.Internal

-- | Create a tactic that applies each of the tactics in the list to one subgoal.
--
-- When the number of subgoals is greater than the number of provided tactics,
-- the identity tactic is applied to the remainder. When the number of subgoals is
-- less than the number of provided tactics, the remaining tactics are ignored.
(<@>) :: (Functor 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
t <@> :: 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]
ts = (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, jdg) -> ProofStateT ext ext err s m (a, jdg)]
-> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, 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 ((TacticT jdg ext err s m a
 -> (a, jdg) -> ProofStateT ext ext err s m (a, jdg))
-> [TacticT jdg ext err s m a]
-> [(a, jdg) -> ProofStateT ext ext err s m (a, jdg)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\TacticT jdg ext err s m a
t' (a
_,jdg
j') -> TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, 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 a
t' jdg
j') [TacticT jdg ext err s m a]
ts) (TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, 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 a
t jdg
j)

infixr 3 <%>

-- | @t1 <%> t2@ will interleave the execution of @t1@ and @t2@. This is useful if @t1@ will
-- produce an infinite number of extracts, as we will still run @t2@. This is contrasted with
-- @t1 <|> t2@, which will not ever consider @t2@ if @t1@ produces an infinite number of extracts.
(<%>) :: 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
t1 <%> :: 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
t2 = (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 -> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, 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 (TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, 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 a
t1 jdg
j) (TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, 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 a
t2 jdg
j)

-- | Tries to run a tactic, backtracking on failure
try :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try :: TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try TacticT jdg ext err s m ()
t = TacticT jdg ext err s m ()
t TacticT jdg ext err s m ()
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> () -> TacticT jdg ext err s m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | @commit t1 t2@ will run @t1@, and then run @t2@ only if @t1@ (and all subsequent tactics) failed to produce any successes.
--
-- NOTE: @commit@ does have some sneaky semantics that you have to be aware of. Specifically, it interacts a bit
-- surprisingly with '>>='. Namely, the following algebraic law holds
-- @
--     commit t1 t2 >>= f = commit (t1 >>= f) (t2 >>= f)
-- @
-- For instance, if you have something like @commit t1 t2 >>= somethingThatMayFail@, then this
-- law implies that this is the same as @commit (t1 >>= somethingThatMayFail) (t2 >>= somethingThatMayFail)@,
-- which means that we might execute @t2@ _even if_ @t1@ seemingly succeeds.
commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit :: TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit TacticT jdg ext err s m a
t1 TacticT jdg ext err s m a
t2 = (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 -> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, 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 (TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, 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 a
t1 jdg
j) (TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, 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 a
t2 jdg
j)

-- | Runs a tactic 0 or more times until it fails.
-- Note that 'many_' is almost always the right choice over 'many'.
-- Due to the semantics of 'Alternative', 'many' will create a bunch
-- of partially solved goals along the way, one for each iteration.
many_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
many_ :: TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
many_ TacticT jdg ext err s m ()
t = TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try (TacticT jdg ext err s m ()
t TacticT jdg ext err s m ()
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
many_ TacticT jdg ext err s m ()
t)

-- | Runs a tactic 1 or more times until it fails.
-- Note that 'some_' is almost always the right choice over 'some'.
-- Due to the semantics of 'Alternative', 'some' will create a bunch
-- of partially solved goals along the way, one for each iteration.
some_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
some_ :: TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
some_ TacticT jdg ext err s m ()
t = TacticT jdg ext err s m ()
t TacticT jdg ext err s m ()
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
many_ TacticT jdg ext err s m ()
t

-- | Get the current goal
goal :: (Functor m) => TacticT jdg ext err s m jdg
goal :: TacticT jdg ext err s m jdg
goal = StateT jdg (ProofStateT ext ext err s m) jdg
-> TacticT jdg ext err s m jdg
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) jdg
forall s (m :: * -> *). MonadState s m => m s
get

-- | Inspect the current goal.
inspect :: (Functor m) => (jdg -> a) -> TacticT jdg ext err s m a
inspect :: (jdg -> a) -> TacticT jdg ext err s m a
inspect jdg -> a
f = 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 -> a) -> StateT jdg (ProofStateT ext ext err s m) a
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets jdg -> a
f

-- | @choice ts@ will run all of the tactics in the list against the current subgoals,
-- and interleave their extracts in a manner similar to '<%>'.
choice :: (Monad m) => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice :: [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice = (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 (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr 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 :: * -> *) 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 (f :: * -> *) a. Alternative f => f a
empty

-- | @failure err@ will create an unsolvable hole that will be ignored by subsequent tactics.
failure :: err -> TacticT jdg ext err s m a
failure :: err -> TacticT jdg ext err s m a
failure err
err = (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
_ -> err
-> (ext -> ProofStateT ext ext err s m (a, jdg))
-> ProofStateT ext ext err s m (a, 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 (a, jdg)
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom

-- | @handler f@ will install an "error handler". These let you add more context to errors, and
-- potentially run effects. For instance, you may want to take note that a particular situation is
-- unsolvable, and that we shouldn't attempt to run this series of tactics against a given goal again.
--
-- Note that handlers further down the stack get run before those higher up the stack.
-- For instance, consider the following example:
-- @
--     handler f >> handler g >> failure err
-- @
-- Here, @g@ will get run before @f@.
handler :: (err -> m err) -> TacticT jdg ext err s m ()
handler :: (err -> m err) -> TacticT jdg ext err s m ()
handler err -> m err
h = (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
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 ((), jdg))
 -> TacticT jdg ext err s m ())
-> (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
j -> 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)
-> (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
j) ext -> ProofStateT ext ext err s m ((), jdg)
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom) err -> m err
h

-- | A variant of 'handler' that doesn't modify the error at all, and solely exists to run effects.
handler_ :: (Functor m) => (err -> m ()) -> TacticT jdg ext err s m ()
handler_ :: (err -> m ()) -> TacticT jdg ext err s m ()
handler_ err -> m ()
h = (err -> m err) -> TacticT jdg ext err s m ()
forall err (m :: * -> *) jdg ext s.
(err -> m err) -> TacticT jdg ext err s m ()
handler (\err
err -> err
err err -> m () -> m err
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ err -> m ()
h err
err)

-- | @progress eq err t@ applies the tactic @t@, and checks to see if the
-- resulting subgoals are all equal to the initial goal by using @eq@. If they
-- are, it throws @err@.
progress :: (Monad m) => (jdg -> jdg -> Bool) -> err ->  TacticT jdg ext err s m a -> TacticT jdg ext err s m a
progress :: (jdg -> jdg -> Bool)
-> err -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
progress jdg -> jdg -> Bool
eq err
err TacticT jdg ext err s m a
t = do
  jdg
j <- TacticT jdg ext err s m jdg
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  a
a <- TacticT jdg ext err s m a
t
  jdg
j' <- TacticT jdg ext err s m jdg
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  if jdg
j jdg -> jdg -> Bool
`eq` jdg
j' then a -> TacticT jdg ext err s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a else err -> TacticT jdg ext err s m a
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure err
err

-- | @ensure p f t@ runs the tactic @t@, and applies a predicate to the state after the execution of @t@. We also run
-- a "cleanup" function @f@. Note that the predicate is applied to the state _before_ the cleanup function is run.
ensure :: (Monad m) => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
ensure :: (s -> Maybe err)
-> (s -> s)
-> TacticT jdg ext err s m ()
-> TacticT jdg ext err s m ()
ensure s -> Maybe err
p s -> s
f TacticT jdg ext err s m ()
t = TacticT jdg ext err s m ()
check TacticT jdg ext err s m ()
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticT jdg ext err s m ()
t
    where
      -- NOTE It may seem backwards to run check _before_ t, but we
      -- need to do the predicate check after the subgoal has been resolved,
      -- and not on every generated subgoal.
      check :: TacticT jdg ext err s m ()
check = (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ())
-> (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
j -> do
          ext
e <- jdg -> RuleT jdg ext err s m ext
forall jdg ext err s (m :: * -> *).
jdg -> RuleT jdg ext err s m ext
subgoal jdg
j
          s
s <- RuleT jdg ext err s m s
forall s (m :: * -> *). MonadState s m => m s
get
          (s -> s) -> RuleT jdg ext err s m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify s -> s
f
          case s -> Maybe err
p s
s of
            Just err
err -> err -> RuleT jdg ext err s m ext
forall err jdg ext s (m :: * -> *).
err -> RuleT jdg ext err s m ext
unsolvable err
err
            Maybe err
Nothing -> ext -> RuleT jdg ext err s m ext
forall (f :: * -> *) a. Applicative f => a -> f a
pure ext
e

-- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.
focus :: (Functor m) => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
focus :: TacticT jdg ext err s m ()
-> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
focus TacticT jdg ext err s m ()
t Int
n TacticT jdg ext err s m ()
t' = TacticT jdg ext err s m ()
t TacticT jdg ext err s m ()
-> [TacticT jdg ext err s m ()] -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> (Int -> TacticT jdg ext err s m () -> [TacticT jdg ext err s m ()]
forall a. Int -> a -> [a]
replicate Int
n (() -> TacticT jdg ext err s m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) [TacticT jdg ext err s m ()]
-> [TacticT jdg ext err s m ()] -> [TacticT jdg ext err s m ()]
forall a. [a] -> [a] -> [a]
++ [TacticT jdg ext err s m ()
t'] [TacticT jdg ext err s m ()]
-> [TacticT jdg ext err s m ()] -> [TacticT jdg ext err s m ()]
forall a. [a] -> [a] -> [a]
++ TacticT jdg ext err s m () -> [TacticT jdg ext err s m ()]
forall a. a -> [a]
repeat (() -> TacticT jdg ext err s m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))

-- | @tweak f t@ lets us modify the extract produced by the tactic @t@.
tweak :: (Functor m) => (ext -> ext) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
tweak :: (ext -> ext)
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
tweak ext -> ext
f TacticT jdg ext err s m ()
t = (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
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 ((), jdg))
 -> TacticT jdg ext err s m ())
-> (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
j -> (ext -> ext)
-> (ext -> ext)
-> ProofStateT ext ext err s m ((), jdg)
-> ProofStateT ext ext 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 ext -> ext
f (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

-- | Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.
-- Note that this function will backtrack on errors. If you want a version that provides partial proofs,
-- use 'runPartialTacticT'
runTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m (Either [err] [(Proof s meta jdg ext)])
runTacticT :: TacticT jdg ext err s m ()
-> jdg -> s -> m (Either [err] [Proof s meta jdg ext])
runTacticT TacticT jdg ext err s m ()
t jdg
j s
s = s
-> ProofStateT ext ext err s m jdg
-> 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
-> m (Either [err] [Proof s meta goal ext])
proofs s
s (ProofStateT ext ext err s m jdg
 -> m (Either [err] [Proof s meta jdg ext]))
-> ProofStateT ext ext err s m jdg
-> 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

-- | Run a tactic, and get just the list of extracts, ignoring any other information.
evalTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m [ext]
evalTacticT :: TacticT jdg ext err s m () -> jdg -> s -> m [ext]
evalTacticT TacticT jdg ext err s m ()
t jdg
j s
s = ([err] -> [ext])
-> ([Proof s meta jdg ext] -> [ext])
-> Either [err] [Proof s meta jdg ext]
-> [ext]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([ext] -> [err] -> [ext]
forall a b. a -> b -> a
const []) ((Proof s meta jdg ext -> ext) -> [Proof s meta jdg ext] -> [ext]
forall a b. (a -> b) -> [a] -> [b]
map Proof s meta jdg ext -> ext
forall s meta goal ext. Proof s meta goal ext -> ext
pf_extract) (Either [err] [Proof s meta jdg ext] -> [ext])
-> m (Either [err] [Proof s meta jdg ext]) -> m [ext]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT jdg ext err s m ()
-> jdg -> s -> m (Either [err] [Proof s meta jdg ext])
forall meta ext err s (m :: * -> *) jdg.
MonadExtract meta ext err s m =>
TacticT jdg ext err s m ()
-> jdg -> s -> m (Either [err] [Proof s meta jdg ext])
runTacticT TacticT jdg ext err s m ()
t jdg
j s
s

-- | Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.
-- Note that this function will produce a so called "Partial Proof". This means that we no longer backtrack on errors,
-- but rather leave an unsolved hole, and continue synthesizing a extract.
-- If you want a version that backgracks on errors, see 'runTacticT'.
--
-- Note that this version is inherently slower than 'runTacticT', as it needs to continue producing extracts.
runPartialTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m (Either [PartialProof s err meta jdg ext] [(Proof s meta jdg ext)])
runPartialTacticT :: TacticT jdg ext err s m ()
-> jdg
-> s
-> m (Either
        [PartialProof s err meta jdg ext] [Proof s meta jdg ext])
runPartialTacticT TacticT jdg ext err s m ()
t jdg
j s
s = s
-> ProofStateT ext ext err s m jdg
-> m (Either
        [PartialProof s err meta jdg ext] [Proof s meta jdg ext])
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
s (ProofStateT ext ext err s m jdg
 -> m (Either
         [PartialProof s err meta jdg ext] [Proof s meta jdg ext]))
-> ProofStateT ext ext err s m jdg
-> m (Either
        [PartialProof s err meta jdg ext] [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

-- | Turn an inference rule that examines the current goal into a tactic.
rule :: (Monad m) => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule :: (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule jdg -> RuleT jdg ext err s m ext
r = (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
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 ((), jdg))
 -> TacticT jdg ext err s m ())
-> (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
j -> (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 ((),) (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
$ RuleT jdg ext err s m ext -> ProofStateT ext ext 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 (jdg -> RuleT jdg ext err s m ext
r jdg
j)

-- | Turn an inference rule into a tactic.
rule_ :: (Monad m) => RuleT jdg ext err s m ext -> TacticT jdg ext err s m ()
rule_ :: RuleT jdg ext err s m ext -> TacticT jdg ext err s m ()
rule_ RuleT jdg ext err s m ext
r = (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
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 ((), jdg))
 -> TacticT jdg ext err s m ())
-> (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
_ -> (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 ((),) (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
$ RuleT jdg ext err s m ext -> ProofStateT ext ext 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 RuleT jdg ext err s m ext
r

introspect :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m a -> (err -> TacticT jdg ext err s m ()) -> (Proof s meta jdg ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
introspect :: TacticT jdg ext err s m a
-> (err -> TacticT jdg ext err s m ())
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
introspect TacticT jdg ext err s m a
t err -> TacticT jdg ext err s m ()
handle Proof s meta jdg ext -> TacticT jdg ext err s m ()
f = (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ())
-> (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
j -> do
    s
s <- RuleT jdg ext err s m s
forall s (m :: * -> *). MonadState s m => m s
get
    (ProofStateT ext (Either err (Proof s meta jdg ext)) err s m jdg
-> RuleT jdg ext err s m (Either err (Proof s meta jdg 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 (Either err (Proof s meta jdg ext)) err s m jdg
 -> RuleT jdg ext err s m (Either err (Proof s meta jdg ext)))
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m jdg
-> RuleT jdg ext err s m (Either err (Proof s meta jdg ext))
forall a b. (a -> b) -> a -> b
$ s
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m jdg
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
s (ProofStateT ext ext err s m jdg
 -> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m jdg)
-> ProofStateT ext ext err s m jdg
-> ProofStateT ext (Either err (Proof s meta jdg ext)) err s m jdg
forall a b. (a -> b) -> a -> b
$ TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s a.
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
t jdg
j) RuleT jdg ext err s m (Either err (Proof s meta jdg ext))
-> (Either err (Proof s meta jdg ext) -> RuleT jdg ext err s m ext)
-> RuleT jdg ext err s m ext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left 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
$ TacticT jdg ext err s m ()
-> jdg -> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg
proofState_ (err -> TacticT jdg ext err s m ()
handle err
err) jdg
j
      Right Proof s meta jdg ext
pf -> 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
$ TacticT jdg ext err s m ()
-> jdg -> ProofStateT ext ext err s m jdg
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m jdg
proofState_ (Proof s meta jdg ext -> TacticT jdg ext err s m ()
f Proof s meta jdg ext
pf) jdg
j

-- | @reify t f@ will execute the tactic @t@, and resolve all of it's subgoals by filling them with holes.
-- The resulting subgoals and partial extract are then passed to @f@.
reify :: forall meta jdg ext err s m . (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> (Proof s meta jdg ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
reify :: TacticT jdg ext err s m ()
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
reify TacticT jdg ext err s m ()
t Proof s meta jdg ext -> TacticT jdg ext err s m ()
f = TacticT jdg ext err s m ()
-> (err -> TacticT jdg ext err s m ())
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
forall meta ext err s (m :: * -> *) jdg a.
MonadExtract meta ext err s m =>
TacticT jdg ext err s m a
-> (err -> TacticT jdg ext err s m ())
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
introspect TacticT jdg ext err s m ()
t err -> TacticT jdg ext err s m ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure Proof s meta jdg ext -> TacticT jdg ext err s m ()
f

-- | @resume goals partial@ allows for resumption of execution after a call to 'reify'.
-- If your language doesn't support dependent subgoals, consider using @resume'@ instead.
resume :: forall meta jdg ext err s m. (DependentMetaSubst meta jdg ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m ()
resume :: Proof s meta jdg ext -> TacticT jdg ext err s m ()
resume (Proof ext
partialExt s
s [(meta, jdg)]
goals) = (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ())
-> (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
_ -> do
    s -> RuleT jdg ext err s m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put s
s
    [(meta, ext)]
solns <- [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)]
dependentSubgoals [(meta, jdg)]
goals
    ext -> RuleT jdg ext err s m ext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ext -> RuleT jdg ext err s m ext)
-> ext -> RuleT jdg ext err s m ext
forall a b. (a -> b) -> a -> b
$ ((meta, ext) -> ext -> ext) -> ext -> [(meta, ext)] -> ext
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(meta
meta, ext
soln) ext
ext -> meta -> ext -> ext -> ext
forall meta ext. MetaSubst meta ext => meta -> ext -> ext -> ext
substMeta meta
meta ext
soln ext
ext) ext
partialExt [(meta, ext)]
solns
    where
      dependentSubgoals :: [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)]
      dependentSubgoals :: [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)]
dependentSubgoals [] = [(meta, ext)] -> RuleT jdg ext err s m [(meta, ext)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      dependentSubgoals ((meta
meta, jdg
g) : [(meta, jdg)]
gs) = do
          ext
soln <- jdg -> RuleT jdg ext err s m ext
forall jdg ext err s (m :: * -> *).
jdg -> RuleT jdg ext err s m ext
subgoal jdg
g
          [(meta, ext)]
solns <- [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)]
dependentSubgoals ([(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)])
-> [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)]
forall a b. (a -> b) -> a -> b
$ ((meta, jdg) -> (meta, jdg)) -> [(meta, jdg)] -> [(meta, jdg)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((jdg -> jdg) -> (meta, jdg) -> (meta, jdg)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (meta -> ext -> jdg -> jdg
forall meta jdg ext.
DependentMetaSubst meta jdg ext =>
meta -> ext -> jdg -> jdg
dependentSubst meta
meta ext
soln)) [(meta, jdg)]
gs
          [(meta, ext)] -> RuleT jdg ext err s m [(meta, ext)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((meta
meta, ext
soln) (meta, ext) -> [(meta, ext)] -> [(meta, ext)]
forall a. a -> [a] -> [a]
: [(meta, ext)]
solns)

-- | A version of @resume@ that doesn't perform substitution into the goal types.
-- This only makes sense if your language doesn't support dependent subgoals.
-- If it does, use @resume@ instead, as this will leave the dependent subgoals with holes in them.
resume' :: forall meta jdg ext err s m. (MetaSubst meta ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m ()
resume' :: Proof s meta jdg ext -> TacticT jdg ext err s m ()
resume' (Proof ext
partialExt s
s [(meta, jdg)]
goals) = (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ())
-> (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
_ -> do
    s -> RuleT jdg ext err s m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put s
s
    [(meta, ext)]
solns <- ((meta, jdg) -> RuleT jdg ext err s m (meta, ext))
-> [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\(meta
meta, jdg
g) -> (meta
meta, ) (ext -> (meta, ext))
-> RuleT jdg ext err s m ext -> RuleT jdg ext err s m (meta, ext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> jdg -> RuleT jdg ext err s m ext
forall jdg ext err s (m :: * -> *).
jdg -> RuleT jdg ext err s m ext
subgoal jdg
g) [(meta, jdg)]
goals
    ext -> RuleT jdg ext err s m ext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ext -> RuleT jdg ext err s m ext)
-> ext -> RuleT jdg ext err s m ext
forall a b. (a -> b) -> a -> b
$ ((meta, ext) -> ext -> ext) -> ext -> [(meta, ext)] -> ext
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(meta
meta, ext
soln) ext
ext -> meta -> ext -> ext -> ext
forall meta ext. MetaSubst meta ext => meta -> ext -> ext -> ext
substMeta meta
meta ext
soln ext
ext) ext
partialExt [(meta, ext)]
solns

-- | @pruning t p@ will execute @t@, and then apply @p@ to any subgoals it generates. If this predicate returns an error, we terminate the execution.
-- Otherwise, we resume execution via 'resume''.
pruning :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning :: TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticT jdg ext err s m ()
t [jdg] -> Maybe err
p = TacticT jdg ext err s m ()
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
forall meta jdg ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
TacticT jdg ext err s m ()
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
reify TacticT jdg ext err s m ()
t ((Proof s meta jdg ext -> TacticT jdg ext err s m ())
 -> TacticT jdg ext err s m ())
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \Proof s meta jdg ext
pf -> case ([jdg] -> Maybe err
p ([jdg] -> Maybe err) -> [jdg] -> Maybe err
forall a b. (a -> b) -> a -> b
$ ((meta, jdg) -> jdg) -> [(meta, jdg)] -> [jdg]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (meta, jdg) -> jdg
forall a b. (a, b) -> b
snd ([(meta, jdg)] -> [jdg]) -> [(meta, jdg)] -> [jdg]
forall a b. (a -> b) -> a -> b
$ Proof s meta jdg ext -> [(meta, jdg)]
forall s meta goal ext. Proof s meta goal ext -> [(meta, goal)]
pf_unsolvedGoals Proof s meta jdg ext
pf) of
  Just err
err -> err -> TacticT jdg ext err s m ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure err
err
  Maybe err
Nothing ->  Proof s meta jdg ext -> TacticT jdg ext err s m ()
forall meta jdg ext err s (m :: * -> *).
(MetaSubst meta ext, Monad m) =>
Proof s meta jdg ext -> TacticT jdg ext err s m ()
resume' Proof s meta jdg ext
pf

-- | @peek t p@ will execute @t@, and then apply @p@ to the extract it produces. If this predicate returns an error, we terminate the execution.
-- Otherwise, we resume execution via 'resume''.
--
-- Note that the extract produced may contain holes, as it is the extract produced by running _just_ @t@ against the current goal.
peek :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> (ext -> Maybe err) -> TacticT jdg ext err s m ()
peek :: TacticT jdg ext err s m ()
-> (ext -> Maybe err) -> TacticT jdg ext err s m ()
peek TacticT jdg ext err s m ()
t ext -> Maybe err
p = TacticT jdg ext err s m ()
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
forall meta jdg ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
TacticT jdg ext err s m ()
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
reify TacticT jdg ext err s m ()
t ((Proof s meta jdg ext -> TacticT jdg ext err s m ())
 -> TacticT jdg ext err s m ())
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \Proof s meta jdg ext
pf -> case (ext -> Maybe err
p (ext -> Maybe err) -> ext -> Maybe err
forall a b. (a -> b) -> a -> b
$ Proof s meta jdg ext -> ext
forall s meta goal ext. Proof s meta goal ext -> ext
pf_extract Proof s meta jdg ext
pf) of
  Just err
err -> err -> TacticT jdg ext err s m ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure err
err
  Maybe err
Nothing ->  Proof s meta jdg ext -> TacticT jdg ext err s m ()
forall meta jdg ext err s (m :: * -> *).
(MetaSubst meta ext, Monad m) =>
Proof s meta jdg ext -> TacticT jdg ext err s m ()
resume' Proof s meta jdg ext
pf

-- | @attempt t1 t2@ will partially execute @t1@, inspect it's result, and only run @t2@ if it fails.
-- If @t1@ succeeded, we will 'resume'' execution of it.
attempt :: (MonadExtract meta ext err s m, MetaSubst meta ext) => TacticT jdg ext err s m () -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
attempt :: TacticT jdg ext err s m ()
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
attempt TacticT jdg ext err s m ()
t1 TacticT jdg ext err s m ()
t2 = TacticT jdg ext err s m ()
-> (err -> TacticT jdg ext err s m ())
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
forall meta ext err s (m :: * -> *) jdg a.
MonadExtract meta ext err s m =>
TacticT jdg ext err s m a
-> (err -> TacticT jdg ext err s m ())
-> (Proof s meta jdg ext -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m ()
introspect TacticT jdg ext err s m ()
t1 (\err
_ -> TacticT jdg ext err s m ()
t2) Proof s meta jdg ext -> TacticT jdg ext err s m ()
forall meta jdg ext err s (m :: * -> *).
(MetaSubst meta ext, Monad m) =>
Proof s meta jdg ext -> TacticT jdg ext err s m ()
resume'