---------------------------------------------------------------------------
-- |
-- Module          : Lang.Crucible.CFG.ExtractSubgraph
-- Description     : Allows for construction of a function based off a subgraph
--                   of an SSA-form function, subject to certain constraints
-- Copyright       : (c) Galois, Inc 2015
-- License         : BSD3
--
---------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.CFG.ExtractSubgraph
  ( extractSubgraph
  ) where

import           Control.Lens
import qualified Data.Bimap as Bimap
import           Data.Parameterized.Context as Ctx
import           Data.Parameterized.Map as MapF
import           Data.Set as S
import qualified Data.Map as Map
import           Debug.Trace

import           What4.FunctionName
import           What4.ProgramLoc

import           Lang.Crucible.CFG.Core
import           Lang.Crucible.FunctionHandle

-- | Given a CFG @cfg@, a set of blocks @cuts@ that take the return type as their sole
-- argument, and a block @bi@ that takes the CFG's init type as its sole argument,
-- construct a CFG that is a maximal subgraph starting at @bi@ and not entering any
-- block in @cuts@.  If the original graph would enter a block in @cuts@, the value
-- passed to that block is returned.  If @bi `member` cuts@, then whenever the subgraph
-- would transition to @bi@, it returns the value that would be passed to @bi@ instead.
extractSubgraph :: (KnownCtx TypeRepr init, KnownRepr TypeRepr ret)
                => CFG ext blocks init ret
                -> Set (BlockID blocks (EmptyCtx ::> ret))
                -> BlockID blocks init
                -> HandleAllocator
                -> IO (Maybe (SomeCFG ext init ret))
extractSubgraph :: forall (init :: Ctx CrucibleType) (ret :: CrucibleType) ext
       (blocks :: Ctx (Ctx CrucibleType)).
(KnownCtx TypeRepr init, KnownRepr TypeRepr ret) =>
CFG ext blocks init ret
-> Set (BlockID blocks (EmptyCtx ::> ret))
-> BlockID blocks init
-> HandleAllocator
-> IO (Maybe (SomeCFG ext init ret))
extractSubgraph (CFG{cfgBlockMap :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap = BlockMap ext blocks ret
orig, cfgBreakpoints :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Bimap BreakpointName (Some (BlockID blocks))
cfgBreakpoints = Bimap BreakpointName (Some (BlockID blocks))
breakpoints}) Set (BlockID blocks (EmptyCtx ::> ret))
cuts BlockID blocks init
bi HandleAllocator
halloc =
  BlockMap ext blocks ret
-> Set (BlockID blocks (EmptyCtx ::> ret))
-> MapF (BlockID blocks) (BlockID 'EmptyCtx)
-> Size 'EmptyCtx
-> BlockID blocks init
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext blocks ret init 'EmptyCtx new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (soFar :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> MapF (BlockID old) (BlockID soFar)
-> Size soFar
-> BlockID old init
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret init soFar new -> r)
   -> r
extractSubgraphFirst BlockMap ext blocks ret
orig Set (BlockID blocks (EmptyCtx ::> ret))
cuts MapF (BlockID blocks) (BlockID 'EmptyCtx)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty Size 'EmptyCtx
forall {k}. Size 'EmptyCtx
zeroSize BlockID blocks init
bi ((forall (new :: Ctx (Ctx CrucibleType)).
  SubgraphIntermediate ext blocks ret init 'EmptyCtx new
  -> IO (Maybe (SomeCFG ext init ret)))
 -> IO (Maybe (SomeCFG ext init ret)))
-> (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext blocks ret init 'EmptyCtx new
    -> IO (Maybe (SomeCFG ext init ret)))
-> IO (Maybe (SomeCFG ext init ret))
forall a b. (a -> b) -> a -> b
$
    \(SubgraphIntermediate MapF (BlockID blocks) (BlockID new)
finalMap MapF (BlockID blocks) (BlockID new)
finalInitMap Size new
_sz BlockID new init
entryID forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID blocks) (BlockID all)
-> MapF (BlockID blocks) (BlockID all)
-> Assignment (Block ext all ret) 'EmptyCtx
-> Maybe (Assignment (Block ext all ret) new)
cb) -> do
        FnHandle init ret
hn <- HandleAllocator -> FunctionName -> IO (FnHandle init ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
(KnownCtx TypeRepr args, KnownRepr TypeRepr ret) =>
HandleAllocator -> FunctionName -> IO (FnHandle args ret)
mkHandle HandleAllocator
halloc FunctionName
startFunctionName
        Maybe (SomeCFG ext init ret) -> IO (Maybe (SomeCFG ext init ret))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (SomeCFG ext init ret) -> IO (Maybe (SomeCFG ext init ret)))
-> Maybe (SomeCFG ext init ret)
-> IO (Maybe (SomeCFG ext init ret))
forall a b. (a -> b) -> a -> b
$ do
          Assignment (Block ext new ret) new
bm <- MapF (BlockID blocks) (BlockID new)
-> MapF (BlockID blocks) (BlockID new)
-> Assignment (Block ext new ret) 'EmptyCtx
-> Maybe (Assignment (Block ext new ret) new)
forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID blocks) (BlockID all)
-> MapF (BlockID blocks) (BlockID all)
-> Assignment (Block ext all ret) 'EmptyCtx
-> Maybe (Assignment (Block ext all ret) new)
cb MapF (BlockID blocks) (BlockID new)
finalMap MapF (BlockID blocks) (BlockID new)
finalInitMap Assignment (Block ext new ret) 'EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty
          SomeCFG ext init ret -> Maybe (SomeCFG ext init ret)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SomeCFG ext init ret -> Maybe (SomeCFG ext init ret))
