{-# 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
annotateCFGStmts ::
TraverseExt ext =>
(forall cin cout. Some (BlockID blocks) -> Ctx.Size cout -> Stmt ext cin cout -> Maybe (StmtSeq ext blocks UnitType cout))
-> (forall ctx'. Some (BlockID blocks) -> Ctx.Size ctx' -> TermStmt blocks ret ctx' -> Maybe (StmtSeq ext blocks UnitType ctx'))
-> 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))
-> (forall ctx'. Some (BlockID blocks) -> Ctx.Size ctx' -> TermStmt blocks ret ctx' -> Maybe (StmtSeq ext blocks UnitType ctx'))
-> 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 ->
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
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) =
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'