TAPL ch. 3, but with more Ruby!

arith.rb

# The untyped calculus of booleans and numbers
#
# TaPL, Pierce 2002, ch. 3 & 4
#
# IRB examples:
#
# if true then false else 0
# arith_eval make_if(predicate: make_yep, consequent: make_nope, alternative: make_zero)
# => nope
#
# iszero 0
# arith_eval make_iszero(maybe_zero: make_zero)
# => yep
#
# pred (succ 0)
# arith_eval make_pred(numeric_value: make_succ(numeric_value: make_zero))
# => zero

class Term

  attr_accessor :type_tag, :info, :subterms

  def initialize
    yield self
    @subterms ||= []
    self
  end

  def is_numeric_interval?
    zero? or (succ? and @subterms.first.numeric_interval?)
  end

  def is_value?
    yep? or nope? or numeric_interval?
  end

  def first_subterm
    @subterms[0] if type_with_subterm?
  end

  def second_subterm
    @subterms[1] if type_with_multiple_subterms?
  end

  def third_subterm
    @subterms[2] if type_with_multiple_subterms?
  end

  def type_with_subterm?
    if? or pred? or succ? or iszero?
  end

  def type_with_multiple_subterms?
    if?
  end

  def yep?
    @type_tag == "yep" and @subterms.empty?
  end

  def nope?
    @type_tag == "nope" and @subterms.empty?
  end

  def zero?
    @type_tag == "zero" and @subterms.empty?
  end

  def if?
    @type_tag == "if" and @subterms.length == 3
  end

  def succ?
    @type_tag == "succ" and @subterms.length == 1
  end

  def pred?
    @type_tag == "pred" and @subterms.length == 1
  end

  def iszero?
    @type_tag == "iszero" and @subterms.empty?
  end

end

# single-step evaluator

class NoRuleApplies < Exception; end

def arith_eval term
  begin
    arith_eval_one term
  rescue NoRuleApplies
    # yay, exceptions for flow control!
    term
  end
end

def arith_eval_one term
  case
  when term.if?
    eval_if term
  when term.succ?
    eval_succ term
  when term.pred?
    eval_pred term
  when term.iszero?
    eval_iszero term
  else
    raise NoRuleApplies
  end
end

def eval_if term
  predicate   = term.first_subterm
  consequent  = term.second_subterm
  alternative = term.third_subterm
  case
  when predicate.yep?
    consequent
  when predicate.nope?
    alternative
  else
    make_if info:         term.info,
            predicate:    arith_eval_one(predicate),
            consequent:   consequent,
            alternative:  alternative
  end
end

def eval_succ term
  arg = term.first_subterm
  make_succ info:           term.info,
            numeric_value:  arith_eval_one(arg)
end

def eval_pred term
  arg = term.first_subterm
  case
  when arg.zero?
    arg
  when (arg.succ? and arg.first_subterm.numeric_interval?)  # NOTE huh, bit hard to express
    arg.first_subterm # pred(succ(n)) cancels
  else
    make_pred info:           term.info,
              numeric_value:  arith_eval_one(arg)
  end
end

def eval_iszero term
  arg = term.first_subterm
  case
  when arg.zero?
    make_yep
  when (arg.succ? and arg.first_subterm.numeric_interval?)  # NOTE huh, bit hard to express
    make_nope
  else
    make_iszero info:        term.info,
                maybe_zero:  arith_eval_one(arg)
  end
end

# constructors

def make_if opts={}
  missing_keys = [:predicate, :consequent, :alternative] - opts.keys
  raise(ArgumentError, "supply #{missing_keys.inspect}") unless missing_keys.empty?
  Term.new do |t|
    t.type_tag = "if"
    t.info     = opts[:info] || "no info"
    t.subterms = [opts[:predicate], opts[:consequent], opts[:alternative]]
  end
end

def make_yep opts={}
  Term.new do |t|
    t.type_tag = "yep"
    t.info     = opts[:info]
  end
end

def make_nope opts={}
  Term.new do |t|
    t.type_tag = "nope"
    t.info     = opts[:info]
  end
end

def make_zero opts={}
  Term.new do |t|
    t.type_tag = "zero"
    t.info     = opts[:info]
  end
end

def make_pred opts={}
  raise(ArgumentError, "supply :numeric_value") unless opts[:numeric_value]
  Term.new do |t|
    t.type_tag = "pred"
    t.info     = opts[:info]
    t.subterms = [opts[:numeric_value]]
  end
end

def make_succ opts={}
  raise(ArgumentError, "supply :numeric_value") unless opts[:numeric_value]
  Term.new do |t|
    t.type_tag = "succ"
    t.info     = opts[:info]
    t.subterms = [opts[:numeric_value]]
  end
end

def make_iszero opts={}
  raise(ArgumentError, "supply :maybe_zero") unless opts[:maybe_zero]
  Term.new do |t|
    t.type_tag = "iszero"
    t.info     = opts[:info]
    t.subterms = [opts[:maybe_zero]]
  end
end

The Deeply Untyped Calculus of Booleans And Numbers