-> SomeCFG ext init ret -> Maybe (SomeCFG ext init ret)
forall a b. (a -> b) -> a -> b
$ CFG ext new init ret -> SomeCFG ext init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> SomeCFG ext init ret
SomeCFG (CFG ext new init ret -> SomeCFG ext init ret)
-> CFG ext new init ret -> SomeCFG ext init ret
forall a b. (a -> b) -> a -> b
$ CFG
            { cfgBlockMap :: Assignment (Block ext new ret) new
cfgBlockMap = Assignment (Block ext new ret) new
bm
            , cfgEntryBlockID :: BlockID new init
cfgEntryBlockID = BlockID new init
entryID
            , cfgHandle :: FnHandle init ret
cfgHandle = FnHandle init ret
hn
            , cfgBreakpoints :: Bimap BreakpointName (Some (BlockID new))
cfgBreakpoints = [(BreakpointName, Some (BlockID new))]
-> Bimap BreakpointName (Some (BlockID new))
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
Bimap.fromList ([(BreakpointName, Some (BlockID new))]
 -> Bimap BreakpointName (Some (BlockID new)))
-> [(BreakpointName, Some (BlockID new))]
-> Bimap BreakpointName (Some (BlockID new))
forall a b. (a -> b) -> a -> b
$ Map BreakpointName (Some (BlockID new))
-> [(BreakpointName, Some (BlockID new))]
forall k a. Map k a -> [(k, a)]
Map.toList (Map BreakpointName (Some (BlockID new))
 -> [(BreakpointName, Some (BlockID new))])
-> Map BreakpointName (Some (BlockID new))
-> [(BreakpointName, Some (BlockID new))]
forall a b. (a -> b) -> a -> b
$
                (Some (BlockID blocks) -> Maybe (Some (BlockID new)))
-> Map BreakpointName (Some (BlockID blocks))
-> Map BreakpointName (Some (BlockID new))
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe ((forall (tp :: Ctx CrucibleType).
 BlockID blocks tp -> Maybe (Some (BlockID new)))
-> Some (BlockID blocks) -> Maybe (Some (BlockID new))
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome ((forall (tp :: Ctx CrucibleType).
  BlockID blocks tp -> Maybe (Some (BlockID new)))
 -> Some (BlockID blocks) -> Maybe (Some (BlockID new)))
-> (forall (tp :: Ctx CrucibleType).
    BlockID blocks tp -> Maybe (Some (BlockID new)))
-> Some (BlockID blocks)
-> Maybe (Some (BlockID new))
forall a b. (a -> b) -> a -> b
$ \BlockID blocks tp
bid -> BlockID new tp -> Some (BlockID new)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (BlockID new tp -> Some (BlockID new))
-> Maybe (BlockID new tp) -> Maybe (Some (BlockID new))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> BlockID blocks tp
-> MapF (BlockID blocks) (BlockID new) -> Maybe (BlockID new tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BlockID blocks tp
bid MapF (BlockID blocks) (BlockID new)
finalMap) (Map BreakpointName (Some (BlockID blocks))
 -> Map BreakpointName (Some (BlockID new)))
-> Map BreakpointName (Some (BlockID blocks))
-> Map BreakpointName (Some (BlockID new))
forall a b. (a -> b) -> a -> b
$
                Bimap BreakpointName (Some (BlockID blocks))
-> Map BreakpointName (Some (BlockID blocks))
forall a b. Bimap a b -> Map a b
Bimap.toMap Bimap BreakpointName (Some (BlockID blocks))
breakpoints
            }

-- | Type for carrying intermediate results through subraph extraction
-- the interesting field is the final one - it holds a callback for transforming
-- the result of the previous portion of the subgraph extraction into the result
-- of this subgraph extraction.
data SubgraphIntermediate ext old ret init soFar new where
  SubgraphIntermediate :: MapF (BlockID old) (BlockID new)
                       -> MapF (BlockID old) (BlockID new)
                       -> Size new
                       -> BlockID new init
                       -> (forall all. (MapF (BlockID old) (BlockID all)
                                        -> MapF (BlockID old) (BlockID all)
                                        -> Assignment (Block ext all ret) soFar
                                        -> Maybe (Assignment (Block ext all ret) new)))
                       -> SubgraphIntermediate ext old ret init soFar new


-- | The inner loop of subgraph extraction
--   produces a callback with an existential type, in order to hide new
extractSubgraph' :: KnownRepr TypeRepr ret
                 => BlockMap ext old ret
                 -> Set (BlockID old (EmptyCtx ::> ret))
                 -> MapF (BlockID old) (BlockID soFar)
                 -> MapF (BlockID old) (BlockID soFar)
                 -> Size soFar
                 -> BlockID old init
                 -> BlockID soFar args
                 -> forall r . (forall new. SubgraphIntermediate ext old ret args soFar new -> r)
                 -> r
extractSubgraph' :: forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (soFar :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType)
       (args :: Ctx CrucibleType).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> MapF (BlockID old) (BlockID soFar)
-> MapF (BlockID old) (BlockID soFar)
-> Size soFar
-> BlockID old init
-> BlockID soFar args
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
extractSubgraph' BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts MapF (BlockID old) (BlockID soFar)
mapF MapF (BlockID old) (BlockID soFar)
initMap Size soFar
sz BlockID old init
bi BlockID soFar args
ident forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f =
  let block :: Block ext old ret init
block = BlockID old init -> BlockMap ext old ret -> Block ext old ret init
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock BlockID old init
bi BlockMap ext old ret
orig
  in  Block ext old ret init
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt old ret ctx -> r)
-> r
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) r.
Block ext blocks ret args
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt blocks ret ctx -> r)
-> r
withBlockTermStmt Block ext old ret init
block ((forall {ctx :: Ctx CrucibleType}.
  ProgramLoc -> TermStmt old ret ctx -> r)
 -> r)
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt old ret ctx -> r)
-> r
forall a b. (a -> b) -> a -> b
$ (\ProgramLoc
_ TermStmt old ret ctx
t ->
        (case TermStmt old ret ctx
t of
          Jump (JumpTarget BlockID old args
bi' CtxRepr args
_ Assignment (Reg ctx) args
_) -> \SubgraphIntermediate ext old ret args soFar (soFar ::> init)
sgi -> BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old args
-> SubgraphIntermediate ext old ret args soFar (soFar ::> init)
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (soFar :: Ctx (Ctx CrucibleType)) (prev :: Ctx (Ctx CrucibleType)).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old init
-> SubgraphIntermediate ext old ret args soFar prev
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
visitChildNode BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts BlockID old args
bi' SubgraphIntermediate ext old ret args soFar (soFar ::> init)
sgi SubgraphIntermediate ext old ret args soFar new -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f
          Br Reg ctx BoolType
_ (JumpTarget BlockID old args
bi1 CtxRepr args
_ Assignment (Reg ctx) args
_) (JumpTarget BlockID old args
bi2 CtxRepr args
_ Assignment (Reg ctx) args
_) -> \SubgraphIntermediate ext old ret args soFar (soFar ::> init)
sgi1 ->
            BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old args
-> SubgraphIntermediate ext old ret args soFar (soFar ::> init)
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (soFar :: Ctx (Ctx CrucibleType)) (prev :: Ctx (Ctx CrucibleType)).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old init
-> SubgraphIntermediate ext old ret args soFar prev
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
visitChildNode BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts BlockID old args
bi1 SubgraphIntermediate ext old ret args soFar (soFar ::> init)
sgi1
              ((forall (new :: Ctx (Ctx CrucibleType)).
  SubgraphIntermediate ext old ret args soFar new -> r)
 -> r)
-> (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \SubgraphIntermediate ext old ret args soFar new
sgi2 -> BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old args
-> SubgraphIntermediate ext old ret args soFar new
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (soFar :: Ctx (Ctx CrucibleType)) (prev :: Ctx (Ctx CrucibleType)).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old init
-> SubgraphIntermediate ext old ret args soFar prev
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
visitChildNode BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts BlockID old args
bi2 SubgraphIntermediate ext old ret args soFar new
sgi2 SubgraphIntermediate ext old ret args soFar new -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f
          Return Reg ctx ret
_ -> SubgraphIntermediate ext old ret args soFar (soFar ::> init) -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f
          TermStmt old ret ctx
_ -> [Char]
-> SubgraphIntermediate ext old ret args soFar (soFar ::> init)
-> r
forall a. HasCallStack => [Char] -> a
error [Char]
"extractSubgraph': unexpected case!")
                (MapF (BlockID old) (BlockID (soFar ::> init))
-> MapF (BlockID old) (BlockID (soFar ::> init))
-> Size (soFar ::> init)
-> BlockID (soFar ::> init) args
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) (soFar ::> init)))
-> SubgraphIntermediate ext old ret args soFar (soFar ::> init)
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) ext
       (ret :: CrucibleType) (soFar :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID new)
