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