{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.CFG.Generator
(
Generator
, FunctionDef
, defineFunction
, defineFunctionOpt
, getPosition
, setPosition
, withPosition
, newReg
, newUnassignedReg
, readReg
, assignReg
, modifyReg
, modifyRegM
, readGlobal
, writeGlobal
, newRef
, newEmptyRef
, readRef
, writeRef
, dropRef
, call
, assertExpr
, assumeExpr
, addPrintStmt
, addBreakpointStmt
, extensionStmt
, mkAtom
, mkFresh
, mkFreshFloat
, forceEvaluation
, newLabel
, newLambdaLabel
, newLambdaLabel'
, currentBlockID
, jump
, jumpToLambda
, branch
, returnFromFunction
, reportError
, branchMaybe
, branchVariant
, tailCall
, defineBlock
, defineLambdaBlock
, defineBlockLabel
, recordCFG
, continue
, continueLambda
, whenCond
, unlessCond
, ifte
, ifte'
, ifte_
, ifteM
, MatchMaybe(..)
, caseMaybe
, caseMaybe_
, fromJustExpr
, assertedJustExpr
, while
, Ctx.Ctx(..)
, Position
, module Lang.Crucible.CFG.Reg
, module Lang.Crucible.CFG.EarlyMergeLoops
) where
import Control.Lens hiding (Index)
import Control.Monad ((>=>))
import qualified Control.Monad.Fail as F
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.State.Strict ()
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Catch
import qualified Data.Foldable as Fold
import Data.Kind
import Data.Parameterized.Context as Ctx
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Text (Text)
import Data.Void
import What4.ProgramLoc
import What4.Symbol
import Lang.Crucible.CFG.Core (AnyCFG(..))
import Lang.Crucible.CFG.Expr(App(..))
import Lang.Crucible.CFG.Extension
import Lang.Crucible.CFG.Reg hiding (AnyCFG)
import Lang.Crucible.CFG.EarlyMergeLoops (earlyMergeLoops)
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Types
import Lang.Crucible.Utils.StateContT
type StmtSeq ext s = Seq (Posd (Stmt ext s))
data CurrentBlockState ext s
= CBS {
forall ext s. CurrentBlockState ext s -> BlockID s
cbsBlockID :: !(BlockID s)
, forall ext s. CurrentBlockState ext s -> ValueSet s
cbsInputValues :: !(ValueSet s)
, forall ext s. CurrentBlockState ext s -> StmtSeq ext s
_cbsStmts :: !(StmtSeq ext s)
}
initCurrentBlockState :: ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState :: forall s ext. ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState ValueSet s
inputs BlockID s
block_id =
CBS { cbsBlockID :: BlockID s
cbsBlockID = BlockID s
block_id
, cbsInputValues :: ValueSet s
cbsInputValues = ValueSet s
inputs
, _cbsStmts :: StmtSeq ext s
_cbsStmts = StmtSeq ext s
forall a. Seq a
Seq.empty
}
cbsStmts :: Simple Lens (CurrentBlockState ext s) (StmtSeq ext s)
cbsStmts :: forall ext s (f :: Type -> Type).
Functor f =>
(StmtSeq ext s -> f (StmtSeq ext s))
-> CurrentBlockState ext s -> f (CurrentBlockState ext s)
cbsStmts = (CurrentBlockState ext s -> StmtSeq ext s)
-> (CurrentBlockState ext s
-> StmtSeq ext s -> CurrentBlockState ext s)
-> Lens
(CurrentBlockState ext s)
(CurrentBlockState ext s)
(StmtSeq ext s)
(StmtSeq ext s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CurrentBlockState ext s -> StmtSeq ext s
forall ext s. CurrentBlockState ext s -> StmtSeq ext s
_cbsStmts (\CurrentBlockState ext s
s StmtSeq ext s
v -> CurrentBlockState ext s
s { _cbsStmts = v })
data IxGeneratorState ext s (t :: Type -> Type) ret m i
= GS { forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Label s
_gsEntryLabel :: !(Label s)
, forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Seq (Block ext s ret)
_gsBlocks :: !(Seq (Block ext s ret))
, forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> NonceGenerator m s
_gsNonceGen :: !(NonceGenerator m s)
, forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> i
_gsCurrent :: !i
, forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Position
_gsPosition :: !Position
, forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> t s
_gsState :: !(t s)
, forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> [AnyCFG ext]
_seenFunctions :: ![AnyCFG ext]
}
type GeneratorState ext s t ret m =
IxGeneratorState ext s t ret m (CurrentBlockState ext s)
type EndState ext s t ret m =
IxGeneratorState ext s t ret m ()
gsEntryLabel :: Getter (IxGeneratorState ext s t ret m i) (Label s)
gsEntryLabel :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(Label s -> f (Label s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsEntryLabel = (IxGeneratorState ext s t ret m i -> Label s)
-> (Label s -> f (Label s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to IxGeneratorState ext s t ret m i -> Label s
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Label s
_gsEntryLabel
gsBlocks :: Simple Lens (IxGeneratorState ext s t ret m i) (Seq (Block ext s ret))
gsBlocks :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Seq (Block ext s ret) -> f (Seq (Block ext s ret)))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsBlocks = (IxGeneratorState ext s t ret m i -> Seq (Block ext s ret))
-> (IxGeneratorState ext s t ret m i
-> Seq (Block ext s ret) -> IxGeneratorState ext s t ret m i)
-> Lens
(IxGeneratorState ext s t ret m i)
(IxGeneratorState ext s t ret m i)
(Seq (Block ext s ret))
(Seq (Block ext s ret))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> Seq (Block ext s ret)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Seq (Block ext s ret)
_gsBlocks (\IxGeneratorState ext s t ret m i
s Seq (Block ext s ret)
v -> IxGeneratorState ext s t ret m i
s { _gsBlocks = v })
gsNonceGen :: Getter (IxGeneratorState ext s t ret m i) (NonceGenerator m s)
gsNonceGen :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(NonceGenerator m s -> f (NonceGenerator m s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsNonceGen = (IxGeneratorState ext s t ret m i -> NonceGenerator m s)
-> (NonceGenerator m s -> f (NonceGenerator m s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to IxGeneratorState ext s t ret m i -> NonceGenerator m s
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> NonceGenerator m s
_gsNonceGen
gsCurrent :: Lens (IxGeneratorState ext s t ret m i) (IxGeneratorState ext s t ret m j) i j
gsCurrent :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent = (IxGeneratorState ext s t ret m i -> i)
-> (IxGeneratorState ext s t ret m i
-> j -> IxGeneratorState ext s t ret m j)
-> Lens
(IxGeneratorState ext s t ret m i)
(IxGeneratorState ext s t ret m j)
i
j
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> i
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> i
_gsCurrent (\IxGeneratorState ext s t ret m i
s j
v -> IxGeneratorState ext s t ret m i
s { _gsCurrent = v })
gsPosition :: Simple Lens (IxGeneratorState ext s t ret m i) Position
gsPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition = (IxGeneratorState ext s t ret m i -> Position)
-> (IxGeneratorState ext s t ret m i
-> Position -> IxGeneratorState ext s t ret m i)
-> Lens
(IxGeneratorState ext s t ret m i)
(IxGeneratorState ext s t ret m i)
Position
Position
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Position
_gsPosition (\IxGeneratorState ext s t ret m i
s Position
v -> IxGeneratorState ext s t ret m i
s { _gsPosition = v })
gsState :: Simple Lens (IxGeneratorState ext s t ret m i) (t s)
gsState :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(t s -> f (t s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsState = (IxGeneratorState ext s t ret m i -> t s)
-> (IxGeneratorState ext s t ret m i
-> t s -> IxGeneratorState ext s t ret m i)
-> Lens
(IxGeneratorState ext s t ret m i)
(IxGeneratorState ext s t ret m i)
(t s)
(t s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> t s
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> t s
_gsState (\IxGeneratorState ext s t ret m i
s t s
v -> IxGeneratorState ext s t ret m i
s { _gsState = v })
seenFunctions :: Simple Lens (IxGeneratorState ext s t ret m i) [AnyCFG ext]
seenFunctions :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
([AnyCFG ext] -> f [AnyCFG ext])
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
seenFunctions = (IxGeneratorState ext s t ret m i -> [AnyCFG ext])
-> (IxGeneratorState ext s t ret m i
-> [AnyCFG ext] -> IxGeneratorState ext s t ret m i)
-> Lens
(IxGeneratorState ext s t ret m i)
(IxGeneratorState ext s t ret m i)
[AnyCFG ext]
[AnyCFG ext]
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> [AnyCFG ext]
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> [AnyCFG ext]
_seenFunctions (\IxGeneratorState ext s t ret m i
s [AnyCFG ext]
v -> IxGeneratorState ext s t ret m i
s { _seenFunctions = v })
startBlock ::
BlockID s ->
EndState ext s t ret m ->
GeneratorState ext s t ret m
startBlock :: forall s ext (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock BlockID s
l EndState ext s t ret m
gs =
EndState ext s t ret m
gs EndState ext s t ret m
-> (EndState ext s t ret m -> GeneratorState ext s t ret m)
-> GeneratorState ext s t ret m
forall a b. a -> (a -> b) -> b
& (() -> Identity (CurrentBlockState ext s))
-> EndState ext s t ret m
-> Identity (GeneratorState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((() -> Identity (CurrentBlockState ext s))
-> EndState ext s t ret m
-> Identity (GeneratorState ext s t ret m))
-> CurrentBlockState ext s
-> EndState ext s t ret m
-> GeneratorState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ValueSet s -> BlockID s -> CurrentBlockState ext s
forall s ext. ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState ValueSet s
forall a. Set a
Set.empty BlockID s
l
terminateBlock ::
IsSyntaxExtension ext =>
TermStmt s ret ->
GeneratorState ext s t ret m ->
EndState ext s t ret m
terminateBlock :: forall ext s (ret :: CrucibleType) (t :: Type -> Type)
(m :: Type -> Type).
IsSyntaxExtension ext =>
TermStmt s ret
-> GeneratorState ext s t ret m -> EndState ext s t ret m
terminateBlock TermStmt s ret
term GeneratorState ext s t ret m
gs =
do let p :: Position
p = GeneratorState ext s t ret m
gsGeneratorState ext s t ret m
-> Getting Position (GeneratorState ext s t ret m) Position
-> Position
forall s a. s -> Getting a s a -> a
^.Getting Position (GeneratorState ext s t ret m) Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition
let cbs :: CurrentBlockState ext s
cbs = GeneratorState ext s t ret m
gsGeneratorState ext s t ret m
-> Getting
(CurrentBlockState ext s)
(GeneratorState ext s t ret m)
(CurrentBlockState ext s)
-> CurrentBlockState ext s
forall s a. s -> Getting a s a -> a
^.Getting
(CurrentBlockState ext s)
(GeneratorState ext s t ret m)
(CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent
let b :: Block ext s ret
b = BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
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 (CurrentBlockState ext s -> BlockID s
forall ext s. CurrentBlockState ext s -> BlockID s
cbsBlockID CurrentBlockState ext s
cbs) (CurrentBlockState ext s -> ValueSet s
forall ext s. CurrentBlockState ext s -> ValueSet s
cbsInputValues CurrentBlockState ext s
cbs) (CurrentBlockState ext s
cbsCurrentBlockState ext s
-> Getting
(Seq (Posd (Stmt ext s)))
(CurrentBlockState ext s)
(Seq (Posd (Stmt ext s)))
-> Seq (Posd (Stmt ext s))
forall s a. s -> Getting a s a -> a
^.Getting
(Seq (Posd (Stmt ext s)))
(CurrentBlockState ext s)
(Seq (Posd (Stmt ext s)))
forall ext s (f :: Type -> Type).
Functor f =>
(StmtSeq ext s -> f (StmtSeq ext s))
-> CurrentBlockState ext s -> f (CurrentBlockState ext s)
cbsStmts) (Position -> TermStmt s ret -> Posd (TermStmt s ret)
forall v. Position -> v -> Posd v
Posd Position
p TermStmt s ret
term)
let gs' :: EndState ext s t ret m
gs' = GeneratorState ext s t ret m
gs GeneratorState ext s t ret m
-> (GeneratorState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (CurrentBlockState ext s -> Identity ())
-> GeneratorState ext s t ret m
-> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((CurrentBlockState ext s -> Identity ())
-> GeneratorState ext s t ret m
-> Identity (EndState ext s t ret m))
-> () -> GeneratorState ext s t ret m -> EndState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ()
EndState ext s t ret m
-> (EndState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (Seq (Block ext s ret) -> Identity (Seq (Block ext s ret)))
-> EndState ext s t ret m -> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Seq (Block ext s ret) -> f (Seq (Block ext s ret)))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsBlocks ((Seq (Block ext s ret) -> Identity (Seq (Block ext s ret)))
-> EndState ext s t ret m -> Identity (EndState ext s t ret m))
-> (Seq (Block ext s ret) -> Seq (Block ext s ret))
-> EndState ext s t ret m
-> EndState ext s t ret m
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Seq (Block ext s ret) -> Block ext s ret -> Seq (Block ext s ret)
forall a. Seq a -> a -> Seq a
Seq.|> Block ext s ret
b)
Block ext s ret -> EndState ext s t ret m -> EndState ext s t ret m
forall a b. a -> b -> b
seq Block ext s ret
b EndState ext s t ret m
gs'
newtype Generator ext s (t :: Type -> Type) (ret :: CrucibleType) m a
= Generator { forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator :: StateContT (GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
a
}
deriving ( (forall a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b)
-> (forall a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a)
-> Functor (Generator ext s t ret m)
forall a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
forall a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
fmap :: forall a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
$c<$ :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
<$ :: forall a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
Functor
, Functor (Generator ext s t ret m)
Functor (Generator ext s t ret m) =>
(forall a. a -> Generator ext s t ret m a)
-> (forall a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b)
-> (forall a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c)
-> (forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b)
-> (forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a)
-> Applicative (Generator ext s t ret m)
forall a. a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
forall a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Functor (Generator ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
a -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
a -> Generator ext s t ret m a
pure :: forall a. a -> Generator ext s t ret m a
$c<*> :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
<*> :: forall a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
$cliftA2 :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
liftA2 :: forall a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
$c*> :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
*> :: forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
$c<* :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
<* :: forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
Applicative
, Monad (Generator ext s t ret m)
Monad (Generator ext s t ret m) =>
(forall e a.
(HasCallStack, Exception e) =>
e -> Generator ext s t ret m a)
-> MonadThrow (Generator ext s t ret m)
forall e a.
(HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
MonadThrow m =>
Monad (Generator ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
forall (m :: Type -> Type).
Monad m =>
(forall e a. (HasCallStack, Exception e) => e -> m a)
-> MonadThrow m
$cthrowM :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
throwM :: forall e a.
(HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
MonadThrow
, MonadThrow (Generator ext s t ret m)
MonadThrow (Generator ext s t ret m) =>
(forall e a.
(HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a)
-> MonadCatch (Generator ext s t ret m)
forall e a.
(HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
MonadCatch m =>
MonadThrow (Generator ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) e a.
(MonadCatch m, HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
forall (m :: Type -> Type).
MonadThrow m =>
(forall e a.
(HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a)
-> MonadCatch m
$ccatch :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) e a.
(MonadCatch m, HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
catch :: forall e a.
(HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
MonadCatch
)
instance MonadTrans (Generator ext s t ret) where
lift :: forall (m :: Type -> Type) a.
Monad m =>
m a -> Generator ext s t ret m a
lift m a
m = StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (m a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall (m :: Type -> Type) a.
Monad m =>
m a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
m)
instance Monad m => Monad (Generator ext s t ret m) where
Generator ext s t ret m a
x >>= :: forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
>>= a -> Generator ext s t ret m b
f = StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b
-> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (Generator ext s t ret m a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator Generator ext s t ret m a
x StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> (a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b)
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall a b.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> (a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b)
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Generator ext s t ret m b
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator (Generator ext s t ret m b
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b)
-> (a -> Generator ext s t ret m b)
-> a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Generator ext s t ret m b
f)
instance F.MonadFail m => F.MonadFail (Generator ext s t ret m) where
fail :: forall a. String -> Generator ext s t ret m a
fail String
msg = StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a)
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall a b. (a -> b) -> a -> b
$ do
Position
p <- Getting Position (GeneratorState ext s t ret m) Position
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m Position
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting Position (GeneratorState ext s t ret m) Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition
String
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall a.
String
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a)
-> String
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"Failure encountered while generating a Crucible CFG:"
, String
"at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
]
instance Monad m => MonadState (t s) (Generator ext s t ret m) where
get :: Generator ext s t ret m (t s)
get = StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(t s)
-> Generator ext s t ret m (t s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(t s)
-> Generator ext s t ret m (t s))
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(t s)
-> Generator ext s t ret m (t s)
forall a b. (a -> b) -> a -> b
$ Getting
(t s)
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(t s)
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(t s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
(t s)
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(t s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(t s -> f (t s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsState
put :: t s -> Generator ext s t ret m ()
put t s
v = StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ())
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ (t s -> Identity (t s))
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(t s -> f (t s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsState ((t s -> Identity (t s))
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> t s
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= t s
v
instance MonadIO m => MonadIO (Generator ext s t ret m) where
liftIO :: forall a. IO a -> Generator ext s t ret m a
liftIO IO a
m = m a -> Generator ext s t ret m a
forall (m :: Type -> Type) a.
Monad m =>
m a -> Generator ext s t ret m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO a -> m a
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO IO a
m)
runGenerator ::
Generator ext s t ret m Void ->
GeneratorState ext s t ret m ->
m (EndState ext s t ret m)
runGenerator :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
m GeneratorState ext s t ret m
gs = StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m Void
-> (Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m
-> m (EndState ext s t ret m)
forall s r (m :: Type -> Type) a.
StateContT s r m a -> (a -> s -> m r) -> s -> m r
runStateContT (Generator ext s t ret m Void
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m Void
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator Generator ext s t ret m Void
m) Void -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall a. Void -> a
absurd GeneratorState ext s t ret m
gs
getPosition :: Generator ext s t ret m Position
getPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Position
getPosition = StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
Position
-> Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
Position
-> Generator ext s t ret m Position)
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
Position
-> Generator ext s t ret m Position
forall a b. (a -> b) -> a -> b
$ Getting
Position
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
Position
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
Position
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
Position
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition
setPosition :: Position -> Generator ext s t ret m ()
setPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition Position
p = StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ())
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ (Position -> Identity Position)
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition ((Position -> Identity Position)
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> Position
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Position
p
withPosition :: Monad m
=> Position
-> Generator ext s t ret m a
-> Generator ext s t ret m a
withPosition :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
Monad m =>
Position -> Generator ext s t ret m a -> Generator ext s t ret m a
withPosition Position
p Generator ext s t ret m a
m =
do Position
old_pos <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Position
getPosition
Position -> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition Position
p
a
v <- Generator ext s t ret m a
m
Position -> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition Position
old_pos
a -> Generator ext s t ret m a
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
v
mkNonce :: Monad m => Generator ext s t ret m (Nonce s tp)
mkNonce :: forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce =
do NonceGenerator m s
ng <- StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(NonceGenerator m s)
-> Generator ext s t ret m (NonceGenerator m s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(NonceGenerator m s)
-> Generator ext s t ret m (NonceGenerator m s))
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(NonceGenerator m s)
-> Generator ext s t ret m (NonceGenerator m s)
forall a b. (a -> b) -> a -> b
$ Getting
(NonceGenerator m s)
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(NonceGenerator m s)
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(NonceGenerator m s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
(NonceGenerator m s)
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(NonceGenerator m s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(NonceGenerator m s -> f (NonceGenerator m s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsNonceGen
StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(Nonce s tp)
-> Generator ext s t ret m (Nonce s tp)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(Nonce s tp)
-> Generator ext s t ret m (Nonce s tp))
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(Nonce s tp)
-> Generator ext s t ret m (Nonce s tp)
forall a b. (a -> b) -> a -> b
$ m (Nonce s tp)
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(Nonce s tp)
forall (m :: Type -> Type) a.
Monad m =>
m a
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Nonce s tp)
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(Nonce s tp))
-> m (Nonce s tp)
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(Nonce s tp)
forall a b. (a -> b) -> a -> b
$ 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
addStmt :: Monad m => Stmt ext s -> Generator ext s t ret m ()
addStmt :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt Stmt ext s
s =
do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Position
getPosition
CurrentBlockState ext s
cbs <- StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(CurrentBlockState ext s)
-> Generator ext s t ret m (CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(CurrentBlockState ext s)
-> Generator ext s t ret m (CurrentBlockState ext s))
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(CurrentBlockState ext s)
-> Generator ext s t ret m (CurrentBlockState ext s)
forall a b. (a -> b) -> a -> b
$ Getting
(CurrentBlockState ext s)
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(CurrentBlockState ext s)
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
(CurrentBlockState ext s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
(CurrentBlockState ext s)
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent
let ps :: Posd (Stmt ext s)
ps = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
p Stmt ext s
s
let cbs' :: CurrentBlockState ext s
cbs' = CurrentBlockState ext s
cbs CurrentBlockState ext s
-> (CurrentBlockState ext s -> CurrentBlockState ext s)
-> CurrentBlockState ext s
forall a b. a -> (a -> b) -> b
& (StmtSeq ext s -> Identity (StmtSeq ext s))
-> CurrentBlockState ext s -> Identity (CurrentBlockState ext s)
forall ext s (f :: Type -> Type).
Functor f =>
(StmtSeq ext s -> f (StmtSeq ext s))
-> CurrentBlockState ext s -> f (CurrentBlockState ext s)
cbsStmts ((StmtSeq ext s -> Identity (StmtSeq ext s))
-> CurrentBlockState ext s -> Identity (CurrentBlockState ext s))
-> (StmtSeq ext s -> StmtSeq ext s)
-> CurrentBlockState ext s
-> CurrentBlockState ext s
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (StmtSeq ext s -> Posd (Stmt ext s) -> StmtSeq ext s
forall a. Seq a -> a -> Seq a
Seq.|> Posd (Stmt ext s)
ps)
Posd (Stmt ext s)
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. a -> b -> b
seq Posd (Stmt ext s)
ps (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ CurrentBlockState ext s
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. a -> b -> b
seq CurrentBlockState ext s
cbs' (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ())
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ (CurrentBlockState ext s -> Identity (CurrentBlockState ext s))
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((CurrentBlockState ext s -> Identity (CurrentBlockState ext s))
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> CurrentBlockState ext s
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= CurrentBlockState ext s
cbs'
freshAtom :: (Monad m, IsSyntaxExtension ext) => AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom AtomValue ext s tp
av =
do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Position
getPosition
Nonce s tp
n <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
let atom :: Atom s tp
atom = 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
Assigned
, typeOfAtom :: TypeRepr tp
typeOfAtom = AtomValue ext s tp -> TypeRepr tp
forall ext s (tp :: CrucibleType).
(TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) =>
AtomValue ext s tp -> TypeRepr tp
typeOfAtomValue AtomValue ext s tp
av
}
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (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
atom AtomValue ext s tp
av)
Atom s tp -> Generator ext s t ret m (Atom s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Atom s tp
atom
mkFresh :: (Monad m, IsSyntaxExtension ext)
=> BaseTypeRepr tp
-> Maybe SolverSymbol
-> Generator ext s t ret m (Atom s (BaseToType tp))
mkFresh :: forall (m :: Type -> Type) ext (tp :: BaseType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BaseTypeRepr tp
-> Maybe SolverSymbol
-> Generator ext s t ret m (Atom s (BaseToType tp))
mkFresh BaseTypeRepr tp
tr Maybe SolverSymbol
symb = AtomValue ext s (BaseToType tp)
-> Generator ext s t ret m (Atom s (BaseToType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (BaseTypeRepr tp
-> Maybe SolverSymbol -> AtomValue ext s (BaseToType tp)
forall (bt :: BaseType) ext s.
BaseTypeRepr bt
-> Maybe SolverSymbol -> AtomValue ext s ('BaseToType bt)
FreshConstant BaseTypeRepr tp
tr Maybe SolverSymbol
symb)
mkFreshFloat :: (Monad m, IsSyntaxExtension ext)
=> FloatInfoRepr fi
-> Maybe SolverSymbol
-> Generator ext s t ret m (Atom s (FloatType fi))
mkFreshFloat :: forall (m :: Type -> Type) ext (fi :: FloatInfo) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
FloatInfoRepr fi
-> Maybe SolverSymbol
-> Generator ext s t ret m (Atom s (FloatType fi))
mkFreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
symb = AtomValue ext s (FloatType fi)
-> Generator ext s t ret m (Atom s (FloatType fi))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s (FloatType fi)
forall (fi :: FloatInfo) ext s.
FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s ('FloatType fi)
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
symb)
mkAtom :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom (AtomExpr Atom s tp
a) = Atom s tp -> Generator ext s t ret m (Atom s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Atom s tp
a
mkAtom (App App ext (Expr ext s) tp
a) = AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (AtomValue ext s tp -> Generator ext s t ret m (Atom s tp))
-> (App ext (Atom s) tp -> AtomValue ext s tp)
-> App ext (Atom s) tp
-> Generator ext s t ret m (Atom s tp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> Generator ext s t ret m (Atom s tp))
-> Generator ext s t ret m (App ext (Atom s) tp)
-> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x))
-> forall (x :: CrucibleType).
App ext (Expr ext s) x
-> Generator ext s t ret 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 Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom App ext (Expr ext s) tp
a
readGlobal :: (Monad m, IsSyntaxExtension ext) => GlobalVar tp -> Generator ext s t ret m (Expr ext s tp)
readGlobal :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
GlobalVar tp -> Generator ext s t ret m (Expr ext s tp)
readGlobal GlobalVar tp
v = 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)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (GlobalVar tp -> AtomValue ext s tp
forall (tp :: CrucibleType) ext s.
GlobalVar tp -> AtomValue ext s tp
ReadGlobal GlobalVar tp
v)
writeGlobal :: (Monad m, IsSyntaxExtension ext) => GlobalVar tp -> Expr ext s tp -> Generator ext s t ret m ()
writeGlobal :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
GlobalVar tp -> Expr ext s tp -> Generator ext s t ret m ()
writeGlobal GlobalVar tp
v Expr ext s tp
e =
do Atom s tp
a <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
e
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (GlobalVar tp -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
GlobalVar tp -> Atom s tp -> Stmt ext s
WriteGlobal GlobalVar tp
v Atom s tp
a)
readRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Generator ext s t ret m (Expr ext s tp)
readRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Expr ext s tp)
readRef Expr ext s (ReferenceType tp)
ref =
do Atom s (ReferenceType tp)
r <- Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (ReferenceType tp)
ref
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)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (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)
r)
writeRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Expr ext s tp -> Generator ext s t ret m ()
writeRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (ReferenceType tp)
-> Expr ext s tp -> Generator ext s t ret m ()
writeRef Expr ext s (ReferenceType tp)
ref Expr ext s tp
val =
do Atom s (ReferenceType tp)
r <- Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (ReferenceType tp)
ref
Atom s tp
v <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
val
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (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)
r Atom s tp
v)
dropRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Generator ext s t ret m ()
dropRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (ReferenceType tp) -> Generator ext s t ret m ()
dropRef Expr ext s (ReferenceType tp)
ref =
do Atom s (ReferenceType tp)
r <- Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (ReferenceType tp)
ref
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s (ReferenceType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Stmt ext s
DropRef Atom s (ReferenceType tp)
r)
newRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newRef Expr ext s tp
val =
do Atom s tp
v <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
val
Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp)
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp))
-> Generator ext s t ret m (Atom s (ReferenceType tp))
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (Atom s tp -> AtomValue ext s (ReferenceType tp)
forall s (tp1 :: CrucibleType) ext.
Atom s tp1 -> AtomValue ext s ('ReferenceType tp1)
NewRef Atom s tp
v)
newEmptyRef :: (Monad m, IsSyntaxExtension ext) => TypeRepr tp -> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newEmptyRef :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
TypeRepr tp
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newEmptyRef TypeRepr tp
tp =
Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp)
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp))
-> Generator ext s t ret m (Atom s (ReferenceType tp))
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (TypeRepr tp -> AtomValue ext s (ReferenceType tp)
forall (tp1 :: CrucibleType) ext s.
TypeRepr tp1 -> AtomValue ext s ('ReferenceType tp1)
NewEmptyRef TypeRepr tp
tp)
newReg :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Reg s tp)
newReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Reg s tp)
newReg Expr ext s tp
e =
do Reg s tp
r <- TypeRepr tp -> Generator ext s t ret m (Reg s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (Reg s tp)
newUnassignedReg (Expr ext s tp -> TypeRepr tp
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s tp
e)
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r Expr ext s tp
e
Reg s tp -> Generator ext s t ret m (Reg s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Reg s tp
r
newUnassignedReg :: Monad m => TypeRepr tp -> Generator ext s t ret m (Reg s tp)
newUnassignedReg :: forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (Reg s tp)
newUnassignedReg TypeRepr tp
tp =
do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Position
getPosition
Nonce s tp
n <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
Reg s tp -> Generator ext s t ret m (Reg s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Reg s tp -> Generator ext s t ret m (Reg s tp))
-> Reg s tp -> Generator ext s t ret m (Reg s tp)
forall a b. (a -> b) -> a -> b
$! Reg { regPosition :: Position
regPosition = Position
p
, regId :: Nonce s tp
regId = Nonce s tp
n
, typeOfReg :: TypeRepr tp
typeOfReg = TypeRepr tp
tp
}
readReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s tp
r = 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)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (Reg s tp -> AtomValue ext s tp
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg Reg s tp
r)
assignReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r Expr ext s tp
e =
do Atom s tp
a <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
e
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (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
a)
modifyReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> (Expr ext s tp -> Expr ext s tp) -> Generator ext s t ret m ()
modifyReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp
-> (Expr ext s tp -> Expr ext s tp) -> Generator ext s t ret m ()
modifyReg Reg s tp
r Expr ext s tp -> Expr ext s tp
f =
do Expr ext s tp
v <- Reg s tp -> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s tp
r
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r (Expr ext s tp -> Generator ext s t ret m ())
-> Expr ext s tp -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$! Expr ext s tp -> Expr ext s tp
f Expr ext s tp
v
modifyRegM :: (Monad m, IsSyntaxExtension ext)
=> Reg s tp
-> (Expr ext s tp -> Generator ext s t ret m (Expr ext s tp))
-> Generator ext s t ret m ()
modifyRegM :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp
-> (Expr ext s tp -> Generator ext s t ret m (Expr ext s tp))
-> Generator ext s t ret m ()
modifyRegM Reg s tp
r Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
f =
do Expr ext s tp
v <- Reg s tp -> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s tp
r
Expr ext s tp
v' <- Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
f Expr ext s tp
v
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r Expr ext s tp
v'
addPrintStmt :: (Monad m, IsSyntaxExtension ext) => Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
addPrintStmt :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
addPrintStmt Expr ext s (StringType Unicode)
e =
do Atom s (StringType Unicode)
e_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s (StringType Unicode) -> Stmt ext s
forall ext s. Atom s (StringType Unicode) -> Stmt ext s
Print Atom s (StringType Unicode)
e_a)
addBreakpointStmt ::
(Monad m, IsSyntaxExtension ext) =>
Text ->
Assignment (Value s) args ->
Generator ext s t r m ()
addBreakpointStmt :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
(t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Text -> Assignment (Value s) args -> Generator ext s t r m ()
addBreakpointStmt Text
nm Assignment (Value s) args
args = Stmt ext s -> Generator ext s t r m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Stmt ext s -> Generator ext s t r m ())
-> Stmt ext s -> Generator ext s t r m ()
forall a b. (a -> b) -> a -> b
$ BreakpointName -> Assignment (Value s) args -> Stmt ext s
forall ext s (args :: Ctx CrucibleType).
BreakpointName -> Assignment (Value s) args -> Stmt ext s
Breakpoint (Text -> BreakpointName
BreakpointName Text
nm) Assignment (Value s) args
args
assertExpr ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType ->
Expr ext s (StringType Unicode) ->
Generator ext s t ret m ()
assertExpr :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
assertExpr Expr ext s BoolType
b Expr ext s (StringType Unicode)
e =
do Atom s BoolType
b_a <- Expr ext s BoolType -> Generator ext s t ret m (Atom s BoolType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s BoolType
b
Atom s (StringType Unicode)
e_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (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
b_a Atom s (StringType Unicode)
e_a)
assumeExpr ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType ->
Expr ext s (StringType Unicode) ->
Generator ext s t ret m ()
assumeExpr :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
assumeExpr Expr ext s BoolType
b Expr ext s (StringType Unicode)
e =
do Atom s BoolType
b_a <- Expr ext s BoolType -> Generator ext s t ret m (Atom s BoolType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s BoolType
b
Atom s (StringType Unicode)
m_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (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
b_a Atom s (StringType Unicode)
m_a)
recordCFG :: AnyCFG ext -> Generator ext s t ret m ()
recordCFG :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
AnyCFG ext -> Generator ext s t ret m ()
recordCFG AnyCFG ext
g = StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ())
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ ([AnyCFG ext] -> Identity [AnyCFG ext])
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
([AnyCFG ext] -> f [AnyCFG ext])
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
seenFunctions (([AnyCFG ext] -> Identity [AnyCFG ext])
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
(IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> ([AnyCFG ext] -> [AnyCFG ext])
-> StateContT
(IxGeneratorState ext s t ret m (CurrentBlockState ext s))
(EndState ext s t ret m)
m
()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (AnyCFG ext
gAnyCFG ext -> [AnyCFG ext] -> [AnyCFG ext]
forall a. a -> [a] -> [a]
:)
newLabel :: Monad m => Generator ext s t ret m (Label s)
newLabel :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel = Nonce s UnitType -> Label s
forall s. Nonce s UnitType -> Label s
Label (Nonce s UnitType -> Label s)
-> Generator ext s t ret m (Nonce s UnitType)
-> Generator ext s t ret m (Label s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Generator ext s t ret m (Nonce s UnitType)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
newLambdaLabel :: Monad m => KnownRepr TypeRepr tp => Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel :: forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, KnownRepr TypeRepr tp) =>
Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel = TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
newLambdaLabel' :: Monad m => TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' :: forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
tpr =
do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Position
getPosition
Nonce s tp
idx <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
Nonce s tp
i <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
let lbl :: LambdaLabel s tp
lbl = 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
idx Atom s tp
a
a :: Atom s tp
a = Atom { atomPosition :: Position
atomPosition = Position
p
, atomId :: Nonce s tp
atomId = Nonce s tp
i
, atomSource :: AtomSource s tp
atomSource = LambdaLabel s tp -> AtomSource s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> AtomSource s tp
LambdaArg LambdaLabel s tp
lbl
, typeOfAtom :: TypeRepr tp
typeOfAtom = TypeRepr tp
tpr
}
LambdaLabel s tp -> Generator ext s t ret m (LambdaLabel s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LambdaLabel s tp -> Generator ext s t ret m (LambdaLabel s tp))
-> LambdaLabel s tp -> Generator ext s t ret m (LambdaLabel s tp)
forall a b. (a -> b) -> a -> b
$! LambdaLabel s tp
lbl
currentBlockID :: Generator ext s t ret m (BlockID s)
currentBlockID :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m (BlockID s)
currentBlockID =
StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(BlockID s)
-> Generator ext s t ret m (BlockID s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(BlockID s)
-> Generator ext s t ret m (BlockID s))
-> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(BlockID s)
-> Generator ext s t ret m (BlockID s)
forall a b. (a -> b) -> a -> b
$
(\GeneratorState ext s t ret m
st -> GeneratorState ext s t ret m
st GeneratorState ext s t ret m
-> Getting
(CurrentBlockState ext s)
(GeneratorState ext s t ret m)
(CurrentBlockState ext s)
-> CurrentBlockState ext s
forall s a. s -> Getting a s a -> a
^. Getting
(CurrentBlockState ext s)
(GeneratorState ext s t ret m)
(CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent CurrentBlockState ext s
-> (CurrentBlockState ext s -> BlockID s) -> BlockID s
forall a b. a -> (a -> b) -> b
& CurrentBlockState ext s -> BlockID s
forall ext s. CurrentBlockState ext s -> BlockID s
cbsBlockID) (GeneratorState ext s t ret m -> BlockID s)
-> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(GeneratorState ext s t ret m)
-> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(BlockID s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(GeneratorState ext s t ret m)
forall s (m :: Type -> Type). MonadState s m => m s
get
continue ::
(Monad m, IsSyntaxExtension ext) =>
Label s ->
(forall a. Generator ext s t ret m a) ->
Generator ext s t ret m ()
continue :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
lbl forall a. Generator ext s t ret m a
action =
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ())
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ ((() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((()
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ())
-> ((()
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall a b. (a -> b) -> a -> b
$ \() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont GeneratorState ext s t ret m
gs ->
do EndState ext s t ret m
gs' <- Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
forall a. Generator ext s t ret m a
action GeneratorState ext s t ret m
gs
() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont () (BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
forall s ext (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
lbl) EndState ext s t ret m
gs')
continueLambda ::
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp ->
(forall a. Generator ext s t ret m a) ->
Generator ext s t ret m (Expr ext s tp)
continueLambda :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
lbl forall a. Generator ext s t ret m a
action =
StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp))
-> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall a b. (a -> b) -> a -> b
$ ((Expr ext s tp
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(Expr ext s tp)
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((Expr ext s tp
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(Expr ext s tp))
-> ((Expr ext s tp
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m)
(EndState ext s t ret m)
m
(Expr ext s tp)
forall a b. (a -> b) -> a -> b
$ \Expr ext s tp
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont GeneratorState ext s t ret m
gs ->
do EndState ext s t ret m
gs' <- Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
forall a. Generator ext s t ret m a
action GeneratorState ext s t ret m
gs
Expr ext s tp
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont (Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
lbl)) (BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
forall s ext (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock (LambdaLabel s tp -> BlockID s
forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s
LambdaID LambdaLabel s tp
lbl) EndState ext s t ret m
gs')
defineSomeBlock ::
(Monad m, IsSyntaxExtension ext) =>
BlockID s ->
Generator ext s t ret m Void ->
Generator ext s t ret m ()
defineSomeBlock :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
defineSomeBlock BlockID s
l Generator ext s t ret m Void
next =
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ())
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ ((() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((()
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ())
-> ((()
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall a b. (a -> b) -> a -> b
$ \() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont GeneratorState ext s t ret m
gs0 ->
do let gs1 :: GeneratorState ext s t ret m
gs1 = BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
forall s ext (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock BlockID s
l (GeneratorState ext s t ret m
gs0 GeneratorState ext s t ret m
-> (GeneratorState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (CurrentBlockState ext s -> Identity ())
-> GeneratorState ext s t ret m
-> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((CurrentBlockState ext s -> Identity ())
-> GeneratorState ext s t ret m
-> Identity (EndState ext s t ret m))
-> () -> GeneratorState ext s t ret m -> EndState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ())
EndState ext s t ret m
gs2 <- Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
next GeneratorState ext s t ret m
gs1
let gs3 :: GeneratorState ext s t ret m
gs3 = EndState ext s t ret m
gs2 EndState ext s t ret m
-> (EndState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (Position -> Identity Position)
-> EndState ext s t ret m -> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition ((Position -> Identity Position)
-> EndState ext s t ret m -> Identity (EndState ext s t ret m))
-> Position -> EndState ext s t ret m -> EndState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ GeneratorState ext s t ret m
gs0GeneratorState ext s t ret m
-> Getting Position (GeneratorState ext s t ret m) Position
-> Position
forall s a. s -> Getting a s a -> a
^.Getting Position (GeneratorState ext s t ret m) Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition
EndState ext s t ret m
-> (EndState ext s t ret m -> GeneratorState ext s t ret m)
-> GeneratorState ext s t ret m
forall a b. a -> (a -> b) -> b
& (() -> Identity (CurrentBlockState ext s))
-> EndState ext s t ret m
-> Identity (GeneratorState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((() -> Identity (CurrentBlockState ext s))
-> EndState ext s t ret m
-> Identity (GeneratorState ext s t ret m))
-> CurrentBlockState ext s
-> EndState ext s t ret m
-> GeneratorState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ GeneratorState ext s t ret m
gs0GeneratorState ext s t ret m
-> Getting
(CurrentBlockState ext s)
(GeneratorState ext s t ret m)
(CurrentBlockState ext s)
-> CurrentBlockState ext s
forall s a. s -> Getting a s a -> a
^.Getting
(CurrentBlockState ext s)
(GeneratorState ext s t ret m)
(CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent
() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont () GeneratorState ext s t ret m
gs3
defineBlock ::
(Monad m, IsSyntaxExtension ext) =>
Label s ->
(forall a. Generator ext s t ret m a) ->
Generator ext s t ret m ()
defineBlock :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
l forall a. Generator ext s t ret m a
action =
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
defineSomeBlock (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
l) Generator ext s t ret m Void
forall a. Generator ext s t ret m a
action
defineLambdaBlock ::
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp ->
(forall a. Expr ext s tp -> Generator ext s t ret m a) ->
Generator ext s t ret m ()
defineLambdaBlock :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
l forall a. Expr ext s tp -> Generator ext s t ret m a
action =
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
defineSomeBlock (LambdaLabel s tp -> BlockID s
forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s
LambdaID LambdaLabel s tp
l) (Expr ext s tp -> Generator ext s t ret m Void
forall a. Expr ext s tp -> Generator ext s t ret m a
action (Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
l)))
defineBlockLabel ::
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a) ->
Generator ext s t ret m (Label s)
defineBlockLabel :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel forall a. Generator ext s t ret m a
action =
do Label s
l <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
l Generator ext s t ret m a
forall a. Generator ext s t ret m a
action
Label s -> Generator ext s t ret m (Label s)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Label s
l
forceEvaluation :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation Expr ext s tp
e = 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)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
e
extensionStmt ::
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp ->
Generator ext s t ret m (Expr ext s tp)
extensionStmt :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt StmtExtension ext (Expr ext s) tp
stmt = do
StmtExtension ext (Atom s) tp
stmt' <- (forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x))
-> forall (x :: CrucibleType).
StmtExtension ext (Expr ext s) x
-> Generator ext s t ret 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 Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom StmtExtension ext (Expr ext s) tp
stmt
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)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (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
stmt')
call :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Expr ext s ret)
call :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
(ret :: CrucibleType) (t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Expr ext s ret)
call Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args = Atom s ret -> Expr ext s ret
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s ret -> Expr ext s ret)
-> Generator ext s t r m (Atom s ret)
-> Generator ext s t r m (Expr ext s ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Atom s ret)
forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
(ret :: CrucibleType) (t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Atom s ret)
call' Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args
call' :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Atom s ret)
call' :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
(ret :: CrucibleType) (t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Atom s ret)
call' Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args = do
case Expr ext s (FunctionHandleType args ret)
-> TypeRepr (FunctionHandleType args ret)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (FunctionHandleType args ret)
h of
FunctionHandleRepr CtxRepr ctx
_ TypeRepr ret
retType -> do
Atom s (FunctionHandleType args ret)
h_a <- Expr ext s (FunctionHandleType args ret)
-> Generator ext s t r m (Atom s (FunctionHandleType args ret))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (FunctionHandleType args ret)
h
Assignment (Atom s) args
args_a <- (forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t r m (Atom s x))
-> forall (x :: Ctx CrucibleType).
Assignment (Expr ext s) x
-> Generator ext s t r 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 Expr ext s x -> Generator ext s t r m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t r m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Assignment (Expr ext s) args
args
AtomValue ext s ret -> Generator ext s t r m (Atom s ret)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (AtomValue ext s ret -> Generator ext s t r m (Atom s ret))
-> AtomValue ext s ret -> Generator ext s t r m (Atom s ret)
forall a b. (a -> b) -> a -> b
$ Atom s (FunctionHandleType args ret)
-> Assignment (Atom s) args -> TypeRepr ret -> AtomValue ext s ret
forall s (args :: Ctx CrucibleType) (tp :: CrucibleType) ext.
Atom s (FunctionHandleType args tp)
-> Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp
Call Atom s (FunctionHandleType args ret)
h_a Assignment (Atom s) args
args_a TypeRepr ret
TypeRepr ret
retType
terminateEarly ::
(Monad m, IsSyntaxExtension ext) => TermStmt s ret -> Generator ext s t ret m a
terminateEarly :: forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly TermStmt s ret
term =
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) a.
StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a)
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall a b. (a -> b) -> a -> b
$ ((a -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a)
-> ((a
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
(GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall a b. (a -> b) -> a -> b
$ \a -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
_cont GeneratorState ext s t ret m
gs ->
EndState ext s t ret m -> m (EndState ext s t ret m)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TermStmt s ret
-> GeneratorState ext s t ret m -> EndState ext s t ret m
forall ext s (ret :: CrucibleType) (t :: Type -> Type)
(m :: Type -> Type).
IsSyntaxExtension ext =>
TermStmt s ret
-> GeneratorState ext s t ret m -> EndState ext s t ret m
terminateBlock TermStmt s ret
term GeneratorState ext s t ret m
gs)
jump :: (Monad m, IsSyntaxExtension ext) => Label s -> Generator ext s t ret m a
jump :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
l = TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Label s -> TermStmt s ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump Label s
l)
jumpToLambda ::
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp ->
Expr ext s tp ->
Generator ext s t ret m a
jumpToLambda :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
lbl Expr ext s tp
v = do
Atom s tp
v_a <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
v
TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (LambdaLabel s tp -> Atom s tp -> TermStmt s ret
forall s (tp :: CrucibleType) (ret :: CrucibleType).
LambdaLabel s tp -> Atom s tp -> TermStmt s ret
Output LambdaLabel s tp
lbl Atom s tp
v_a)
branch ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType ->
Label s ->
Label s ->
Generator ext s t ret m a
branch :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch (App (Not Expr ext s BoolType
e)) Label s
x_id Label s
y_id = do
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
y_id Label s
x_id
branch Expr ext s BoolType
e Label s
x_id Label s
y_id = do
Atom s BoolType
a <- Expr ext s BoolType -> Generator ext s t ret m (Atom s BoolType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s BoolType
e
TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (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
a Label s
x_id Label s
y_id)
returnFromFunction ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s ret -> Generator ext s t ret m a
returnFromFunction :: forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s ret -> Generator ext s t ret m a
returnFromFunction Expr ext s ret
e = do
Atom s ret
e_a <- Expr ext s ret -> Generator ext s t ret m (Atom s ret)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s ret
e
TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Atom s ret -> TermStmt s ret
forall s (ret :: CrucibleType). Atom s ret -> TermStmt s ret
Return Atom s ret
e_a)
reportError ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError Expr ext s (StringType Unicode)
e = do
Atom s (StringType Unicode)
e_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Atom s (StringType Unicode) -> TermStmt s ret
forall s (ret :: CrucibleType).
Atom s (StringType Unicode) -> TermStmt s ret
ErrorStmt Atom s (StringType Unicode)
e_a)
branchMaybe ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp) ->
LambdaLabel s tp ->
Label s ->
Generator ext s t ret m a
branchMaybe :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
v LambdaLabel s tp
l1 Label s
l2 =
case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
v of
MaybeRepr TypeRepr tp1
etp ->
do Atom s (MaybeType tp)
v_a <- Expr ext s (MaybeType tp)
-> Generator ext s t ret m (Atom s (MaybeType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (MaybeType tp)
v
TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (TypeRepr tp1
-> Atom s ('MaybeType tp1)
-> LambdaLabel s tp1
-> Label s
-> TermStmt s ret
forall (tp :: CrucibleType) s (ret :: CrucibleType).
TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
MaybeBranch TypeRepr tp1
etp Atom s (MaybeType tp)
Atom s ('MaybeType tp1)
v_a LambdaLabel s tp
LambdaLabel s tp1
l1 Label s
l2)
branchVariant ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (VariantType varctx) ->
Assignment (LambdaLabel s) varctx ->
Generator ext s t ret m a
branchVariant :: forall (m :: Type -> Type) ext s (varctx :: Ctx CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx -> Generator ext s t ret m a
branchVariant Expr ext s (VariantType varctx)
v Assignment (LambdaLabel s) varctx
lbls =
case Expr ext s (VariantType varctx) -> TypeRepr (VariantType varctx)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (VariantType varctx)
v of
VariantRepr CtxRepr ctx
typs ->
do Atom s (VariantType varctx)
v_a <- Expr ext s (VariantType varctx)
-> Generator ext s t ret m (Atom s (VariantType varctx))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (VariantType varctx)
v
TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (CtxRepr ctx
-> Atom s ('VariantType ctx)
-> Assignment (LambdaLabel s) ctx
-> TermStmt s ret
forall (varctx :: Ctx CrucibleType) s (ret :: CrucibleType).
CtxRepr varctx
-> Atom s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx
-> TermStmt s ret
VariantElim CtxRepr ctx
typs Atom s (VariantType varctx)
Atom s ('VariantType ctx)
v_a Assignment (LambdaLabel s) varctx
Assignment (LambdaLabel s) ctx
lbls)
tailCall ::
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret) ->
Assignment (Expr ext s) args ->
Generator ext s t ret m a
tailCall :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
(ret :: CrucibleType) (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args -> Generator ext s t ret m a
tailCall Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args =
case Expr ext s (FunctionHandleType args ret)
-> TypeRepr (FunctionHandleType args ret)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (FunctionHandleType args ret)
h of
FunctionHandleRepr CtxRepr ctx
argTypes TypeRepr ret
_retType ->
do Atom s (FunctionHandleType args ret)
h_a <- Expr ext s (FunctionHandleType args ret)
-> Generator ext s t ret m (Atom s (FunctionHandleType args ret))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (FunctionHandleType args ret)
h
Assignment (Atom s) args
args_a <- (forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x))
-> forall (x :: Ctx CrucibleType).
Assignment (Expr ext s) x
-> Generator ext s t ret 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 Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Assignment (Expr ext s) args
args
TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (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)
h_a CtxRepr args
CtxRepr ctx
argTypes Assignment (Atom s) args
args_a)
ifte :: (Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp)
=> Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp) =>
Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte Expr ext s BoolType
e Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y = do
LambdaLabel s tp
c_id <- Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, KnownRepr TypeRepr tp) =>
Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel
Label s
x_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
Label s
y_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
y Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
x_id Label s
y_id)
ifte' :: (Monad m, IsSyntaxExtension ext)
=> TypeRepr tp
-> Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte' :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
TypeRepr tp
-> Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte' TypeRepr tp
repr Expr ext s BoolType
e Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y = do
LambdaLabel s tp
c_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
repr
Label s
x_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
Label s
y_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
y Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
x_id Label s
y_id)
ifte_ :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s BoolType
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
ifte_ :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
ifte_ Expr ext s BoolType
e Generator ext s t ret m ()
x Generator ext s t ret m ()
y = do
Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Label s
x_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
x Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
Label s
y_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
y Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
x_id Label s
y_id)
ifteM :: (Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp)
=> Generator ext s t ret m (Expr ext s BoolType)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifteM :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp) =>
Generator ext s t ret m (Expr ext s BoolType)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifteM Generator ext s t ret m (Expr ext s BoolType)
em Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y = do { Expr ext s BoolType
m <- Generator ext s t ret m (Expr ext s BoolType)
em; Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext (tp :: CrucibleType) s
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp) =>
Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte Expr ext s BoolType
m Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y }
whenCond :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s BoolType
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
whenCond :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Generator ext s t ret m () -> Generator ext s t ret m ()
whenCond Expr ext s BoolType
e Generator ext s t ret m ()
x = do
Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Label s
t_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
x Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
t_id Label s
c_id)
unlessCond :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s BoolType
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
unlessCond :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Generator ext s t ret m () -> Generator ext s t ret m ()
unlessCond Expr ext s BoolType
e Generator ext s t ret m ()
x = do
Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Label s
f_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
x Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
c_id Label s
f_id)
data MatchMaybe j r
= MatchMaybe
{ forall j r. MatchMaybe j r -> j -> r
onJust :: j -> r
, forall j r. MatchMaybe j r -> r
onNothing :: r
}
caseMaybe :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s (MaybeType tp)
-> TypeRepr r
-> MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
-> Generator ext s t ret m (Expr ext s r)
caseMaybe :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(r :: CrucibleType) (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> TypeRepr r
-> MatchMaybe
(Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
-> Generator ext s t ret m (Expr ext s r)
caseMaybe Expr ext s (MaybeType tp)
v TypeRepr r
retType MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
cases = do
let etp :: TypeRepr tp
etp = case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
v of
MaybeRepr TypeRepr tp1
etp' -> TypeRepr tp
TypeRepr tp1
etp'
LambdaLabel s tp
j_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
Label s
n_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
LambdaLabel s r
c_id <- TypeRepr r -> Generator ext s t ret m (LambdaLabel s r)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr r
retType
LambdaLabel s tp
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
j_id ((forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
-> Expr ext s tp -> Generator ext s t ret m (Expr ext s r)
forall j r. MatchMaybe j r -> j -> r
onJust MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
cases (Expr ext s tp -> Generator ext s t ret m (Expr ext s r))
-> (Expr ext s r -> Generator ext s t ret m a)
-> Expr ext s tp
-> Generator ext s t ret m a
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> LambdaLabel s r -> Expr ext s r -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s r
c_id
Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
n_id ((forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
-> Generator ext s t ret m (Expr ext s r)
forall j r. MatchMaybe j r -> r
onNothing MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
cases Generator ext s t ret m (Expr ext s r)
-> (Expr ext s r -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s r -> Expr ext s r -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s r
c_id
LambdaLabel s r
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s r)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s r
c_id (Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
v LambdaLabel s tp
j_id Label s
n_id)
caseMaybe_ :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s (MaybeType tp)
-> MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
-> Generator ext s t ret m ()
caseMaybe_ :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
-> Generator ext s t ret m ()
caseMaybe_ Expr ext s (MaybeType tp)
v MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
cases = do
let etp :: TypeRepr tp
etp = case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
v of
MaybeRepr TypeRepr tp1
etp' -> TypeRepr tp
TypeRepr tp1
etp'
LambdaLabel s tp
j_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
Label s
n_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
LambdaLabel s tp
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
j_id ((forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ \Expr ext s tp
e -> MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
-> Expr ext s tp -> Generator ext s t ret m ()
forall j r. MatchMaybe j r -> j -> r
onJust MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
cases Expr ext s tp
e Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
n_id ((forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
-> Generator ext s t ret m ()
forall j r. MatchMaybe j r -> r
onNothing MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
cases Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
v LambdaLabel s tp
j_id Label s
n_id)
fromJustExpr :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Expr ext s tp)
fromJustExpr :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Expr ext s tp)
fromJustExpr Expr ext s (MaybeType tp)
e Expr ext s (StringType Unicode)
msg = do
let etp :: TypeRepr tp
etp = case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
e of
MaybeRepr TypeRepr tp1
etp' -> TypeRepr tp
TypeRepr tp1
etp'
LambdaLabel s tp
j_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
Label s
n_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
LambdaLabel s tp
c_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
LambdaLabel s tp
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
j_id ((forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
n_id ((forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ Expr ext s (StringType Unicode) -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError Expr ext s (StringType Unicode)
msg
LambdaLabel s tp
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
c_id (Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
e LambdaLabel s tp
j_id Label s
n_id)
assertedJustExpr :: (Monad m, IsSyntaxExtension ext)
=> Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Expr ext s tp)
assertedJustExpr :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Expr ext s tp)
assertedJustExpr Expr ext s (MaybeType tp)
e Expr ext s (StringType Unicode)
msg =
case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
e of
MaybeRepr TypeRepr tp1
tp ->
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation (Expr ext s tp -> Generator ext s t ret m (Expr ext s tp))
-> Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forall a b. (a -> b) -> a -> b
$! 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 (TypeRepr tp
-> Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> App ext (Expr ext s) tp
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp
-> f (MaybeType tp) -> f (StringType Unicode) -> App ext f tp
FromJustValue TypeRepr tp
TypeRepr tp1
tp Expr ext s (MaybeType tp)
e Expr ext s (StringType Unicode)
msg)
while :: (Monad m, IsSyntaxExtension ext)
=> (Position, Generator ext s t ret m (Expr ext s BoolType))
-> (Position, Generator ext s t ret m ())
-> Generator ext s t ret m ()
while :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(Position, Generator ext s t ret m (Expr ext s BoolType))
-> (Position, Generator ext s t ret m ())
-> Generator ext s t ret m ()
while (Position
pcond,Generator ext s t ret m (Expr ext s BoolType)
cond) (Position
pbody,Generator ext s t ret m ()
body) = do
Label s
cond_lbl <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Label s
loop_lbl <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Label s
exit_lbl <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
Position
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
Monad m =>
Position -> Generator ext s t ret m a -> Generator ext s t ret m a
withPosition Position
pcond (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$
Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
cond_lbl ((forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ do
Expr ext s BoolType
b <- Generator ext s t ret m (Expr ext s BoolType)
cond
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
b Label s
loop_lbl Label s
exit_lbl
Position
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
Monad m =>
Position -> Generator ext s t ret m a -> Generator ext s t ret m a
withPosition Position
pbody (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$
Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
loop_lbl ((forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ do
Generator ext s t ret m ()
body
Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
cond_lbl
Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
exit_lbl (Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
cond_lbl)
cfgFromGenerator :: FnHandle init ret
-> IxGeneratorState ext s t ret m i
-> CFG ext s init ret
cfgFromGenerator :: forall (init :: Ctx CrucibleType) (ret :: CrucibleType) ext s
(t :: Type -> Type) (m :: Type -> Type) i.
FnHandle init ret
-> IxGeneratorState ext s t ret m i -> CFG ext s init ret
cfgFromGenerator FnHandle init ret
h IxGeneratorState ext s t ret m i
s =
CFG { cfgHandle :: FnHandle init ret
cfgHandle = FnHandle init ret
h
, cfgEntryLabel :: Label s
cfgEntryLabel = IxGeneratorState ext s t ret m i
sIxGeneratorState ext s t ret m i
-> Getting (Label s) (IxGeneratorState ext s t ret m i) (Label s)
-> Label s
forall s a. s -> Getting a s a -> a
^.Getting (Label s) (IxGeneratorState ext s t ret m i) (Label s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(Label s -> f (Label s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsEntryLabel
, cfgBlocks :: [Block ext s ret]
cfgBlocks = Seq (Block ext s ret) -> [Block ext s ret]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Fold.toList (IxGeneratorState ext s t ret m i
sIxGeneratorState ext s t ret m i
-> Getting
(Seq (Block ext s ret))
(IxGeneratorState ext s t ret m i)
(Seq (Block ext s ret))
-> Seq (Block ext s ret)
forall s a. s -> Getting a s a -> a
^.Getting
(Seq (Block ext s ret))
(IxGeneratorState ext s t ret m i)
(Seq (Block ext s ret))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Seq (Block ext s ret) -> f (Seq (Block ext s ret)))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsBlocks)
}
type FunctionDef ext t init ret m =
forall s .
Assignment (Atom s) init ->
(t s, Generator ext s t ret m (Expr ext s ret))
defineFunction :: (Monad m, IsSyntaxExtension ext)
=> Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunction :: forall (m :: Type -> Type) ext (init :: Ctx CrucibleType)
(ret :: CrucibleType) (t :: Type -> Type).
(Monad m, IsSyntaxExtension ext) =>
Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunction Position
p Some (NonceGenerator m)
sng FnHandle init ret
h FunctionDef ext t init ret m
f = Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> (forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall (m :: Type -> Type) ext (init :: Ctx CrucibleType)
(ret :: CrucibleType) (t :: Type -> Type).
(Monad m, IsSyntaxExtension ext) =>
Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> (forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunctionOpt Position
p Some (NonceGenerator m)
sng FnHandle init ret
h Assignment (Atom s) init
-> (t s, Generator ext s t ret m (Expr ext s ret))
FunctionDef ext t init ret m
f (\NonceGenerator m s
_ CFG ext s init ret
cfg -> CFG ext s init ret -> m (CFG ext s init ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CFG ext s init ret
cfg)
defineFunctionOpt :: (Monad m, IsSyntaxExtension ext)
=> Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> (forall s. NonceGenerator m s
-> CFG ext s init ret
-> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunctionOpt :: forall (m :: Type -> Type) ext (init :: Ctx CrucibleType)
(ret :: CrucibleType) (t :: Type -> Type).
(Monad m, IsSyntaxExtension ext) =>
Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> (forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunctionOpt Position
p Some (NonceGenerator m)
sng FnHandle init ret
h FunctionDef ext t init ret m
f forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)
optPass = FnHandle init ret
-> m (SomeCFG ext init ret, [AnyCFG ext])
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall a b. a -> b -> b
seq FnHandle init ret
h (m (SomeCFG ext init ret, [AnyCFG ext])
-> m (SomeCFG ext init ret, [AnyCFG ext]))
-> m (SomeCFG ext init ret, [AnyCFG ext])
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall a b. (a -> b) -> a -> b
$ do
let argTypes :: CtxRepr init
argTypes = FnHandle init ret -> CtxRepr init
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes FnHandle init ret
h
Some NonceGenerator m x
ng <- Some (NonceGenerator m) -> m (Some (NonceGenerator m))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (NonceGenerator m)
sng
Assignment (Atom x) init
inputs <- NonceGenerator m x
-> Position -> CtxRepr init -> m (Assignment (Atom x) init)
forall (m :: Type -> Type) s (init :: Ctx CrucibleType).
Monad m =>
NonceGenerator m s
-> Position -> CtxRepr init -> m (Assignment (Atom s) init)
mkInputAtoms NonceGenerator m x
ng Position
p CtxRepr init
argTypes
let inputSet :: Set (Some (Value x))
inputSet = [Some (Value x)] -> Set (Some (Value x))
forall a. Ord a => [a] -> Set a
Set.fromList ((forall (x :: CrucibleType). Atom x x -> Some (Value x))
-> forall (x :: Ctx CrucibleType).
Assignment (Atom x) x -> [Some (Value x)]
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 x x -> Some (Value x)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Value x x -> Some (Value x))
-> (Atom x x -> Value x x) -> Atom x x -> Some (Value x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom x x -> Value x x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) Assignment (Atom x) init
inputs)
let (t x
init_state, Generator ext x t ret m (Expr ext x ret)
action) = Assignment (Atom x) init
-> (t x, Generator ext x t ret m (Expr ext x ret))
FunctionDef ext t init ret m
f (Assignment (Atom x) init
-> (t x, Generator ext x t ret m (Expr ext x ret)))
-> Assignment (Atom x) init
-> (t x, Generator ext x t ret m (Expr ext x ret))
forall a b. (a -> b) -> a -> b
$! Assignment (Atom x) init
inputs
Label x
lbl <- Nonce x UnitType -> Label x
forall s. Nonce s UnitType -> Label s
Label (Nonce x UnitType -> Label x)
-> m (Nonce x UnitType) -> m (Label x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NonceGenerator m x -> m (Nonce x UnitType)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m x
ng
let cbs :: CurrentBlockState ext x
cbs = Set (Some (Value x)) -> BlockID x -> CurrentBlockState ext x
forall s ext. ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState Set (Some (Value x))
inputSet (Label x -> BlockID x
forall s. Label s -> BlockID s
LabelID Label x
lbl)
let ts :: IxGeneratorState ext x t ret m (CurrentBlockState ext x)
ts = GS { _gsEntryLabel :: Label x
_gsEntryLabel = Label x
lbl
, _gsBlocks :: Seq (Block ext x ret)
_gsBlocks = Seq (Block ext x ret)
forall a. Seq a
Seq.empty
, _gsNonceGen :: NonceGenerator m x
_gsNonceGen = NonceGenerator m x
ng
, _gsCurrent :: CurrentBlockState ext x
_gsCurrent = CurrentBlockState ext x
cbs
, _gsPosition :: Position
_gsPosition = Position
p
, _gsState :: t x
_gsState = t x
init_state
, _seenFunctions :: [AnyCFG ext]
_seenFunctions = []
}
EndState ext x t ret m
ts' <- Generator ext x t ret m Void
-> IxGeneratorState ext x t ret m (CurrentBlockState ext x)
-> m (EndState ext x t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator (Generator ext x t ret m (Expr ext x ret)
action Generator ext x t ret m (Expr ext x ret)
-> (Expr ext x ret -> Generator ext x t ret m Void)
-> Generator ext x t ret m Void
forall a b.
Generator ext x t ret m a
-> (a -> Generator ext x t ret m b) -> Generator ext x t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr ext x ret -> Generator ext x t ret m Void
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
(t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s ret -> Generator ext s t ret m a
returnFromFunction) (IxGeneratorState ext x t ret m (CurrentBlockState ext x)
-> m (EndState ext x t ret m))
-> IxGeneratorState ext x t ret m (CurrentBlockState ext x)
-> m (EndState ext x t ret m)
forall a b. (a -> b) -> a -> b
$! IxGeneratorState ext x t ret m (CurrentBlockState ext x)
ts
CFG ext x init ret
g <- NonceGenerator m x -> CFG ext x init ret -> m (CFG ext x init ret)
forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)
optPass NonceGenerator m x
ng (FnHandle init ret -> EndState ext x t ret m -> CFG ext x init ret
forall (init :: Ctx CrucibleType) (ret :: CrucibleType) ext s
(t :: Type -> Type) (m :: Type -> Type) i.
FnHandle init ret
-> IxGeneratorState ext s t ret m i -> CFG ext s init ret
cfgFromGenerator FnHandle init ret
h EndState ext x t ret m
ts')
(SomeCFG ext init ret, [AnyCFG ext])
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (CFG ext x init ret -> SomeCFG ext init ret
forall ext (init :: Ctx CrucibleType) (ret :: CrucibleType) s.
CFG ext s init ret -> SomeCFG ext init ret
SomeCFG CFG ext x init ret
g, EndState ext x t ret m
ts'EndState ext x t ret m
-> Getting [AnyCFG ext] (EndState ext x t ret m) [AnyCFG ext]
-> [AnyCFG ext]
forall s a. s -> Getting a s a -> a
^.Getting [AnyCFG ext] (EndState ext x t ret m) [AnyCFG ext]
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
([AnyCFG ext] -> f [AnyCFG ext])
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
seenFunctions)