{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module Lang.Crucible.Backend.AssumptionStack
(
ProofGoal(..)
, Goals(..)
, FrameIdentifier
, AssumptionFrame(..)
, AssumptionFrames(..)
, AssumptionStack(..)
, initAssumptionStack
, saveAssumptionStack
, restoreAssumptionStack
, pushFrame
, popFrame
, popFrameAndGoals
, popFramesUntil
, resetStack
, getProofObligations
, clearProofObligations
, addProofObligation
, inFreshFrame
, 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)
data AssumptionFrame asmp =
AssumptionFrame
{ forall asmp. AssumptionFrame asmp -> FrameIdentifier
assumeFrameIdent :: FrameIdentifier
, forall asmp. AssumptionFrame asmp -> asmp
assumeFrameCond :: asmp
}
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)
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
}
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)
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)
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)
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)
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))
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)
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
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
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
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
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
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))