{-|
Module      : Lang.Crucible.Backend.AssumptionStack
Copyright   : (c) Galois, Inc 2018
License     : BSD3
Maintainer  : Rob Dockins <rdockins@galois.com>

This module provides management support for keeping track
of a context of logical assumptions.  The API provided here
is similar to the interactive mode of an SMT solver.  Logical
conditions can be assumed into the current context, and bundles
of assumptions are organized into frames which are pushed and
popped by the user to manage the state.

Additionally, proof goals can be asserted to the system.  These will be
turned into complete logical statements by assuming the current context
and be stashed in a collection of remembered goals for later dispatch to
solvers.
-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module Lang.Crucible.Backend.AssumptionStack
  ( -- * Assertions and proof goals
    ProofGoal(..)
  , Goals(..)

    -- * Frames and assumption stacks
    -- ** Basic data types
  , FrameIdentifier
  , AssumptionFrame(..)
  , AssumptionFrames(..)
  , AssumptionStack(..)
    -- ** Manipulating assumption stacks
  , initAssumptionStack
  , saveAssumptionStack
  , restoreAssumptionStack
  , pushFrame
  , popFrame
  , popFrameAndGoals
  , popFramesUntil
  , resetStack
  , getProofObligations
  , clearProofObligations
  , addProofObligation
  , inFreshFrame
    -- ** Assumption management
  , collectAssumptions
  , appendAssumptions
  , allAssumptionFrames

  ) where

import           Control.Exception (bracketOnError)
import qualified Data.Foldable as F
import           Data.IORef
import           Data.Parameterized.Nonce

import           Lang.Crucible.Backend.ProofGoals
import           Lang.Crucible.Panic (panic)

-- | A single @AssumptionFrame@ represents a collection
--   of assumptions.  They will later be rescinded when
--   the associated frame is popped from the stack.
data AssumptionFrame asmp =
  AssumptionFrame
  { forall asmp. AssumptionFrame asmp -> FrameIdentifier
assumeFrameIdent :: FrameIdentifier
  , forall asmp. AssumptionFrame asmp -> asmp
assumeFrameCond  :: asmp
  }

-- | An assumption stack is a data structure for tracking
--   logical assumptions and proof obligations.  Assumptions
--   can be added to the current stack frame, and stack frames
--   may be pushed (to remember a previous state) or popped
--   to restore a previous state.
data AssumptionStack asmp ast =
  AssumptionStack
  { forall asmp ast. AssumptionStack asmp ast -> IO FrameIdentifier
assumeStackGen   :: IO FrameIdentifier
  , forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations :: IORef (GoalCollector asmp ast)
  }


allAssumptionFrames :: Monoid asmp => AssumptionStack asmp ast -> IO (AssumptionFrames asmp)
allAssumptionFrames :: forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (AssumptionFrames asmp)
allAssumptionFrames AssumptionStack asmp ast
stk =
  GoalCollector asmp ast -> AssumptionFrames asmp
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> AssumptionFrames asmp
gcFrames (GoalCollector asmp ast -> AssumptionFrames asmp)
-> IO (GoalCollector asmp ast) -> IO (AssumptionFrames asmp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (GoalCollector asmp ast) -> IO (GoalCollector asmp ast)
forall a. IORef a -> IO a
readIORef (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk)

-- | Produce a fresh assumption stack.
initAssumptionStack :: NonceGenerator IO t -> IO (AssumptionStack asmp ast)
initAssumptionStack :: forall t asmp ast.
NonceGenerator IO t -> IO (AssumptionStack asmp ast)
initAssumptionStack NonceGenerator IO t
gen =
  do let genM :: IO FrameIdentifier
genM = Word64 -> FrameIdentifier
FrameIdentifier (Word64 -> FrameIdentifier)
-> (Nonce t Any -> Word64) -> Nonce t Any -> FrameIdentifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nonce t Any -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Nonce t Any -> FrameIdentifier)
-> IO (Nonce t Any) -> IO FrameIdentifier
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NonceGenerator IO t -> IO (Nonce t Any)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
gen
     IORef (GoalCollector asmp ast)
oblsRef <- GoalCollector asmp ast -> IO (IORef (GoalCollector asmp ast))
forall a. a -> IO (IORef a)
newIORef GoalCollector asmp ast
forall asmp goal. GoalCollector asmp goal
emptyGoalCollector
     AssumptionStack asmp ast -> IO (AssumptionStack asmp ast)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return AssumptionStack
            { assumeStackGen :: IO FrameIdentifier
assumeStackGen = IO FrameIdentifier
genM
            , proofObligations :: IORef (GoalCollector asmp ast)
proofObligations = IORef (GoalCollector asmp ast)
oblsRef
            }

-- | Record the current state of the assumption stack in a
--   data structure that can later be used to restore the current
--   assumptions.
--
--   NOTE! however, that proof obligations are NOT copied into the saved
--   stack data. Instead, proof obligations remain only in the original
--   @AssumptionStack@ and the new stack has an empty obligation list.
saveAssumptionStack :: Monoid asmp => AssumptionStack asmp ast -> IO (GoalCollector asmp ast)
saveAssumptionStack :: forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (GoalCollector asmp ast)
saveAssumptionStack AssumptionStack asmp ast
stk =
  GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> GoalCollector asmp goal
gcRemoveObligations (GoalCollector asmp ast -> GoalCollector asmp ast)
-> IO (GoalCollector asmp ast) -> IO (GoalCollector asmp ast)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (GoalCollector asmp ast) -> IO (GoalCollector asmp ast)
forall a. IORef a -> IO a
readIORef (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk)

-- | Restore a previously saved assumption stack.  Any proof
--   obligations in the saved stack will be copied into the
--   assumption stack, which will also retain any proof obligations
--   it had previously.  A saved stack created with `saveAssumptionStack`
--   will have no included proof obligations; restoring such a stack will
--   have no effect on the current proof obligations.
restoreAssumptionStack ::
  Monoid asmp => 
  GoalCollector asmp ast ->
  AssumptionStack asmp ast ->
  IO ()
restoreAssumptionStack :: forall asmp ast.
Monoid asmp =>
GoalCollector asmp ast -> AssumptionStack asmp ast -> IO ()
restoreAssumptionStack GoalCollector asmp ast
gc AssumptionStack asmp ast
stk =
  IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> GoalCollector asmp ast) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) (GoalCollector asmp ast
-> GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcRestore GoalCollector asmp ast
gc)

