{-|
Module      : Lang.Crucible.Backend.ProofGoals
Copyright   : (c) Galois, Inc 2014-2018
License     : BSD3

This module defines a data strucutre for storing a collection of
proof obligations, and the current state of assumptions.
-}

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

module Lang.Crucible.Backend.ProofGoals
  ( -- * Goals
    ProofGoal(..), Goals(..), goalsToList, proveAll, goalsConj
    -- ** traversals
  , traverseGoals, traverseOnlyGoals
  , traverseGoalsWithAssumptions
  , traverseGoalsSeq

    -- * Goal collector
  , FrameIdentifier(..), GoalCollector
  , emptyGoalCollector

    -- ** traversals
  , traverseGoalCollector
  , traverseGoalCollectorWithAssumptions

    -- ** Context management
  , gcAddAssumes, gcProve
  , gcPush, gcPop, gcAddGoals,

    -- ** Global operations on context
    gcRemoveObligations, gcRestore, gcReset, gcFinish

    -- ** Viewing the assumption state
  , AssumptionFrames(..), gcFrames
  )
  where

import           Control.Monad.Reader
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Word (Word64)

import           Lang.Crucible.Backend.Goals

-- | A @FrameIdentifier@ is a value that identifies an
--   an assumption frame.  These are expected to be unique
--   when a new frame is pushed onto the stack.  This is
--   primarily a debugging aid, to ensure that stack management
--   remains well-bracketed.
newtype FrameIdentifier = FrameIdentifier Word64
 deriving(FrameIdentifier -> FrameIdentifier -> Bool
(FrameIdentifier -> FrameIdentifier -> Bool)
-> (FrameIdentifier -> FrameIdentifier -> Bool)
-> Eq FrameIdentifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FrameIdentifier -> FrameIdentifier -> Bool
== :: FrameIdentifier -> FrameIdentifier -> Bool
$c/= :: FrameIdentifier -> FrameIdentifier -> Bool
/= :: FrameIdentifier -> FrameIdentifier -> Bool
Eq,Eq FrameIdentifier
Eq FrameIdentifier =>
(FrameIdentifier -> FrameIdentifier -> Ordering)
-> (FrameIdentifier -> FrameIdentifier -> Bool)
-> (FrameIdentifier -> FrameIdentifier -> Bool)
-> (FrameIdentifier -> FrameIdentifier -> Bool)
-> (FrameIdentifier -> FrameIdentifier -> Bool)
-> (FrameIdentifier -> FrameIdentifier -> FrameIdentifier)
-> (FrameIdentifier -> FrameIdentifier -> FrameIdentifier)
-> Ord FrameIdentifier
FrameIdentifier -> FrameIdentifier -> Bool
FrameIdentifier -> FrameIdentifier -> Ordering
FrameIdentifier -> FrameIdentifier -> FrameIdentifier
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FrameIdentifier -> FrameIdentifier -> Ordering
compare :: FrameIdentifier -> FrameIdentifier -> Ordering
$c< :: FrameIdentifier -> FrameIdentifier -> Bool
< :: FrameIdentifier -> FrameIdentifier -> Bool
$c<= :: FrameIdentifier -> FrameIdentifier -> Bool
<= :: FrameIdentifier -> FrameIdentifier -> Bool
$c> :: FrameIdentifier -> FrameIdentifier -> Bool
> :: FrameIdentifier -> FrameIdentifier -> Bool
$c>= :: FrameIdentifier -> FrameIdentifier -> Bool
>= :: FrameIdentifier -> FrameIdentifier -> Bool
$cmax :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier
max :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier
$cmin :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier
min :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier
Ord,Int -> FrameIdentifier -> ShowS
[FrameIdentifier] -> ShowS
FrameIdentifier -> String
(Int -> FrameIdentifier -> ShowS)
-> (FrameIdentifier -> String)
-> ([FrameIdentifier] -> ShowS)
-> Show FrameIdentifier
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FrameIdentifier -> ShowS
showsPrec :: Int -> FrameIdentifier -> ShowS
$cshow :: FrameIdentifier -> String
show :: FrameIdentifier -> String
$cshowList :: [FrameIdentifier] -> ShowS
showList :: [FrameIdentifier] -> ShowS
Show)