-> MapF (BlockID old) (BlockID new)
-> Size new
-> BlockID new init
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) new))
-> SubgraphIntermediate ext old ret init soFar new
SubgraphIntermediate
                  (BlockID old init
-> BlockID (soFar ::> init) init
-> MapF (BlockID old) (BlockID (soFar ::> init))
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert BlockID old init
bi (Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID (Index (soFar ::> init) init -> BlockID (soFar ::> init) init)
-> Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall a b. (a -> b) -> a -> b
$ Size soFar -> Index (soFar ::> init) init
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size soFar
sz) ((forall (tp :: Ctx CrucibleType).
 BlockID soFar tp -> BlockID (soFar ::> init) tp)
-> MapF (BlockID old) (BlockID soFar)
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map BlockID soFar tp -> BlockID (soFar ::> init) tp
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
forall (tp :: Ctx CrucibleType).
BlockID soFar tp -> BlockID (soFar ::> init) tp
extendBlockID MapF (BlockID old) (BlockID soFar)
mapF))
                  ((forall (tp :: Ctx CrucibleType).
 BlockID soFar tp -> BlockID (soFar ::> init) tp)
-> MapF (BlockID old) (BlockID soFar)
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map BlockID soFar tp -> BlockID (soFar ::> init) tp
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
forall (tp :: Ctx CrucibleType).
BlockID soFar tp -> BlockID (soFar ::> init) tp
extendBlockID MapF (BlockID old) (BlockID soFar)
initMap)
                  (Size soFar -> Size (soFar ::> init)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size soFar
sz)
                  (BlockID soFar args -> BlockID (soFar ::> init) args
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
extendBlockID BlockID soFar args
ident)
                  (\MapF (BlockID old) (BlockID all)
finalMap MapF (BlockID old) (BlockID all)
_finalInitMap Assignment (Block ext all ret) soFar
assn ->
                    (Block ext all ret init
 -> Assignment (Block ext all ret) (soFar ::> init))
-> Maybe (Block ext all ret init)
-> Maybe (Assignment (Block ext all ret) (soFar ::> init))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Assignment (Block ext all ret) soFar
-> Block ext all ret init
-> Assignment (Block ext all ret) (soFar ::> init)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend Assignment (Block ext all ret) soFar
assn) (do
                      BlockID all init
finalID <- BlockID old init
-> MapF (BlockID old) (BlockID all) -> Maybe (BlockID all init)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BlockID old init
bi MapF (BlockID old) (BlockID all)
finalMap
                      MapF (BlockID old) (BlockID all)
-> BlockID all init
-> Block ext old ret init
-> Maybe (Block ext all ret init)
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) ext
       (ret :: CrucibleType).
MapF (BlockID old) (BlockID new)
-> BlockID new ctx
-> Block ext old ret ctx
-> Maybe (Block ext new ret ctx)
cloneBlock MapF (BlockID old) (BlockID all)
finalMap BlockID all init
finalID Block ext old ret init
block))))

-- code duplication... but the types need to be different between iterations
-- FIXME: write a generic version that this and extractSubgraph' can be wrappers
-- around
extractSubgraphFirst :: KnownRepr TypeRepr ret
                     => BlockMap ext old ret
                     -> Set (BlockID old (EmptyCtx ::> ret))
                     -> MapF (BlockID old) (BlockID soFar)
                     -> Size soFar
                     -> BlockID old init
                     -> forall r . (forall new. SubgraphIntermediate ext old ret init soFar new -> r)
                     -> r
extractSubgraphFirst :: forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (soFar :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> MapF (BlockID old) (BlockID soFar)
-> Size soFar
-> BlockID old init
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret init soFar new -> r)
   -> r
extractSubgraphFirst BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts MapF (BlockID old) (BlockID soFar)
mapF Size soFar
sz BlockID old init
bi forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret init soFar new -> r
f =
  let block :: Block ext old ret init
block = BlockID old init -> BlockMap ext old ret -> Block ext old ret init
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock BlockID old init
bi BlockMap ext old ret
orig
  in  Block ext old ret init
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt old ret ctx -> r)
-> r
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) r.
Block ext blocks ret args
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt blocks ret ctx -> r)
-> r
withBlockTermStmt Block ext old ret init
block ((forall {ctx :: Ctx CrucibleType}.
  ProgramLoc -> TermStmt old ret ctx -> r)
 -> r)
-> (forall {ctx :: Ctx CrucibleType}.
    ProgramLoc -> TermStmt old ret ctx -> r)
-> r
forall a b. (a -> b) -> a -> b
$ (\ProgramLoc
_ TermStmt old ret ctx
t ->
        (case TermStmt old ret ctx
t of
          Jump (JumpTarget BlockID old args
bi' CtxRepr args
_ Assignment (Reg ctx) args
_) -> \SubgraphIntermediate ext old ret init soFar (soFar ::> init)
sgi -> BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old args
-> SubgraphIntermediate ext old ret init soFar (soFar ::> init)
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret init soFar new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (soFar :: Ctx (Ctx CrucibleType)) (prev :: Ctx (Ctx CrucibleType)).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old init
-> SubgraphIntermediate ext old ret args soFar prev
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
visitChildNode BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts BlockID old args
bi' SubgraphIntermediate ext old ret init soFar (soFar ::> init)
sgi SubgraphIntermediate ext old ret init soFar new -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret init soFar new -> r
f
          Br Reg ctx BoolType
_ (JumpTarget BlockID old args
bi1 CtxRepr args
_ Assignment (Reg ctx) args
_) (JumpTarget BlockID old args
bi2 CtxRepr args
_ Assignment (Reg ctx) args
_) -> \SubgraphIntermediate ext old ret init soFar (soFar ::> init)
sgi1 ->
            BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old args
-> SubgraphIntermediate ext old ret init soFar (soFar ::> init)
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret init soFar new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (soFar :: Ctx (Ctx CrucibleType)) (prev :: Ctx (Ctx CrucibleType)).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old init
-> SubgraphIntermediate ext old ret args soFar prev
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
visitChildNode BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts BlockID old args
bi1 SubgraphIntermediate ext old ret init soFar (soFar ::> init)
sgi1
              ((forall (new :: Ctx (Ctx CrucibleType)).
  SubgraphIntermediate ext old ret init soFar new -> r)
 -> r)
-> (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret init soFar new -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \SubgraphIntermediate ext old ret init soFar new
sgi2 -> BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old args
-> SubgraphIntermediate ext old ret init soFar new
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret init soFar new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (soFar :: Ctx (Ctx CrucibleType)) (prev :: Ctx (Ctx CrucibleType)).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old init
-> SubgraphIntermediate ext old ret args soFar prev
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
visitChildNode BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts BlockID old args
bi2 SubgraphIntermediate ext old ret init soFar new
sgi2 SubgraphIntermediate ext old ret init soFar new -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret init soFar new -> r
f
          Return Reg ctx ret
_ -> SubgraphIntermediate ext old ret init soFar (soFar ::> init) -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret init soFar new -> r
f
          TermStmt old ret ctx
_ -> [Char]
-> SubgraphIntermediate ext old ret init soFar (soFar ::> init)
-> r
forall a. HasCallStack => [Char] -> a
error [Char]
"extractSubgraphFirst: unexpected case!")
                (MapF (BlockID old) (BlockID (soFar ::> init))
-> MapF (BlockID old) (BlockID (soFar ::> init))
-> Size (soFar ::> init)
-> BlockID (soFar ::> init) init
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) (soFar ::> init)))
-> SubgraphIntermediate ext old ret init soFar (soFar ::> init)
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) ext
       (ret :: CrucibleType) (soFar :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID new)
