Skip to content

Instantly share code, notes, and snippets.

@risgk risgk/untyped.rb
Last active Dec 20, 2015

Embed
What would you like to do?
TAPL 第7章より / 型無しラムダ計算のRuby実装 / 小ステップスタイル
# Modifying http://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/ for learning TAPL.
# TYPES AND PROGRAMMING LANGUAGES by Benjamin C. Pierce Copyright (c)2002 Benjamin C. Pierce
def isnamebound(ctx, x)
if ctx[0].nil?
false
else
y = ctx[0][0]; rest = ctx.drop(1)
if y == x
true
else
isnamebound(rest, x)
end
end
end
def pickfreshname(ctx, x)
if isnamebound(ctx, x)
pickfreshname(ctx, x + "'")
else
[[[x, "NameBind"]] + ctx, x]
end
end
def index2name(ctx, x)
if ctx[x].nil?
puts "Variable lookup failure!"
nil
else
ctx[x][0]
end
end
def ctxlength(ctx)
ctx.length
end
def sprinttm(ctx, t)
case
when t[0] == :abs
x = t[1]; t1 = t[2]
ctxp, xp = pickfreshname(ctx, x)
"(lambda " + xp + ". " + sprinttm(ctxp, t1) + ")"
when t[0] == :app
t1 = t[1]; t2 = t[2]
"(" + sprinttm(ctx, t1) + " " + sprinttm(ctx, t2) + ")"
when t[0] == :var
x = t[1]; n = t[2]
if ctxlength(ctx) == n
index2name(ctx, x)
else
puts "[bad index]"
end
end
end
def termShift(d, t)
def walkShift(c, t, d)
case
when t[0] == :var
x = t[1]; n = t[2]
if x >= c
[:var, x + d, n + d]
else
[:var, x, n + d]
end
when t[0] == :abs
x = t[1]; t1 = t[2]
[:abs, x, walkShift(c + 1, t1, d)]
when t[0] == :app
t1 = t[1]; t2 = t[2]
[:app, walkShift(c, t1, d), walkShift(c, t2, d)]
end
end
walkShift(0, t, d)
end
def termSubst(j, s, t)
def walkSubst(c, t, j, s)
case
when t[0] == :var
x = t[1]; n = t[2]
if x == j + c
termShift(c, s)
else
[:var, x, n]
end
when t[0] == :abs
x = t[1]; t1 = t[2]
[:abs, x, walkSubst(c + 1, t1, j, s)]
when t[0] == :app
t1 = t[1]; t2 = t[2]
[:app, walkSubst(c, t1, j, s), walkSubst(c, t2, j, s)]
end
end
walkSubst(0, t, j, s)
end
def termSubstTop(s, t)
termShift(-1, (termSubst(0, (termShift(1, s)), t)))
end
def isval(ctx, t)
case
when t[0] == :abs
true
else
false
end
end
class NoRuleApplies < Exception; end
def eval1(ctx, t)
# p sprinttm(ctx, t)
case
when t[0] == :app && t[1][0] == :abs && isval(ctx, t[2])
termSubstTop(t[2], t[1][2])
when t[0] == :app && isval(ctx, t[1])
t2p = eval1(ctx, t[2])
[:app, t[1], t2p]
when t[0] == :app
t1p = eval1(ctx, t[1])
[:app, t1p, t[2]]
else
raise NoRuleApplies
end
end
def eval(ctx, t)
begin
eval(ctx, eval1(ctx, t))
rescue NoRuleApplies
t
end
end
# tests
printf "test1.1: %s\n", isnamebound([], "x") == false
printf "test1.2: %s\n", isnamebound([["y", "NameBind"]], "x") == false
printf "test1.3: %s\n", isnamebound([["x", "NameBind"]], "x") == true
printf "test1.4: %s\n", isnamebound([["y", "NameBind"], ["x", "NameBind"]], "x") == true
printf "test2.1: %s\n", pickfreshname([], "x") == [[["x", "NameBind"]], "x"]
printf "test2.2: %s\n", pickfreshname([["x", "NameBind"]], "x") == [[["x'", "NameBind"], ["x", "NameBind"]], "x'"]
printf "test3.1: %s\n", index2name([["y", "NameBind"], ["x", "NameBind"]], 0) == "y"
printf "test3.2: %s\n", index2name([["y", "NameBind"], ["x", "NameBind"]], 1) == "x"
printf "test4.1: %s\n", sprinttm([["x", "NameBind"]], [:var, 0, 1]) == "x"
printf "test4.2: %s\n", sprinttm([], [:abs, "x", [:var, 0, 1]]) == "(lambda x. x)"
printf "test4.3: %s\n", sprinttm([], [:app, [:abs, "x", [:var, 0, 1]], [:abs, "x", [:var, 0, 1]]]) == "((lambda x. x) (lambda x. x))"
printf "test4.4: %s\n", sprinttm([], [:app, [:abs, "x", [:var, 0, 1]], [:abs, "y", [:app, [:var, 0, 1], [:var, 0, 1]]]]) == "((lambda x. x) (lambda y. (y y)))"
# ((lambda x. x) (lambda y. (y y))) -> (lambda y. (y y))
# ((lambda x. x) (lambda y. y)) -> (lambda y. y)
# ((lambda x. (lambda y. x)) (lambda z. z)) -> (lambda y. (lambda z. z))
# ((lambda x. (lambda x'. x)) (lambda x. x)) -> (lambda x. (lambda x'. x'))
# (((lambda x. (lambda y. x)) (lambda z. z)) (lambda w. w)) -> (lambda z. z)
# ((lambda x. x) ((lambda y. y) (lambda z. z))) -> (lambda z. z)
printf "test5.1: %s\n", sprinttm([], eval([], [:app, [:abs, "x", [:var, 0, 1]], [:abs, "y", [:app, [:var, 0, 1], [:var, 0, 1]]]])) == "(lambda y. (y y))"
printf "test5.2: %s\n", sprinttm([], eval([], [:app, [:abs, "x", [:var, 0, 1]], [:abs, "y", [:var, 0, 1]]])) == "(lambda y. y)"
printf "test5.3: %s\n", sprinttm([], eval([], [:app, [:abs, "x", [:abs, "y", [:var, 1, 2]]], [:abs, "z", [:var, 0, 1]]])) == "(lambda y. (lambda z. z))"
printf "test5.4: %s\n", sprinttm([], eval([], [:app, [:abs, "x", [:abs, "x", [:var, 1, 2]]], [:abs, "x", [:var, 0, 1]]])) == "(lambda x. (lambda x'. x'))"
printf "test5.5: %s\n", sprinttm([], eval([], [:app, [:app, [:abs, "x", [:abs, "y", [:var, 1, 2]]], [:abs, "z", [:var, 0, 1]]], [:abs, "w", [:var, 0, 1]]])) == "(lambda z. z)"
printf "test5.6: %s\n", sprinttm([], eval([], [:app, [:abs, "x", [:var, 0, 1]], [:app, [:abs, "y", [:var, 0, 1]], [:abs, "z", [:var, 0, 1]]]])) == "(lambda z. z)"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.