-- | Add the given collection logical assumptions to the current stack frame.
appendAssumptions ::
  Monoid asmp => asmp -> AssumptionStack asmp ast -> IO ()
appendAssumptions :: forall asmp ast.
Monoid asmp =>
asmp -> AssumptionStack asmp ast -> IO ()
appendAssumptions asmp
ps AssumptionStack asmp ast
stk =
  IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> GoalCollector asmp ast) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) (asmp -> GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
Monoid asmp =>
asmp -> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddAssumes asmp
ps)

-- | Add a new proof obligation to the current collection of obligations based
--   on all the assumptions currently in scope and the predicate in the
--   given assertion.
addProofObligation :: ast -> AssumptionStack asmp ast -> IO ()
addProofObligation :: forall ast asmp. ast -> AssumptionStack asmp ast -> IO ()
addProofObligation ast
p AssumptionStack asmp ast
stk = IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> GoalCollector asmp ast) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) (ast -> GoalCollector asmp ast -> GoalCollector asmp ast
forall goal asmp.
goal -> GoalCollector asmp goal -> GoalCollector asmp goal
gcProve ast
p)


-- | Collect all the assumptions currently in scope in this stack frame
--   and all previously-pushed stack frames.
collectAssumptions :: Monoid asmp => AssumptionStack asmp ast -> IO asmp
collectAssumptions :: forall asmp ast. Monoid asmp => AssumptionStack asmp ast -> IO asmp
collectAssumptions AssumptionStack asmp ast
stk =
  do AssumptionFrames asmp
