------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Utils.CoreRewrite
-- Description      : Operations for manipulating Core CFGs
-- Copyright        : (c) Galois, Inc 2016
-- License          : BSD3
-- Maintainer       : Simon Winwood <sjw@galois.com>
-- Stability        : provisional
--
------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}

module Lang.Crucible.Utils.CoreRewrite
( annotateCFGStmts
) where

import           Control.Lens

import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Map (Pair(..))
import           Data.Parameterized.TraversableFC

import           Lang.Crucible.CFG.Core
import           Lang.Crucible.CFG.Extension

------------------------------------------------------------------------
-- CFG annotation


-- | This function walks through all the blocks in the CFG calling
-- @fS@ on each @Stmt@ and @fT@ on each @TermStmt@.  These functions
-- return a possible annotaition statement (which has access to the
-- result of the statement, if any) along with a context diff which
-- describes any new variables.
annotateCFGStmts ::
   TraverseExt ext =>
   (forall cin cout. Some (BlockID blocks) -> Ctx.Size cout -> Stmt ext cin cout -> Maybe (StmtSeq ext blocks UnitType cout))
  -- ^ This is the annotation function.  The resulting @StmtSeq@ gets
  -- spliced in after the statement so that they can inspect the
  -- result if desired.  The terminal statement is ignored.
  -> (forall ctx'. Some (BlockID blocks)  -> Ctx.Size ctx' -> TermStmt blocks ret ctx' -> Maybe (StmtSeq ext blocks UnitType ctx'))
  -- ^ As above but for the final term stmt, where the annotation will
  -- be _before_ the term stmt.
  -> CFG ext blocks ctx ret -> CFG ext blocks ctx ret
annotateCFGStmts :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TraverseExt ext =>
(forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
 Some (BlockID blocks)
 -> Size cout
 -> Stmt ext cin cout
 -> Maybe (StmtSeq ext blocks UnitType cout))
