module WLP.LogicalExpression
  ( LogicalExpression(..)
  , replace
  )
where

import WLP.MathExpression (MathExpression, replaceInExpr)

data LogicalExpression
  = Constant Bool
  | Variable String
  | Expression MathExpression
  | Not LogicalExpression
  | LogicalExpression :/\: LogicalExpression
  | LogicalExpression :\/: LogicalExpression
  | LogicalExpression :=>: LogicalExpression
  | LogicalExpression :<=>: LogicalExpression

instance Show LogicalExpression where
  show (Constant x)   = show x
  show (Variable s)   = s
  show (Expression e) = "(" ++ show e ++ ")"
  show (Not le)       = "!" ++ show le

  show (e1 :/\: e2)   = "(" ++ show e1 ++ ") /\\ (" ++ show e2 ++ ")"
  show (e1 :\/: e2)   = "(" ++ show e1 ++ ") \\/ (" ++ show e2 ++ ")"
  show (e1 :=>: e2)   = "(" ++ show e1 ++  ") => (" ++ show e2 ++ ")"
  show (e1 :<=>: e2)  = "(" ++ show e1 ++ ") <=> (" ++ show e2 ++ ")"

-- | Substitutes the variable given by the string with the value given in the expression.
replace :: String -> MathExpression -> LogicalExpression -> LogicalExpression
replace _   _ x@(Constant _) = x
replace var e x@(Variable v) = if v == var then Expression e else x
replace var e x@(Expression expr) = Expression $ replaceInExpr var e expr
replace var e x@(e1 :/\: e2) = replace var e e1 :/\: replace var e e2
replace var e x@(e1 :\/: e2) = replace var e e1 :/\: replace var e e2
replace var e x@(e1 :=>: e2) = replace var e e1 :=>: replace var e e2
replace var e x@(e1 :<=>: e2) = replace var e e1 :<=>: replace var e e2