base Seq (FrameIdentifier, asmp)
frms <- GoalCollector asmp ast -> AssumptionFrames asmp
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> AssumptionFrames asmp
gcFrames (GoalCollector asmp ast -> AssumptionFrames asmp)
-> IO (GoalCollector asmp ast) -> IO (AssumptionFrames asmp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (GoalCollector asmp ast) -> IO (GoalCollector asmp ast)
forall a. IORef a -> IO a
readIORef (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk)
     asmp -> IO asmp
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (asmp
base asmp -> asmp -> asmp
forall a. Semigroup a => a -> a -> a
<> Seq asmp -> asmp
forall m. Monoid m => Seq m -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
F.fold (((FrameIdentifier, asmp) -> asmp)
-> Seq (FrameIdentifier, asmp) -> Seq asmp
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (FrameIdentifier, asmp) -> asmp
forall a b. (a, b) -> b
snd Seq (FrameIdentifier, asmp)
frms))

-- | Retrieve the current collection of proof obligations.
getProofObligations :: Monoid asmp => AssumptionStack asmp ast -> IO (Maybe (Goals asmp ast))
getProofObligations :: forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (Maybe (Goals asmp ast))
getProofObligations AssumptionStack asmp ast
stk = GoalCollector asmp ast -> Maybe (Goals asmp ast)
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> Maybe (Goals asmp goal)
gcFinish (GoalCollector asmp ast -> Maybe (Goals asmp ast))
-> IO (GoalCollector asmp ast) -> IO (Maybe (Goals asmp ast))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (GoalCollector asmp ast) -> IO (GoalCollector asmp ast)
forall a. IORef a -> IO a
readIORef (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk)

-- | Remove all pending proof obligations.
clearProofObligations :: Monoid asmp => AssumptionStack asmp ast -> IO ()
clearProofObligations :: forall asmp ast. Monoid asmp => AssumptionStack asmp ast -> IO ()
clearProofObligations AssumptionStack asmp ast
stk =
  IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> GoalCollector asmp ast) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> GoalCollector asmp goal
gcRemoveObligations

-- | Reset the 'AssumptionStack' to an empty set of assumptions,
--   but retain any pending proof obligations.
resetStack :: Monoid asmp => AssumptionStack asmp ast -> IO ()
resetStack :: forall asmp ast. Monoid asmp => AssumptionStack asmp ast -> IO ()
resetStack AssumptionStack asmp ast
stk = IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> GoalCollector asmp ast) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> GoalCollector asmp goal
gcReset

-- | Push a new assumption frame on top of the stack.  The
--   returned @FrameIdentifier@ can be used later to pop this
--   frame.  Frames must be pushed and popped in a coherent,
--   well-bracketed way.
pushFrame :: AssumptionStack asmp ast -> IO FrameIdentifier
pushFrame :: forall asmp ast. AssumptionStack asmp ast -> IO FrameIdentifier
pushFrame AssumptionStack asmp ast
stk =
  do FrameIdentifier
ident <- AssumptionStack asmp ast -> IO FrameIdentifier
forall asmp ast. AssumptionStack asmp ast -> IO FrameIdentifier
assumeStackGen AssumptionStack asmp ast
stk
     IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> GoalCollector asmp ast) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) (FrameIdentifier -> GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
FrameIdentifier
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcPush FrameIdentifier
ident)
     FrameIdentifier -> IO FrameIdentifier
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return FrameIdentifier
ident

-- | Pop all frames up to and including the frame with the
--   given identifier.  The return value indicates how
--   many stack frames were popped.
popFramesUntil :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO Int
popFramesUntil :: forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO Int
popFramesUntil FrameIdentifier
ident AssumptionStack asmp ast
stk = IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> (GoalCollector asmp ast, Int))
-> IO Int
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) (Int -> GoalCollector asmp ast -> (GoalCollector asmp ast, Int)
go Int
1)
 where
 go :: Int -> GoalCollector asmp ast -> (GoalCollector asmp ast, Int)
go Int
n GoalCollector asmp ast
gc =
    case GoalCollector asmp ast
-> Either
     (FrameIdentifier, asmp, Maybe (Goals asmp ast),
      GoalCollector asmp ast)
     (Maybe (Goals asmp ast))
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 ast
gc of
      Left (FrameIdentifier
ident', asmp
_assumes, Maybe (Goals asmp ast)
mg, GoalCollector asmp ast
gc1)
        | FrameIdentifier
