trampoline_terp.req

# a simple interpreter, in trampolined style,
# but with only curried functions: (((f x) y) z)
#
# TODO: figure out how to do uncurried functions like (f x y z)
#
# to get to a fueled interpreter,
# we need to thread a "fuel" argument through the control flow,
# test-and-decrementing the fuel wherever we
# want to charge a "step" of computation.
# 
# an expression can be a symbol
# exp ::= Sym(name)
# the value of a symbol is looked up in the environment, then returned
ev(Sym(?name), ?env, ?k) == apply_cont(?k, lookup(?env, ?name))

# an expression can be a nonpair
#   all nonpairs are already values; just return it
# exp ::= Nonpair(val)

ev(Nonpair(?val), ?env, ?k) == apply_cont(?k, ?val)
# an expression can be a quote
# exp ::= Quote(?x)
#   take the quotes off and return whatever is inside
ev(Quote(?x), ?env, ?k) == apply_cont(?k, ?x)

# an expression can be an if
# exp ::= If(?test, ?truebranch, ?falsebranch)
#   to eval an if
#   first eval the test of the if
#   then use the host-language "if"
#   to decide whether to eval and return the
#   true branch or the false branch of the if
ev(If(?test, ?truebranch, ?falsebranch), ?env, ?k) == ev(?test, ?env, Decide(?truebranch, ?falsebranch, ?env, ?k))
apply_cont(Decide(?truebranch, ?falsebranch, ?env, ?k), True) == ev(?truebranch, ?env, ?k)
apply_cont(Decide(?truebranch, ?falsebranch, ?env, ?k), False) == ev(?falsebranch, ?env, ?k)

# an expression can be a lambda
# exp ::= Lambda(?param, ?body)
#   construct something that will be sufficient to eval the body,
#   once we get an actual to bind to that param
ev(Lambda(?param, ?body), ?env, ?k) == apply_cont(?k, Closure(?param, ?body, ?env))

# an expression can be a function application
# exp ::= App(?f, ?x)
#   to eval a function application,
#   eval the function,
#   then eval the arg,
#   then combine the formals with the actuals 
ev(App(?f, ?x), ?env, ?k) == ev(?f, ?env, Arg(?x, ?env, ?k))
apply_cont(Arg(?x, ?env, ?k), ?proc) == ev(?x, ?env, Enter(?proc, ?k))
apply_cont(Enter(Closure(?formal, ?body, ?env), ?k), ?actual) == ev(?body, Extend(?formal, ?actual, ?env), ?k)

# stuff regarding the environment
# environments can be empty
# env ::= Empty
# environments can be extensions of other environments
# where a particular name is bound to a particular value
# env ::= Extend(name, value, env)

## bind is a helper function that takes a list of names and
## a list of values, and binds each name to the corresponding value
## there's some nonsense about shadowing - just don't do it, mkay?
#bind(Cons(?n, ?ns), Cons(?v, ?vs), ?env) == bind(?ns, ?vs, Extend(?n, ?v, ?env))
#bind(Nil, Nil, ?env) == ?env

# lookup looks up a particular name and returns the first one it finds
lookup(Extend(?n1, ?v, ?env), ?n2) == if ?n1 = ?n2 then ?v else lookup(?env, ?n2)

# Done is the intial continuation
apply_cont(Done, ?val) == ?val

# the same, insufficient, test as in direct_terp.req:
ev(App(Lambda(x, Sym(x)), Quote(123)), Empty, Done)

# does not terminate
ev(App(Lambda(x, App(Sym(x), Sym(x))), Lambda(x, App(Sym(x), Sym(x)))), Empty, Done)