# closed algebraic data types for ruby
# pesco 2009, isc license

class Class
    def ctor(ctorname, argtypes)
        # add singleton constructor method to self
        self_ = (class << self; self; end)
        self_.module_eval do
            define_method(ctorname) do |argvalues|
                x = allocate

                # check argument types
                argtypes.each do |k,t|
                    v = argvalues[k]
                    if v.nil? then
                        raise("#{ctorname}: missing field #{k}")
                    elsif !v.is_a?(t) then
                        raise "#{ctorname}: #{k}: type mismatch: " +
                              "expected #{t}, got #{v.class}"
                    end
                end

                # fill instance variables of x
                x.instance_eval do
                    @ctor = ctorname
                    @args = argvalues
                end

                x
            end # constructor
        end # singleton methods of our ADT

        # inspection methods
        attr_reader :ctor
        attr_reader :args

        define_method("is_#{ctorname}?".to_sym) { ctor == ctorname }

        # argument accessors
        argtypes.keys.each do |k|
            define_method(k) do
                args[k] || raise("#{ctor}: #{k}: no such field")
            end

            define_method("#{k}=".to_sym) do |v|
                if args.key?(k) then
                    args[k] = v
                else
                    raise("#{ctor}: #{k}: no such field")
                end
            end
        end

        # equality
        define_method(:==) do |x|
            ctor == x.ctor && args == x.args
        end
    end # 'ctor' method of Class
end


# demo:

class Expr
    ctor :lam, :var => String, :body => Expr
    ctor :app, :op => Expr, :arg => Expr
    ctor :var, :name => String

    def to_s
        if is_lam? then
            "(\#{var}. #{body})"
        elsif is_app? then
            "#{op} #{arg}"
        elsif is_var? then
            "#{name}"
        end
    end

    def eval(env={})
        if is_lam? then
            self
        elsif is_app? then
            f = op.eval(env)
            if f.is_lam?
                x = arg.eval(env)
                f.body.subst(f.var,x).eval
            else
                raise "operator is not a function"
            end
        elsif is_var? then
            env[name] || self
        end
    end

    def subst(v,x)
        if is_lam? && var!=v then
            Expr.lam(:var=>var, :body=>body.subst(v,x))
        elsif is_app? then
            Expr.app(:op=>op.subst(v,x), :arg=>arg.subst(v,x))
        elsif is_var? && v==name then
            x
        else
            self
        end
    end

    def eval!
        if is_app? then
            f = op.eval!
            if f.is_lam?
                f.body.subst!(op.var,arg).eval!
            else
                raise "#{op}: operator is not a function"
            end
        else
            self
        end
    end

    def subst!(v,x)
        if is_lam? && var!=v then
            self.body = body.subst!(v,x)
            self
        elsif is_app? then
            self.op = op.subst!(v,x)
            self.arg = arg.subst!(v,x)
            self
        elsif is_var? && v==name then
            x
        else
            self
        end
    end
end

# tests:

def id; Expr.lam(:var=>"x", :body=>Expr.var(:name=>"x")); end   # (\x.x)
def id_id; Expr.app(:op=>id, :arg=>id); end                     # (\x.x) (\x.x)
id_id.eval == id || puts("id test FAIL")
id_id.eval! == id || puts("in-place id test FAIL")

# (\x. x z) (\y.x) => x  (wrong: \y.x)
def varcap;
    x = Expr.var(:name=>"x")
    z = Expr.var(:name=>"z")
    y_x = Expr.lam(:var=>"y", :body=>x)
    x_xz = Expr.lam(:var=>"x", :body=>Expr.app(:op=>x, :arg=>z))
    Expr.app(:op=>x_xz, :arg=>y_x)
end
varcap.eval == Expr.var(:name=>"x") || puts("varcap test FAIL")
varcap.eval! == Expr.var(:name=>"x") || puts("in-place varcap test FAIL")