content: {-# 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
  t <@> ts = tactic $ \j -> subgoals (fmap (\t' (_,j') -> proofState t' j') ts) (proofState t 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
  t1 <%> t2 = tactic $ \j -> Interleave (proofState t1 j) (proofState t2 j)
  
  -- | Tries to run a tactic, backtracking on failure
  try :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
  try t = t <|> pure ()
  
  -- | @commit t1 t2@ will run @t1@, and then run @t2@ only if @t1@ (and all subsequent tactics) failed to produce any successes.
  --
  -- NOTE: @commit@ does have some sneaky semantics that you have to be aware of. Specifically, it interacts a bit
  -- surprisingly with '>>='. Namely, the following algebraic law holds
  -- @
  --     commit t1 t2 >>= f = commit (t1 >>= f) (t2 >>= f)
  -- @
  -- For instance, if you have something like @commit t1 t2 >>= somethingThatMayFail@, then this
  -- law implies that this is the same as @commit (t1 >>= somethingThatMayFail) (t2 >>= somethingThatMayFail)@,
  -- which means that we might execute @t2@ _even if_ @t1@ seemingly succeeds.
  commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
  commit t1 t2 = tactic $ \j -> Commit (proofState t1 j) (proofState t2 j)
  
  -- | Runs a tactic 0 or more times until it fails.
  -- Note that 'many_' is almost always the right choice over 'many'.
  -- Due to the semantics of 'Alternative', 'many' will create a bunch
  -- of partially solved goals along the way, one for each iteration.
  many_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
  many_ t = try (t >> many_ t)
  
  -- | Runs a tactic 1 or more times until it fails.
  -- Note that 'some_' is almost always the right choice over 'some'.
  -- Due to the semantics of 'Alternative', 'some' will create a bunch
  -- of partially solved goals along the way, one for each iteration.
  some_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
  some_ t = t >> many_ t
  
  -- | Get the current goal
  goal :: (Functor m) => TacticT jdg ext err s m jdg
  goal = TacticT get
  
  -- | Inspect the current goal.
  inspect :: (Functor m) => (jdg -> a) -> TacticT jdg ext err s m a
  inspect f = TacticT $ gets f
  
  -- | @choice ts@ will run all of the tactics in the list against the current subgoals,
  -- and interleave their extracts in a manner similar to '<%>'.
  choice :: (Monad m) => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
  choice = foldr (<%>) empty
  
  -- | @failure err@ will create an unsolvable hole that will be ignored by subsequent tactics.
  failure :: err -> TacticT jdg ext err s m a
  failure err = tactic $ \_ -> Failure err Axiom
  
  -- | @handler f@ will install an "error handler". These let you add more context to errors, and
  -- potentially run effects. For instance, you may want to take note that a particular situation is
  -- unsolvable, and that we shouldn't attempt to run this series of tactics against a given goal again.
  --
  -- Note that handlers further down the stack get run before those higher up the stack.
  -- For instance, consider the following example:
  -- @
  --     handler f >> handler g >> failure err
  -- @
  -- Here, @g@ will get run before @f@.
  handler :: (err -> m err) -> TacticT jdg ext err s m ()
  handler h = tactic $ \j -> Handle (Subgoal ((), j) Axiom) h
  
  -- | A variant of 'handler' that doesn't modify the error at all, and solely exists to run effects.
  handler_ :: (Functor m) => (err -> m ()) -> TacticT jdg ext err s m ()
  handler_ h = handler (\err -> err <$ h err)
  
  -- | @progress eq err t@ applies the tactic @t@, and checks to see if the
  -- resulting subgoals are all equal to the initial goal by using @eq@. If they
  -- are, it throws @err@.
  progress :: (Monad m) => (jdg -> jdg -> Bool) -> err ->  TacticT jdg ext err s m a -> TacticT jdg ext err s m a
  progress eq err t = do
    j <- goal
    a <- t
    j' <- goal
    if j `eq` j' then pure a else failure 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 p f t = check >> 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 = rule $ \j -> do
            e <- subgoal j
            s <- get
            modify f
            case p s of
              Just err -> unsolvable err
              Nothing -> pure e
  
  -- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.
  focus :: (Functor m) => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
  focus t n t' = t <@> (replicate n (pure ()) ++ [t'] ++ repeat (pure ()))
  
  -- | @tweak f t@ lets us modify the extract produced by the tactic @t@.
  tweak :: (Functor m) => (ext -> ext) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
  tweak f t = tactic $ \j -> mapExtract id f $ proofState t j
  
  -- | Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.
  -- Note that this function will backtrack on errors. If you want a version that provides partial proofs,
  -- use 'runPartialTacticT'
  runTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m (Either [err] [(Proof s meta jdg ext)])
  runTacticT t j s = proofs s $ fmap snd $ proofState t j
  
  -- | Run a tactic, and get just the list of extracts, ignoring any other information.
  evalTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m [ext]
  evalTacticT t j s = either (const []) (map pf_extract) <$> runTacticT t j s
  
  -- | Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.
  -- Note that this function will produce a so called "Partial Proof". This means that we no longer backtrack on errors,
  -- but rather leave an unsolved hole, and continue synthesizing a extract.
  -- If you want a version that backgracks on errors, see 'runTacticT'.
  --
  -- Note that this version is inherently slower than 'runTacticT', as it needs to continue producing extracts.
  runPartialTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> m (Either [PartialProof s err meta jdg ext] [(Proof s meta jdg ext)])
  runPartialTacticT t j s = partialProofs s $ fmap snd $ proofState t j
  
  -- | Turn an inference rule that examines the current goal into a tactic.
  rule :: (Monad m) => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
  rule r = tactic $ \j -> fmap ((),) $ unRuleT (r j)
  
  -- | Turn an inference rule into a tactic.
  rule_ :: (Monad m) => RuleT jdg ext err s m ext -> TacticT jdg ext err s m ()
  rule_ r = tactic $ \_ -> fmap ((),) $ unRuleT r
  
  introspect :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m a -> (err -> TacticT jdg ext err s m ()) -> (Proof s meta jdg ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
  introspect t handle f = rule $ \j -> do
      s <- get
      (RuleT $ speculate s $ proofState_ t j) >>= \case
        Left err -> RuleT $ proofState_ (handle err) j
        Right pf -> RuleT $ proofState_ (f pf) j
  
  -- | @reify t f@ will execute the tactic @t@, and resolve all of it's subgoals by filling them with holes.
  -- The resulting subgoals and partial extract are then passed to @f@.
  reify :: forall meta jdg ext err s m . (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> (Proof s meta jdg ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
  reify t f = introspect t failure f
  
  -- | @resume goals partial@ allows for resumption of execution after a call to 'reify'.
  -- If your language doesn't support dependent subgoals, consider using @resume'@ instead.
  resume :: forall meta jdg ext err s m. (DependentMetaSubst meta jdg ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m ()
  resume (Proof partialExt s goals) = rule $ \_ -> do
      put s
      solns <- dependentSubgoals goals
      pure $ foldr (\(meta, soln) ext -> substMeta meta soln ext) partialExt solns
      where
        dependentSubgoals :: [(meta, jdg)] -> RuleT jdg ext err s m [(meta, ext)]
        dependentSubgoals [] = pure []
        dependentSubgoals ((meta, g) : gs) = do
            soln <- subgoal g
            solns <- dependentSubgoals $ fmap (second (dependentSubst meta soln)) gs
            pure ((meta, soln) : solns)
  
  -- | A version of @resume@ that doesn't perform substitution into the goal types.
  -- This only makes sense if your language doesn't support dependent subgoals.
  -- If it does, use @resume@ instead, as this will leave the dependent subgoals with holes in them.
  resume' :: forall meta jdg ext err s m. (MetaSubst meta ext, Monad m) => Proof s meta jdg ext -> TacticT jdg ext err s m ()
  resume' (Proof partialExt s goals) = rule $ \_ -> do
      put s
      solns <- traverse (\(meta, g) -> (meta, ) <$> subgoal g) goals
      pure $ foldr (\(meta, soln) ext -> substMeta meta soln ext) partialExt solns
  
  -- | @pruning t p@ will execute @t@, and then apply @p@ to any subgoals it generates. If this predicate returns an error, we terminate the execution.
  -- Otherwise, we resume execution via 'resume''.
  pruning :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
  pruning t p = reify t $ \pf -> case (p $ fmap snd $ pf_unsolvedGoals pf) of
    Just err -> failure err
    Nothing ->  resume' pf
  
  -- | @peek t p@ will execute @t@, and then apply @p@ to the extract it produces. If this predicate returns an error, we terminate the execution.
  -- Otherwise, we resume execution via 'resume''.
  --
  -- Note that the extract produced may contain holes, as it is the extract produced by running _just_ @t@ against the current goal.
  peek :: (MetaSubst meta ext, MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> (ext -> Maybe err) -> TacticT jdg ext err s m ()
  peek t p = reify t $ \pf -> case (p $ pf_extract pf) of
    Just err -> failure err
    Nothing ->  resume' pf
  
  -- | @attempt t1 t2@ will partially execute @t1@, inspect it's result, and only run @t2@ if it fails.
  -- If @t1@ succeeded, we will 'resume'' execution of it.
  attempt :: (MonadExtract meta ext err s m, MetaSubst meta ext) => TacticT jdg ext err s m () -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
  attempt t1 t2 = introspect t1 (\_ -> t2) resume'
  