-- | A data-strucutre that can incrementally collect goals in context.
--   It keeps track both of the collection of assumptions that lead to
--   the current state, as well as any proof obligations incurred along
--   the way.
data GoalCollector asmp goal
  = TopCollector !(Seq (Goals asmp goal))
  | CollectorFrame !FrameIdentifier !(GoalCollector asmp goal)
  | CollectingAssumptions !asmp !(GoalCollector asmp goal)
  | CollectingGoals !(Seq (Goals asmp goal)) !(GoalCollector asmp goal)

-- | A collector with no goals and no context.
emptyGoalCollector :: GoalCollector asmp goal
emptyGoalCollector :: forall asmp goal. GoalCollector asmp goal
emptyGoalCollector = Seq (Goals asmp goal) -> GoalCollector asmp goal
forall asmp goal. Seq (Goals asmp goal) -> GoalCollector asmp goal
TopCollector Seq (Goals asmp goal)
forall a. Monoid a => a
mempty

-- | Traverse the goals in a 'GoalCollector.  See 'traverseGoals'
--   for an explaination of the action arguments.
traverseGoalCollector :: (Applicative f, Monoid asmp') =>
  (forall a. asmp -> f a -> f (asmp', a)) ->
  (goal -> f (Maybe goal')) ->
  GoalCollector asmp goal -> f (GoalCollector asmp' goal')
traverseGoalCollector :: forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> GoalCollector asmp goal
-> f (GoalCollector asmp' goal')
traverseGoalCollector forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl = GoalCollector asmp goal -> f (GoalCollector asmp' goal')
go
 where
 go :: GoalCollector asmp goal -> f (GoalCollector asmp' goal')
go (TopCollector Seq (Goals asmp goal)
gls) = Seq (Goals asmp' goal') -> GoalCollector asmp' goal'
forall asmp goal. Seq (Goals asmp goal) -> GoalCollector asmp goal
TopCollector (Seq (Goals asmp' goal') -> GoalCollector asmp' goal')
-> f (Seq (Goals asmp' goal')) -> f (GoalCollector asmp' goal')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Seq (Goals asmp goal)
-> f (Seq (Goals asmp' goal'))
forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Seq (Goals asmp goal)
-> f (Seq (Goals asmp' goal'))
traverseGoalsSeq asmp -> f a -> f (asmp', a)
forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl Seq (Goals asmp goal)
gls
 go (CollectorFrame FrameIdentifier
fid GoalCollector asmp goal
gls) = FrameIdentifier
-> GoalCollector asmp' goal' -> GoalCollector asmp' goal'
forall asmp goal.
FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectorFrame FrameIdentifier
fid (GoalCollector asmp' goal' -> GoalCollector asmp' goal')
-> f (GoalCollector asmp' goal') -> f (GoalCollector asmp' goal')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GoalCollector asmp goal -> f (GoalCollector asmp' goal')
go GoalCollector asmp goal
gls
 go (CollectingAssumptions asmp
asmps GoalCollector asmp goal
gls) = asmp' -> GoalCollector asmp' goal' -> GoalCollector asmp' goal'
forall asmp goal.
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingAssumptions (asmp' -> GoalCollector asmp' goal' -> GoalCollector asmp' goal')
-> f asmp'
-> f (GoalCollector asmp' goal' -> GoalCollector asmp' goal')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((asmp', ()) -> asmp'
forall a b. (a, b) -> a
fst ((asmp', ()) -> asmp') -> f (asmp', ()) -> f asmp'
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> asmp -> f () -> f (asmp', ())
forall a. asmp -> f a -> f (asmp', a)
fas asmp
asmps (() -> f ()
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ())) f (GoalCollector asmp' goal' -> GoalCollector asmp' goal')
-> f (GoalCollector asmp' goal') -> f (GoalCollector asmp' goal')
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> GoalCollector asmp goal -> f (GoalCollector asmp' goal')
go GoalCollector asmp goal
gls
 go (CollectingGoals Seq (Goals asmp goal)
gs GoalCollector asmp goal
gls) = Seq (Goals asmp' goal')
-> GoalCollector asmp' goal' -> GoalCollector asmp' goal'
forall asmp goal.
Seq (Goals asmp goal)
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingGoals (Seq (Goals asmp' goal')
 -> GoalCollector asmp' goal' -> GoalCollector asmp' goal')
-> f (Seq (Goals asmp' goal'))
-> f (GoalCollector asmp' goal' -> GoalCollector asmp' goal')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Seq (Goals asmp goal)
-> f (Seq (Goals asmp' goal'))
forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Seq (Goals asmp goal)
-> f (Seq (Goals asmp' goal'))
traverseGoalsSeq asmp -> f a -> f (asmp', a)
forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl Seq (Goals asmp goal)
gs f (GoalCollector asmp' goal' -> GoalCollector asmp' goal')
-> f (GoalCollector asmp' goal') -> f (GoalCollector asmp' goal')
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> GoalCollector asmp goal -> f (GoalCollector asmp' goal')
go GoalCollector asmp goal
gls

-- | Traverse the goals in a 'GoalCollector', keeping track,
--   for each goal, of the assumptions leading to that goal.
traverseGoalCollectorWithAssumptions :: (Applicative f, Monoid asmp) =>
  (asmp -> goal -> f (Maybe goal')) ->
  GoalCollector asmp goal -> f (GoalCollector asmp goal')
traverseGoalCollectorWithAssumptions :: forall (f :: Type -> Type) asmp goal goal'.
(Applicative f, Monoid asmp) =>
(asmp -> goal -> f (Maybe goal'))
-> GoalCollector asmp goal -> f (GoalCollector asmp goal')
traverseGoalCollectorWithAssumptions asmp -> goal -> f (Maybe goal')
f GoalCollector asmp goal
gc =
    ReaderT asmp f (GoalCollector asmp goal')
-> asmp -> f (GoalCollector asmp goal')
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT ((forall a. asmp -> ReaderT asmp f a -> ReaderT asmp f (asmp, a))
-> (goal -> ReaderT asmp f (Maybe goal'))
-> GoalCollector asmp goal
-> ReaderT asmp f (GoalCollector asmp goal')
forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> GoalCollector asmp goal
-> f (GoalCollector asmp' goal')
traverseGoalCollector asmp -> ReaderT asmp f a -> ReaderT asmp f (asmp, a)
forall a. asmp -> ReaderT asmp f a -> ReaderT asmp f (asmp, a)
forall {m :: Type -> Type} {r} {a}.
(Functor m, Semigroup r) =>
r -> ReaderT r m a -> ReaderT r m (r, a)
fas goal -> ReaderT asmp f (Maybe goal')
fgl GoalCollector asmp goal
gc) asmp
forall a. Monoid a => a
mempty
  where
  fas :: r -> ReaderT r m a -> ReaderT r m (r, a)
fas r
a ReaderT r m a
m = (r
a,) (a -> (r, a)) -> ReaderT r m a -> ReaderT r m (r, a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (r -> r) -> ReaderT r m a -> ReaderT r m a
forall r' r (m :: Type -> Type) a.
(r' -> r) -> ReaderT r m a -> ReaderT r' m a
withReaderT (r -> r -> r
forall a. Semigroup a => a -> a -> a
<> r
a) ReaderT r m a
m
  fgl :: goal -> ReaderT asmp f (Maybe goal')
fgl goal
gl  = (asmp -> f (Maybe goal')) -> ReaderT asmp f (Maybe goal')
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((asmp -> f (Maybe goal')) -> ReaderT asmp f (Maybe goal'))
-> (asmp -> f (Maybe goal')) -> ReaderT asmp f (Maybe goal')
forall a b. (a -> b) -> a -> b
$ \asmp
as -> asmp -> goal -> f (Maybe goal')
f asmp
as goal
gl


-- | The 'AssumptionFrames' data structure captures the current state of
--   assumptions made inside a 'GoalCollector'.
data AssumptionFrames asmp =
  AssumptionFrames
  { -- | Assumptions made at the top level of a solver.
    forall asmp. AssumptionFrames asmp -> asmp
baseFrame    :: !asmp
    -- | A sequence of pushed frames, together with the assumptions that
    --   were made in each frame.  The sequence is organized with newest
    --   frames on the end (right side) of the sequence.
  , forall asmp. AssumptionFrames asmp -> Seq (FrameIdentifier, asmp)
pushedFrames :: !(Seq (FrameIdentifier, asmp))
  }

-- | Return a list of all the assumption frames in this goal collector.
--   The first element of the pair is a collection of assumptions made
--   unconditionaly at top level.  The remaining list is a sequence of
--   assumption frames, each consisting of a collection of assumptions
--   made in that frame.  Frames closer to the front of the list
--   are older.  A `gcPop` will remove the newest (rightmost) frame from the list.
gcFrames :: forall asmp goal. Monoid asmp => GoalCollector asmp goal -> AssumptionFrames asmp
gcFrames :: forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> AssumptionFrames asmp
gcFrames = asmp
-> Seq (FrameIdentifier, asmp)
-> GoalCollector asmp goal
-> AssumptionFrames asmp
go asmp
forall a. Monoid a => a
mempty Seq (FrameIdentifier, asmp)
forall a. Monoid a => a
mempty
  where
  go ::
    asmp ->
    Seq (FrameIdentifier, asmp) ->
    GoalCollector asmp goal ->
    AssumptionFrames asmp

  go :: asmp
-> Seq (FrameIdentifier, asmp)
-> GoalCollector asmp goal
-> AssumptionFrames asmp
go asmp
as Seq (FrameIdentifier, asmp)
fs (TopCollector Seq (Goals asmp goal)
_)
    = asmp -> Seq (FrameIdentifier, asmp) -> AssumptionFrames asmp
forall asmp.
asmp -> Seq (FrameIdentifier, asmp) -> AssumptionFrames asmp
AssumptionFrames asmp
as Seq (FrameIdentifier, asmp)
fs

  go asmp
as Seq (FrameIdentifier, asmp)
fs (CollectorFrame FrameIdentifier
frmid GoalCollector asmp goal
gc) =
    asmp
-> Seq (FrameIdentifier, asmp)
-> GoalCollector asmp goal
-> AssumptionFrames asmp
go asmp
forall a. Monoid a => a
mempty ((FrameIdentifier
frmid, asmp
as) (FrameIdentifier, asmp)
-> Seq (FrameIdentifier, asmp) -> Seq (FrameIdentifier, asmp)
forall a. a -> Seq a -> Seq a
Seq.<| Seq (FrameIdentifier, asmp)
fs) GoalCollector asmp goal
gc

  go asmp
as Seq (FrameIdentifier, asmp)
fs (CollectingAssumptions asmp
as' GoalCollector asmp goal
gc) =
    asmp
-> Seq (FrameIdentifier, asmp)
-> GoalCollector asmp goal
-> AssumptionFrames asmp
go (asmp
as' asmp -> asmp -> asmp
forall a. Semigroup a => a -> a -> a
<> asmp
as) Seq (FrameIdentifier, asmp)
fs GoalCollector asmp goal
gc

  go asmp
as Seq (FrameIdentifier, asmp)
fs (CollectingGoals Seq (Goals asmp goal)
_ GoalCollector asmp goal
gc) =
    asmp
-> Seq (FrameIdentifier, asmp)
-> GoalCollector asmp goal
-> AssumptionFrames asmp
go asmp
as Seq (FrameIdentifier, asmp)
fs GoalCollector asmp goal
gc

-- | Mark the current frame.  Using 'gcPop' will unwind to here.
gcPush :: FrameIdentifier -> GoalCollector asmp goal -> GoalCollector asmp goal
gcPush :: forall asmp goal.
FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcPush FrameIdentifier
frmid GoalCollector asmp goal
gc = FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectorFrame FrameIdentifier
frmid GoalCollector asmp goal
gc

gcAddGoals :: Goals asmp goal -> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddGoals :: forall asmp goal.
Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddGoals Goals asmp goal
g (TopCollector Seq (Goals asmp goal)
gs) = Seq (Goals asmp goal) -> GoalCollector asmp goal
forall asmp goal. Seq (Goals asmp goal) -> GoalCollector asmp goal
TopCollector (Seq (Goals asmp goal)
gs Seq (Goals asmp goal) -> Goals asmp goal -> Seq (Goals asmp goal)
forall a. Seq a -> a -> Seq a
Seq.|> Goals asmp goal
g)
gcAddGoals Goals asmp goal
g (CollectingGoals Seq (Goals asmp goal)
gs GoalCollector asmp goal
gc) = Seq (Goals asmp goal)
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
Seq (Goals asmp goal)
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingGoals (Seq (Goals asmp goal)
gs Seq (Goals asmp goal) -> Goals asmp goal -> Seq (Goals asmp goal)
forall a. Seq a -> a -> Seq a
Seq.|> Goals asmp goal
g) GoalCollector asmp goal
gc
gcAddGoals Goals asmp goal
g GoalCollector asmp goal
gc = Seq (Goals asmp goal)
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
Seq (Goals asmp goal)
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingGoals (Goals asmp goal -> Seq (Goals asmp goal)
forall a. a -> Seq a
Seq.singleton Goals asmp goal
g) GoalCollector asmp goal
gc

-- | Add a new proof obligation to the current context.
gcProve :: goal -> GoalCollector asmp goal -> GoalCollector asmp goal
gcProve :: forall goal asmp.
goal -> GoalCollector asmp goal -> GoalCollector asmp goal
gcProve goal
g = Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddGoals (goal -> Goals asmp goal
forall asmp goal. goal -> Goals asmp goal
Prove goal
g)

-- | Add a sequence of extra assumptions to the current context.
gcAddAssumes :: Monoid asmp => asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddAssumes :: forall asmp goal.
Monoid asmp =>
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddAssumes asmp
as' (CollectingAssumptions asmp
as GoalCollector asmp goal
gls) = asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingAssumptions (asmp
as asmp -> asmp -> asmp
forall a. Semigroup a => a -> a -> a
<> asmp
as') GoalCollector asmp goal
gls
gcAddAssumes asmp
as' GoalCollector asmp goal
gls = asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingAssumptions asmp
as' GoalCollector asmp goal
gls

{- | Pop to the last push, or all the way to the top, if there were no more pushes.
If the result is 'Left', then we popped until an explicitly marked push;
in that case we return:

    1. the frame identifier of the popped frame,
    2. the assumptions that were forgotten,
    3. any proof goals that were generated since the frame push, and
    4. the state of the collector before the push.

If the result is 'Right', then we popped all the way to the top, and the
result is the goal tree, or 'Nothing' if there were no goals. -}

gcPop ::
  Monoid asmp =>
  GoalCollector asmp goal ->
  Either (FrameIdentifier, asmp, Maybe (Goals asmp goal), GoalCollector asmp goal)
         (Maybe (Goals asmp goal))
gcPop :: forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal
-> Either
     (FrameIdentifier, asmp, Maybe (Goals asmp goal),
      GoalCollector asmp goal)
     (Maybe (Goals asmp goal))
gcPop = Maybe (Goals asmp goal)
-> asmp
-> GoalCollector asmp goal
-> Either
     (FrameIdentifier, asmp, Maybe (Goals asmp goal),
      GoalCollector asmp goal)
     (Maybe (Goals asmp goal))
forall {t} {goal}.
Monoid t =>
Maybe (Goals t goal)
-> t
-> GoalCollector t goal
-> Either
     (FrameIdentifier, t, Maybe (Goals t goal), GoalCollector t goal)
     (Maybe (Goals t goal))
go Maybe (Goals asmp goal)
forall a. Maybe a
Nothing asmp
forall a. Monoid a => a
mempty
  where

  {- The function `go` completes frames one at a time.  The "hole" is what
     we should use to complete the current path.  If it is 'Nothing', then
     there was nothing interesting on the current path, and we discard
     assumptions that lead to here -}
  go :: Maybe (Goals t goal)
-> t
-> GoalCollector t goal
-> Either
     (FrameIdentifier, t, Maybe (Goals t goal), GoalCollector t goal)
     (Maybe (Goals t goal))
go Maybe (Goals t goal)
hole t
_as (TopCollector Seq (Goals t goal)
gs) =
    Maybe (Goals t goal)
-> Either
     (FrameIdentifier, t, Maybe (Goals t goal), GoalCollector t goal)
     (Maybe (Goals t goal))
forall a b. b -> Either a b
Right (Maybe (Goals t goal)
-> Maybe (Goals t goal) -> Maybe (Goals t goal)
forall asmp goal.
Maybe (Goals asmp goal)
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj (Seq (Goals t goal) -> Maybe (Goals t goal)
forall (t :: Type -> Type) asmp goal.
Foldable t =>
t (Goals asmp goal) -> Maybe (Goals asmp goal)
proveAll Seq (Goals t goal)
gs) Maybe (Goals t goal)
hole)

  go Maybe (Goals t goal)
hole t
as (CollectorFrame FrameIdentifier
fid GoalCollector t goal
gc) =
    (FrameIdentifier, t, Maybe (Goals t goal), GoalCollector t goal)
-> Either
     (FrameIdentifier, t, Maybe (Goals t goal), GoalCollector t goal)
     (Maybe (Goals t goal))
forall a b. a -> Either a b
Left (FrameIdentifier
fid, t
as, Maybe (Goals t goal)
hole, GoalCollector t goal
gc)

  go Maybe (Goals t goal)
hole t
as (CollectingAssumptions t
as' GoalCollector t goal
gc) =
    Maybe (Goals t goal)
-> t
-> GoalCollector t goal
-> Either
     (FrameIdentifier, t, Maybe (Goals t goal), GoalCollector t goal)
     (Maybe (Goals t goal))
go (t -> Goals t goal -> Goals t goal
forall asmp goal.
Monoid asmp =>
asmp -> Goals asmp goal -> Goals asmp goal
assuming t
as' (Goals t goal -> Goals t goal)
-> Maybe (Goals t goal) -> Maybe (Goals t goal)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Goals t goal)
hole) (t
as' t -> t -> t
forall a. Semigroup a => a -> a -> a
<> t
as) GoalCollector t goal
gc

  go Maybe (Goals t goal)
hole t
as (CollectingGoals Seq (Goals t goal)
gs GoalCollector t goal
gc) =
    Maybe (Goals t goal)
-> t
-> GoalCollector t goal
-> Either
     (FrameIdentifier, t, Maybe (Goals t goal), GoalCollector t goal)
     (Maybe (Goals t goal))
go (Maybe (Goals t goal)
-> Maybe (Goals t goal) -> Maybe (Goals t goal)
forall asmp goal.
Maybe (Goals asmp goal)
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj (Seq (Goals t goal) -> Maybe (Goals t goal)
forall (t :: Type -> Type) asmp goal.
Foldable t =>
t (Goals asmp goal) -> Maybe (Goals asmp goal)
proveAll Seq (Goals t goal)
gs) Maybe (Goals t goal)
hole) t
as GoalCollector t goal
gc

-- | Get all currently collected goals.
gcFinish :: Monoid asmp => GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish :: forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish GoalCollector asmp goal
gc = case GoalCollector asmp goal
-> Either
     (FrameIdentifier, asmp, Maybe (Goals asmp goal),
      GoalCollector asmp goal)
     (Maybe (Goals asmp goal))
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal
-> Either
     (FrameIdentifier, asmp, Maybe (Goals asmp goal),
      GoalCollector asmp goal)
     (Maybe (Goals asmp goal))
gcPop GoalCollector asmp goal
gc of
                Left (FrameIdentifier
_,asmp
_,Just Goals asmp goal
g,GoalCollector asmp goal
gc1)  -> GoalCollector asmp goal -> Maybe (Goals asmp goal)
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish (Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddGoals Goals asmp goal
g GoalCollector asmp goal
gc1)
                Left (FrameIdentifier
_,asmp
_,Maybe (Goals asmp goal)
Nothing,GoalCollector asmp goal
gc1) -> GoalCollector asmp goal -> Maybe (Goals asmp goal)
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish GoalCollector asmp goal
gc1
                Right Maybe (Goals asmp goal)
a -> Maybe (Goals asmp goal)
a

-- | Reset the goal collector to the empty assumption state; but first
--   collect all the pending proof goals and stash them.
gcReset :: Monoid asmp => GoalCollector asmp goal -> GoalCollector asmp goal
gcReset :: forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> GoalCollector asmp goal
gcReset GoalCollector asmp goal
gc = Seq (Goals asmp goal) -> GoalCollector asmp goal
forall asmp goal. Seq (Goals asmp goal) -> GoalCollector asmp goal
TopCollector Seq (Goals asmp goal)
gls
  where
  gls :: Seq (Goals asmp goal)
gls = case GoalCollector asmp goal -> Maybe (Goals asmp goal)
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish GoalCollector asmp goal
gc of
          Maybe (Goals asmp goal)
Nothing     -> Seq (Goals asmp goal)
forall a. Monoid a => a
mempty
          Just Goals asmp goal
p      -> Goals asmp goal -> Seq (Goals asmp goal)
forall a. a -> Seq a
Seq.singleton Goals asmp goal
p

pushGoalsToTop :: Goals asmp goal -> GoalCollector asmp goal -> GoalCollector asmp goal
pushGoalsToTop :: forall asmp goal.
Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
pushGoalsToTop Goals asmp goal
gls = GoalCollector asmp goal -> GoalCollector asmp goal
go
 where
 go :: GoalCollector asmp goal -> GoalCollector asmp goal
go (TopCollector Seq (Goals asmp goal)
gls') = Seq (Goals asmp goal) -> GoalCollector asmp goal
forall asmp goal. Seq (Goals asmp goal) -> GoalCollector asmp goal
TopCollector (Seq (Goals asmp goal)
gls' Seq (Goals asmp goal) -> Goals asmp goal -> Seq (Goals asmp goal)
forall a. Seq a -> a -> Seq a
Seq.|> Goals asmp goal
gls)
 go (CollectorFrame FrameIdentifier
fid GoalCollector asmp goal
gc) = FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectorFrame FrameIdentifier
fid (GoalCollector asmp goal -> GoalCollector asmp goal
go GoalCollector asmp goal
gc)
 go (CollectingAssumptions asmp
as GoalCollector asmp goal
gc) = asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingAssumptions asmp
as (GoalCollector asmp goal -> GoalCollector asmp goal
go GoalCollector asmp goal
gc)
 go (CollectingGoals Seq (Goals asmp goal)
gs GoalCollector asmp goal
gc) = Seq (Goals asmp goal)
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
Seq (Goals asmp goal)
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingGoals Seq (Goals asmp goal)
gs (GoalCollector asmp goal -> GoalCollector asmp goal
go GoalCollector asmp goal
gc)

-- | This operation restores the assumption state of the first given
--   `GoalCollector`, overwriting the assumptions state of the second
--   collector.  However, all proof obligations in the second collector
--   are retained and placed into the the first goal collector in the
--   base assumption level.
--
--   The end result is a goal collector that maintains all the active
--   proof obligations of both collectors, and has the same
--   assumption context as the first collector.
gcRestore ::
  Monoid asmp =>
  GoalCollector asmp goal {- ^ The assumption state to restore -} ->
  GoalCollector asmp goal {- ^ The assumptions state to overwrite -} ->
  GoalCollector asmp goal
gcRestore :: forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcRestore GoalCollector asmp goal
restore GoalCollector asmp goal
old =
  case GoalCollector asmp goal -> Maybe (Goals asmp goal)
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish GoalCollector asmp goal
old of
    Maybe (Goals asmp goal)
Nothing -> GoalCollector asmp goal
restore
    Just Goals asmp goal
p  -> Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
pushGoalsToTop Goals asmp goal
p GoalCollector asmp goal
restore

-- | Remove all collected proof obligations, but keep the current set
-- of assumptions.
gcRemoveObligations :: Monoid asmp => GoalCollector asmp goal -> GoalCollector asmp goal
gcRemoveObligations :: forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> GoalCollector asmp goal
gcRemoveObligations = GoalCollector asmp goal -> GoalCollector asmp goal
forall {asmp} {goal} {goal}.
Semigroup asmp =>
GoalCollector asmp goal -> GoalCollector asmp goal
go
 where
 go :: GoalCollector asmp goal -> GoalCollector asmp goal
go (TopCollector Seq (Goals asmp goal)
_) = Seq (Goals asmp goal) -> GoalCollector asmp goal
forall asmp goal. Seq (Goals asmp goal) -> GoalCollector asmp goal
TopCollector Seq (Goals asmp goal)
forall a. Monoid a => a
mempty
 go (CollectorFrame FrameIdentifier
fid GoalCollector asmp goal
gc) = FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
CollectorFrame FrameIdentifier
fid (GoalCollector asmp goal -> GoalCollector asmp goal
go GoalCollector asmp goal
gc)
 go (CollectingAssumptions asmp
as GoalCollector asmp goal
gc) =
      case GoalCollector asmp goal -> GoalCollector asmp goal
go GoalCollector asmp goal
gc of
        CollectingAssumptions asmp
as' GoalCollector asmp goal
gc' -> asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingAssumptions (asmp
as asmp -> asmp -> asmp
forall a. Semigroup a => a -> a -> a
<> asmp
as') GoalCollector asmp goal
gc'
        GoalCollector asmp goal
gc' -> asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
forall asmp goal.
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
CollectingAssumptions asmp
as GoalCollector asmp goal
gc'
 go (CollectingGoals Seq (Goals asmp goal)
_ GoalCollector asmp goal
gc) = GoalCollector asmp goal -> GoalCollector asmp goal
go GoalCollector asmp goal
gc