ident FrameIdentifier -> FrameIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== FrameIdentifier
ident' -> (GoalCollector asmp ast
gc',Int
n)
        | Bool
otherwise -> Int -> GoalCollector asmp ast -> (GoalCollector asmp ast, Int)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) GoalCollector asmp ast
gc'
       where gc' :: GoalCollector asmp ast
gc' = case Maybe (Goals asmp ast)
mg of
                     Maybe (Goals asmp ast)
Nothing -> GoalCollector asmp ast
gc1
                     Just Goals asmp ast
g  -> Goals asmp ast -> GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddGoals Goals asmp ast
g GoalCollector asmp ast
gc1
      Right Maybe (Goals asmp ast)
_ ->
        String -> [String] -> (GoalCollector asmp ast, Int)
forall a. HasCallStack => String -> [String] -> a
panic String
"AssumptionStack.popFrameUntil"
          [ String
"Frame not found in stack."
          , String
"*** Frame to pop: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FrameIdentifier -> String
showFrameId FrameIdentifier
ident
          ]

 showFrameId :: FrameIdentifier -> String
showFrameId (FrameIdentifier Word64
x) = Word64 -> String
forall a. Show a => a -> String
show Word64
x

-- | Pop a previously-pushed assumption frame from the stack.
--   All assumptions in that frame will be forgotten.  The
--   assumptions contained in the popped frame are returned.
popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
popFrame :: forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
popFrame FrameIdentifier
ident AssumptionStack asmp ast
stk =
  IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast -> (GoalCollector asmp ast, asmp))
-> IO asmp
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) ((GoalCollector asmp ast -> (GoalCollector asmp ast, asmp))
 -> IO asmp)
-> (GoalCollector asmp ast -> (GoalCollector asmp ast, asmp))
-> IO asmp
forall a b. (a -> b) -> a -> b
$ \GoalCollector asmp ast
gc ->
       case GoalCollector asmp ast
-> Either
     (FrameIdentifier, asmp, Maybe (Goals asmp ast),
      GoalCollector asmp ast)
     (Maybe (Goals asmp ast))
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 ast
gc of
         Left (FrameIdentifier
ident', asmp
assumes, Maybe (Goals asmp ast)
mg, GoalCollector asmp ast
gc1)
           | FrameIdentifier
ident FrameIdentifier -> FrameIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== FrameIdentifier
ident' ->
                let gc' :: GoalCollector asmp ast
gc' = case Maybe (Goals asmp ast)
mg of
                            Maybe (Goals asmp ast)
Nothing -> GoalCollector asmp ast
gc1
                            Just Goals asmp ast
g  -> Goals asmp ast -> GoalCollector asmp ast -> GoalCollector asmp ast
forall asmp goal.
Goals asmp goal
-> GoalCollector asmp goal -> GoalCollector asmp goal
gcAddGoals Goals asmp ast
g GoalCollector asmp ast
gc1
                 in (GoalCollector asmp ast
gc', asmp
assumes)
           | Bool
otherwise ->
               String -> [String] -> (GoalCollector asmp ast, asmp)
forall a. HasCallStack => String -> [String] -> a
panic String
"AssumptionStack.popFrame"
                [ String
"Push/pop mismatch in assumption stack!"
                , String
"*** Current frame:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FrameIdentifier -> String
showFrameId FrameIdentifier
ident
                , String
"*** Expected ident: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FrameIdentifier -> String
showFrameId FrameIdentifier
ident'
                ]
         Right Maybe (Goals asmp ast)
_  ->
           String -> [String] -> (GoalCollector asmp ast, asmp)
forall a. HasCallStack => String -> [String] -> a
panic String
"AssumptionStack.popFrame"
             [ String
"Pop with no push in goal collector."
             , String
"*** Current frame: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FrameIdentifier -> String
showFrameId FrameIdentifier
ident
             ]

  where
  showFrameId :: FrameIdentifier -> String
showFrameId (FrameIdentifier Word64
x) = Word64 -> String
forall a. Show a => a -> String
show Word64
x


popFrameAndGoals ::
  Monoid asmp =>
  FrameIdentifier ->
  AssumptionStack asmp ast ->
  IO (asmp, Maybe (Goals asmp ast))