-> MapF (BlockID old) (BlockID new)
-> Size new
-> BlockID new init
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) new))
-> SubgraphIntermediate ext old ret init soFar new
SubgraphIntermediate
                  (if case Set (BlockID old (EmptyCtx ::> ret))
-> Maybe
     (BlockID old (EmptyCtx ::> ret),
      Set (BlockID old (EmptyCtx ::> ret)))
forall a. Set a -> Maybe (a, Set a)
S.minView Set (BlockID old (EmptyCtx ::> ret))
cuts of
                      Just (BlockID old (EmptyCtx ::> ret)
bi', Set (BlockID old (EmptyCtx ::> ret))
_) -> case Assignment TypeRepr init
-> Assignment TypeRepr (EmptyCtx ::> ret)
-> Maybe (init :~: (EmptyCtx ::> ret))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
testEquality (Block ext old ret init -> Assignment TypeRepr init
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext old ret init
block) (Block ext old ret (EmptyCtx ::> ret)
-> Assignment TypeRepr (EmptyCtx ::> ret)
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs (Block ext old ret (EmptyCtx ::> ret)
 -> Assignment TypeRepr (EmptyCtx ::> ret))
-> Block ext old ret (EmptyCtx ::> ret)
-> Assignment TypeRepr (EmptyCtx ::> ret)
forall a b. (a -> b) -> a -> b
$ BlockMap ext old ret
orig BlockMap ext old ret
-> Index old (EmptyCtx ::> ret)
-> Block ext old ret (EmptyCtx ::> ret)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! BlockID old (EmptyCtx ::> ret) -> Index old (EmptyCtx ::> ret)
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID old (EmptyCtx ::> ret)
bi') of
                        Just init :~: (EmptyCtx ::> ret)
Refl -> BlockID old init
bi BlockID old init -> Set (BlockID old init) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (BlockID old init)
Set (BlockID old (EmptyCtx ::> ret))
cuts
                        Maybe (init :~: (EmptyCtx ::> ret))
Nothing -> Bool
False
                      Maybe
  (BlockID old (EmptyCtx ::> ret),
   Set (BlockID old (EmptyCtx ::> ret)))
Nothing -> Bool
False
                    then (forall (tp :: Ctx CrucibleType).
 BlockID soFar tp -> BlockID (soFar ::> init) tp)
-> MapF (BlockID old) (BlockID soFar)
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map BlockID soFar tp -> BlockID (soFar ::> init) tp
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
forall (tp :: Ctx CrucibleType).
BlockID soFar tp -> BlockID (soFar ::> init) tp
extendBlockID MapF (BlockID old) (BlockID soFar)
mapF
                    else BlockID old init
-> BlockID (soFar ::> init) init
-> MapF (BlockID old) (BlockID (soFar ::> init))
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert BlockID old init
bi (Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID (Index (soFar ::> init) init -> BlockID (soFar ::> init) init)
-> Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall a b. (a -> b) -> a -> b
$ Size soFar -> Index (soFar ::> init) init
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size soFar
sz) ((forall (tp :: Ctx CrucibleType).
 BlockID soFar tp -> BlockID (soFar ::> init) tp)
-> MapF (BlockID old) (BlockID soFar)
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map BlockID soFar tp -> BlockID (soFar ::> init) tp
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
forall (tp :: Ctx CrucibleType).
BlockID soFar tp -> BlockID (soFar ::> init) tp
extendBlockID MapF (BlockID old) (BlockID soFar)
mapF))
                  (BlockID old init
-> BlockID (soFar ::> init) init
-> MapF (BlockID old) (BlockID (soFar ::> init))
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert BlockID old init
bi (Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID (Index (soFar ::> init) init -> BlockID (soFar ::> init) init)
-> Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall a b. (a -> b) -> a -> b
$ Size soFar -> Index (soFar ::> init) init
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size soFar
sz) ((forall (tp :: Ctx CrucibleType).
 BlockID soFar tp -> BlockID (soFar ::> init) tp)
-> MapF (BlockID old) (BlockID soFar)
-> MapF (BlockID old) (BlockID (soFar ::> init))
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map BlockID soFar tp -> BlockID (soFar ::> init) tp
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
forall (tp :: Ctx CrucibleType).
BlockID soFar tp -> BlockID (soFar ::> init) tp
extendBlockID MapF (BlockID old) (BlockID soFar)
mapF))
                  (Size soFar -> Size (soFar ::> init)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size soFar
sz)
                  (Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID (Index (soFar ::> init) init -> BlockID (soFar ::> init) init)
-> Index (soFar ::> init) init -> BlockID (soFar ::> init) init
forall a b. (a -> b) -> a -> b
$ Size soFar -> Index (soFar ::> init) init
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size soFar
sz)
                  (\MapF (BlockID old) (BlockID all)
finalMap MapF (BlockID old) (BlockID all)
finalInitMap Assignment (Block ext all ret) soFar
assn -> (Block ext all ret init
 -> Assignment (Block ext all ret) (soFar ::> init))
-> Maybe (Block ext all ret init)
-> Maybe (Assignment (Block ext all ret) (soFar ::> init))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Assignment (Block ext all ret) soFar
-> Block ext all ret init
-> Assignment (Block ext all ret) (soFar ::> init)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend Assignment (Block ext all ret) soFar
assn) (do
                      BlockID all init
finalID <- BlockID old init
-> MapF (BlockID old) (BlockID all) -> Maybe (BlockID all init)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BlockID old init
bi MapF (BlockID old) (BlockID all)
finalInitMap
                      MapF (BlockID old) (BlockID all)
-> BlockID all init
-> Block ext old ret init
-> Maybe (Block ext all ret init)
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) ext
       (ret :: CrucibleType).
MapF (BlockID old) (BlockID new)
-> BlockID new ctx
-> Block ext old ret ctx
-> Maybe (Block ext new ret ctx)
cloneBlock MapF (BlockID old) (BlockID all)
finalMap BlockID all init
finalID Block ext old ret init
block))))

