{-|
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.Functor.Const
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Word

-- | A proof goal consists of a collection of assumptions
--   that were in scope when an assertion was made, together
--   with the given assertion.
data ProofGoal asmp goal =
  ProofGoal
  { forall asmp goal. ProofGoal asmp goal -> asmp
proofAssumptions :: asmp
  , forall asmp goal. ProofGoal asmp goal -> goal
proofGoal        :: goal
  }

-- | A collection of goals, which can represent shared assumptions.
data Goals asmp goal =
    -- | Make an assumption that is in context for all the
    --   contained goals.
    Assuming asmp !(Goals asmp goal)

    -- | A proof obligation, to be proved in the context of
    --   all previously-made assumptions.
  | Prove goal

    -- | A conjunction of two goals.
  | ProveConj !(Goals asmp goal) !(Goals asmp goal)
    deriving Int -> Goals asmp goal -> ShowS
[Goals asmp goal] -> ShowS
Goals asmp goal -> String
(Int -> Goals asmp goal -> ShowS)
-> (Goals asmp goal -> String)
-> ([Goals asmp goal] -> ShowS)
-> Show (Goals asmp goal)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall asmp goal.
(Show asmp, Show goal) =>
Int -> Goals asmp goal -> ShowS
forall asmp goal.
(Show asmp, Show goal) =>
[Goals asmp goal] -> ShowS
forall asmp goal.
(Show asmp, Show goal) =>
Goals asmp goal -> String
$cshowsPrec :: forall asmp goal.
(Show asmp, Show goal) =>
Int -> Goals asmp goal -> ShowS
showsPrec :: Int -> Goals asmp goal -> ShowS
$cshow :: forall asmp goal.
(Show asmp, Show goal) =>
Goals asmp goal -> String
show :: Goals asmp goal -> String
$cshowList :: forall asmp goal.
(Show asmp, Show goal) =>
[Goals asmp goal] -> ShowS
showList :: [Goals asmp goal] -> ShowS
Show

-- | Construct a goal that first assumes a collection of
--   assumptions and then states a goal.
assuming :: Monoid asmp => asmp -> Goals asmp goal -> Goals asmp goal
assuming :: forall asmp goal.
Monoid asmp =>
asmp -> Goals asmp goal -> Goals asmp goal
assuming asmp
as (Assuming asmp
bs Goals asmp goal
g) = asmp -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Monoid asmp =>
asmp -> Goals asmp goal -> Goals asmp goal
assuming (asmp
as asmp -> asmp -> asmp
forall a. Semigroup a => a -> a -> a
<> asmp
bs) Goals asmp goal
g
assuming asmp
as Goals asmp goal
g = asmp -> Goals asmp goal -> Goals asmp goal
forall asmp goal. asmp -> Goals asmp goal -> Goals asmp goal
Assuming asmp
as Goals asmp goal
g

-- | Construct a 'Goals' object from a collection of subgoals, all of
--   which are to be proved.  This yields 'Nothing' if the collection
--   of goals is empty, and otherwise builds a conjunction of all the
--   goals.  Note that there is no new sharing in the resulting structure.
proveAll :: Foldable t => t (Goals asmp goal) -> Maybe (Goals asmp goal)
proveAll :: forall (t :: Type -> Type) asmp goal.
Foldable t =>
t (Goals asmp goal) -> Maybe (Goals asmp goal)
proveAll = (Goals asmp goal
 -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal))
-> Maybe (Goals asmp goal)
-> t (Goals asmp goal)
-> Maybe (Goals asmp goal)
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goals asmp goal
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
forall {asmp} {goal}.
Goals asmp goal
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
f Maybe (Goals asmp goal)
forall a. Maybe a
Nothing
 where
 f :: Goals asmp goal
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
f Goals asmp goal
x Maybe (Goals asmp goal)
Nothing  = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Maybe (Goals asmp goal))
-> Goals asmp goal -> Maybe (Goals asmp goal)
forall a b. (a -> b) -> a -> b
$! Goals asmp goal
x
 f Goals asmp goal
x (Just Goals asmp goal
y) = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Maybe (Goals asmp goal))
-> Goals asmp goal -> Maybe (Goals asmp goal)
forall a b. (a -> b) -> a -> b
$! Goals asmp goal -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Goals asmp goal -> Goals asmp goal -> Goals asmp goal
ProveConj Goals asmp goal
x Goals asmp goal
y

