content: module Language.SMV.Substitution where
  
  import qualified Language.SMV.AbsSMV as SMV
  
  substituteBoolExpr subs e = foldr subBS e subs
  
  -- Substitute name x if it matches the old name oName
  subsName (oName, nName) x = if x == oName then nName else x
  
  -- Substitute a name in all identifiers in a boolean expression
  subBS sub' = mapBoolSpecIdent (subsName sub')
  
  -- Traverse a boolean expression applying a function to all identifiers
  mapBoolSpecIdent :: (String -> String) -> SMV.BoolSpec -> SMV.BoolSpec
  mapBoolSpecIdent f boolSpec =
    case boolSpec of
      SMV.BoolSpecSignal (SMV.Ident i) -> SMV.BoolSpecSignal (SMV.Ident (f i))
  
      SMV.BoolSpecConst bc -> SMV.BoolSpecConst bc
  
      SMV.BoolSpecNum e -> SMV.BoolSpecNum (mapNumExprIdent f e)
  
      SMV.BoolSpecCmp spec1 op2 spec2 -> SMV.BoolSpecCmp
                                           (mapBoolSpecIdent f spec1) op2
                                           (mapBoolSpecIdent f spec2)
  
      SMV.BoolSpecNeg spec -> SMV.BoolSpecNeg (mapBoolSpecIdent f spec)
  
      SMV.BoolSpecAnd spec1 spec2 -> SMV.BoolSpecAnd
                                           (mapBoolSpecIdent f spec1)
                                           (mapBoolSpecIdent f spec2)
  
      SMV.BoolSpecOr spec1 spec2 -> SMV.BoolSpecOr
                                          (mapBoolSpecIdent f spec1)
                                          (mapBoolSpecIdent f spec2)
  
      SMV.BoolSpecXor spec1 spec2 -> SMV.BoolSpecXor
                                           (mapBoolSpecIdent f spec1)
                                           (mapBoolSpecIdent f spec2)
  
      SMV.BoolSpecImplies spec1 spec2 -> SMV.BoolSpecImplies
                                               (mapBoolSpecIdent f spec1)
                                               (mapBoolSpecIdent f spec2)
  
      SMV.BoolSpecEquivs spec1 spec2 -> SMV.BoolSpecEquivs
                                              (mapBoolSpecIdent f spec1)
                                              (mapBoolSpecIdent f spec2)
  
      SMV.BoolSpecOp1 op spec -> SMV.BoolSpecOp1 op (mapBoolSpecIdent f spec)
  
      SMV.BoolSpecOp2 spec1 op2 spec2 -> SMV.BoolSpecOp2
                                           (mapBoolSpecIdent f spec1) op2
                                           (mapBoolSpecIdent f spec2)
  
  -- Traverse a numeric expression applying a function to all identifiers
  mapNumExprIdent :: (String -> String) -> SMV.NumExpr -> SMV.NumExpr
  mapNumExprIdent f numExpr =
    case numExpr of
      SMV.NumId (SMV.Ident i)    -> SMV.NumId (SMV.Ident (f i))
      SMV.NumConstI c            -> SMV.NumConstI c
      SMV.NumConstD c            -> SMV.NumConstD c
      SMV.NumAdd expr1 op expr2  -> SMV.NumAdd
                                          (mapNumExprIdent f expr1)
                                          op
                                          (mapNumExprIdent f expr2)
      SMV.NumMult expr1 op expr2 -> SMV.NumMult
                                          (mapNumExprIdent f expr1)
                                          op
                                          (mapNumExprIdent f expr2)
  