class Rule
  def forall(*syms)
    syms.each do |sym|
      forall_single(sym)
    end

    self
  end

  def forall_single(sym)
    @generality ||= 0
    @generality += 1
    @syms ||= []
    @syms += [sym]

    self
  end

  def initialize(name, hash)
    @name = name
    @lhs = hash.keys.last
    @rhs = hash.values.last
    @syms ||= []
    @generality ||= 0
  end

  def general?
    @generality.positive?
  end

  def concrete?
    !general?
  end

  # concrete is a verb :]
  def concrete(*xs)
    xs.each { |x| concrete_single(x) }
    self
  end

  def concrete_single(x)
    unless concrete?
      sym = @syms.delete_at 0
      replace_rule = Rule.new(sym => x)
      @lhs = simp_single(@lhs, replace_rule)
      @rhs = simp_single(@rhs, replace_rule)

      @generality -= 1
      @sym = nil
    end

    self
  end

  def apply(expr)
    simp_single(expr, self)
  end

  def swap
    rule = dup
    rule.lhs = @rhs
    rule.rhs = @lhs
    rule
  end

  def inspect
    "#<Rule \"#{@name}\": #{forall_display}#{pretty_side @lhs} <=> #{pretty_side @rhs}>"
  end

  def forall_display
    if concrete?
      ''
    else
      "∀#{@syms.join ' '}, "
    end
  end

  attr_accessor :lhs, :rhs, :generality, :name

  def ==(other)
    other.is_a? Rule and
      @lhs == other.lhs and
      @rhs == other.rhs and
      @generality == other.generality
  end
end

def pretty_side(side)
  if side.is_a? Array
    "(#{side.map { |side_| pretty_side side_ }.join ' '})"
  else
    side.to_s
  end
end

def rule(*syms)
  Rule.new(*syms)
end