module Language.SMV.Substitution where
import qualified Language.SMV.AbsSMV as SMV
substituteBoolExpr :: t (String, String) -> BoolSpec -> BoolSpec
substituteBoolExpr t (String, String)
subs BoolSpec
e = ((String, String) -> BoolSpec -> BoolSpec)
-> BoolSpec -> t (String, String) -> BoolSpec
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, String) -> BoolSpec -> BoolSpec
subBS BoolSpec
e t (String, String)
subs
subsName :: (b, b) -> b -> b
subsName (b
oName, b
nName) b
x = if b
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
oName then b
nName else b
x
subBS :: (String, String) -> BoolSpec -> BoolSpec
subBS (String, String)
sub' = (String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent ((String, String) -> String -> String
forall {b}. Eq b => (b, b) -> b -> b
subsName (String, String)
sub')
mapBoolSpecIdent :: (String -> String) -> SMV.BoolSpec -> SMV.BoolSpec
mapBoolSpecIdent :: (String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
boolSpec =
case BoolSpec
boolSpec of
SMV.BoolSpecSignal (SMV.Ident String
i) -> Ident -> BoolSpec
SMV.BoolSpecSignal (String -> Ident
SMV.Ident (String -> String
f String
i))
SMV.BoolSpecConst BoolConst
bc -> BoolConst -> BoolSpec
SMV.BoolSpecConst BoolConst
bc
SMV.BoolSpecNum NumExpr
e -> NumExpr -> BoolSpec
SMV.BoolSpecNum ((String -> String) -> NumExpr -> NumExpr
mapNumExprIdent String -> String
f NumExpr
e)
SMV.BoolSpecCmp BoolSpec
spec1 OrdOp
op2 BoolSpec
spec2 -> BoolSpec -> OrdOp -> BoolSpec -> BoolSpec
SMV.BoolSpecCmp
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec1) OrdOp
op2
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec2)
SMV.BoolSpecNeg BoolSpec
spec -> BoolSpec -> BoolSpec
SMV.BoolSpecNeg ((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec)
SMV.BoolSpecAnd BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> BoolSpec -> BoolSpec
SMV.BoolSpecAnd
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec1)
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec2)
SMV.BoolSpecOr BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> BoolSpec -> BoolSpec
SMV.BoolSpecOr
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec1)
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec2)
SMV.BoolSpecXor BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> BoolSpec -> BoolSpec
SMV.BoolSpecXor
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec1)
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec2)
SMV.BoolSpecImplies BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> BoolSpec -> BoolSpec
SMV.BoolSpecImplies
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec1)
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec2)
SMV.BoolSpecEquivs BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> BoolSpec -> BoolSpec
SMV.BoolSpecEquivs
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec1)
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec2)
SMV.BoolSpecOp1 OpOne
op BoolSpec
spec -> OpOne -> BoolSpec -> BoolSpec
SMV.BoolSpecOp1 OpOne
op ((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec)
SMV.BoolSpecOp2 BoolSpec
spec1 OpTwo
op2 BoolSpec
spec2 -> BoolSpec -> OpTwo -> BoolSpec -> BoolSpec
SMV.BoolSpecOp2
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec1) OpTwo
op2
((String -> String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent String -> String
f BoolSpec
spec2)
mapNumExprIdent :: (String -> String) -> SMV.NumExpr -> SMV.NumExpr
mapNumExprIdent :: (String -> String) -> NumExpr -> NumExpr
mapNumExprIdent String -> String
f NumExpr
numExpr =
case NumExpr
numExpr of
SMV.NumId (SMV.Ident String
i) -> Ident -> NumExpr
SMV.NumId (String -> Ident
SMV.Ident (String -> String
f String
i))
SMV.NumConstI Integer
c -> Integer -> NumExpr
SMV.NumConstI Integer
c
SMV.NumConstD Double
c -> Double -> NumExpr
SMV.NumConstD Double
c
SMV.NumAdd NumExpr
expr1 AdditiveOp
op NumExpr
expr2 -> NumExpr -> AdditiveOp -> NumExpr -> NumExpr
SMV.NumAdd
((String -> String) -> NumExpr -> NumExpr
mapNumExprIdent String -> String
f NumExpr
expr1)
AdditiveOp
op
((String -> String) -> NumExpr -> NumExpr
mapNumExprIdent String -> String
f NumExpr
expr2)
SMV.NumMult NumExpr
expr1 MultOp
op NumExpr
expr2 -> NumExpr -> MultOp -> NumExpr -> NumExpr
SMV.NumMult
((String -> String) -> NumExpr -> NumExpr
mapNumExprIdent String -> String
f NumExpr
expr1)
MultOp
op
((String -> String) -> NumExpr -> NumExpr
mapNumExprIdent String -> String
f NumExpr
expr2)