-- does the building of a new node - mutually recursive with exrtactSubgraph'
visitChildNode :: KnownRepr TypeRepr ret
               => BlockMap ext old ret
               -> Set (BlockID old (EmptyCtx ::> ret))
               -> BlockID old init
               -> SubgraphIntermediate ext old ret args soFar prev
               -> (forall r. (forall new . SubgraphIntermediate ext old ret args soFar new -> r)
               -> r)
visitChildNode :: forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (soFar :: Ctx (Ctx CrucibleType)) (prev :: Ctx (Ctx CrucibleType)).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> BlockID old init
-> SubgraphIntermediate ext old ret args soFar prev
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
visitChildNode BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts BlockID old init
bi (SubgraphIntermediate MapF (BlockID old) (BlockID prev)
sgMap MapF (BlockID old) (BlockID prev)
initMap Size prev
sz BlockID prev args
ident forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) soFar
-> Maybe (Assignment (Block ext all ret) prev)
cb) forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f=
  case BlockID old init
-> MapF (BlockID old) (BlockID prev) -> Maybe (BlockID prev init)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BlockID old init
bi MapF (BlockID old) (BlockID prev)
sgMap of
    Just BlockID prev init
_bi' -> SubgraphIntermediate ext old ret args soFar prev -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f (SubgraphIntermediate ext old ret args soFar prev -> r)
-> SubgraphIntermediate ext old ret args soFar prev -> r
forall a b. (a -> b) -> a -> b
$ MapF (BlockID old) (BlockID prev)
-> MapF (BlockID old) (BlockID prev)
-> Size prev
-> BlockID prev args
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) prev))
-> SubgraphIntermediate ext old ret args soFar prev
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) ext
       (ret :: CrucibleType) (soFar :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID new)
-> MapF (BlockID old) (BlockID new)
-> Size new
-> BlockID new init
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) new))
-> SubgraphIntermediate ext old ret init soFar new
SubgraphIntermediate MapF (BlockID old) (BlockID prev)
sgMap MapF (BlockID old) (BlockID prev)
initMap Size prev
sz BlockID prev args
ident MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) soFar
-> Maybe (Assignment (Block ext all ret) prev)
forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) soFar
-> Maybe (Assignment (Block ext all ret) prev)
cb
    Maybe (BlockID prev init)
Nothing -> case Set (BlockID old (EmptyCtx ::> ret))
-> Maybe
     (BlockID old (EmptyCtx ::> ret),
      Set (BlockID old (EmptyCtx ::> ret)))
forall a. Set a -> Maybe (a, Set a)
S.minView Set (BlockID old (EmptyCtx ::> ret))
cuts of
      Just (BlockID old (EmptyCtx ::> ret)
cut, Set (BlockID old (EmptyCtx ::> ret))
_)
        | Just init :~: (EmptyCtx ::> ret)
Refl <- Assignment TypeRepr init
-> Assignment TypeRepr (EmptyCtx ::> ret)
-> Maybe (init :~: (EmptyCtx ::> ret))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
testEquality (Block ext old ret init -> Assignment TypeRepr init
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs (Block ext old ret init -> Assignment TypeRepr init)
-> Block ext old ret init -> Assignment TypeRepr init
forall a b. (a -> b) -> a -> b
$ BlockMap ext old ret
orig BlockMap ext old ret -> Index old init -> Block ext old ret init
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! BlockID old init -> Index old init
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID old init
bi) (Block ext old ret (EmptyCtx ::> ret)
-> Assignment TypeRepr (EmptyCtx ::> ret)
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs (Block ext old ret (EmptyCtx ::> ret)
 -> Assignment TypeRepr (EmptyCtx ::> ret))
-> Block ext old ret (EmptyCtx ::> ret)
-> Assignment TypeRepr (EmptyCtx ::> ret)
forall a b. (a -> b) -> a -> b
$ BlockMap ext old ret
orig BlockMap ext old ret
-> Index old (EmptyCtx ::> ret)
-> Block ext old ret (EmptyCtx ::> ret)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! BlockID old (EmptyCtx ::> ret) -> Index old (EmptyCtx ::> ret)
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID old (EmptyCtx ::> ret)
cut)
        , BlockID old init -> Set (BlockID old init) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member BlockID old init
bi Set (BlockID old init)
Set (BlockID old (EmptyCtx ::> ret))
cuts ->
            SubgraphIntermediate ext old ret args soFar (prev ::> init) -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f (SubgraphIntermediate ext old ret args soFar (prev ::> init) -> r)
-> SubgraphIntermediate ext old ret args soFar (prev ::> init) -> r
forall a b. (a -> b) -> a -> b
$ MapF (BlockID old) (BlockID (prev ::> init))
-> MapF (BlockID old) (BlockID (prev ::> init))
-> Size (prev ::> init)
-> BlockID (prev ::> init) args
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) (prev ::> init)))
-> SubgraphIntermediate ext old ret args soFar (prev ::> init)
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) ext
       (ret :: CrucibleType) (soFar :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID new)
-> MapF (BlockID old) (BlockID new)
-> Size new
-> BlockID new init
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) new))
-> SubgraphIntermediate ext old ret init soFar new
SubgraphIntermediate
              (BlockID old init
-> BlockID (prev ::> init) init
-> MapF (BlockID old) (BlockID (prev ::> init))
-> MapF (BlockID old) (BlockID (prev ::> init))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert BlockID old init
bi (Index (prev ::> init) init -> BlockID (prev ::> init) init
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID (Index (prev ::> init) init -> BlockID (prev ::> init) init)
-> Index (prev ::> init) init -> BlockID (prev ::> init) init
forall a b. (a -> b) -> a -> b
$ Size prev -> Index (prev ::> init) init
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size prev
sz) ((forall (tp :: Ctx CrucibleType).
 BlockID prev tp -> BlockID (prev ::> init) tp)
-> MapF (BlockID old) (BlockID prev)
-> MapF (BlockID old) (BlockID (prev ::> init))
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map BlockID prev tp -> BlockID (prev ::> init) tp
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
forall (tp :: Ctx CrucibleType).
BlockID prev tp -> BlockID (prev ::> init) tp
extendBlockID MapF (BlockID old) (BlockID prev)
sgMap))
              ((forall (tp :: Ctx CrucibleType).
 BlockID prev tp -> BlockID (prev ::> init) tp)
-> MapF (BlockID old) (BlockID prev)
-> MapF (BlockID old) (BlockID (prev ::> init))
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> g tp) -> MapF ktp f -> MapF ktp g
MapF.map BlockID prev tp -> BlockID (prev ::> init) tp
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
forall (tp :: Ctx CrucibleType).
BlockID prev tp -> BlockID (prev ::> init) tp
extendBlockID MapF (BlockID old) (BlockID prev)
initMap)
              (Size prev -> Size (prev ::> init)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size prev
sz)
              (BlockID prev args -> BlockID (prev ::> init) args
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
extendBlockID BlockID prev args
ident)
              (\MapF (BlockID old) (BlockID all)
finalMap MapF (BlockID old) (BlockID all)
finalCutMap Assignment (Block ext all ret) soFar
assn -> do
                Assignment (Block ext all ret) prev
assn' <- MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) soFar
-> Maybe (Assignment (Block ext all ret) prev)
forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) soFar
-> Maybe (Assignment (Block ext all ret) prev)
cb MapF (BlockID old) (BlockID all)
finalMap MapF (BlockID old) (BlockID all)
finalCutMap Assignment (Block ext all ret) soFar
assn
                Block ext all ret (EmptyCtx ::> ret)