-- | Helper to conjoin two possibly trivial 'Goals' objects.
goalsConj :: Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj :: forall asmp goal.
Maybe (Goals asmp goal)
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj Maybe (Goals asmp goal)
Nothing Maybe (Goals asmp goal)
y = Maybe (Goals asmp goal)
y
goalsConj Maybe (Goals asmp goal)
x Maybe (Goals asmp goal)
Nothing = Maybe (Goals asmp goal)
x
goalsConj (Just Goals asmp goal
x) (Just Goals asmp goal
y) = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Goals asmp goal -> Goals asmp goal -> Goals asmp goal
ProveConj Goals asmp goal
x Goals asmp goal
y)

-- | Render the tree of goals as a list instead, duplicating
--   shared assumptions over each goal as necessary.
goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal]
goalsToList :: forall asmp goal.
Monoid asmp =>
Goals asmp goal -> [ProofGoal asmp goal]
goalsToList =
  Const [ProofGoal asmp goal] (Maybe (Goals asmp Any))
-> [ProofGoal asmp goal]
forall {k} a (b :: k). Const a b -> a
getConst (Const [ProofGoal asmp goal] (Maybe (Goals asmp Any))
 -> [ProofGoal asmp goal])
-> (Goals asmp goal
    -> Const [ProofGoal asmp goal] (Maybe (Goals asmp Any)))
