sealed abstract class Identifier {
  val id: String
  override def toString: String = id
}
case class InputIdentifier(id: String) extends Identifier
case class StateIdentifier(id: String) extends Identifier
case class AuxiliaryIdentifier(id: String) extends Identifier

sealed abstract class Expr {
  def bar: Expr = Not(this)

  def interpret(env: Map[Identifier, Boolean]): Boolean = this match {
    case Var(id) => env(id)
    case BooleanLiteral(b) => b
    case Equal(e1, e2) => e1.interpret(env) == e2.interpret(env)
    case Implies(e1, e2) => !e1.interpret(env) || e2.interpret(env)
    case And(e1, e2) => e1.interpret(env) && e2.interpret(env)
    case Or(e1, e2) => e1.interpret(env) || e2.interpret(env)
    case Xor(e1, e2) => e1.interpret(env) ^ e2.interpret(env)
    case Not(e) => !e.interpret(env)
  }

  def subst(l: Map[Identifier, Identifier]): Expr = this match {
    case Var(id) => Var(l(id))
    case BooleanLiteral(_) => this
    case Equal(e1, e2) => Equal(e1.subst(l), e2.subst(l))
    case Implies(e1, e2) => Implies(e1.subst(l), e2.subst(l))
    case And(e1, e2) => And(e1.subst(l), e2.subst(l))
    case Or(e1, e2) => Or(e1.subst(l), e2.subst(l))
    case Xor(e1, e2) => Xor(e1.subst(l), e2.subst(l))
    case Not(e) => Not(e.subst(l))
  }

  def fv: Set[Identifier] = this match {
    case Var(id) => Set(id)
    case BooleanLiteral(_) => Set()
    case Equal(e1, e2) => e1.fv ++ e2.fv
    case Implies(e1, e2) => e1.fv ++ e2.fv
    case And(e1, e2) => e1.fv ++ e2.fv
    case Or(e1, e2) => e1.fv ++ e2.fv
    case Xor(e1, e2) => e1.fv ++ e2.fv
    case Not(e) => e.fv
  }

  override def toString: String = this match {
    case Var(id) => id.toString
    case BooleanLiteral(b) => b.toString
    case Equal(e1, e2) => s"($e1 ⇔ $e2)"
    case Implies(e1, e2) => s"($e1 ⇒ $e2)"
    case And(e1, e2) => s"($e1 ∧ $e2)"
    case Or(e1, e2) => s"($e1 ∨ $e2)"
    case Xor(e1, e2) => s"($e1 ⊕ $e2)"
    case Not(e) => s"¬$e"
  }
}

case class Var(id: Identifier) extends Expr
case class BooleanLiteral(b: Boolean) extends Expr
case class Equal(e1: Expr, e2: Expr) extends Expr
case class Implies(e1: Expr, e2: Expr) extends Expr
case class And(e1: Expr, e2: Expr) extends Expr
case class Or(e1: Expr, e2: Expr) extends Expr
case class Xor(e1: Expr, e2: Expr) extends Expr
case class Not(e: Expr) extends Expr

object Expr {
  def not(e: Expr): Expr = Not(e)

  def and(es: Iterable[Expr]): Expr = {
    if (es.isEmpty) BooleanLiteral(true)
    else es.tail.foldLeft(es.head)(And(_,_))
  }

  def and(e: Expr, es: Expr*): Expr = {
    es.foldLeft(e)(And(_,_))
  }

  def or(es: Iterable[Expr]): Expr = {
    if (es.isEmpty) BooleanLiteral(false)
    else es.tail.foldLeft(es.head)(Or(_,_))
  }

  def or(e: Expr, es: Expr*): Expr = {
    es.foldLeft(e)(Or(_,_))
  }

  def xor(es: Iterable[Expr]): Expr = {
    if (es.isEmpty) BooleanLiteral(false)
    else es.tail.foldLeft(es.head)(Xor(_,_))
  }

  def xor(e: Expr, es: Expr*): Expr = {
    es.foldLeft(e)(Xor(_,_))
  }

  def random(fv: Array[Identifier]): Expr = {
    val r = util.Random.nextInt(100)
    if (r <= 30) Var(fv(util.Random.nextInt(fv.length)))
    else if (r <= 60) BooleanLiteral(util.Random.nextBoolean())
    else if (r <= 66) Equal(random(fv), random(fv))
    else if (r <= 72) Implies(random(fv), random(fv))
    else if (r <= 79) And(random(fv), random(fv))
    else if (r <= 86) Or(random(fv), random(fv))
    else if (r <= 94) Xor(random(fv), random(fv))
    else Not(random(fv))
  }
}