newBlock <- MapF (BlockID old) (BlockID all)
-> BlockMap ext old ret
-> BlockID old (EmptyCtx ::> ret)
-> Maybe (Block ext all ret (EmptyCtx ::> ret))
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) ext (ret :: CrucibleType).
MapF (BlockID old) (BlockID new)
-> BlockMap ext old ret
-> BlockID old (EmptyCtx ::> ret)
-> Maybe (Block ext new ret (EmptyCtx ::> ret))
mkRetBlock MapF (BlockID old) (BlockID all)
finalMap BlockMap ext old ret
orig BlockID old init
BlockID old (EmptyCtx ::> ret)
bi
                Assignment (Block ext all ret) (prev ::> init)
-> Maybe (Assignment (Block ext all ret) (prev ::> init))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Assignment (Block ext all ret) (prev ::> init)
 -> Maybe (Assignment (Block ext all ret) (prev ::> init)))
-> Assignment (Block ext all ret) (prev ::> init)
-> Maybe (Assignment (Block ext all ret) (prev ::> init))
forall a b. (a -> b) -> a -> b
$ Assignment (Block ext all ret) prev
-> Block ext all ret init
-> Assignment (Block ext all ret) (prev ::> init)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend Assignment (Block ext all ret) prev
assn' Block ext all ret init
Block ext all ret (EmptyCtx ::> ret)
newBlock)
      Maybe
  (BlockID old (EmptyCtx ::> ret),
   Set (BlockID old (EmptyCtx ::> ret)))
_ -> BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> MapF (BlockID old) (BlockID prev)
-> MapF (BlockID old) (BlockID prev)
-> Size prev
-> BlockID old init
-> BlockID prev args
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args prev new -> r)
   -> r
forall (ret :: CrucibleType) ext (old :: Ctx (Ctx CrucibleType))
       (soFar :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType)
       (args :: Ctx CrucibleType).
KnownRepr TypeRepr ret =>
BlockMap ext old ret
-> Set (BlockID old (EmptyCtx ::> ret))
-> MapF (BlockID old) (BlockID soFar)
-> MapF (BlockID old) (BlockID soFar)
-> Size soFar
-> BlockID old init
-> BlockID soFar args
-> forall r.
   (forall (new :: Ctx (Ctx CrucibleType)).
    SubgraphIntermediate ext old ret args soFar new -> r)
   -> r
extractSubgraph' BlockMap ext old ret
orig Set (BlockID old (EmptyCtx ::> ret))
cuts MapF (BlockID old) (BlockID prev)
sgMap MapF (BlockID old) (BlockID prev)
initMap Size prev
sz BlockID old init
bi BlockID prev args
ident
            (\ (SubgraphIntermediate MapF (BlockID old) (BlockID new)
sgMap' MapF (BlockID old) (BlockID new)
initMap' Size new
sz' BlockID new args
ident' forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) prev
-> Maybe (Assignment (Block ext all ret) new)
ccb) ->
              SubgraphIntermediate ext old ret args soFar new -> r
forall (new :: Ctx (Ctx CrucibleType)).
SubgraphIntermediate ext old ret args soFar new -> r
f (SubgraphIntermediate ext old ret args soFar new -> r)
-> SubgraphIntermediate ext old ret args soFar new -> r
forall a b. (a -> b) -> a -> b
$ MapF (BlockID old) (BlockID new)
-> MapF (BlockID old) (BlockID new)
-> Size new
-> BlockID new args
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) new))
-> SubgraphIntermediate ext old ret args soFar new
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) ext
       (ret :: CrucibleType) (soFar :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID new)
-> MapF (BlockID old) (BlockID new)
-> Size new
-> BlockID new init
-> (forall (all :: Ctx (Ctx CrucibleType)).
    MapF (BlockID old) (BlockID all)
    -> MapF (BlockID old) (BlockID all)
    -> Assignment (Block ext all ret) soFar
    -> Maybe (Assignment (Block ext all ret) new))
-> SubgraphIntermediate ext old ret init soFar new
SubgraphIntermediate MapF (BlockID old) (BlockID new)
sgMap' MapF (BlockID old) (BlockID new)
initMap' Size new
sz' BlockID new args
ident'
                (\MapF (BlockID old) (BlockID all)
finalMap MapF (BlockID old) (BlockID all)
finalCutMap Assignment (Block ext all ret) soFar
assn ->
                  MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) prev
-> Maybe (Assignment (Block ext all ret) new)
forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) prev
-> Maybe (Assignment (Block ext all ret) new)
ccb MapF (BlockID old) (BlockID all)
finalMap MapF (BlockID old) (BlockID all)
finalCutMap  (Assignment (Block ext all ret) prev
 -> Maybe (Assignment (Block ext all ret) new))
-> Maybe (Assignment (Block ext all ret) prev)
-> Maybe (Assignment (Block ext all ret) new)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) soFar
-> Maybe (Assignment (Block ext all ret) prev)
forall (all :: Ctx (Ctx CrucibleType)).
MapF (BlockID old) (BlockID all)
-> MapF (BlockID old) (BlockID all)
-> Assignment (Block ext all ret) soFar
-> Maybe (Assignment (Block ext all ret) prev)
cb MapF (BlockID old) (BlockID all)
finalMap MapF (BlockID old) (BlockID all)
finalCutMap Assignment (Block ext all ret) soFar
assn))


mkRetBlock :: MapF (BlockID old) (BlockID new)
           -> BlockMap ext old ret
           -> BlockID old (EmptyCtx ::> ret)
           -> Maybe (Block ext new ret (EmptyCtx ::> ret))
mkRetBlock :: forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) ext (ret :: CrucibleType).
MapF (BlockID old) (BlockID new)
-> BlockMap ext old ret
-> BlockID old (EmptyCtx ::> ret)
-> Maybe (Block ext new ret (EmptyCtx ::> ret))
mkRetBlock MapF (BlockID old) (BlockID new)
mapF BlockMap ext old ret
bm BlockID old (EmptyCtx ::> ret)
ident =
  case BlockID old (EmptyCtx ::> ret)
-> MapF (BlockID old) (BlockID new)
-> Maybe (BlockID new (EmptyCtx ::> ret))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BlockID old (EmptyCtx ::> ret)
ident MapF (BlockID old) (BlockID new)
mapF of
    Just BlockID new (EmptyCtx ::> ret)
id' ->
      let block :: Block ext old ret (EmptyCtx ::> ret)
