{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Lang.Crucible.CFG.Reg
(
CFG(..)
, cfgEntryBlock
, cfgInputTypes
, cfgArgTypes
, cfgReturnType
, substCFG
, SomeCFG(..)
, AnyCFG(..)
, Label(..)
, substLabel
, LambdaLabel(..)
, substLambdaLabel
, BlockID(..)
, substBlockID
, Reg(..)
, substReg
, traverseCFG
, Atom(..)
, substAtom
, AtomSource(..)
, substAtomSource
, mkInputAtoms
, AtomValue(..)
, typeOfAtomValue
, substAtomValue
, Value(..)
, typeOfValue
, substValue
, ValueSet
, substValueSet
, Block
, mkBlock
, blockID
, blockStmts
, blockTerm
, blockExtraInputs
, blockKnownInputs
, blockAssignedValues
, substBlock
, Stmt(..)
, substStmt, substPosdStmt, mapStmtAtom
, TermStmt(..)
, termStmtInputs
, termNextLabels
, substTermStmt, substPosdTermStmt
, foldStmtInputs
, Expr(..)
, exprType
, substExpr
, module Lang.Crucible.CFG.Common
) where
import qualified Data.Foldable as Fold
import Data.Kind (Type)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe)
import Data.Parameterized.Classes
import Data.Parameterized.Context as Ctx
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Sequence (Seq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String
import Data.Word (Word64)
import Prettyprinter
import What4.ProgramLoc
import What4.Symbol
import Lang.Crucible.CFG.Common
import Lang.Crucible.CFG.Expr
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Panic (panic)
import Lang.Crucible.Syntax (IsExpr(..))
import Lang.Crucible.Types
commas :: [Doc ann] -> Doc ann
commas :: forall ann. [Doc ann] -> Doc ann
commas [Doc ann]
l = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hcat (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate (Doc ann
forall ann. Doc ann
comma Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
' ') [Doc ann]
l)
newtype Label s = Label { forall s. Label s -> Nonce s UnitType
labelId :: Nonce s UnitType }
labelInt :: Label s -> Word64
labelInt :: forall s. Label s -> Word64
labelInt = Nonce s UnitType -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Nonce s UnitType -> Word64)
-> (Label s -> Nonce s UnitType) -> Label s -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label s -> Nonce s UnitType
forall s. Label s -> Nonce s UnitType
labelId
instance Eq (Label s) where
Label Nonce s UnitType
i == :: Label s -> Label s -> Bool
== Label Nonce s UnitType
j = Nonce s UnitType
i Nonce s UnitType -> Nonce s UnitType -> Bool
forall a. Eq a => a -> a -> Bool
== Nonce s UnitType
j
instance Ord (Label s) where
Label Nonce s UnitType
i compare :: Label s -> Label s -> Ordering
`compare` Label Nonce s UnitType
j = Nonce s UnitType
i Nonce s UnitType -> Nonce s UnitType -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Nonce s UnitType
j
instance Show (Label s) where
show :: Label s -> String
show (Label Nonce s UnitType
i) = Char
'%' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s UnitType -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce s UnitType
i)
instance Pretty (Label s) where
pretty :: forall ann. Label s -> Doc ann
pretty (Label Nonce s UnitType
i) = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'%' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s UnitType -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce s UnitType
i)
substLabel :: Functor m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s
-> m (Label s')
substLabel :: forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l = Nonce s' UnitType -> Label s'
forall s. Nonce s UnitType -> Label s
Label (Nonce s' UnitType -> Label s')
-> m (Nonce s' UnitType) -> m (Label s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Nonce s UnitType -> m (Nonce s' UnitType)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Label s -> Nonce s UnitType
forall s. Label s -> Nonce s UnitType
labelId Label s
l)
data LambdaLabel (s :: Type) (tp :: CrucibleType)
= LambdaLabel
{ forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId :: !(Nonce s tp)
, forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom :: Atom s tp
}
lambdaInt :: LambdaLabel s tp -> Word64
lambdaInt :: forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt = Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Nonce s tp -> Word64)
-> (LambdaLabel s tp -> Nonce s tp) -> LambdaLabel s tp -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId
instance Show (LambdaLabel s tp) where
show :: LambdaLabel s tp -> String
show LambdaLabel s tp
l = Char
'%' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
l))
instance Pretty (LambdaLabel s tp) where
pretty :: forall ann. LambdaLabel s tp -> Doc ann
pretty LambdaLabel s tp
l = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'%' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
l))
substLambdaLabel :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp
-> m (LambdaLabel s' tp)
substLambdaLabel :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll =
Nonce s' tp -> Atom s' tp -> LambdaLabel s' tp
forall s (tp :: CrucibleType).
Nonce s tp -> Atom s tp -> LambdaLabel s tp
LambdaLabel (Nonce s' tp -> Atom s' tp -> LambdaLabel s' tp)
-> m (Nonce s' tp) -> m (Atom s' tp -> LambdaLabel s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Nonce s tp -> m (Nonce s' tp)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
ll) m (Atom s' tp -> LambdaLabel s' tp)
-> m (Atom s' tp) -> m (LambdaLabel s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
ll)
data BlockID (s :: Type) where
LabelID :: Label s -> BlockID s
LambdaID :: LambdaLabel s tp -> BlockID s
instance Show (BlockID s) where
show :: BlockID s -> String
show (LabelID Label s
l) = Label s -> String
forall a. Show a => a -> String
show Label s
l
show (LambdaID LambdaLabel s tp
l) = LambdaLabel s tp -> String
forall a. Show a => a -> String
show LambdaLabel s tp
l
instance Eq (BlockID s) where
LabelID Label s
x == :: BlockID s -> BlockID s -> Bool
== LabelID Label s
y = Label s
x Label s -> Label s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s
y
LambdaID LambdaLabel s tp
x == LambdaID LambdaLabel s tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (LambdaLabel s tp -> LambdaLabel s tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s tp
x LambdaLabel s tp
y)
BlockID s
_ == BlockID s
_ = Bool
False
instance Ord (BlockID s) where
LabelID Label s
x compare :: BlockID s -> BlockID s -> Ordering
`compare` LambdaID LambdaLabel s tp
y = Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Label s -> Word64
forall s. Label s -> Word64
labelInt Label s
x) (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
y)
LabelID Label s
x `compare` LabelID Label s
y = Label s -> Label s -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Label s
x Label s
y
LambdaID LambdaLabel s tp
x `compare` LabelID Label s
y = Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
x) (Label s -> Word64
forall s. Label s -> Word64
labelInt Label s
y)
LambdaID LambdaLabel s tp
x `compare` LambdaID LambdaLabel s tp
y = Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
x) (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
y)
substBlockID :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> BlockID s
-> m (BlockID s')
substBlockID :: forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> BlockID s -> m (BlockID s')
substBlockID forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f BlockID s
bid =
case BlockID s
bid of
LabelID Label s
l -> Label s' -> BlockID s'
forall s. Label s -> BlockID s
LabelID (Label s' -> BlockID s') -> m (Label s') -> m (BlockID s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l
LambdaID LambdaLabel s tp
ll -> LambdaLabel s' tp -> BlockID s'
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
LambdaID (LambdaLabel s' tp -> BlockID s')
-> m (LambdaLabel s' tp) -> m (BlockID s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll
data AtomSource s (tp :: CrucibleType)
= Assigned
| FnInput
| LambdaArg !(LambdaLabel s tp)
substAtomSource :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomSource s tp
-> m (AtomSource s' tp)
substAtomSource :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomSource s tp -> m (AtomSource s' tp)
substAtomSource forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f AtomSource s tp
as =
case AtomSource s tp
as of
AtomSource s tp
Assigned -> AtomSource s' tp -> m (AtomSource s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure AtomSource s' tp
forall s (tp :: CrucibleType). AtomSource s tp
Assigned
AtomSource s tp
FnInput -> AtomSource s' tp -> m (AtomSource s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure AtomSource s' tp
forall s (tp :: CrucibleType). AtomSource s tp
FnInput
LambdaArg LambdaLabel s tp
ll -> LambdaLabel s' tp -> AtomSource s' tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> AtomSource s tp
LambdaArg (LambdaLabel s' tp -> AtomSource s' tp)
-> m (LambdaLabel s' tp) -> m (AtomSource s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll
data Atom s (tp :: CrucibleType)
= Atom { forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition :: !Position
, forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId :: !(Nonce s tp)
, forall s (tp :: CrucibleType). Atom s tp -> AtomSource s tp
atomSource :: !(AtomSource s tp)
, forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom :: !(TypeRepr tp)
}
mkInputAtoms :: forall m s init
. Monad m
=> NonceGenerator m s
-> Position
-> CtxRepr init
-> m (Assignment (Atom s) init)
mkInputAtoms :: forall (m :: Type -> Type) s (init :: Ctx CrucibleType).
Monad m =>
NonceGenerator m s
-> Position -> CtxRepr init -> m (Assignment (Atom s) init)
mkInputAtoms NonceGenerator m s
ng Position
p CtxRepr init
argTypes = Size init
-> (forall (tp :: CrucibleType). Index init tp -> m (Atom s tp))
-> m (Assignment (Atom s) init)
forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
Ctx.generateM (CtxRepr init -> Size init
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size CtxRepr init
argTypes) Index init tp -> m (Atom s tp)
forall (tp :: CrucibleType). Index init tp -> m (Atom s tp)
f
where f :: Index init tp -> m (Atom s tp)
f :: forall (tp :: CrucibleType). Index init tp -> m (Atom s tp)
f Index init tp
i = do
Nonce s tp
n <- NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
Atom s tp -> m (Atom s tp)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Atom s tp -> m (Atom s tp)) -> Atom s tp -> m (Atom s tp)
forall a b. (a -> b) -> a -> b
$
Atom { atomPosition :: Position
atomPosition = Position
p
, atomId :: Nonce s tp
atomId = Nonce s tp
n
, atomSource :: AtomSource s tp
atomSource = AtomSource s tp
forall s (tp :: CrucibleType). AtomSource s tp
FnInput
, typeOfAtom :: TypeRepr tp
typeOfAtom = CtxRepr init
argTypes CtxRepr init -> Index init tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index init tp
i
}
instance TestEquality (Atom s) where
testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
Atom s a -> Atom s b -> Maybe (a :~: b)
testEquality Atom s a
x Atom s b
y = Nonce s a -> Nonce s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce s a -> Nonce s b -> Maybe (a :~: b)
testEquality (Atom s a -> Nonce s a
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s a
x) (Atom s b -> Nonce s b
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s b
y)
instance OrdF (Atom s) where
compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
Atom s x -> Atom s y -> OrderingF x y
compareF Atom s x
x Atom s y
y = Nonce s x -> Nonce s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce s x -> Nonce s y -> OrderingF x y
compareF (Atom s x -> Nonce s x
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s x
x) (Atom s y -> Nonce s y
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s y
y)
instance Show (Atom s tp) where
show :: Atom s tp -> String
show Atom s tp
a = Char
'$' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Atom s tp -> Nonce s tp
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s tp
a))
instance Pretty (Atom s tp) where
pretty :: forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'$' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Atom s tp -> Nonce s tp
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s tp
a))
substAtom :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp
-> m (Atom s' tp)
substAtom :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a =
Position
-> Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp
forall s (tp :: CrucibleType).
Position
-> Nonce s tp -> AtomSource s tp -> TypeRepr tp -> Atom s tp
Atom (Position
-> Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
-> m Position
-> m (Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a)
m (Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
-> m (Nonce s' tp)
-> m (AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Nonce s tp -> m (Nonce s' tp)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Atom s tp -> Nonce s tp
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s tp
a)
m (AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
-> m (AtomSource s' tp) -> m (TypeRepr tp -> Atom s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomSource s tp -> m (AtomSource s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomSource s tp -> m (AtomSource s' tp)
substAtomSource Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Atom s tp -> AtomSource s tp
forall s (tp :: CrucibleType). Atom s tp -> AtomSource s tp
atomSource Atom s tp
a)
m (TypeRepr tp -> Atom s' tp) -> m (TypeRepr tp) -> m (Atom s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a)
data Reg s (tp :: CrucibleType)
= Reg {
forall s (tp :: CrucibleType). Reg s tp -> Position
regPosition :: !Position
, forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId :: !(Nonce s tp)
, forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg :: !(TypeRepr tp)
}
instance Pretty (Reg s tp) where
pretty :: forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'r' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Reg s tp -> Nonce s tp
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s tp
r))
instance Show (Reg s tp) where
show :: Reg s tp -> String
show Reg s tp
r = Char
'r' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Reg s tp -> Nonce s tp
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s tp
r))
instance ShowF (Reg s)
instance TestEquality (Reg s) where
testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
Reg s a -> Reg s b -> Maybe (a :~: b)
testEquality Reg s a
x Reg s b
y = Nonce s a -> Nonce s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce s a -> Nonce s b -> Maybe (a :~: b)
testEquality (Reg s a -> Nonce s a
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s a
x) (Reg s b -> Nonce s b
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s b
y)
instance OrdF (Reg s) where
compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
Reg s x -> Reg s y -> OrderingF x y
compareF Reg s x
x Reg s y
y = Nonce s x -> Nonce s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce s x -> Nonce s y -> OrderingF x y
compareF (Reg s x -> Nonce s x
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s x
x) (Reg s y -> Nonce s y
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s y
y)
substReg :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp
-> m (Reg s' tp)
substReg :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r =
Position -> Nonce s' tp -> TypeRepr tp -> Reg s' tp
forall s (tp :: CrucibleType).
Position -> Nonce s tp -> TypeRepr tp -> Reg s tp
Reg (Position -> Nonce s' tp -> TypeRepr tp -> Reg s' tp)
-> m Position -> m (Nonce s' tp -> TypeRepr tp -> Reg s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Reg s tp -> Position
forall s (tp :: CrucibleType). Reg s tp -> Position
regPosition Reg s tp
r)
m (Nonce s' tp -> TypeRepr tp -> Reg s' tp)
-> m (Nonce s' tp) -> m (TypeRepr tp -> Reg s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Nonce s tp -> m (Nonce s' tp)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Reg s tp -> Nonce s tp
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s tp
r)
m (TypeRepr tp -> Reg s' tp) -> m (TypeRepr tp) -> m (Reg s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Reg s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s tp
r)
instance TestEquality (LambdaLabel s) where
testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s a
x LambdaLabel s b
y = Nonce s a -> Nonce s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce s a -> Nonce s b -> Maybe (a :~: b)
testEquality (LambdaLabel s a -> Nonce s a
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s a
x) (LambdaLabel s b -> Nonce s b
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s b
y)
instance OrdF (LambdaLabel s) where
compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
LambdaLabel s x -> LambdaLabel s y -> OrderingF x y
compareF LambdaLabel s x
x LambdaLabel s y
y = Nonce s x -> Nonce s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce s x -> Nonce s y -> OrderingF x y
compareF (LambdaLabel s x -> Nonce s x
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s x
x) (LambdaLabel s y -> Nonce s y
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s y
y)
data Value s (tp :: CrucibleType)
= RegValue !(Reg s tp)
| AtomValue !(Atom s tp)
instance TestEquality (Value s) where
testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
Value s a -> Value s b -> Maybe (a :~: b)
testEquality (RegValue Reg s a
x) (RegValue Reg s b
y) = Reg s a -> Reg s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Reg s a -> Reg s b -> Maybe (a :~: b)
testEquality Reg s a
x Reg s b
y
testEquality (AtomValue Atom s a
x) (AtomValue Atom s b
y) = Atom s a -> Atom s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Atom s a -> Atom s b -> Maybe (a :~: b)
testEquality Atom s a
x Atom s b
y
testEquality Value s a
_ Value s b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing
instance OrdF (Value s) where
compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
Value s x -> Value s y -> OrderingF x y
compareF (RegValue Reg s x
x) (RegValue Reg s y
y) = Reg s x -> Reg s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Reg s x -> Reg s y -> OrderingF x y
compareF Reg s x
x Reg s y
y
compareF RegValue{} Value s y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
compareF Value s x
_ RegValue{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
compareF (AtomValue Atom s x
x) (AtomValue Atom s y
y) = Atom s x -> Atom s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Atom s x -> Atom s y -> OrderingF x y
compareF Atom s x
x Atom s y
y
instance Pretty (Value s tp) where
pretty :: forall ann. Value s tp -> Doc ann
pretty (RegValue Reg s tp
r) = Reg s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r
pretty (AtomValue Atom s tp
a) = Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a
instance Show (Value s tp) where
show :: Value s tp -> String
show (RegValue Reg s tp
r) = Reg s tp -> String
forall a. Show a => a -> String
show Reg s tp
r
show (AtomValue Atom s tp
a) = Atom s tp -> String
forall a. Show a => a -> String
show Atom s tp
a
instance ShowF (Value s)
typeOfValue :: Value s tp -> TypeRepr tp
typeOfValue :: forall s (tp :: CrucibleType). Value s tp -> TypeRepr tp
typeOfValue (RegValue Reg s tp
r) = Reg s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s tp
r
typeOfValue (AtomValue Atom s tp
a) = Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a
substValue :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s tp
-> m (Value s' tp)
substValue :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s tp -> m (Value s' tp)
substValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Value s tp
v =
case Value s tp
v of
RegValue Reg s tp
r -> Reg s' tp -> Value s' tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue (Reg s' tp -> Value s' tp) -> m (Reg s' tp) -> m (Value s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r
AtomValue Atom s tp
a -> Atom s' tp -> Value s' tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue (Atom s' tp -> Value s' tp) -> m (Atom s' tp) -> m (Value s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
substValueAtom :: Applicative m
=> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Value s tp
-> m (Value s tp)
substValueAtom :: forall (m :: Type -> Type) s (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Value s tp -> m (Value s tp)
substValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Value s tp
v =
case Value s tp
v of
RegValue Reg s tp
r -> Value s tp -> m (Value s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value s tp -> m (Value s tp)) -> Value s tp -> m (Value s tp)
forall a b. (a -> b) -> a -> b
$ Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r
AtomValue Atom s tp
a -> Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue (Atom s tp -> Value s tp) -> m (Atom s tp) -> m (Value s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a
type ValueSet s = Set (Some (Value s))
substValueSet :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s
-> m (ValueSet s')
substValueSet :: forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f ValueSet s
vs =
[Some (Value s')] -> Set (Some (Value s'))
forall a. Ord a => [a] -> Set a
Set.fromList ([Some (Value s')] -> Set (Some (Value s')))
-> m [Some (Value s')] -> m (Set (Some (Value s')))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Some (Value s) -> m (Some (Value s')))
-> [Some (Value s)] -> m [Some (Value s')]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(Some Value s x
v) -> Value s' x -> Some (Value s')
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Value s' x -> Some (Value s'))
-> m (Value s' x) -> m (Some (Value s'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s x -> m (Value s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s tp -> m (Value s' tp)
substValue Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Value s x
v) (ValueSet s -> [Some (Value s)]
forall a. Set a -> [a]
Set.toList ValueSet s
vs)
data Expr ext s (tp :: CrucibleType)
= App !(App ext (Expr ext s) tp)
| AtomExpr !(Atom s tp)
instance PrettyExt ext => Pretty (Expr ext s tp) where
pretty :: forall ann. Expr ext s tp -> Doc ann
pretty (App App ext (Expr ext s) tp
a) = (forall (x :: CrucibleType). Expr ext s x -> Doc ann)
-> forall (x :: CrucibleType). App ext (Expr ext s) x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). App ext f x -> Doc ann
ppApp Expr ext s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Expr ext s x -> Doc ann
forall (x :: CrucibleType). Expr ext s x -> Doc ann
pretty App ext (Expr ext s) tp
a
pretty (AtomExpr Atom s tp
a) = Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a
instance PrettyExt ext => Show (Expr ext s tp) where
show :: Expr ext s tp -> String
show Expr ext s tp
e = Doc Any -> String
forall a. Show a => a -> String
show (Expr ext s tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Expr ext s tp -> Doc ann
pretty Expr ext s tp
e)
instance PrettyExt ext => ShowF (Expr ext s)
instance TypeApp (ExprExtension ext) => IsExpr (Expr ext s) where
type ExprExt (Expr ext s) = ext
app :: forall (tp :: CrucibleType).
App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp
app = App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App
asApp :: forall (tp :: CrucibleType).
Expr ext s tp -> Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp)
asApp (App App ext (Expr ext s) tp
x) = App ext (Expr ext s) tp -> Maybe (App ext (Expr ext s) tp)
forall a. a -> Maybe a
Just App ext (Expr ext s) tp
x
asApp Expr ext s tp
_ = Maybe (App ext (Expr ext s) tp)
Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp)
forall a. Maybe a
Nothing
exprType :: forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
exprType (App App ext (Expr ext s) tp
a) = App ext (Expr ext s) tp -> TypeRepr tp
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
App ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
(f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType App ext (Expr ext s) tp
a
exprType (AtomExpr Atom s tp
a) = Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a
instance IsString (Expr ext s (StringType Unicode)) where
fromString :: String -> Expr ext s (StringType Unicode)
fromString String
s = App ext (Expr ext s) (StringType Unicode)
-> Expr ext s (StringType Unicode)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (StringLiteral Unicode -> App ext (Expr ext s) (StringType Unicode)
forall (si :: StringInfo) ext (f :: CrucibleType -> Type).
StringLiteral si -> App ext f ('BaseToType (BaseStringType si))
StringLit (String -> StringLiteral Unicode
forall a. IsString a => String -> a
fromString String
s))
substExpr :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Expr ext s tp
-> m (Expr ext s' tp)
substExpr :: forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Expr ext s tp -> m (Expr ext s' tp)
substExpr forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Expr ext s tp
expr =
case Expr ext s tp
expr of
App App ext (Expr ext s) tp
ap -> App ext (Expr ext s') tp -> Expr ext s' tp
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App ext (Expr ext s') tp -> Expr ext s' tp)
-> m (App ext (Expr ext s') tp) -> m (Expr ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Expr ext s x -> m (Expr ext s' x))
-> forall (x :: CrucibleType).
App ext (Expr ext s) x -> m (App ext (Expr ext s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Expr ext s x -> m (Expr ext s' x)
forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Expr ext s tp -> m (Expr ext s' tp)
substExpr Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) App ext (Expr ext s) tp
ap
AtomExpr Atom s tp
a -> Atom s' tp -> Expr ext s' tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s' tp -> Expr ext s' tp)
-> m (Atom s' tp) -> m (Expr ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
data AtomValue ext s (tp :: CrucibleType) where
EvalApp :: !(App ext (Atom s) tp) -> AtomValue ext s tp
ReadReg :: !(Reg s tp) -> AtomValue ext s tp
EvalExt :: !(StmtExtension ext (Atom s) tp) -> AtomValue ext s tp
ReadGlobal :: !(GlobalVar tp) -> AtomValue ext s tp
ReadRef :: !(Atom s (ReferenceType tp)) -> AtomValue ext s tp
NewRef :: !(Atom s tp) -> AtomValue ext s (ReferenceType tp)
NewEmptyRef :: !(TypeRepr tp) -> AtomValue ext s (ReferenceType tp)
FreshConstant :: !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> AtomValue ext s (BaseToType bt)
FreshFloat :: !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> AtomValue ext s (FloatType fi)
FreshNat :: !(Maybe SolverSymbol) -> AtomValue ext s NatType
Call :: !(Atom s (FunctionHandleType args ret))
-> !(Assignment (Atom s) args)
-> !(TypeRepr ret)
-> AtomValue ext s ret
instance PrettyExt ext => Show (AtomValue ext s tp) where
show :: AtomValue ext s tp -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (AtomValue ext s tp -> Doc Any) -> AtomValue ext s tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomValue ext s tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomValue ext s tp -> Doc ann
pretty
instance PrettyExt ext => Pretty (AtomValue ext s tp) where
pretty :: forall ann. AtomValue ext s tp -> Doc ann
pretty AtomValue ext s tp
v =
case AtomValue ext s tp
v of
EvalApp App ext (Atom s) tp
ap -> (forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: CrucibleType). App ext (Atom s) x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). App ext f x -> Doc ann
ppApp Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty App ext (Atom s) tp
ap
EvalExt StmtExtension ext (Atom s) tp
st -> (forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: CrucibleType).
StmtExtension ext (Atom s) x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). StmtExtension ext f x -> Doc ann
ppApp Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty StmtExtension ext (Atom s) tp
st
ReadReg Reg s tp
r -> Reg s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r
ReadGlobal GlobalVar tp
g -> Doc ann
"global" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. GlobalVar tp -> Doc ann
pretty GlobalVar tp
g
ReadRef Atom s (ReferenceType tp)
r -> Doc ann
"!" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Atom s (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (ReferenceType tp) -> Doc ann
pretty Atom s (ReferenceType tp)
r
NewRef Atom s tp
a -> Doc ann
"newref" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a
NewEmptyRef TypeRepr tp
tp -> Doc ann
"emptyref" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr tp -> Doc ann
pretty TypeRepr tp
tp
FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
nm -> Doc ann
"fresh" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> BaseTypeRepr bt -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BaseTypeRepr bt -> Doc ann
pretty BaseTypeRepr bt
bt Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
-> (SolverSymbol -> Doc ann) -> Maybe SolverSymbol -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
forall a. Monoid a => a
mempty SolverSymbol -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Maybe SolverSymbol
nm
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
nm -> Doc ann
"fresh" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FloatInfoRepr fi -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FloatInfoRepr fi -> Doc ann
pretty FloatInfoRepr fi
fi Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
-> (SolverSymbol -> Doc ann) -> Maybe SolverSymbol -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
forall a. Monoid a => a
mempty SolverSymbol -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Maybe SolverSymbol
nm
FreshNat Maybe SolverSymbol
nm -> Doc ann
"fresh nat" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
-> (SolverSymbol -> Doc ann) -> Maybe SolverSymbol -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
forall a. Monoid a => a
mempty SolverSymbol -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Maybe SolverSymbol
nm
Call Atom s (FunctionHandleType args tp)
f Assignment (Atom s) args
args TypeRepr tp
_ -> Atom s (FunctionHandleType args tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (FunctionHandleType args tp) -> Doc ann
pretty Atom s (FunctionHandleType args tp)
f Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: Ctx CrucibleType).
Assignment (Atom s) x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty Assignment (Atom s) args
args))
typeOfAtomValue :: (TypeApp (StmtExtension ext) , TypeApp (ExprExtension ext))
=> AtomValue ext s tp -> TypeRepr tp
typeOfAtomValue :: forall ext s (tp :: CrucibleType).
(TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) =>
AtomValue ext s tp -> TypeRepr tp
typeOfAtomValue AtomValue ext s tp
v =
case AtomValue ext s tp
v of
EvalApp App ext (Atom s) tp
a -> App ext (Atom s) tp -> TypeRepr tp
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
App ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
(f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType App ext (Atom s) tp
a
EvalExt StmtExtension ext (Atom s) tp
stmt -> StmtExtension ext (Atom s) tp -> TypeRepr tp
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
StmtExtension ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
(f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType StmtExtension ext (Atom s) tp
stmt
ReadReg Reg s tp
r -> Reg s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s tp
r
ReadGlobal GlobalVar tp
r -> GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
r
ReadRef Atom s (ReferenceType tp)
r -> case Atom s (ReferenceType tp) -> TypeRepr (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s (ReferenceType tp)
r of
ReferenceRepr TypeRepr a
tpr -> TypeRepr tp
TypeRepr a
tpr
NewRef Atom s tp
a -> TypeRepr tp -> TypeRepr ('ReferenceType tp)
forall (a :: CrucibleType).
TypeRepr a -> TypeRepr ('ReferenceType a)
ReferenceRepr (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a)
NewEmptyRef TypeRepr tp
tp -> TypeRepr tp -> TypeRepr ('ReferenceType tp)
forall (a :: CrucibleType).
TypeRepr a -> TypeRepr ('ReferenceType a)
ReferenceRepr TypeRepr tp
tp
FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
_ -> BaseTypeRepr bt -> TypeRepr ('BaseToType bt)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr bt
bt
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
FreshNat Maybe SolverSymbol
_ -> TypeRepr tp
TypeRepr 'NatType
NatRepr
Call Atom s (FunctionHandleType args tp)
_ Assignment (Atom s) args
_ TypeRepr tp
r -> TypeRepr tp
r
foldAtomValueInputs :: TraverseExt ext
=> (forall x . Value s x -> b -> b)
-> AtomValue ext s tp -> b -> b
foldAtomValueInputs :: forall ext s b (tp :: CrucibleType).
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> AtomValue ext s tp -> b -> b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (ReadReg Reg s tp
r) b
b = Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r) b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (EvalExt StmtExtension ext (Atom s) tp
stmt) b
b = (forall (x :: CrucibleType). Atom s x -> b -> b)
-> forall (x :: CrucibleType).
b -> StmtExtension ext (Atom s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: CrucibleType). b -> StmtExtension ext f x -> b
foldrFC (Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Value s x -> b -> b)
-> (Atom s x -> Value s x) -> Atom s x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) b
b StmtExtension ext (Atom s) tp
stmt
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (ReadGlobal GlobalVar tp
_) b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (ReadRef Atom s (ReferenceType tp)
r) b
b = Value s (ReferenceType tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (ReferenceType tp) -> Value s (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (ReferenceType tp)
r) b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (NewEmptyRef TypeRepr tp
_) b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (NewRef Atom s tp
a) b
b = Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (EvalApp App ext (Atom s) tp
app0) b
b = (forall (x :: CrucibleType). Atom s x -> b -> b)
-> b -> App ext (Atom s) tp -> b
forall ext (f :: CrucibleType -> Type) r (tp :: CrucibleType).
TraversableFC (ExprExtension ext) =>
(forall (x :: CrucibleType). f x -> r -> r)
-> r -> App ext f tp -> r
foldApp (Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Value s x -> b -> b)
-> (Atom s x -> Value s x) -> Atom s x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) b
b App ext (Atom s) tp
app0
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (FreshConstant BaseTypeRepr bt
_ Maybe SolverSymbol
_) b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (FreshFloat FloatInfoRepr fi
_ Maybe SolverSymbol
_) b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (FreshNat Maybe SolverSymbol
_) b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (Call Atom s (FunctionHandleType args tp)
g Assignment (Atom s) args
a TypeRepr tp
_) b
b = Value s (FunctionHandleType args tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (FunctionHandleType args tp)
-> Value s (FunctionHandleType args tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (FunctionHandleType args tp)
g) ((forall (x :: CrucibleType). Atom s x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment (Atom s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
foldrFC' (Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Value s x -> b -> b)
-> (Atom s x -> Value s x) -> Atom s x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) b
b Assignment (Atom s) args
a)
substAtomValue :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomValue ext s tp
-> m (AtomValue ext s' tp)
substAtomValue :: forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomValue ext s tp -> m (AtomValue ext s' tp)
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (ReadReg Reg s tp
r) = Reg s' tp -> AtomValue ext s' tp
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg (Reg s' tp -> AtomValue ext s' tp)
-> m (Reg s' tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (EvalExt StmtExtension ext (Atom s) tp
stmt) = StmtExtension ext (Atom s') tp -> AtomValue ext s' tp
forall ext s (tp :: CrucibleType).
StmtExtension ext (Atom s) tp -> AtomValue ext s tp
EvalExt (StmtExtension ext (Atom s') tp -> AtomValue ext s' tp)
-> m (StmtExtension ext (Atom s') tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: CrucibleType).
StmtExtension ext (Atom s) x -> m (StmtExtension ext (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
StmtExtension ext f x -> m (StmtExtension ext g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) StmtExtension ext (Atom s) tp
stmt
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (ReadGlobal GlobalVar tp
g) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ GlobalVar tp -> AtomValue ext s' tp
forall (tp :: CrucibleType) ext s.
GlobalVar tp -> AtomValue ext s tp
ReadGlobal GlobalVar tp
g
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (ReadRef Atom s (ReferenceType tp)
r) = Atom s' (ReferenceType tp) -> AtomValue ext s' tp
forall s (tp :: CrucibleType) ext.
Atom s (ReferenceType tp) -> AtomValue ext s tp
ReadRef (Atom s' (ReferenceType tp) -> AtomValue ext s' tp)
-> m (Atom s' (ReferenceType tp)) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (ReferenceType tp) -> m (Atom s' (ReferenceType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (ReferenceType tp)
r
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (NewEmptyRef TypeRepr tp
tp) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ TypeRepr tp -> AtomValue ext s' ('ReferenceType tp)
forall (args :: CrucibleType) ext s.
TypeRepr args -> AtomValue ext s (ReferenceType args)
NewEmptyRef TypeRepr tp
tp
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (NewRef Atom s tp
a) = Atom s' tp -> AtomValue ext s' tp
Atom s' tp -> AtomValue ext s' ('ReferenceType tp)
forall s (args :: CrucibleType) ext.
Atom s args -> AtomValue ext s (ReferenceType args)
NewRef (Atom s' tp -> AtomValue ext s' tp)
-> m (Atom s' tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (EvalApp App ext (Atom s) tp
ap) = App ext (Atom s') tp -> AtomValue ext s' tp
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (App ext (Atom s') tp -> AtomValue ext s' tp)
-> m (App ext (Atom s') tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: CrucibleType).
App ext (Atom s) x -> m (App ext (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) App ext (Atom s) tp
ap
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr bt
-> Maybe SolverSymbol -> AtomValue ext s' ('BaseToType bt)
forall (args :: BaseType) ext s.
BaseTypeRepr args
-> Maybe SolverSymbol -> AtomValue ext s (BaseToType args)
FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s' ('FloatType fi)
forall (args :: FloatInfo) ext s.
FloatInfoRepr args
-> Maybe SolverSymbol -> AtomValue ext s (FloatType args)
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (FreshNat Maybe SolverSymbol
sym) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ Maybe SolverSymbol -> AtomValue ext s' 'NatType
forall ext s. Maybe SolverSymbol -> AtomValue ext s 'NatType
FreshNat Maybe SolverSymbol
sym
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Call Atom s (FunctionHandleType args tp)
g Assignment (Atom s) args
as TypeRepr tp
ret) = Atom s' (FunctionHandleType args tp)
-> Assignment (Atom s') args -> TypeRepr tp -> AtomValue ext s' tp
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType) ext.
Atom s (FunctionHandleType args ret)
-> Assignment (Atom s) args -> TypeRepr ret -> AtomValue ext s ret
Call (Atom s' (FunctionHandleType args tp)
-> Assignment (Atom s') args -> TypeRepr tp -> AtomValue ext s' tp)
-> m (Atom s' (FunctionHandleType args tp))
-> m (Assignment (Atom s') args
-> TypeRepr tp -> AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (FunctionHandleType args tp)
-> m (Atom s' (FunctionHandleType args tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (FunctionHandleType args tp)
g
m (Assignment (Atom s') args -> TypeRepr tp -> AtomValue ext s' tp)
-> m (Assignment (Atom s') args)
-> m (TypeRepr tp -> AtomValue ext s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: Ctx CrucibleType).
Assignment (Atom s) x -> m (Assignment (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (Atom s) args
as
m (TypeRepr tp -> AtomValue ext s' tp)
-> m (TypeRepr tp) -> m (AtomValue ext s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TypeRepr tp
ret
mapAtomValueAtom :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> AtomValue ext s tp
-> m (AtomValue ext s tp)
mapAtomValueAtom :: forall (m :: Type -> Type) ext s (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (ReadReg Reg s tp
r) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ Reg s tp -> AtomValue ext s tp
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg Reg s tp
r
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (EvalExt StmtExtension ext (Atom s) tp
stmt) = StmtExtension ext (Atom s) tp -> AtomValue ext s tp
forall ext s (tp :: CrucibleType).
StmtExtension ext (Atom s) tp -> AtomValue ext s tp
EvalExt (StmtExtension ext (Atom s) tp -> AtomValue ext s tp)
-> m (StmtExtension ext (Atom s) tp) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> forall (x :: CrucibleType).
StmtExtension ext (Atom s) x -> m (StmtExtension ext (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
StmtExtension ext f x -> m (StmtExtension ext g x)
traverseFC Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f StmtExtension ext (Atom s) tp
stmt
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (ReadGlobal GlobalVar tp
g) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ GlobalVar tp -> AtomValue ext s tp
forall (tp :: CrucibleType) ext s.
GlobalVar tp -> AtomValue ext s tp
ReadGlobal GlobalVar tp
g
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (ReadRef Atom s (ReferenceType tp)
r) = Atom s (ReferenceType tp) -> AtomValue ext s tp
forall s (tp :: CrucibleType) ext.
Atom s (ReferenceType tp) -> AtomValue ext s tp
ReadRef (Atom s (ReferenceType tp) -> AtomValue ext s tp)
-> m (Atom s (ReferenceType tp)) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (ReferenceType tp) -> m (Atom s (ReferenceType tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (ReferenceType tp)
r
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (NewEmptyRef TypeRepr tp
tp) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ TypeRepr tp -> AtomValue ext s ('ReferenceType tp)
forall (args :: CrucibleType) ext s.
TypeRepr args -> AtomValue ext s (ReferenceType args)
NewEmptyRef TypeRepr tp
tp
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (NewRef Atom s tp
a) = Atom s tp -> AtomValue ext s tp
Atom s tp -> AtomValue ext s ('ReferenceType tp)
forall s (args :: CrucibleType) ext.
Atom s args -> AtomValue ext s (ReferenceType args)
NewRef (Atom s tp -> AtomValue ext s tp)
-> m (Atom s tp) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (EvalApp App ext (Atom s) tp
ap) = App ext (Atom s) tp -> AtomValue ext s tp
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (App ext (Atom s) tp -> AtomValue ext s tp)
-> m (App ext (Atom s) tp) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> forall (x :: CrucibleType).
App ext (Atom s) x -> m (App ext (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f App ext (Atom s) tp
ap
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr bt
-> Maybe SolverSymbol -> AtomValue ext s ('BaseToType bt)
forall (args :: BaseType) ext s.
BaseTypeRepr args
-> Maybe SolverSymbol -> AtomValue ext s (BaseToType args)
FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s ('FloatType fi)
forall (args :: FloatInfo) ext s.
FloatInfoRepr args
-> Maybe SolverSymbol -> AtomValue ext s (FloatType args)
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (FreshNat Maybe SolverSymbol
sym) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ Maybe SolverSymbol -> AtomValue ext s 'NatType
forall ext s. Maybe SolverSymbol -> AtomValue ext s 'NatType
FreshNat Maybe SolverSymbol
sym
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (Call Atom s (FunctionHandleType args tp)
g Assignment (Atom s) args
as TypeRepr tp
ret) = Atom s (FunctionHandleType args tp)
-> Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType) ext.
Atom s (FunctionHandleType args ret)
-> Assignment (Atom s) args -> TypeRepr ret -> AtomValue ext s ret
Call (Atom s (FunctionHandleType args tp)
-> Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp)
-> m (Atom s (FunctionHandleType args tp))
-> m (Assignment (Atom s) args
-> TypeRepr tp -> AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (FunctionHandleType args tp)
-> m (Atom s (FunctionHandleType args tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (FunctionHandleType args tp)
g
m (Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp)
-> m (Assignment (Atom s) args)
-> m (TypeRepr tp -> AtomValue ext s tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> forall (x :: Ctx CrucibleType).
Assignment (Atom s) x -> m (Assignment (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
Assignment f x -> m (Assignment g x)
traverseFC Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Assignment (Atom s) args
as
m (TypeRepr tp -> AtomValue ext s tp)
-> m (TypeRepr tp) -> m (AtomValue ext s tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TypeRepr tp
ret
ppAtomBinding :: PrettyExt ext => Atom s tp -> AtomValue ext s tp -> Doc ann
ppAtomBinding :: forall ext s (tp :: CrucibleType) ann.
PrettyExt ext =>
Atom s tp -> AtomValue ext s tp -> Doc ann
ppAtomBinding Atom s tp
a AtomValue ext s tp
v = Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> AtomValue ext s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomValue ext s tp -> Doc ann
pretty AtomValue ext s tp
v
data Stmt ext s
= forall tp . SetReg !(Reg s tp) !(Atom s tp)
| forall tp . WriteGlobal !(GlobalVar tp) !(Atom s tp)
| forall tp . WriteRef !(Atom s (ReferenceType tp)) !(Atom s tp)
| forall tp . DropRef !(Atom s (ReferenceType tp))
| forall tp . DefineAtom !(Atom s tp) !(AtomValue ext s tp)
| Print !(Atom s (StringType Unicode))
| Assert !(Atom s BoolType) !(Atom s (StringType Unicode))
| Assume !(Atom s BoolType) !(Atom s (StringType Unicode))
| forall args . Breakpoint BreakpointName !(Assignment (Value s) args)
instance PrettyExt ext => Show (Stmt ext s) where
show :: Stmt ext s -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (Stmt ext s -> Doc Any) -> Stmt ext s -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stmt ext s -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Stmt ext s -> Doc ann
pretty
instance PrettyExt ext => Pretty (Stmt ext s) where
pretty :: forall ann. Stmt ext s -> Doc ann
pretty Stmt ext s
s =
case Stmt ext s
s of
SetReg Reg s tp
r Atom s tp
e -> Reg s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
e
WriteGlobal GlobalVar tp
g Atom s tp
r -> Doc ann
"global" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. GlobalVar tp -> Doc ann
pretty GlobalVar tp
g Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
r
WriteRef Atom s (ReferenceType tp)
r Atom s tp
v -> Doc ann
"ref" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (ReferenceType tp) -> Doc ann
pretty Atom s (ReferenceType tp)
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
v
DropRef Atom s (ReferenceType tp)
r -> Doc ann
"drop" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (ReferenceType tp) -> Doc ann
pretty Atom s (ReferenceType tp)
r
DefineAtom Atom s tp
a AtomValue ext s tp
v -> Atom s tp -> AtomValue ext s tp -> Doc ann
forall ext s (tp :: CrucibleType) ann.
PrettyExt ext =>
Atom s tp -> AtomValue ext s tp -> Doc ann
ppAtomBinding Atom s tp
a AtomValue ext s tp
v
Print Atom s (StringType Unicode)
v -> Doc ann
"print" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
v
Assert Atom s BoolType
c Atom s (StringType Unicode)
m -> Doc ann
"assert" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s BoolType -> Doc ann
pretty Atom s BoolType
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
m
Assume Atom s BoolType
c Atom s (StringType Unicode)
m -> Doc ann
"assume" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s BoolType -> Doc ann
pretty Atom s BoolType
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
m
Breakpoint BreakpointName
nm Assignment (Value s) args
args -> Doc ann
"breakpoint" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> BreakpointName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BreakpointName -> Doc ann
pretty BreakpointName
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((forall (x :: CrucibleType). Value s x -> Doc ann)
-> forall (x :: Ctx CrucibleType).
Assignment (Value s) x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC Value s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Value s x -> Doc ann
forall (x :: CrucibleType). Value s x -> Doc ann
pretty Assignment (Value s) args
args))
stmtAssignedValue :: Stmt ext s -> Maybe (Some (Value s))
stmtAssignedValue :: forall ext s. Stmt ext s -> Maybe (Some (Value s))
stmtAssignedValue Stmt ext s
s =
case Stmt ext s
s of
SetReg Reg s tp
r Atom s tp
_ -> Some (Value s) -> Maybe (Some (Value s))
forall a. a -> Maybe a
Just (Value s tp -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r))
DefineAtom Atom s tp
a AtomValue ext s tp
_ -> Some (Value s) -> Maybe (Some (Value s))
forall a. a -> Maybe a
Just (Value s tp -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a))
WriteGlobal{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
WriteRef{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
DropRef{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
Print{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
Assert{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
Assume{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
Breakpoint{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
foldStmtInputs :: TraverseExt ext => (forall x . Value s x -> b -> b) -> Stmt ext s -> b -> b
foldStmtInputs :: forall ext s b.
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> Stmt ext s -> b -> b
foldStmtInputs forall (x :: CrucibleType). Value s x -> b -> b
f Stmt ext s
s b
b =
case Stmt ext s
s of
SetReg Reg s tp
_ Atom s tp
e -> Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
e) b
b
WriteGlobal GlobalVar tp
_ Atom s tp
a -> Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) b
b
WriteRef Atom s (ReferenceType tp)
r Atom s tp
a -> Value s (ReferenceType tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (ReferenceType tp) -> Value s (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (ReferenceType tp)
r) (Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) b
b)
DropRef Atom s (ReferenceType tp)
r -> Value s (ReferenceType tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (ReferenceType tp) -> Value s (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (ReferenceType tp)
r) b
b
DefineAtom Atom s tp
_ AtomValue ext s tp
v -> (forall (x :: CrucibleType). Value s x -> b -> b)
-> AtomValue ext s tp -> b -> b
forall ext s b (tp :: CrucibleType).
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> AtomValue ext s tp -> b -> b
foldAtomValueInputs Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f AtomValue ext s tp
v b
b
Print Atom s (StringType Unicode)
e -> Value s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (StringType Unicode) -> Value s (StringType Unicode)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (StringType Unicode)
e) b
b
Assert Atom s BoolType
c Atom s (StringType Unicode)
m -> Value s BoolType -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s BoolType -> Value s BoolType
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s BoolType
c) (Value s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (StringType Unicode) -> Value s (StringType Unicode)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (StringType Unicode)
m) b
b)
Assume Atom s BoolType
c Atom s (StringType Unicode)
m -> Value s BoolType -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s BoolType -> Value s BoolType
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s BoolType
c) (Value s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (StringType Unicode) -> Value s (StringType Unicode)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (StringType Unicode)
m) b
b)
Breakpoint BreakpointName
_ Assignment (Value s) args
args -> (forall (x :: CrucibleType). Value s x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment (Value s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
foldrFC' Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f b
b Assignment (Value s) args
args
substStmt :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Stmt ext s
-> m (Stmt ext s')
substStmt :: forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Stmt ext s -> m (Stmt ext s')
substStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Stmt ext s
s =
case Stmt ext s
s of
SetReg Reg s tp
r Atom s tp
e -> Reg s' tp -> Atom s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg (Reg s' tp -> Atom s' tp -> Stmt ext s')
-> m (Reg s' tp) -> m (Atom s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r m (Atom s' tp -> Stmt ext s') -> m (Atom s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
e
WriteGlobal GlobalVar tp
g Atom s tp
a -> GlobalVar tp -> Atom s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
GlobalVar tp -> Atom s tp -> Stmt ext s
WriteGlobal (GlobalVar tp -> Atom s' tp -> Stmt ext s')
-> m (GlobalVar tp) -> m (Atom s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalVar tp -> m (GlobalVar tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GlobalVar tp
g m (Atom s' tp -> Stmt ext s') -> m (Atom s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
WriteRef Atom s (ReferenceType tp)
r Atom s tp
a -> Atom s' (ReferenceType tp) -> Atom s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
WriteRef (Atom s' (ReferenceType tp) -> Atom s' tp -> Stmt ext s')
-> m (Atom s' (ReferenceType tp)) -> m (Atom s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (ReferenceType tp) -> m (Atom s' (ReferenceType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (ReferenceType tp)
r m (Atom s' tp -> Stmt ext s') -> m (Atom s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
DropRef Atom s (ReferenceType tp)
r -> Atom s' (ReferenceType tp) -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Stmt ext s
DropRef (Atom s' (ReferenceType tp) -> Stmt ext s')
-> m (Atom s' (ReferenceType tp)) -> m (Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (ReferenceType tp) -> m (Atom s' (ReferenceType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (ReferenceType tp)
r
DefineAtom Atom s tp
a AtomValue ext s tp
v -> Atom s' tp -> AtomValue ext s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom (Atom s' tp -> AtomValue ext s' tp -> Stmt ext s')
-> m (Atom s' tp) -> m (AtomValue ext s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a m (AtomValue ext s' tp -> Stmt ext s')
-> m (AtomValue ext s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomValue ext s tp -> m (AtomValue ext s' tp)
forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomValue ext s tp -> m (AtomValue ext s' tp)
substAtomValue Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f AtomValue ext s tp
v
Print Atom s (StringType Unicode)
e -> Atom s' (StringType Unicode) -> Stmt ext s'
forall ext s. Atom s (StringType Unicode) -> Stmt ext s
Print (Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' (StringType Unicode)) -> m (Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
e
Assert Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s'
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assert (Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' BoolType)
-> m (Atom s' (StringType Unicode) -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s BoolType -> m (Atom s' BoolType)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s BoolType
c m (Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' (StringType Unicode)) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
m
Assume Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s'
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assume (Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' BoolType)
-> m (Atom s' (StringType Unicode) -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s BoolType -> m (Atom s' BoolType)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s BoolType
c m (Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' (StringType Unicode)) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
m
Breakpoint BreakpointName
nm Assignment (Value s) args
args -> BreakpointName -> Assignment (Value s') args -> Stmt ext s'
forall ext s (args :: Ctx CrucibleType).
BreakpointName -> Assignment (Value s) args -> Stmt ext s
Breakpoint BreakpointName
nm (Assignment (Value s') args -> Stmt ext s')
-> m (Assignment (Value s') args) -> m (Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Value s x -> m (Value s' x))
-> forall (x :: Ctx CrucibleType).
Assignment (Value s) x -> m (Assignment (Value s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s x -> m (Value s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s tp -> m (Value s' tp)
substValue Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (Value s) args
args
mapStmtAtom :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Stmt ext s
-> m (Stmt ext s)
mapStmtAtom :: forall (m :: Type -> Type) ext s.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Stmt ext s -> m (Stmt ext s)
mapStmtAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Stmt ext s
s =
case Stmt ext s
s of
SetReg Reg s tp
r Atom s tp
e -> Reg s tp -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg Reg s tp
r (Atom s tp -> Stmt ext s) -> m (Atom s tp) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
e
WriteGlobal GlobalVar tp
g Atom s tp
a -> GlobalVar tp -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
GlobalVar tp -> Atom s tp -> Stmt ext s
WriteGlobal (GlobalVar tp -> Atom s tp -> Stmt ext s)
-> m (GlobalVar tp) -> m (Atom s tp -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalVar tp -> m (GlobalVar tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GlobalVar tp
g m (Atom s tp -> Stmt ext s) -> m (Atom s tp) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a
WriteRef Atom s (ReferenceType tp)
r Atom s tp
a -> Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
WriteRef (Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s)
-> m (Atom s (ReferenceType tp)) -> m (Atom s tp -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (ReferenceType tp) -> m (Atom s (ReferenceType tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (ReferenceType tp)
r m (Atom s tp -> Stmt ext s) -> m (Atom s tp) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a
DropRef Atom s (ReferenceType tp)
r -> Atom s (ReferenceType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Stmt ext s
DropRef (Atom s (ReferenceType tp) -> Stmt ext s)
-> m (Atom s (ReferenceType tp)) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (ReferenceType tp) -> m (Atom s (ReferenceType tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (ReferenceType tp)
r
DefineAtom Atom s tp
a AtomValue ext s tp
v -> Atom s tp -> AtomValue ext s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom (Atom s tp -> AtomValue ext s tp -> Stmt ext s)
-> m (Atom s tp) -> m (AtomValue ext s tp -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a m (AtomValue ext s tp -> Stmt ext s)
-> m (AtomValue ext s tp) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
mapAtomValueAtom Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f AtomValue ext s tp
v
Print Atom s (StringType Unicode)
e -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s. Atom s (StringType Unicode) -> Stmt ext s
Print (Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s (StringType Unicode)) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (StringType Unicode) -> m (Atom s (StringType Unicode))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (StringType Unicode)
e
Assert Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assert (Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s BoolType)
-> m (Atom s (StringType Unicode) -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s BoolType -> m (Atom s BoolType)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s BoolType
c m (Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s (StringType Unicode)) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s (StringType Unicode) -> m (Atom s (StringType Unicode))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (StringType Unicode)
m
Assume Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assume (Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s BoolType)
-> m (Atom s (StringType Unicode) -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s BoolType -> m (Atom s BoolType)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s BoolType
c m (Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s (StringType Unicode)) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s (StringType Unicode) -> m (Atom s (StringType Unicode))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (StringType Unicode)
m
Breakpoint BreakpointName
nm Assignment (Value s) args
args -> BreakpointName -> Assignment (Value s) args -> Stmt ext s
forall ext s (args :: Ctx CrucibleType).
BreakpointName -> Assignment (Value s) args -> Stmt ext s
Breakpoint BreakpointName
nm (Assignment (Value s) args -> Stmt ext s)
-> m (Assignment (Value s) args) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Value s x -> m (Value s x))
-> forall (x :: Ctx CrucibleType).
Assignment (Value s) x -> m (Assignment (Value s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Value s x -> m (Value s x)
forall (m :: Type -> Type) s (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Value s tp -> m (Value s tp)
substValueAtom Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f) Assignment (Value s) args
args
substPosdStmt :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (Stmt ext s)
-> m (Posd (Stmt ext s'))
substPosdStmt :: forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
substPosdStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Posd (Stmt ext s)
s =
Position -> Stmt ext s' -> Posd (Stmt ext s')
forall v. Position -> v -> Posd v
Posd (Position -> Stmt ext s' -> Posd (Stmt ext s'))
-> m Position -> m (Stmt ext s' -> Posd (Stmt ext s'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Posd (Stmt ext s) -> Position
forall v. Posd v -> Position
pos Posd (Stmt ext s)
s) m (Stmt ext s' -> Posd (Stmt ext s'))
-> m (Stmt ext s') -> m (Posd (Stmt ext s'))
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Stmt ext s -> m (Stmt ext s')
forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Stmt ext s -> m (Stmt ext s')
substStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
s)
data TermStmt s (ret :: CrucibleType) where
Jump :: !(Label s)
-> TermStmt s ret
Br :: !(Atom s BoolType)
-> !(Label s)
-> !(Label s)
-> TermStmt s ret
MaybeBranch :: !(TypeRepr tp)
-> !(Atom s (MaybeType tp))
-> !(LambdaLabel s tp)
-> !(Label s)
-> TermStmt s ret
VariantElim :: !(CtxRepr varctx)
-> !(Atom s (VariantType varctx))
-> !(Ctx.Assignment (LambdaLabel s) varctx)
-> TermStmt s ret
Return :: !(Atom s ret) -> TermStmt s ret
TailCall :: !(Atom s (FunctionHandleType args ret))
-> !(CtxRepr args)
-> !(Ctx.Assignment (Atom s) args)
-> TermStmt s ret
ErrorStmt :: !(Atom s (StringType Unicode)) -> TermStmt s ret
Output :: !(LambdaLabel s tp)
-> !(Atom s tp)
-> TermStmt s ret
instance Show (TermStmt s ret) where
show :: TermStmt s ret -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (TermStmt s ret -> Doc Any) -> TermStmt s ret -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermStmt s ret -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. TermStmt s ret -> Doc ann
pretty
instance Pretty (TermStmt s ret) where
pretty :: forall ann. TermStmt s ret -> Doc ann
pretty TermStmt s ret
t0 =
case TermStmt s ret
t0 of
Jump Label s
l -> Doc ann
"jump" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
l
Br Atom s BoolType
c Label s
x Label s
y -> Doc ann
"branch" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s BoolType -> Doc ann
pretty Atom s BoolType
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
y
MaybeBranch TypeRepr tp
_ Atom s (MaybeType tp)
c LambdaLabel s tp
j Label s
n -> Doc ann
"switchMaybe" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (MaybeType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (MaybeType tp) -> Doc ann
pretty Atom s (MaybeType tp)
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LambdaLabel s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. LambdaLabel s tp -> Doc ann
pretty LambdaLabel s tp
j Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
n
VariantElim CtxRepr varctx
_ Atom s (VariantType varctx)
e Assignment (LambdaLabel s) varctx
l ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
[ Doc ann
"switch" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (VariantType varctx) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (VariantType varctx) -> Doc ann
pretty Atom s (VariantType varctx)
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"{"
, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((forall (tp :: CrucibleType).
String -> LambdaLabel s tp -> Doc ann)
-> Assignment (LambdaLabel s) varctx -> [Doc ann]
forall (tgt :: CrucibleType -> Type) (ctx :: Ctx CrucibleType) ann.
(forall (tp :: CrucibleType). String -> tgt tp -> Doc ann)
-> Assignment tgt ctx -> [Doc ann]
ppSwitch String -> LambdaLabel s tp -> Doc ann
forall {a} {a} {ann}. (Pretty a, Pretty a) => a -> a -> Doc ann
forall (tp :: CrucibleType). String -> LambdaLabel s tp -> Doc ann
pp Assignment (LambdaLabel s) varctx
l))
, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
"}"
]
where pp :: a -> a -> Doc ann
pp a
nm a
v = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
nm Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
v
Return Atom s ret
e -> Doc ann
"return" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s ret -> Doc ann
pretty Atom s ret
e
TailCall Atom s (FunctionHandleType args ret)
f CtxRepr args
_ Assignment (Atom s) args
a -> Doc ann
"tail_call" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (FunctionHandleType args ret) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (FunctionHandleType args ret) -> Doc ann
pretty Atom s (FunctionHandleType args ret)
f Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
args
where args :: Doc ann
args = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: Ctx CrucibleType).
Assignment (Atom s) x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty Assignment (Atom s) args
a)
ErrorStmt Atom s (StringType Unicode)
e -> Doc ann
"error" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
e
Output LambdaLabel s tp
l Atom s tp
e -> Doc ann
"output" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LambdaLabel s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. LambdaLabel s tp -> Doc ann
pretty LambdaLabel s tp
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
e
ppSwitch :: forall tgt ctx ann. (forall (tp :: CrucibleType). String -> tgt tp -> Doc ann) -> Ctx.Assignment tgt ctx -> [Doc ann]
ppSwitch :: forall (tgt :: CrucibleType -> Type) (ctx :: Ctx CrucibleType) ann.
(forall (tp :: CrucibleType). String -> tgt tp -> Doc ann)
-> Assignment tgt ctx -> [Doc ann]
ppSwitch forall (tp :: CrucibleType). String -> tgt tp -> Doc ann
pp Assignment tgt ctx
asgn = Size ctx
-> (forall (tp :: CrucibleType).
[Doc ann] -> Index ctx tp -> [Doc ann])
-> [Doc ann]
-> [Doc ann]
forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndex (Assignment tgt ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment tgt ctx
asgn) [Doc ann] -> Index ctx tp -> [Doc ann]
forall (tp :: CrucibleType). [Doc ann] -> Index ctx tp -> [Doc ann]
f [Doc ann]
forall a. Monoid a => a
mempty
where f :: [Doc ann] -> Ctx.Index ctx (tp :: CrucibleType) -> [Doc ann]
f :: forall (tp :: CrucibleType). [Doc ann] -> Index ctx tp -> [Doc ann]
f [Doc ann]
rs Index ctx tp
idx = [Doc ann]
rs [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
Prelude.++ [ String -> tgt tp -> Doc ann
forall (tp :: CrucibleType). String -> tgt tp -> Doc ann
pp (Int -> String
forall a. Show a => a -> String
show (Index ctx tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index ctx tp
idx)) (Assignment tgt ctx
asgn Assignment tgt ctx -> Index ctx tp -> tgt tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
idx)]
foldTermStmtAtoms :: (forall x . Atom s x -> b -> b)
-> TermStmt s ret
-> b
-> b
foldTermStmtAtoms :: forall s b (ret :: CrucibleType).
(forall (x :: CrucibleType). Atom s x -> b -> b)
-> TermStmt s ret -> b -> b
foldTermStmtAtoms forall (x :: CrucibleType). Atom s x -> b -> b
f TermStmt s ret
stmt0 b
b =
case TermStmt s ret
stmt0 of
Jump Label s
_ -> b
b
Output LambdaLabel s tp
_ Atom s tp
e -> Atom s tp -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s tp
e b
b
Br Atom s BoolType
e Label s
_ Label s
_ -> Atom s BoolType -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s BoolType
e b
b
MaybeBranch TypeRepr tp
_ Atom s (MaybeType tp)
e LambdaLabel s tp
_ Label s
_ -> Atom s (MaybeType tp) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (MaybeType tp)
e b
b
VariantElim CtxRepr varctx
_ Atom s (VariantType varctx)
e Assignment (LambdaLabel s) varctx
_ -> Atom s (VariantType varctx) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (VariantType varctx)
e b
b
Return Atom s ret
e -> Atom s ret -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s ret
e b
b
TailCall Atom s (FunctionHandleType args ret)
fn CtxRepr args
_ Assignment (Atom s) args
a -> Atom s (FunctionHandleType args ret) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (FunctionHandleType args ret)
fn ((forall (x :: CrucibleType). Atom s x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment (Atom s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
foldrFC' Atom s x -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f b
b Assignment (Atom s) args
a)
ErrorStmt Atom s (StringType Unicode)
e -> Atom s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (StringType Unicode)
e b
b
substTermStmt :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> TermStmt s ret
-> m (TermStmt s' ret)
substTermStmt :: forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> TermStmt s ret -> m (TermStmt s' ret)
substTermStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f TermStmt s ret
stmt =
case TermStmt s ret
stmt of
Jump Label s
l -> Label s' -> TermStmt s' ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump (Label s' -> TermStmt s' ret)
-> m (Label s') -> m (TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l
Output LambdaLabel s tp
ll Atom s tp
a -> LambdaLabel s' tp -> Atom s' tp -> TermStmt s' ret
forall s (args :: CrucibleType) (ret :: CrucibleType).
LambdaLabel s args -> Atom s args -> TermStmt s ret
Output (LambdaLabel s' tp -> Atom s' tp -> TermStmt s' ret)
-> m (LambdaLabel s' tp) -> m (Atom s' tp -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll m (Atom s' tp -> TermStmt s' ret)
-> m (Atom s' tp) -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
Br Atom s BoolType
e Label s
c Label s
a -> Atom s' BoolType -> Label s' -> Label s' -> TermStmt s' ret
forall s (ret :: CrucibleType).
Atom s BoolType -> Label s -> Label s -> TermStmt s ret
Br (Atom s' BoolType -> Label s' -> Label s' -> TermStmt s' ret)
-> m (Atom s' BoolType)
-> m (Label s' -> Label s' -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s BoolType -> m (Atom s' BoolType)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s BoolType
e m (Label s' -> Label s' -> TermStmt s' ret)
-> m (Label s') -> m (Label s' -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
c m (Label s' -> TermStmt s' ret)
-> m (Label s') -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
a
MaybeBranch TypeRepr tp
tp Atom s (MaybeType tp)
a LambdaLabel s tp
ll Label s
l -> TypeRepr tp
-> Atom s' (MaybeType tp)
-> LambdaLabel s' tp
-> Label s'
-> TermStmt s' ret
forall (args :: CrucibleType) s (ret :: CrucibleType).
TypeRepr args
-> Atom s (MaybeType args)
-> LambdaLabel s args
-> Label s
-> TermStmt s ret
MaybeBranch (TypeRepr tp
-> Atom s' (MaybeType tp)
-> LambdaLabel s' tp
-> Label s'
-> TermStmt s' ret)
-> m (TypeRepr tp)
-> m (Atom s' (MaybeType tp)
-> LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TypeRepr tp
tp
m (Atom s' (MaybeType tp)
-> LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
-> m (Atom s' (MaybeType tp))
-> m (LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (MaybeType tp) -> m (Atom s' (MaybeType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (MaybeType tp)
a
m (LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
-> m (LambdaLabel s' tp) -> m (Label s' -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll
m (Label s' -> TermStmt s' ret)
-> m (Label s') -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l
VariantElim CtxRepr varctx
ctx Atom s (VariantType varctx)
a Assignment (LambdaLabel s) varctx
lls -> CtxRepr varctx
-> Atom s' (VariantType varctx)
-> Assignment (LambdaLabel s') varctx
-> TermStmt s' ret
forall (args :: Ctx CrucibleType) s (ret :: CrucibleType).
CtxRepr args
-> Atom s (VariantType args)
-> Assignment (LambdaLabel s) args
-> TermStmt s ret
VariantElim (CtxRepr varctx
-> Atom s' (VariantType varctx)
-> Assignment (LambdaLabel s') varctx
-> TermStmt s' ret)
-> m (CtxRepr varctx)
-> m (Atom s' (VariantType varctx)
-> Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CtxRepr varctx -> m (CtxRepr varctx)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CtxRepr varctx
ctx
m (Atom s' (VariantType varctx)
-> Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
-> m (Atom s' (VariantType varctx))
-> m (Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (VariantType varctx) -> m (Atom s' (VariantType varctx))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (VariantType varctx)
a
m (Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
-> m (Assignment (LambdaLabel s') varctx) -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType).
LambdaLabel s x -> m (LambdaLabel s' x))
-> forall (x :: Ctx CrucibleType).
Assignment (LambdaLabel s) x -> m (Assignment (LambdaLabel s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s x -> m (LambdaLabel s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (LambdaLabel s) varctx
lls
Return Atom s ret
e -> Atom s' ret -> TermStmt s' ret
forall s (ret :: CrucibleType). Atom s ret -> TermStmt s ret
Return (Atom s' ret -> TermStmt s' ret)
-> m (Atom s' ret) -> m (TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s ret -> m (Atom s' ret)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s ret
e
TailCall Atom s (FunctionHandleType args ret)
fn CtxRepr args
ctx Assignment (Atom s) args
args -> Atom s' (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType).
Atom s (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s) args -> TermStmt s ret
TailCall (Atom s' (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret)
-> m (Atom s' (FunctionHandleType args ret))
-> m (CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (FunctionHandleType args ret)
-> m (Atom s' (FunctionHandleType args ret))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (FunctionHandleType args ret)
fn
m (CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret)
-> m (CtxRepr args)
-> m (Assignment (Atom s') args -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> CtxRepr args -> m (CtxRepr args)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CtxRepr args
ctx
m (Assignment (Atom s') args -> TermStmt s' ret)
-> m (Assignment (Atom s') args) -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: Ctx CrucibleType).
Assignment (Atom s) x -> m (Assignment (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (Atom s) args
args
ErrorStmt Atom s (StringType Unicode)
e -> Atom s' (StringType Unicode) -> TermStmt s' ret
forall s (ret :: CrucibleType).
Atom s (StringType Unicode) -> TermStmt s ret
ErrorStmt (Atom s' (StringType Unicode) -> TermStmt s' ret)
-> m (Atom s' (StringType Unicode)) -> m (TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
e
substPosdTermStmt :: Applicative m
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (TermStmt s ret)
-> m (Posd (TermStmt s' ret))
substPosdTermStmt :: forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
substPosdTermStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Posd (TermStmt s ret)
posd
= Position -> TermStmt s' ret -> Posd (TermStmt s' ret)
forall v. Position -> v -> Posd v
Posd (Position -> TermStmt s' ret -> Posd (TermStmt s' ret))
-> m Position -> m (TermStmt s' ret -> Posd (TermStmt s' ret))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Posd (TermStmt s ret) -> Position
forall v. Posd v -> Position
pos Posd (TermStmt s ret)
posd) m (TermStmt s' ret -> Posd (TermStmt s' ret))
-> m (TermStmt s' ret) -> m (Posd (TermStmt s' ret))
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> TermStmt s ret -> m (TermStmt s' ret)
forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> TermStmt s ret -> m (TermStmt s' ret)
substTermStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val Posd (TermStmt s ret)
posd)
termStmtInputs :: TermStmt s ret
-> ValueSet s
termStmtInputs :: forall s (ret :: CrucibleType). TermStmt s ret -> ValueSet s
termStmtInputs TermStmt s ret
stmt = (forall (x :: CrucibleType). Atom s x -> ValueSet s -> ValueSet s)
-> TermStmt s ret -> ValueSet s -> ValueSet s
forall s b (ret :: CrucibleType).
(forall (x :: CrucibleType). Atom s x -> b -> b)
-> TermStmt s ret -> b -> b
foldTermStmtAtoms (Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert (Some (Value s) -> ValueSet s -> ValueSet s)
-> (Atom s x -> Some (Value s))
-> Atom s x
-> ValueSet s
-> ValueSet s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value s x -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Value s x -> Some (Value s))
-> (Atom s x -> Value s x) -> Atom s x -> Some (Value s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) TermStmt s ret
stmt ValueSet s
forall a. Set a
Set.empty
termNextLabels :: TermStmt s ret
-> Maybe [BlockID s]
termNextLabels :: forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s]
termNextLabels TermStmt s ret
s0 =
case TermStmt s ret
s0 of
Jump Label s
l -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
l]
Output LambdaLabel s tp
l Atom s tp
_ -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [LambdaLabel s tp -> BlockID s
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
LambdaID LambdaLabel s tp
l]
Br Atom s BoolType
_ Label s
x Label s
y -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
x, Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
y]
MaybeBranch TypeRepr tp
_ Atom s (MaybeType tp)
_ LambdaLabel s tp
x Label s
y -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [LambdaLabel s tp -> BlockID s
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
LambdaID LambdaLabel s tp
x, Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
y]
VariantElim CtxRepr varctx
_ Atom s (VariantType varctx)
_ Assignment (LambdaLabel s) varctx
s -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just ([BlockID s] -> Maybe [BlockID s])
-> [BlockID s] -> Maybe [BlockID s]
forall a b. (a -> b) -> a -> b
$ (forall (x :: CrucibleType). LambdaLabel s x -> BlockID s)
-> forall (x :: Ctx CrucibleType).
Assignment (LambdaLabel s) x -> [BlockID s]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC LambdaLabel s x -> BlockID s
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
forall (x :: CrucibleType). LambdaLabel s x -> BlockID s
LambdaID Assignment (LambdaLabel s) varctx
s
Return Atom s ret
_ -> Maybe [BlockID s]
forall a. Maybe a
Nothing
TailCall{} -> Maybe [BlockID s]
forall a. Maybe a
Nothing
ErrorStmt Atom s (StringType Unicode)
_ -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just []
data Block ext s (ret :: CrucibleType)
= Block { forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID :: !(BlockID s)
, forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts :: !(Seq (Posd (Stmt ext s)))
, forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm :: !(Posd (TermStmt s ret))
, :: !(ValueSet s)
, forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockKnownInputs :: !(ValueSet s)
, forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockAssignedValues :: !(ValueSet s)
}
instance Eq (Block ext s ret) where
Block ext s ret
x == :: Block ext s ret -> Block ext s ret -> Bool
== Block ext s ret
y = Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
x BlockID s -> BlockID s -> Bool
forall a. Eq a => a -> a -> Bool
== Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
y
instance Ord (Block ext s ret) where
compare :: Block ext s ret -> Block ext s ret -> Ordering
compare Block ext s ret
x Block ext s ret
y = BlockID s -> BlockID s -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
x) (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
y)
instance PrettyExt ext => Show (Block ext s ret) where
show :: Block ext s ret -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (Block ext s ret -> Doc Any) -> Block ext s ret -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block ext s ret -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Block ext s ret -> Doc ann
pretty
instance Pretty (ValueSet s) where
pretty :: forall ann. ValueSet s -> Doc ann
pretty ValueSet s
vs = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((Some (Value s) -> Doc ann) -> [Some (Value s)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\(Some Value s x
v) -> Value s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Value s x -> Doc ann
pretty Value s x
v) (ValueSet s -> [Some (Value s)]
forall a. Set a -> [a]
Set.toList ValueSet s
vs))
instance PrettyExt ext => Pretty (Block ext s ret) where
pretty :: forall ann. Block ext s ret -> Doc ann
pretty Block ext s ret
b = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [BlockID s -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b), Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
stmts]
where stmts :: Doc ann
stmts = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Stmt ext s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Stmt ext s -> Doc ann
pretty (Stmt ext s -> Doc ann)
-> (Posd (Stmt ext s) -> Stmt ext s)
-> Posd (Stmt ext s)
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val (Posd (Stmt ext s) -> Doc ann) -> [Posd (Stmt ext s)] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (Posd (Stmt ext s)) -> [Posd (Stmt ext s)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Fold.toList (Block ext s ret -> Seq (Posd (Stmt ext s))
forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts Block ext s ret
b))
, TermStmt s ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TermStmt s ret -> Doc ann
pretty (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
b)) ]
mkBlock :: forall ext s ret
. TraverseExt ext
=> BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
mkBlock :: forall ext s (ret :: CrucibleType).
TraverseExt ext =>
BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
mkBlock BlockID s
block_id ValueSet s
inputs Seq (Posd (Stmt ext s))
stmts Posd (TermStmt s ret)
term =
Block { blockID :: BlockID s
blockID = BlockID s
block_id
, blockStmts :: Seq (Posd (Stmt ext s))
blockStmts = Seq (Posd (Stmt ext s))
stmts
, blockTerm :: Posd (TermStmt s ret)
blockTerm = Posd (TermStmt s ret)
term
, blockExtraInputs :: ValueSet s
blockExtraInputs = ValueSet s
inputs
, blockAssignedValues :: ValueSet s
blockAssignedValues = ValueSet s
assigned_values
, blockKnownInputs :: ValueSet s
blockKnownInputs = ValueSet s
all_input_values
}
where inputs_with_lambda :: ValueSet s
inputs_with_lambda =
case BlockID s
block_id of
LabelID{} -> ValueSet s
inputs
LambdaID LambdaLabel s tp
l -> Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert (Value s tp -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
l))) ValueSet s
inputs
initState :: (ValueSet s, ValueSet s)
initState = (ValueSet s
inputs_with_lambda, ValueSet s
inputs)
addUnassigned :: ValueSet s -> Value s x -> ValueSet s -> ValueSet s
addUnassigned :: forall (x :: CrucibleType).
ValueSet s -> Value s x -> ValueSet s -> ValueSet s
addUnassigned ValueSet s
ar Value s x
r ValueSet s
s
| Some (Value s) -> ValueSet s -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Value s x -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Value s x
r) ValueSet s
ar = ValueSet s
s
| Bool
otherwise = Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert (Value s x -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Value s x
r) ValueSet s
s
all_input_values :: ValueSet s
all_input_values
= (forall (x :: CrucibleType). Atom s x -> ValueSet s -> ValueSet s)
-> TermStmt s ret -> ValueSet s -> ValueSet s
forall s b (ret :: CrucibleType).
(forall (x :: CrucibleType). Atom s x -> b -> b)
-> TermStmt s ret -> b -> b
foldTermStmtAtoms (ValueSet s -> Value s x -> ValueSet s -> ValueSet s
forall (x :: CrucibleType).
ValueSet s -> Value s x -> ValueSet s -> ValueSet s
addUnassigned ValueSet s
assigned_values (Value s x -> ValueSet s -> ValueSet s)
-> (Atom s x -> Value s x) -> Atom s x -> ValueSet s -> ValueSet s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue)
(Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val Posd (TermStmt s ret)
term)
ValueSet s
missing_values
f :: (ValueSet s, ValueSet s) -> Posd (Stmt ext s) -> (ValueSet s, ValueSet s)
f :: (ValueSet s, ValueSet s)
-> Posd (Stmt ext s) -> (ValueSet s, ValueSet s)
f (ValueSet s
ar, ValueSet s
mr) Posd (Stmt ext s)
s = (ValueSet s
ar', ValueSet s
mr')
where ar' :: ValueSet s
ar' = case Stmt ext s -> Maybe (Some (Value s))
forall ext s. Stmt ext s -> Maybe (Some (Value s))
stmtAssignedValue (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
s) of
Maybe (Some (Value s))
Nothing -> ValueSet s
ar
Just Some (Value s)
r -> Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert Some (Value s)
r ValueSet s
ar
mr' :: ValueSet s
mr' = (forall (x :: CrucibleType). Value s x -> ValueSet s -> ValueSet s)
-> Stmt ext s -> ValueSet s -> ValueSet s
forall ext s b.
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> Stmt ext s -> b -> b
foldStmtInputs (ValueSet s -> Value s x -> ValueSet s -> ValueSet s
forall (x :: CrucibleType).
ValueSet s -> Value s x -> ValueSet s -> ValueSet s
addUnassigned ValueSet s
ar) (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
s) ValueSet s
mr
(ValueSet s
assigned_values, ValueSet s
missing_values) = ((ValueSet s, ValueSet s)
-> Posd (Stmt ext s) -> (ValueSet s, ValueSet s))
-> (ValueSet s, ValueSet s)
-> Seq (Posd (Stmt ext s))
-> (ValueSet s, ValueSet s)
forall b a. (b -> a -> b) -> b -> Seq a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' (ValueSet s, ValueSet s)
-> Posd (Stmt ext s) -> (ValueSet s, ValueSet s)
f (ValueSet s, ValueSet s)
initState Seq (Posd (Stmt ext s))
stmts
substBlock :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Block ext s ret
-> m (Block ext s' ret)
substBlock :: forall (m :: Type -> Type) ext s s' (ret :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Block ext s ret -> m (Block ext s' ret)
substBlock forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Block ext s ret
b =
BlockID s'
-> Seq (Posd (Stmt ext s'))
-> Posd (TermStmt s' ret)
-> ValueSet s'
-> ValueSet s'
-> ValueSet s'
-> Block ext s' ret
forall ext s (ret :: CrucibleType).
BlockID s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> ValueSet s
-> ValueSet s
-> ValueSet s
-> Block ext s ret
Block (BlockID s'
-> Seq (Posd (Stmt ext s'))
-> Posd (TermStmt s' ret)
-> ValueSet s'
-> ValueSet s'
-> ValueSet s'
-> Block ext s' ret)
-> m (BlockID s')
-> m (Seq (Posd (Stmt ext s'))
-> Posd (TermStmt s' ret)
-> ValueSet s'
-> ValueSet s'
-> ValueSet s'
-> Block ext s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> BlockID s -> m (BlockID s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> BlockID s -> m (BlockID s')
substBlockID Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b)
m (Seq (Posd (Stmt ext s'))
-> Posd (TermStmt s' ret)
-> ValueSet s'
-> ValueSet s'
-> ValueSet s'
-> Block ext s' ret)
-> m (Seq (Posd (Stmt ext s')))
-> m (Posd (TermStmt s' ret)
-> ValueSet s' -> ValueSet s' -> ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Posd (Stmt ext s) -> m (Posd (Stmt ext s')))
-> Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s')))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Seq a -> f (Seq b)
traverse ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
substPosdStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) (Block ext s ret -> Seq (Posd (Stmt ext s))
forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts Block ext s ret
b)
m (Posd (TermStmt s' ret)
-> ValueSet s' -> ValueSet s' -> ValueSet s' -> Block ext s' ret)
-> m (Posd (TermStmt s' ret))
-> m (ValueSet s'
-> ValueSet s' -> ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
substPosdTermStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
b)
m (ValueSet s' -> ValueSet s' -> ValueSet s' -> Block ext s' ret)
-> m (ValueSet s')
-> m (ValueSet s' -> ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs Block ext s ret
b)
m (ValueSet s' -> ValueSet s' -> Block ext s' ret)
-> m (ValueSet s') -> m (ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockKnownInputs Block ext s ret
b)
m (ValueSet s' -> Block ext s' ret)
-> m (ValueSet s') -> m (Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockAssignedValues Block ext s ret
b)
data CFG ext s (init :: Ctx CrucibleType) (ret :: CrucibleType)
= CFG { forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle :: !(FnHandle init ret)
, forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel :: !(Label s)
, forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks :: ![Block ext s ret]
}
cfgEntryBlock :: CFG ext s init ret -> Block ext s ret
cfgEntryBlock :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Block ext s ret
cfgEntryBlock CFG ext s init ret
g =
Block ext s ret -> Maybe (Block ext s ret) -> Block ext s ret
forall a. a -> Maybe a -> a
fromMaybe
(String -> Block ext s ret
forall a. HasCallStack => String -> a
error String
"Missing entry block")
((Block ext s ret -> Bool)
-> [Block ext s ret] -> Maybe (Block ext s ret)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
Fold.find (\Block ext s ret
b -> Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b BlockID s -> BlockID s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID (CFG ext s init ret -> Label s
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel CFG ext s init ret
g)) (CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
g))
cfgInputTypes :: CFG ext s init ret -> CtxRepr init
cfgInputTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> CtxRepr init
cfgInputTypes = CFG ext s init ret -> CtxRepr init
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> CtxRepr init
cfgArgTypes
{-# DEPRECATED cfgInputTypes "Use cfgArgTypes instead" #-}
cfgArgTypes :: CFG ext s init ret -> CtxRepr init
cfgArgTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> CtxRepr init
cfgArgTypes CFG ext s init ret
g = FnHandle init ret -> CtxRepr init
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
g)
cfgReturnType :: CFG ext s init ret -> TypeRepr ret
cfgReturnType :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> TypeRepr ret
cfgReturnType CFG ext s init ret
g = FnHandle init ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
g)
substCFG :: ( Applicative m, TraverseExt ext )
=> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> CFG ext s init ret
-> m (CFG ext s' init ret)
substCFG :: forall (m :: Type -> Type) ext s s' (init :: Ctx CrucibleType)
(ret :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> CFG ext s init ret -> m (CFG ext s' init ret)
substCFG forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f CFG ext s init ret
cfg =
FnHandle init ret
-> Label s' -> [Block ext s' ret] -> CFG ext s' init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle init ret
-> Label s -> [Block ext s ret] -> CFG ext s init ret
CFG (FnHandle init ret
-> Label s' -> [Block ext s' ret] -> CFG ext s' init ret)
-> m (FnHandle init ret)
-> m (Label s' -> [Block ext s' ret] -> CFG ext s' init ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> FnHandle init ret -> m (FnHandle init ret)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
cfg)
m (Label s' -> [Block ext s' ret] -> CFG ext s' init ret)
-> m (Label s') -> m ([Block ext s' ret] -> CFG ext s' init ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (CFG ext s init ret -> Label s
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel CFG ext s init ret
cfg)
m ([Block ext s' ret] -> CFG ext s' init ret)
-> m [Block ext s' ret] -> m (CFG ext s' init ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Block ext s ret -> m (Block ext s' ret))
-> [Block ext s ret] -> m [Block ext s' ret]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Block ext s ret -> m (Block ext s' ret)
forall (m :: Type -> Type) ext s s' (ret :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Block ext s ret -> m (Block ext s' ret)
substBlock Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) (CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
cfg)
traverseCFG :: ( Monad m, TraverseExt ext )
=> (genv -> penv -> Block ext s ret -> m (genv, penv))
-> genv
-> penv
-> Block ext s ret
-> CFG ext s init ret
-> m genv
traverseCFG :: forall (m :: Type -> Type) ext genv penv s (ret :: CrucibleType)
(init :: Ctx CrucibleType).
(Monad m, TraverseExt ext) =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> genv -> penv -> Block ext s ret -> CFG ext s init ret -> m genv
traverseCFG genv -> penv -> Block ext s ret -> m (genv, penv)
f genv
genv0 penv
penv0 Block ext s ret
b0 CFG ext s init ret
cfg =
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
forall (m :: Type -> Type) genv penv ext s (ret :: CrucibleType).
Monad m =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
traverseStep genv -> penv -> Block ext s ret -> m (genv, penv)
f Map (BlockID s) (Block ext s ret)
bmap0 genv
genv0 penv
penv0 Set (BlockID s)
forall a. Monoid a => a
mempty Block ext s ret
b0
where
bmap0 :: Map (BlockID s) (Block ext s ret)
bmap0 = [(BlockID s, Block ext s ret)] -> Map (BlockID s) (Block ext s ret)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b, Block ext s ret
b) | Block ext s ret
b <- CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
cfg ]
traverseStep :: forall m genv penv ext s ret.
Monad m
=> (genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map.Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set.Set (BlockID s)
-> (Block ext s ret)
-> m genv
traverseStep :: forall (m :: Type -> Type) genv penv ext s (ret :: CrucibleType).
Monad m =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
traverseStep genv -> penv -> Block ext s ret -> m (genv, penv)
f Map (BlockID s) (Block ext s ret)
bmap genv
genv penv
penv Set (BlockID s)
seen Block ext s ret
blk
| Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk BlockID s -> Set (BlockID s) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (BlockID s)
seen =
genv -> m genv
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return genv
genv
| Bool
otherwise =
do (genv
genv', penv
penv') <- genv -> penv -> Block ext s ret -> m (genv, penv)
f genv
genv penv
penv Block ext s ret
blk
(genv -> BlockID s -> m genv) -> genv -> [BlockID s] -> m genv
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
Fold.foldlM (penv -> Set (BlockID s) -> genv -> BlockID s -> m genv
go penv
penv' (BlockID s -> Set (BlockID s) -> Set (BlockID s)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk) Set (BlockID s)
seen)) genv
genv' [BlockID s]
next
where
next :: [BlockID s]
next = [BlockID s] -> Maybe [BlockID s] -> [BlockID s]
forall a. a -> Maybe a -> a
fromMaybe [] (TermStmt s ret -> Maybe [BlockID s]
forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s]
termNextLabels (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
blk)))
go :: penv -> Set (BlockID s) -> genv -> BlockID s -> m genv
go penv
penv' Set (BlockID s)
seen' genv
genv' BlockID s
blkId
| Just Block ext s ret
blk' <- BlockID s
-> Map (BlockID s) (Block ext s ret) -> Maybe (Block ext s ret)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockID s
blkId Map (BlockID s) (Block ext s ret)
bmap
= (genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
forall (m :: Type -> Type) genv penv ext s (ret :: CrucibleType).
Monad m =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
traverseStep genv -> penv -> Block ext s ret -> m (genv, penv)
f Map (BlockID s) (Block ext s ret)
bmap genv
genv' penv
penv' Set (BlockID s)
seen' Block ext s ret
blk'
| Bool
otherwise
= String -> [String] -> m genv
forall a. HasCallStack => String -> [String] -> a
panic String
"Reg.traverseStep"
[ String
"Block " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BlockID s -> String
forall a. Show a => a -> String
show BlockID s
blkId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not found in block map" ]
instance PrettyExt ext => Show (CFG ext s init ret) where
show :: CFG ext s init ret -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (CFG ext s init ret -> Doc Any) -> CFG ext s init ret -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CFG ext s init ret -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. CFG ext s init ret -> Doc ann
pretty
instance PrettyExt ext => Pretty (CFG ext s init ret) where
pretty :: forall ann. CFG ext s init ret -> Doc ann
pretty CFG ext s init ret
g = do
let nm :: Doc ann
nm = FunctionName -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (FnHandle init ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
g))
let args :: Doc ann
args =
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (Some (Value s) -> Doc ann) -> [Some (Value s)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (tp :: CrucibleType). Value s tp -> Doc ann)
-> Some (Value s) -> Doc ann
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome Value s tp -> Doc ann
forall a ann. Show a => a -> Doc ann
forall (tp :: CrucibleType). Value s tp -> Doc ann
viaShow) ([Some (Value s)] -> [Doc ann]) -> [Some (Value s)] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Set (Some (Value s)) -> [Some (Value s)]
forall a. Set a -> [a]
Set.toList (Set (Some (Value s)) -> [Some (Value s)])
-> Set (Some (Value s)) -> [Some (Value s)]
forall a b. (a -> b) -> a -> b
$
Block ext s ret -> Set (Some (Value s))
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs (CFG ext s init ret -> Block ext s ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Block ext s ret
cfgEntryBlock CFG ext s init ret
g)
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ TypeRepr ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr ret -> Doc ann
pretty (CFG ext s init ret -> TypeRepr ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> TypeRepr ret
cfgReturnType CFG ext s init ret
g) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
args
, [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Block ext s ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Block ext s ret -> Doc ann
pretty (Block ext s ret -> Doc ann) -> [Block ext s ret] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
g) ]
data SomeCFG ext init ret = forall s . SomeCFG !(CFG ext s init ret)
data AnyCFG ext where
AnyCFG :: CFG ext blocks init ret
-> AnyCFG ext
instance PrettyExt ext => Show (AnyCFG ext) where
show :: AnyCFG ext -> String
show AnyCFG ext
cfg = case AnyCFG ext
cfg of AnyCFG CFG ext blocks init ret
c -> CFG ext blocks init ret -> String
forall a. Show a => a -> String
show CFG ext blocks init ret
c