-> Goals asmp goal
-> [ProofGoal asmp goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (asmp -> goal -> Const [ProofGoal asmp goal] (Maybe Any))
-> Goals asmp goal
-> Const [ProofGoal asmp goal] (Maybe (Goals asmp Any))
forall (f :: Type -> Type) asmp goal goal'.
(Applicative f, Monoid asmp) =>
(asmp -> goal -> f (Maybe goal'))
-> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseGoalsWithAssumptions
    (\asmp
as goal
g -> [ProofGoal asmp goal] -> Const [ProofGoal asmp goal] (Maybe Any)
forall {k} a (b :: k). a -> Const a b
Const [asmp -> goal -> ProofGoal asmp goal
forall asmp goal. asmp -> goal -> ProofGoal asmp goal
ProofGoal asmp
as goal
g])

-- | Traverse the structure of a 'Goals' data structure.  The function for
--   visiting goals my decide to remove the goal from the structure.  If
--   no goals remain after the traversal, the resulting value will be a 'Nothing'.
--
--   In a call to 'traverseGoals assumeAction transformer goals', the
--   arguments are used as follows:
--
--   * 'traverseGoals' is an action is called every time we encounter
--     an 'Assuming' constructor.  The first argument is the original
--     sequence of assumptions.  The second argument is a continuation
--     action.  The result is a sequence of transformed assumptions
--     and the result of the continuation action.
--
--   * 'assumeAction' is a transformer action on goals.  Return
--     'Nothing' if you wish to remove the goal from the overall tree.
traverseGoals :: (Applicative f, Monoid asmp') =>
                 (forall a. asmp -> f a -> f (asmp', a))
              -> (goal -> f (Maybe goal'))
              -> Goals asmp goal
              -> f (Maybe (Goals asmp' goal'))
traverseGoals :: forall (f :: Type -> Type) asmp' asmp goal goal'.
(Applicative f, Monoid asmp') =>
(forall a. asmp -> f a -> f (asmp', a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl = Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go
  where
  go :: Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go (Prove goal
gl)        = (goal' -> Goals asmp' goal')
-> Maybe goal' -> Maybe (Goals asmp' goal')
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap goal' -> Goals asmp' goal'
forall asmp goal. goal -> Goals asmp goal
Prove (Maybe goal' -> Maybe (Goals asmp' goal'))
-> f (Maybe goal') -> f (Maybe (Goals asmp' goal'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> goal -> f (Maybe goal')
fgl goal
gl
  go (Assuming asmp
as Goals asmp goal
gl)  = (asmp', Maybe (Goals asmp' goal')) -> Maybe (Goals asmp' goal')
forall {asmp} {goal}.
Monoid asmp =>
(asmp, Maybe (Goals asmp goal)) -> Maybe (Goals asmp goal)
assuming' ((asmp', Maybe (Goals asmp' goal')) -> Maybe (Goals asmp' goal'))
-> f (asmp', Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> asmp
-> f (Maybe (Goals asmp' goal'))
-> f (asmp', Maybe (Goals asmp' goal'))
forall a. asmp -> f a -> f (asmp', a)
fas asmp
as (Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go Goals asmp goal
gl)
  go (ProveConj Goals asmp goal
g1 Goals asmp goal
g2) = Maybe (Goals asmp' goal')
-> Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal')
forall asmp goal.
Maybe (Goals asmp goal)
-> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)
goalsConj (Maybe (Goals asmp' goal')
 -> Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go Goals asmp goal
g1 f (Maybe (Goals asmp' goal') -> Maybe (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal')) -> f (Maybe (Goals 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
<*> Goals asmp goal -> f (Maybe (Goals asmp' goal'))
go Goals asmp goal
g2

  assuming' :: (asmp, Maybe (Goals asmp goal)) -> Maybe (Goals asmp goal)
assuming' (asmp
_, Maybe (Goals asmp goal)
Nothing) = Maybe (Goals asmp goal)
forall a. Maybe a
Nothing
  assuming' (asmp
as, Just Goals asmp goal
g) = Goals asmp goal -> Maybe (Goals asmp goal)
forall a. a -> Maybe a
Just (Goals asmp goal -> Maybe (Goals asmp goal))
-> Goals asmp goal -> Maybe (Goals asmp goal)
forall a b. (a -> b) -> a -> b
$! asmp -> Goals asmp goal -> Goals asmp goal
forall asmp goal.
Monoid asmp =>
asmp -> Goals asmp goal -> Goals asmp goal
assuming asmp
as Goals asmp goal
g


traverseOnlyGoals :: (Applicative f, Monoid asmp) =>
  (goal -> f (Maybe goal')) ->
  Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseOnlyGoals :: forall (f :: Type -> Type) asmp goal goal'.
(Applicative f, Monoid asmp) =>
(goal -> f (Maybe goal'))
-> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseOnlyGoals goal -> f (Maybe goal')
f = (forall a. asmp -> f a -> f (asmp, a))
-> (goal -> f (Maybe goal'))
-> Goals asmp goal
-> f (Maybe (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'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals (\asmp
as f a
m -> (asmp
as,) (a -> (asmp, a)) -> f a -> f (asmp, a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
m) goal -> f (Maybe goal')
f

-- | Traverse a sequence of 'Goals' data structures.  See 'traverseGoals'
--   for an explanation of the action arguments.  The resulting sequence
--   may be shorter than the original if some 'Goals' become trivial.
traverseGoalsSeq :: (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 :: 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 forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl = Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))
go
  where
  go :: Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))
go Seq (Goals asmp goal)
Seq.Empty      = Seq (Goals asmp' goal') -> f (Seq (Goals asmp' goal'))
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Seq (Goals asmp' goal')
forall a. Seq a
Seq.Empty
  go (Goals asmp goal
g Seq.:<| Seq (Goals asmp goal)
gs) = Maybe (Goals asmp' goal')
-> Seq (Goals asmp' goal') -> Seq (Goals asmp' goal')
forall {a}. Maybe a -> Seq a -> Seq a
combine (Maybe (Goals asmp' goal')
 -> Seq (Goals asmp' goal') -> Seq (Goals asmp' goal'))
-> f (Maybe (Goals asmp' goal'))
-> f (Seq (Goals asmp' goal') -> Seq (Goals 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'))
-> Goals asmp goal
-> f (Maybe (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'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals asmp -> f a -> f (asmp', a)
forall a. asmp -> f a -> f (asmp', a)
fas goal -> f (Maybe goal')
fgl Goals asmp goal
g f (Seq (Goals asmp' goal') -> Seq (Goals asmp' goal'))
-> f (Seq (Goals asmp' goal')) -> f (Seq (Goals 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
<*> Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))
go Seq (Goals asmp goal)
gs

  combine :: Maybe a -> Seq a -> Seq a
combine Maybe a
Nothing Seq a
gs  = Seq a
gs
  combine (Just a
g) Seq a
gs = a
g a -> Seq a -> Seq a
forall a. a -> Seq a -> Seq a
Seq.<| Seq a
gs

-- | Visit every goal in a 'Goals' structure, remembering the sequence of
--   assumptions along the way to that goal.
traverseGoalsWithAssumptions :: (Applicative f, Monoid asmp) =>
  (asmp -> goal -> f (Maybe goal')) ->
  Goals asmp goal -> f (Maybe (Goals asmp goal'))

traverseGoalsWithAssumptions :: forall (f :: Type -> Type) asmp goal goal'.
(Applicative f, Monoid asmp) =>
(asmp -> goal -> f (Maybe goal'))
-> Goals asmp goal -> f (Maybe (Goals asmp goal'))
traverseGoalsWithAssumptions asmp -> goal -> f (Maybe goal')
f Goals asmp goal
gls =
   ReaderT asmp f (Maybe (Goals asmp goal'))
-> asmp -> f (Maybe (Goals 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'))
-> Goals asmp goal
-> ReaderT asmp f (Maybe (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'))
-> Goals asmp goal
-> f (Maybe (Goals asmp' goal'))
traverseGoals 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 Goals asmp goal
gls) 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


-- | 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)


-- | 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