Delimited Continuations in Lambda Calculus in Soar

shift-reset.soar

# This is a lambda-calculus interpreter with shift and reset,
# an implementation of BRICS-RS-3-41 "An Operational Foundation for Delimited Continuations",
# by Biernacka, Biernacki, and Danvy.
#
# Mistakes, misunderstandings and terrible un-idiomatic Soar style by Johnicholas
#
#
# This is the grammar:
#
# A term can have a single outgoing ^reset leading to a reset.
# A reset has a single outgoing ^exp which leads to a term
#
# A term can have a single outgoing ^shift leading to a shift.
# A shift has a ^name which leads to an unstructured node,
# and an ^exp which leads to a term.
#
# A term can have a single outgoing ^app leading to a shift.
# A shift has a ^major which leads to a term,
# and a ^minor which leads to a term.
#
# A term can have a single outgoing ^var (variable reference) leading to a symbol.
#
# A term can have a single outgoing ^int (integer literal) leading to an integer.
#
# A term can have a single outgoing ^lam (lambda) leading to a lam
# A lam has a ^name which leads to a symbol,
# and a ^exp which leads to a term.
#
# A cont (continuation) can have a single outgoing ^appK1 (app continuation 1).
# An appK1 has a ^term leading to a term,
# an ^env leading to an environment,
# and a ^cont leading to a continuation.
#
# A cont can have a single outgoing ^appK2.
# An appK2 has a ^value leading to a value,
# and a ^cont leading to a continuation.
#
# A cont can have a single outgoing ^succK
# A ^succK has a ^cont leading to a continuation.
#
# A cont can be holeC1.
#
# A metacontinuation can have a single outgoing ^resetK leading to a resetK.
# A resetK has a ^cont leading to a continuation,
# and a ^metacont leading to a metacontinuation.
#
# a metacontinuation can be holeC2.
#
# An environment can be emptyenv.
#
# An environment can have a single ^bind leading to a bind
# A bind has a ^name leading to a symbol,
# a ^value leading to a value,
# and an ^env leading to an environment.
#
# A value can have a single ^cap (captured) leading to a continuation.
#
# A value can have a single ^clo (closure) leading to a closure.
# A closure has a ^name leading to a symbol,
# a ^exp leading to a term,
# and an ^env leading to an environment.
#
# A value can be an integer.
# 
#
###################### run
# run is an operator that takes a term (a.k.a. an exp),
# and location where to put the answer.
#
# In prolog:
#
# run(T, Out) :- !,
#   step(T, emptyenv, holeC1, holeC2, Out).

sp {run*initialize
  (state <s> ^superstate.operator <o>)
  (<o> ^name run ^term <t> ^return-to <r>)
-->
  (<s> ^name run ^term <t> ^return-to <r>)}

sp {run*propose*step
  (state <s> ^name run ^term <t> ^return-to <r>)
-->
  (<s> ^operator <o> +)
  (<o> ^name step ^term <t> ^env emptyenv ^cont holeC1 ^metacont holeC2 ^return-to <r>)}

######################### step
# step is an operator that takes 
# an exp, an environment, a cont, a metacont,
# and a place to put the answer
#
# In Prolog:
#
# step(int(N), _Env, C1, C2, Out) :- !,
#   cont1(C1, N, C2, Out).
# step(var(X), Env, C1, C2, Out) :- !,
#   lookup(Env, X, C1, C2, Out).
# step(lam(X, Exp), Env, C1, C2, Out) :- !,
#   cont1(C1, clo(X, Exp, Env), C2, Out).
# step(app(T0, T1), Env, C1, C2, Out) :- !,
#   step(T0, Env, appK1(T1, Env, C1), C2, Out).
# step(succ(Exp), Env, C1, C2, Out) :- !,
#   step(Exp, Env, succK(C1), C2, Out).
# step(shift(K, Exp), Env, C1, C2, Out) :- !,
#   step(Exp, bind(K, cap(C1), Env), holeC1, C2, Out).
# step(reset(Exp), Env, C1, C2, Out) :- !,
#   step(Exp, Env, holeC1, resetK(C1, C2), Out).
 
sp {step*initialize
  (state <s> ^superstate.operator <o>)
  (<o> ^name step ^term <t> ^env <e> ^cont <c1> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^name step ^term <t> ^env <e> ^cont <c1> ^metacont <c2> ^return-to <r>)}

