    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)