popFrameAndGoals :: forall asmp ast.
Monoid asmp =>
FrameIdentifier
-> AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast))
popFrameAndGoals FrameIdentifier
ident AssumptionStack asmp ast
stk =
  IORef (GoalCollector asmp ast)
-> (GoalCollector asmp ast
    -> (GoalCollector asmp ast, (asmp, Maybe (Goals asmp ast))))
-> IO (asmp, Maybe (Goals asmp ast))
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
forall asmp ast.
AssumptionStack asmp ast -> IORef (GoalCollector asmp ast)
proofObligations AssumptionStack asmp ast
stk) ((GoalCollector asmp ast
  -> (GoalCollector asmp ast, (asmp, Maybe (Goals asmp ast))))
 -> IO (asmp, Maybe (Goals asmp ast)))
-> (GoalCollector asmp ast
    -> (GoalCollector asmp ast, (asmp, Maybe (Goals asmp ast))))
-> IO (asmp, Maybe (Goals asmp ast))
forall a b. (a -> b) -> a -> b
$ \GoalCollector asmp ast
gc ->
       case GoalCollector asmp ast
-> Either
     (FrameIdentifier, asmp, Maybe (Goals asmp ast),
      GoalCollector asmp ast)
     (Maybe (Goals asmp ast))
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 ast
gc of
         Left (FrameIdentifier
ident', asmp
assumes, Maybe (Goals asmp ast)
mg, GoalCollector asmp ast
gc1)
           | FrameIdentifier
ident FrameIdentifier -> FrameIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== FrameIdentifier
ident' -> (GoalCollector asmp ast
gc1, (asmp
assumes, Maybe (Goals asmp ast)
mg))
           | Bool
otherwise ->
               String
-> [String]
-> (GoalCollector asmp ast, (asmp, Maybe (Goals asmp ast)))
forall a. HasCallStack => String -> [String] -> a
panic String
"AssumptionStack.popFrameAndGoals"
                [ String
"Push/pop mismatch in assumption stack!"
                , String
"*** Current frame:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FrameIdentifier -> String
showFrameId FrameIdentifier
ident
                , String
"*** Expected ident: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FrameIdentifier -> String
showFrameId FrameIdentifier
ident'
                ]
         Right Maybe (Goals asmp ast)
_  ->
           String
-> [String]
-> (GoalCollector asmp ast, (asmp, Maybe (Goals asmp ast)))
forall a. HasCallStack => String -> [String] -> a
panic String
"AssumptionStack.popFrameAndGoals"
             [ String
"Pop with no push in goal collector."
             , String
"*** Current frame: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FrameIdentifier -> String
showFrameId FrameIdentifier
ident
             ]

  where
  showFrameId :: FrameIdentifier -> String
showFrameId (FrameIdentifier Word64
x) = Word64 -> String
forall a. Show a => a -> String
show Word64
x


-- | Run an action in the scope of a fresh assumption frame.
--   The frame will be popped and returned on successful
--   completion of the action.  If the action raises an exception,
--   the frame will be popped and discarded.
inFreshFrame :: Monoid asmp => AssumptionStack asmp ast -> IO a -> IO (asmp, a)
inFreshFrame :: forall asmp ast a.
Monoid asmp =>
AssumptionStack asmp ast -> IO a -> IO (asmp, a)
inFreshFrame AssumptionStack asmp ast
stk IO a
action =
  IO FrameIdentifier
-> (FrameIdentifier -> IO asmp)
-> (FrameIdentifier -> IO (asmp, a))
-> IO (asmp, a)
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracketOnError
     (AssumptionStack asmp ast -> IO FrameIdentifier
forall asmp ast. AssumptionStack asmp ast -> IO FrameIdentifier
pushFrame AssumptionStack asmp ast
stk)
     (\FrameIdentifier
ident -> FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
popFrame FrameIdentifier
ident AssumptionStack asmp ast
stk)
     (\FrameIdentifier
ident -> do a
x <- IO a
action
                   asmp
frm <- FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
popFrame FrameIdentifier
ident AssumptionStack asmp ast
stk
                   (asmp, a) -> IO (asmp, a)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (asmp
frm, a
x))