sp {step*int*propose*cont1
  (state <s> ^name step ^term.int <n> ^cont <c1> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^operator <o> +)
  (<o> ^name cont1 ^cont <c1> ^value <n> ^metacont <c2> ^return-to <r>)}

sp {step*var*propose*lookup
  (state <s> ^name step ^term.var <x> ^env <env> ^cont <c1> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^operator <o> +)
  (<o> ^name lookup ^env <env> ^key <x> ^cont <c1> ^metacont <c2> ^return-to <r>)}

sp {step*lam*propose*cont1
  (state <s> ^name step ^term.lam <l> ^env <env> ^cont <c1> ^metacont <c2> ^return-to <r>)
  (<l> ^name <x> ^exp <exp>)
-->
  (<s> ^operator <o> +)
  (<o> ^name cont1 ^cont <c1> ^value.clo <closure> ^metacont <c2> ^return-to <r>)
  (<closure> ^name <x> ^exp <exp> ^env <env>)}

sp {step*app*propose*recurse
  (state <s> ^name step ^term.app <a> ^env <env> ^cont <c1> ^metacont <c2> ^return-to <r>)
  (<a> ^major <t0> ^minor <t1>)
-->
  (<s> ^operator <o> +)
  (<o> ^name step ^term <t0> ^env <env> ^cont.appK1 <ak> ^metacont <c2> ^return-to <r>)
  (<ak> ^term <t1> ^env <env> ^cont <c1>)}

sp {step*succ*propose*recurse
  (state <s> ^name step ^term.succ <t> ^env <env> ^cont <c1> ^metacont <c2> ^return-to <r>)
  (<t> ^exp <exp>)
-->
  (<s> ^operator <o> +)
  (<o> ^name step ^term <exp> ^env <env> ^cont.succK.cont <c1> ^metacont <c2> ^return-to <r>)}

sp {step*shift*propose*recurse
  (state <s> ^name step ^term.shift <sh> ^env <env> ^cont <c1> ^metacont <c2> ^return-to <r>)
  (<sh> ^name <k> ^exp <exp>)
-->
  (<s> ^operator <o> +)
  (<o> ^name step ^term <exp> ^env.bind <b> ^cont holeC1 ^metacont <c2> ^return-to <r>)
  (<b> ^name <k> ^value.cap <c1> ^env <env>)}

sp {step*reset*propose*recurse
  (state <s> ^name step ^term.reset.exp <exp> ^env <env> ^cont <c1> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^operator <o> +)
  (<o> ^name step ^term <exp> ^env <env> ^cont holeC1 ^metacont.resetK <resetK> ^return-to <r>)
  (<resetK> ^cont <c1> ^metacont <c2>)}

############################ lookup
# lookup is an operator that takes:
#  an environment, a key, a cont and metacont, and where to put the answer.
#
# In Prolog:
#  lookup(bind(K1, V, _Env), K2, C1, C2, Out) :- K1 = K2, !,
#    cont1(C1, V, C2, Out).
#  lookup(bind(K1, _V, Env), K2, C1, C2, Out) :- K1 \= K2, !,
#    lookup(Env, K2, C1, C2, Out).
#
sp {lookup*initialize
  (state <s> ^superstate.operator <o>)
  (<o> ^name lookup ^env <e> ^key <k> ^cont <c1> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^name lookup ^env <e> ^key <k> ^cont <c1> ^metacont <c2> ^return-to <r>)}

sp {lookup*found*propose*cont1
  (state <s> ^name lookup ^env.bind <b> ^key <k> ^cont <c1> ^metacont <c2> ^return-to <r>)
  (<b> ^name <k> ^value <v>)
-->
  (<s> ^operator <o> +)
  (<o> ^name cont1 ^cont <c1> ^value <v> ^metacont <c2> ^return-to <r>)}

sp {lookup*notfound*propose*recurse
  (state <s> ^name lookup ^env.bind <b> ^key <k1> ^cont <c1> ^metacont <c2> ^return-to <r>)
  (<b> ^name <k2> <> <k1> ^env <env>)
-->
  (<s> ^operator <o> +)
  (<o> ^name lookup ^env <env> ^key <k1> ^cont <c1> ^metacont <c2> ^return-to <r>)}