block = BlockMap ext old ret
bm BlockMap ext old ret
-> Index old (EmptyCtx ::> ret)
-> Block ext old ret (EmptyCtx ::> ret)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! BlockID old (EmptyCtx ::> ret) -> Index old (EmptyCtx ::> ret)
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID old (EmptyCtx ::> ret)
ident
      in Block ext new ret (EmptyCtx ::> ret)
-> Maybe (Block ext new ret (EmptyCtx ::> ret))
forall a. a -> Maybe a
Just (Block ext new ret (EmptyCtx ::> ret)
 -> Maybe (Block ext new ret (EmptyCtx ::> ret)))
-> Block ext new ret (EmptyCtx ::> ret)
-> Maybe (Block ext new ret (EmptyCtx ::> ret))
forall a b. (a -> b) -> a -> b
$
           let name :: FunctionName
name = ProgramLoc -> FunctionName
plFunction (Block ext old ret (EmptyCtx ::> ret) -> ProgramLoc
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> ProgramLoc
blockLoc Block ext old ret (EmptyCtx ::> ret)
block)
               term :: TermStmt blocks ret (EmptyCtx ::> ret)
term = Reg (EmptyCtx ::> ret) ret
-> TermStmt blocks ret (EmptyCtx ::> ret)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx ret -> TermStmt blocks ret ctx
Return Reg (EmptyCtx ::> ret) ret
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
KnownContext ctx =>
Reg (ctx ::> tp) tp
lastReg
              in Block{ blockID :: BlockID new (EmptyCtx ::> ret)
blockID       = BlockID new (EmptyCtx ::> ret)
id'
                      , blockInputs :: CtxRepr (EmptyCtx ::> ret)
blockInputs   = Block ext old ret (EmptyCtx ::> ret) -> CtxRepr (EmptyCtx ::> ret)
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext old ret (EmptyCtx ::> ret)
block
                      , _blockStmts :: StmtSeq ext new ret (EmptyCtx ::> ret)
_blockStmts   = ProgramLoc
-> TermStmt new ret (EmptyCtx ::> ret)
-> StmtSeq ext new ret (EmptyCtx ::> ret)
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ext.
ProgramLoc -> TermStmt blocks ret ctx -> StmtSeq ext blocks ret ctx
TermStmt (FunctionName -> Position -> ProgramLoc
mkProgramLoc FunctionName
name Position
InternalPos) TermStmt new ret (EmptyCtx ::> ret)
forall {blocks :: Ctx (Ctx CrucibleType)} {ret :: CrucibleType}.
TermStmt blocks ret (EmptyCtx ::> ret)
term
                      }
    Maybe (BlockID new (EmptyCtx ::> ret))
Nothing -> [Char]
-> Maybe (Block ext new ret (EmptyCtx ::> ret))
-> Maybe (Block ext new ret (EmptyCtx ::> ret))
forall a. [Char] -> a -> a
trace ([Char]
"could not lookup return block id " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Index old (EmptyCtx ::> ret) -> [Char]
forall a. Show a => a -> [Char]
show (BlockID old (EmptyCtx ::> ret) -> Index old (EmptyCtx ::> ret)
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID old (EmptyCtx ::> ret)
ident)) Maybe (Block ext new ret (EmptyCtx ::> ret))
forall a. Maybe a
Nothing


cloneBlock :: MapF (BlockID old) (BlockID new)
           -> BlockID new ctx -> Block ext old ret ctx -> Maybe (Block ext new ret ctx)
cloneBlock :: forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) ext
       (ret :: CrucibleType).
MapF (BlockID old) (BlockID new)
-> BlockID new ctx
-> Block ext old ret ctx
-> Maybe (Block ext new ret ctx)
cloneBlock MapF (BlockID old) (BlockID new)
mapF BlockID new ctx
newID Block ext old ret ctx
b = do
  StmtSeq ext new ret ctx