-> (forall (ctx' :: Ctx CrucibleType).
    Some (BlockID blocks)
    -> Size ctx'
    -> TermStmt blocks ret ctx'
    -> Maybe (StmtSeq ext blocks UnitType ctx'))
-> CFG ext blocks ctx ret
-> CFG ext blocks ctx ret
annotateCFGStmts forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size cout
-> Stmt ext cin cout
-> Maybe (StmtSeq ext blocks UnitType cout)
fS forall (ctx' :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size ctx'
-> TermStmt blocks ret ctx'
-> Maybe (StmtSeq ext blocks UnitType ctx')
fT = (forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> Block ext blocks ret x)
-> CFG ext blocks ctx ret -> CFG ext blocks ctx ret
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
(forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> Block ext blocks ret x)
-> CFG ext blocks ctx ret -> CFG ext blocks ctx ret
mapCFGBlocks ((forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
 Some (BlockID blocks)
 -> Size cout
 -> Stmt ext cin cout
 -> Maybe (StmtSeq ext blocks UnitType cout))
-> (forall (ctx' :: Ctx CrucibleType).
    Some (BlockID blocks)
    -> Size ctx'
    -> TermStmt blocks ret ctx'
    -> Maybe (StmtSeq ext blocks UnitType ctx'))
-> Block ext blocks ret x
-> Block ext blocks ret x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TraverseExt ext =>
(forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
 Some (BlockID blocks)
 -> Size cout
 -> Stmt ext cin cout
 -> Maybe (StmtSeq ext blocks UnitType cout))
-> (forall (ctx' :: Ctx CrucibleType).
    Some (BlockID blocks)
    -> Size ctx'
    -> TermStmt blocks ret ctx'
    -> Maybe (StmtSeq ext blocks UnitType ctx'))
-> Block ext blocks ret ctx
-> Block ext blocks ret ctx
annotateBlockStmts Some (BlockID blocks)
-> Size cout
-> Stmt ext cin cout
-> Maybe (StmtSeq ext blocks UnitType cout)
forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size cout
-> Stmt ext cin cout
-> Maybe (StmtSeq ext blocks UnitType cout)
fS Some (BlockID blocks)
-> Size ctx'
-> TermStmt blocks ret ctx'
-> Maybe (StmtSeq ext blocks UnitType ctx')
forall (ctx' :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size ctx'
-> TermStmt blocks ret ctx'
-> Maybe (StmtSeq ext blocks UnitType ctx')
fT)

mapCFGBlocks :: (forall x. Block ext blocks ret x -> Block ext blocks ret x)
             -> CFG ext blocks ctx ret -> CFG ext blocks ctx ret
mapCFGBlocks :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
(forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> Block ext blocks ret x)
-> CFG ext blocks ctx ret -> CFG ext blocks ctx ret
mapCFGBlocks forall (x :: Ctx CrucibleType).
Block ext blocks ret x -> Block ext blocks ret x
f CFG ext blocks ctx ret
cfg = CFG ext blocks ctx ret
cfg { cfgBlockMap = fmapFC f (cfgBlockMap cfg) }

annotateBlockStmts ::
  forall ext blocks ret ctx.
  TraverseExt ext =>
  (forall cin cout. Some (BlockID blocks) -> Ctx.Size cout -> Stmt ext cin cout -> Maybe (StmtSeq ext blocks UnitType cout))
  -- ^ This is the annotation function.  Annotation statements go
  -- after the statement so that they can inspect the result if
  -- desired.  We use Diff here over CtxEmbedding as the remainder of
  -- the statements can't use the result of the annotation function
  -> (forall ctx'. Some (BlockID blocks) -> Ctx.Size ctx' -> TermStmt blocks ret ctx' -> Maybe (StmtSeq ext blocks UnitType ctx'))
  -- ^ As above but for the final term stmt, where the annotation will
  -- be _before_ the term stmt.
  -> Block ext blocks ret ctx
  -> Block ext blocks ret ctx
annotateBlockStmts :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TraverseExt ext =>
(forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
 Some (BlockID blocks)
 -> Size cout
 -> Stmt ext cin cout
 -> Maybe (StmtSeq ext blocks UnitType cout))
-> (forall (ctx' :: Ctx CrucibleType).
    Some (BlockID blocks)
    -> Size ctx'
    -> TermStmt blocks ret ctx'
    -> Maybe (StmtSeq ext blocks UnitType ctx'))
-> Block ext blocks ret ctx
-> Block ext blocks ret ctx
annotateBlockStmts forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size cout
-> Stmt ext cin cout
-> Maybe (StmtSeq ext blocks UnitType cout)
fS forall (ctx' :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size ctx'
-> TermStmt blocks ret ctx'
-> Maybe (StmtSeq ext blocks UnitType ctx')
fT Block ext blocks ret ctx
b = Block ext blocks ret ctx
b Block ext blocks ret ctx
-> (Block ext blocks ret ctx -> Block ext blocks ret ctx)
-> Block ext blocks ret ctx
forall a b. a -> (a -> b) -> b
& (StmtSeq ext blocks ret ctx
 -> Identity (StmtSeq ext blocks ret ctx))
-> Block ext blocks ret ctx -> Identity (Block ext blocks 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 ((StmtSeq ext blocks ret ctx
  -> Identity (StmtSeq ext blocks ret ctx))
 -> Block ext blocks ret ctx -> Identity (Block ext blocks ret ctx))
-> (StmtSeq ext blocks ret ctx -> StmtSeq ext blocks ret ctx)
-> Block ext blocks ret ctx
-> Block ext blocks ret ctx
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ CtxEmbedding ctx ctx
-> StmtSeq ext blocks ret ctx -> StmtSeq ext blocks ret ctx
forall (ctx' :: Ctx CrucibleType) (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx' ctx''
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret ctx''
goStmts CtxEmbedding ctx ctx
initialCtxe
  where
    initialCtxe :: CtxEmbedding ctx ctx
initialCtxe = Size ctx -> CtxEmbedding ctx ctx
forall {k} (ctx :: Ctx k). Size ctx -> CtxEmbedding ctx ctx
Ctx.identityEmbedding (Assignment TypeRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size (Block ext blocks ret ctx -> Assignment TypeRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext blocks ret ctx
b))
    goStmts :: forall ctx' ctx''. Ctx.CtxEmbedding ctx' ctx''
            -> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret ctx''
    goStmts :: forall (ctx' :: Ctx CrucibleType) (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx' ctx''
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret ctx''
goStmts CtxEmbedding ctx' ctx''
ctxe (ConsStmt ProgramLoc
loc Stmt ext ctx' ctx'
stmt StmtSeq ext blocks ret ctx'
rest) =
      case CtxEmbedding ctx' ctx''
-> Stmt ext ctx' ctx' -> Pair (Stmt ext ctx'') (CtxEmbedding ctx')
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (sctx :: Ctx CrucibleType).
TraverseExt ext =>
CtxEmbedding ctx ctx'
-> Stmt ext ctx sctx -> Pair (Stmt ext ctx') (CtxEmbedding sctx)
applyEmbeddingStmt CtxEmbedding ctx' ctx''
ctxe Stmt ext ctx' ctx'
stmt of
        Pair Stmt ext ctx'' tp
stmt' CtxEmbedding ctx' tp
ctxe' ->
          case Some (BlockID blocks)
-> Size tp
-> Stmt ext ctx'' tp
-> Maybe (StmtSeq ext blocks UnitType tp)
forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size cout
-> Stmt ext cin cout
-> Maybe (StmtSeq ext blocks UnitType cout)
fS (BlockID blocks ctx -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (BlockID blocks ctx -> Some (BlockID blocks))
-> BlockID blocks ctx -> Some (BlockID blocks)
forall a b. (a -> b) -> a -> b
$ Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
b) (CtxEmbedding ctx' tp
ctxe' CtxEmbedding ctx' tp
-> Getting (Size tp) (CtxEmbedding ctx' tp) (Size tp) -> Size tp
forall s a. s -> Getting a s a -> a
^. Getting (Size tp) (CtxEmbedding ctx' tp) (Size tp)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (f :: Type -> Type).
Functor f =>
(Size ctx' -> f (Size ctx'))
-> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx')
Ctx.ctxeSize) Stmt ext ctx'' tp
stmt' of
            Maybe (StmtSeq ext blocks UnitType tp)
Nothing  -> ProgramLoc
-> Stmt ext ctx'' tp
-> StmtSeq ext blocks ret tp
-> StmtSeq ext blocks 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'' tp
stmt' (CtxEmbedding ctx' tp
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret tp
forall (ctx' :: Ctx CrucibleType) (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx' ctx''
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret ctx''
goStmts CtxEmbedding ctx' tp
ctxe' StmtSeq ext blocks ret ctx'
rest)
            Just StmtSeq ext blocks UnitType tp
annotSeq ->
              ProgramLoc
-> Stmt ext ctx'' tp
-> StmtSeq ext blocks ret tp
-> StmtSeq ext blocks 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'' tp
stmt' (CtxEmbedding ctx' tp
-> StmtSeq ext blocks UnitType tp
-> (forall (ctx'' :: Ctx CrucibleType).
    CtxEmbedding ctx' ctx'' -> StmtSeq ext blocks ret ctx'')
-> StmtSeq ext blocks ret tp
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ret' :: CrucibleType) (ctx :: Ctx CrucibleType)
       (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> (forall (ctx'' :: Ctx CrucibleType).
    CtxEmbedding ctx ctx'' -> StmtSeq ext blocks ret' ctx'')
-> StmtSeq ext blocks ret' ctx'
appendStmtSeq CtxEmbedding ctx' tp
ctxe' StmtSeq ext blocks UnitType tp
annotSeq ((CtxEmbedding ctx' ctx''
 -> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret ctx'')
-> StmtSeq ext blocks ret ctx'
-> CtxEmbedding ctx' ctx''
-> StmtSeq ext blocks ret ctx''
forall a b c. (a -> b -> c) -> b -> a -> c
flip CtxEmbedding ctx' ctx''
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret ctx''
forall (ctx' :: Ctx CrucibleType) (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx' ctx''
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret ctx''
goStmts StmtSeq ext blocks ret ctx'
rest))
    goStmts CtxEmbedding ctx' ctx''
ctxe (TermStmt ProgramLoc
loc TermStmt blocks ret ctx'
term) =
      let term' :: TermStmt blocks ret ctx''
term' = CtxEmbedding ctx' ctx''
-> TermStmt blocks ret ctx' -> TermStmt blocks ret ctx''
forall k (f :: Ctx k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k).
ApplyEmbedding f =>
CtxEmbedding ctx ctx' -> f ctx -> f ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> TermStmt blocks ret ctx -> TermStmt blocks ret ctx'
Ctx.applyEmbedding CtxEmbedding ctx' ctx''
ctxe TermStmt blocks ret ctx'
term in
      case Some (BlockID blocks)
-> Size ctx''
-> TermStmt blocks ret ctx''
-> Maybe (StmtSeq ext blocks UnitType ctx'')
forall (ctx' :: Ctx CrucibleType).
Some (BlockID blocks)
-> Size ctx'
-> TermStmt blocks ret ctx'
-> Maybe (StmtSeq ext blocks UnitType ctx')
fT (BlockID blocks ctx -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (BlockID blocks ctx -> Some (BlockID blocks))
-> BlockID blocks ctx -> Some (BlockID blocks)
forall a b. (a -> b) -> a -> b
$ Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
b) (CtxEmbedding ctx' ctx''
ctxe CtxEmbedding ctx' ctx''
-> Getting (Size ctx'') (CtxEmbedding ctx' ctx'') (Size ctx'')
-> Size ctx''
forall s a. s -> Getting a s a -> a
^. Getting (Size ctx'') (CtxEmbedding ctx' ctx'') (Size ctx'')
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (f :: Type -> Type).
Functor f =>
(Size ctx' -> f (Size ctx'))
-> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx')
Ctx.ctxeSize) TermStmt blocks ret ctx''
term' of
        Maybe (StmtSeq ext blocks UnitType ctx'')
Nothing -> ProgramLoc
-> TermStmt blocks ret ctx'' -> StmtSeq ext blocks 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 blocks ret ctx''
term'
        Just StmtSeq ext blocks UnitType ctx''
annotSeq ->
          -- FIXME: we could use extendContext here instead
          let restf :: forall fctx. Ctx.CtxEmbedding ctx' fctx -> StmtSeq ext blocks ret fctx
              restf :: forall (fctx :: Ctx CrucibleType).
CtxEmbedding ctx' fctx -> StmtSeq ext blocks ret fctx
restf CtxEmbedding ctx' fctx
ctxe'' = ProgramLoc
-> TermStmt blocks ret fctx -> StmtSeq ext blocks ret fctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ext.
ProgramLoc -> TermStmt blocks ret ctx -> StmtSeq ext blocks ret ctx
TermStmt ProgramLoc
loc (CtxEmbedding ctx' fctx
-> TermStmt blocks ret ctx' -> TermStmt blocks ret fctx
forall k (f :: Ctx k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k).
ApplyEmbedding f =>
CtxEmbedding ctx ctx' -> f ctx -> f ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> TermStmt blocks ret ctx -> TermStmt blocks ret ctx'
Ctx.applyEmbedding CtxEmbedding ctx' fctx
ctxe'' TermStmt blocks ret ctx'
term)
          in CtxEmbedding ctx' ctx''
-> StmtSeq ext blocks UnitType ctx''
-> (forall (fctx :: Ctx CrucibleType).
    CtxEmbedding ctx' fctx -> StmtSeq ext blocks ret fctx)
-> StmtSeq ext blocks ret ctx''
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ret' :: CrucibleType) (ctx :: Ctx CrucibleType)
       (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> (forall (ctx'' :: Ctx CrucibleType).
    CtxEmbedding ctx ctx'' -> StmtSeq ext blocks ret' ctx'')
-> StmtSeq ext blocks ret' ctx'
appendStmtSeq CtxEmbedding ctx' ctx''
ctxe StmtSeq ext blocks UnitType ctx''
annotSeq CtxEmbedding ctx' ctx'' -> StmtSeq ext blocks ret ctx''
forall (fctx :: Ctx CrucibleType).
CtxEmbedding ctx' fctx -> StmtSeq ext blocks ret fctx
restf

stmtDiff :: Stmt ext ctx ctx' -> Ctx.Diff ctx ctx'
stmtDiff :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
Stmt ext ctx ctx' -> Diff ctx ctx'
stmtDiff Stmt ext ctx ctx'
stmt =
  case Stmt ext ctx ctx'
stmt of
    SetReg {}        -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    ExtendAssign{}   -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    CallHandle {}    -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    Print {}         -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    ReadGlobal {}    -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    WriteGlobal {}   -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    FreshConstant{}  -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    FreshFloat{}     -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    FreshNat{}       -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    NewRefCell {}    -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    NewEmptyRefCell{}-> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    ReadRefCell {}   -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    WriteRefCell {}  -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    DropRefCell {}   -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    Assert {}        -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff
    Assume {}        -> Diff ctx ctx'
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
Ctx.knownDiff

-- | This appends two @StmtSeq@, throwing away the @TermStmt@ from the first @StmtSeq@
-- It could probably be generalized to @Ctx.Diff@ instead of an embedding.
appendStmtSeq :: forall ext blocks ret ret' ctx ctx'.
                 Ctx.CtxEmbedding ctx ctx'
              -> StmtSeq ext blocks ret  ctx'
              -> (forall ctx''. Ctx.CtxEmbedding ctx ctx'' -> StmtSeq ext blocks ret' ctx'')
              -> StmtSeq ext blocks ret' ctx'
appendStmtSeq :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ret' :: CrucibleType) (ctx :: Ctx CrucibleType)
       (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> (forall (ctx'' :: Ctx CrucibleType).
    CtxEmbedding ctx ctx'' -> StmtSeq ext blocks ret' ctx'')
-> StmtSeq ext blocks ret' ctx'
appendStmtSeq CtxEmbedding ctx ctx'
ctxe StmtSeq ext blocks ret ctx'
seq1 forall (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'' -> StmtSeq ext blocks ret' ctx''
seq2f = CtxEmbedding ctx ctx'
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret' ctx'
forall (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx ctx''
-> StmtSeq ext blocks ret ctx'' -> StmtSeq ext blocks ret' ctx''
go CtxEmbedding ctx ctx'
ctxe StmtSeq ext blocks ret ctx'
seq1
  where
    go :: forall ctx''.
          Ctx.CtxEmbedding ctx ctx''
          -> StmtSeq ext blocks ret ctx''
          -> StmtSeq ext blocks ret' ctx''
    go :: forall (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx ctx''
-> StmtSeq ext blocks ret ctx'' -> StmtSeq ext blocks ret' ctx''
go CtxEmbedding ctx ctx''
ctxe' (ConsStmt ProgramLoc
loc Stmt ext ctx'' ctx'
stmt StmtSeq ext blocks ret ctx'
rest) =
      -- This just throws away the new variables, which is OK as seq2
      -- can't reference them.
      let ctxe'' :: CtxEmbedding ctx ctx'
ctxe'' = Diff ctx'' ctx' -> CtxEmbedding ctx ctx'' -> CtxEmbedding ctx ctx'
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k).
Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
Ctx.extendEmbeddingRightDiff (Stmt ext ctx'' ctx' -> Diff ctx'' ctx'
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
Stmt ext ctx ctx' -> Diff ctx ctx'
stmtDiff Stmt ext ctx'' ctx'
stmt) CtxEmbedding ctx ctx''
ctxe'
      in ProgramLoc
-> Stmt ext ctx'' ctx'
-> StmtSeq ext blocks ret' ctx'
-> StmtSeq ext blocks 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 (CtxEmbedding ctx ctx'
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret' ctx'
forall (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx ctx''
-> StmtSeq ext blocks ret ctx'' -> StmtSeq ext blocks ret' ctx''
go CtxEmbedding ctx ctx'
ctxe'' StmtSeq ext blocks ret ctx'
rest)
    go CtxEmbedding ctx ctx''
ctxe' (TermStmt ProgramLoc
_loc TermStmt blocks ret ctx''
_term)    = CtxEmbedding ctx ctx'' -> StmtSeq ext blocks ret' ctx''
forall (ctx'' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'' -> StmtSeq ext blocks ret' ctx''
seq2f CtxEmbedding ctx ctx''
ctxe'