############################ cont
# Cont1 is an operator that takes
# a continuation, a value, a metacontinuation, and a place to put the result.
#
# In Prolog:
# cont1(holeC1, V, C2, Out) :- !,
#   cont2(C2, V, Out).
# cont1(appK1(Exp, Env, C1), V, C2, Out) :- !,
#   step(Exp, Env, appK2(V, C1), C2, Out).
# cont1(appK2(clo(X, Exp, Env), C1), V, C2, Out) :- !,
#   step(Exp, bind(X, V, Env), C1, C2, Out).
# cont1(appK2(cap(C1p), C1), V, C2, Out) :- !,
#   cont1(C1p, V, resetK(C1, C2), Out).
# cont1(succK(C1), N, C2, Out) :- !,
#   NPlus is N + 1,
#   cont1(C1, NPlus, C2, Out).
#
sp {cont1*initialize
  (state <s> ^superstate.operator <o>)
  (<o> ^name cont1 ^cont <c1> ^value <v> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^name cont1 ^cont <c1> ^value <v> ^metacont <c2> ^return-to <r>)}

sp {cont1*holeC1*propose*cont2
  (state <s> ^name cont1 ^cont holeC1 ^value <v> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^operator <o> +)
  (<o> ^name cont2 ^metacont <c2> ^value <v> ^return-to <r>)}

sp {cont1*appK1*propose*step
  (state <s> ^name cont1 ^cont.appK1 <a1> ^value <v> ^metacont <c2> ^return-to <r>)
  (<a1> ^term <t> ^env <env> ^cont <c1>)
-->
  (<s> ^operator <o> +)
  (<o> ^name step ^term <t> ^env <env> ^cont.appK2 <a2> ^metacont <c2> ^return-to <r>)
  (<a2> ^value <v> ^cont <c1>)}

sp {cont1*appK2*clo*propose*step
  (state <s> ^name cont1 ^cont.appK2 <a2> ^value <v> ^metacont <c2> ^return-to <r>)
  (<a2> ^value.clo <closure> ^cont <c1>)
  (<closure> ^name <x> ^exp <exp> ^env <env>)
-->
  (<s> ^operator <o> +)
  (<o> ^name step ^term <exp> ^env.bind <b> ^cont <c1> ^metacont <c2> ^return-to <r>)
  (<b> ^name <x> ^value <v> ^env <env>)}

sp {cont1*appK2*cap*propose*cont1
  (state <s> ^name cont1 ^cont.appK2 <a2> ^value <v> ^metacont <c2> ^return-to <r>)
  (<a2> ^value.cap <c1p> ^cont <c1>)
-->
  (<s> ^operator <o> +)
  (<o> ^name cont1 ^cont <c1p> ^value <v> ^metacont.resetK <rk> ^return-to <r>)
  (<rk> ^cont <c1> ^metacont <c2>)}

sp { cont1*succK*propose*recurse
  (state <s> ^name cont1 ^cont.succK.cont <c1> ^value <n> ^metacont <c2> ^return-to <r>)
-->
  (<s> ^operator <o> +)
  (<o> ^name cont1 ^cont <c1> ^value (+ <n> 1) ^metacont <c2> ^return-to <r>)}




############################ cont2
# cont2 is an operator that takes a metacontinuation, a value,
# and where to put the answer.
#
# In Prolog:
# cont2(resetK(C1, C2), V, Out) :- !,
#   cont1(C1, V, C2, Out).
# cont2(holeC2, V, Out) :- !,
#   Out = V.

sp {cont2*initialize
  (state <s> ^superstate.operator <o>)
  (<o> ^name cont2 ^metacont <c2> ^value <v> ^return-to <r>)
-->
  (<s> ^name cont2 ^metacont <c2> ^value <v> ^return-to <r>)}

sp {cont2*resetK*propose*cont1
  (state <s> ^name cont2 ^metacont.resetK <rk> ^value <v> ^return-to <r>)
  (<rk> ^cont <c1> ^metacont <c2>)
-->
  (<s> ^operator <o> +)
  (<o> ^name cont1 ^cont <c1> ^value <v> ^metacont <c2> ^return-to <r>)}

sp {cont2*holeC2*done
  (state <s> ^name cont2 ^metacont holeC2 ^value <v> ^return-to <r>)
-->
  (<r> ^run-done <v>)}