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

-- Substitute name x if it matches the old name oName
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

-- Substitute a name in all identifiers in a boolean expression
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')

-- Traverse a boolean expression applying a function to all identifiers
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)

-- Traverse a numeric expression applying a function to all identifiers
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)