stmts' <- MapF (BlockID old) (BlockID new)
-> StmtSeq ext old ret ctx -> Maybe (StmtSeq ext new ret ctx)
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) ext (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
MapF (BlockID old) (BlockID new)
-> StmtSeq ext old ret ctx -> Maybe (StmtSeq ext new ret ctx)
cloneStmtSeq MapF (BlockID old) (BlockID new)
mapF (Block ext old ret ctx
bBlock ext old ret ctx
-> Getting
     (StmtSeq ext old ret ctx)
     (Block ext old ret ctx)
     (StmtSeq ext old ret ctx)
-> StmtSeq ext old ret ctx
forall s a. s -> Getting a s a -> a
^.Getting
  (StmtSeq ext old ret ctx)
  (Block ext old ret ctx)
  (StmtSeq ext old ret ctx)
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (c :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(StmtSeq ext b r c -> f (StmtSeq ext b r c))
-> Block ext b r c -> f (Block ext b r c)
blockStmts)
  Block ext new ret ctx -> Maybe (Block ext new ret ctx)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Block{ blockID :: BlockID new ctx
blockID       = BlockID new ctx
newID
              , blockInputs :: CtxRepr ctx
blockInputs   = Block ext old ret ctx -> CtxRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext old ret ctx
b
              , _blockStmts :: StmtSeq ext new ret ctx
_blockStmts   = StmtSeq ext new ret ctx
stmts'
              }

cloneStmtSeq :: MapF (BlockID old) (BlockID new) -> StmtSeq ext old ret ctx -> Maybe (StmtSeq ext new ret ctx)
cloneStmtSeq :: forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) ext (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
MapF (BlockID old) (BlockID new)
-> StmtSeq ext old ret ctx -> Maybe (StmtSeq ext new ret ctx)
cloneStmtSeq MapF (BlockID old) (BlockID new)
mapF (ConsStmt ProgramLoc
loc Stmt ext ctx ctx'
stmt StmtSeq ext old ret ctx'
rest) = do
  StmtSeq ext new ret ctx'
rest' <- MapF (BlockID old) (BlockID new)
-> StmtSeq ext old ret ctx' -> Maybe (StmtSeq ext new ret ctx')
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) ext (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
MapF (BlockID old) (BlockID new)
-> StmtSeq ext old ret ctx -> Maybe (StmtSeq ext new ret ctx)
cloneStmtSeq MapF (BlockID old) (BlockID new)
mapF StmtSeq ext old ret ctx'
rest
  StmtSeq ext new ret ctx -> Maybe (StmtSeq ext new ret ctx)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (StmtSeq ext new ret ctx -> Maybe (StmtSeq ext new ret ctx))
-> StmtSeq ext new ret ctx -> Maybe (StmtSeq ext new ret ctx)
forall a b. (a -> b) -> a -> b
$ ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext new ret ctx'
-> StmtSeq ext new ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
ConsStmt ProgramLoc
loc Stmt ext ctx ctx'
stmt StmtSeq ext new ret ctx'
rest'
cloneStmtSeq MapF (BlockID old) (BlockID new)
mapF (TermStmt ProgramLoc
loc TermStmt old ret ctx
term) = do
  TermStmt new ret ctx
term' <- MapF (BlockID old) (BlockID new)
-> TermStmt old ret ctx -> Maybe (TermStmt new ret ctx)
forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
MapF (BlockID old) (BlockID new)
-> TermStmt old ret ctx -> Maybe (TermStmt new ret ctx)
cloneTerm MapF (BlockID old) (BlockID new)
mapF TermStmt old ret ctx
term
  StmtSeq ext new ret ctx -> Maybe (StmtSeq ext new ret ctx)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (StmtSeq ext new ret ctx -> Maybe (StmtSeq ext new ret ctx))
-> StmtSeq ext new ret ctx -> Maybe (StmtSeq ext new ret ctx)
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> TermStmt new ret ctx -> StmtSeq ext new ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ext.
ProgramLoc -> TermStmt blocks ret ctx -> StmtSeq ext blocks ret ctx
TermStmt ProgramLoc
loc TermStmt new ret ctx
term'

cloneTerm :: MapF (BlockID old) (BlockID new) -> TermStmt old ret ctx -> Maybe (TermStmt new ret ctx)
cloneTerm :: forall (old :: Ctx (Ctx CrucibleType))
       (new :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
MapF (BlockID old) (BlockID new)
-> TermStmt old ret ctx -> Maybe (TermStmt new ret ctx)
cloneTerm MapF (BlockID old) (BlockID new)
mapF (Jump JumpTarget old ctx
jt) = (JumpTarget new ctx -> TermStmt new ret ctx)
-> Maybe (JumpTarget new ctx) -> Maybe (TermStmt new ret ctx)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap JumpTarget new ctx -> TermStmt new ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
Jump (Maybe (JumpTarget new ctx) -> Maybe (TermStmt new ret ctx))
-> Maybe (JumpTarget new ctx) -> Maybe (TermStmt new ret ctx)
forall a b. (a -> b) -> a -> b
$ MapF (BlockID old) (BlockID new)
-> JumpTarget old ctx -> Maybe (JumpTarget new ctx)
forall (blocks1 :: Ctx (Ctx CrucibleType))
       (blocks2 :: Ctx (Ctx CrucibleType)) (t :: Ctx CrucibleType).
MapF (BlockID blocks1) (BlockID blocks2)
-> JumpTarget blocks1 t -> Maybe (JumpTarget blocks2 t)
cloneJumpTarget MapF (BlockID old) (BlockID new)
mapF JumpTarget old ctx
jt
cloneTerm MapF (BlockID old) (BlockID new)
mapF (Br Reg ctx BoolType
reg JumpTarget old ctx
jt1 JumpTarget old ctx
jt2) = do
  JumpTarget new ctx
jt1' <- MapF (BlockID old) (BlockID new)
-> JumpTarget old ctx -> Maybe (JumpTarget new ctx)
forall (blocks1 :: Ctx (Ctx CrucibleType))
       (blocks2 :: Ctx (Ctx CrucibleType)) (t :: Ctx CrucibleType).
MapF (BlockID blocks1) (BlockID blocks2)
-> JumpTarget blocks1 t -> Maybe (JumpTarget blocks2 t)
cloneJumpTarget MapF (BlockID old) (BlockID new)
mapF JumpTarget old ctx
jt1
  JumpTarget new ctx
jt2' <- MapF (BlockID old) (BlockID new)
-> JumpTarget old ctx -> Maybe (JumpTarget new ctx)
forall (blocks1 :: Ctx (Ctx CrucibleType))
       (blocks2 :: Ctx (Ctx CrucibleType)) (t :: Ctx CrucibleType).
MapF (BlockID blocks1) (BlockID blocks2)
-> JumpTarget blocks1 t -> Maybe (JumpTarget blocks2 t)
cloneJumpTarget MapF (BlockID old) (BlockID new)
mapF JumpTarget old ctx
jt2
  TermStmt new ret ctx -> Maybe (TermStmt new ret ctx)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TermStmt new ret ctx -> Maybe (TermStmt new ret ctx))
-> TermStmt new ret ctx -> Maybe (TermStmt new ret ctx)
forall a b. (a -> b) -> a -> b
$ Reg ctx BoolType
-> JumpTarget new ctx -> JumpTarget new ctx -> TermStmt new ret ctx
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
Br Reg ctx BoolType
reg JumpTarget new ctx
jt1' JumpTarget new ctx
jt2'
cloneTerm MapF (BlockID old) (BlockID new)
_mapF (Return Reg ctx ret
reg) = TermStmt new ret ctx -> Maybe (TermStmt new ret ctx)
forall a. a -> Maybe a
Just (TermStmt new ret ctx -> Maybe (TermStmt new ret ctx))
-> TermStmt new ret ctx -> Maybe (TermStmt new ret ctx)
forall a b. (a -> b) -> a -> b
$ Reg ctx ret -> TermStmt new ret ctx
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx ret -> TermStmt blocks ret ctx
Return Reg ctx ret
reg
cloneTerm MapF (BlockID old) (BlockID new)
_ TermStmt old ret ctx
_ = [Char] -> Maybe (TermStmt new ret ctx)
forall a. HasCallStack => [Char] -> a
error [Char]
"cloneTerm: unexpected case!"

cloneJumpTarget :: MapF (BlockID blocks1) (BlockID blocks2)
                -> JumpTarget blocks1 t
                -> Maybe (JumpTarget blocks2 t)
cloneJumpTarget :: forall (blocks1 :: Ctx (Ctx CrucibleType))
       (blocks2 :: Ctx (Ctx CrucibleType)) (t :: Ctx CrucibleType).
MapF (BlockID blocks1) (BlockID blocks2)
-> JumpTarget blocks1 t -> Maybe (JumpTarget blocks2 t)
cloneJumpTarget MapF (BlockID blocks1) (BlockID blocks2)
mapF (JumpTarget BlockID blocks1 args
ident CtxRepr args
args Assignment (Reg t) args
assn) = do
  case BlockID blocks1 args
-> MapF (BlockID blocks1) (BlockID blocks2)
-> Maybe (BlockID blocks2 args)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BlockID blocks1 args
ident MapF (BlockID blocks1) (BlockID blocks2)
mapF of
    Just BlockID blocks2 args
id' -> JumpTarget blocks2 t -> Maybe (JumpTarget blocks2 t)
forall a. a -> Maybe a
Just (JumpTarget blocks2 t -> Maybe (JumpTarget blocks2 t))
-> JumpTarget blocks2 t -> Maybe (JumpTarget blocks2 t)
forall a b. (a -> b) -> a -> b
$ BlockID blocks2 args
-> CtxRepr args -> Assignment (Reg t) args -> JumpTarget blocks2 t
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx) args
-> JumpTarget blocks ctx
JumpTarget BlockID blocks2 args
id' CtxRepr args
args Assignment (Reg t) args
assn
    Maybe (BlockID blocks2 args)
Nothing -> [Char]
-> Maybe (JumpTarget blocks2 t) -> Maybe (JumpTarget blocks2 t)
forall a. [Char] -> a -> a
trace ([Char]
"could not lookup jump target id " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Index blocks1 args -> [Char]
forall a. Show a => a -> [Char]
show (BlockID blocks1 args -> Index blocks1 args
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID blocks1 args
ident)) Maybe (JumpTarget blocks2 t)
forall a. Maybe a
Nothing