107 lines
3.9 KiB
Standard ML
107 lines
3.9 KiB
Standard ML
structure LambdaCalcDelConts = struct
|
|
(* Lambda term (encoded using de bruijn indices),
|
|
booleans and delimited continuations *)
|
|
datatype term =
|
|
Bool of bool
|
|
| Int of Int64.int
|
|
| Branch of term * term * term
|
|
| Var of int
|
|
| Lambda of term
|
|
| App of term * term
|
|
| BuiltinApp of builtin_op * term * term
|
|
| Fix of term
|
|
| Shift of term
|
|
| Reset of term
|
|
and builtin_op = Sum | Sub | LessThan | Equal
|
|
|
|
(* Value, the result of a computation *)
|
|
datatype value =
|
|
Closure of env * term
|
|
| Continuation of value -> value
|
|
| BoolV of bool
|
|
| IntV of Int64.int
|
|
| Loop
|
|
|
|
(* Why a ref? Because of Fix! We want to update this value post-hoc *)
|
|
and env = Env of value ref list
|
|
|
|
|
|
fun pretty_print_value (Closure _) = "<closure>"
|
|
| pretty_print_value (Continuation _) = "<cont>"
|
|
| pretty_print_value (BoolV b) = Bool.toString b
|
|
| pretty_print_value (IntV n) = Int64.toString n
|
|
| pretty_print_value Loop = "<loop>"
|
|
|
|
|
|
val empty_env = Env []
|
|
|
|
fun env_push_ref (r, Env e) = Env (r :: e)
|
|
fun env_push_value (v, e) = env_push_ref (ref v, e)
|
|
|
|
exception UnboundVar
|
|
|
|
fun env_lookup (idx, Env e) = !(List.nth (e, idx))
|
|
handle Subscript => raise UnboundVar
|
|
|
|
exception Stuck of string
|
|
|
|
(* Handle a possibly recursion record *)
|
|
fun unpack_recursion Loop = raise Stuck "<infinite loop>"
|
|
| unpack_recursion x = x
|
|
|
|
fun identity x = x
|
|
|
|
(* To interpret continuations, we define a continuation
|
|
passing style evaluator. This makes them very straightforward to implement.
|
|
Although WARNING: performances are degraded.
|
|
A first solution is defunctionalization. But it is not enough! *)
|
|
|
|
fun eval env (Bool b) k = k (BoolV b)
|
|
| eval env (Int n) k = k (IntV n)
|
|
| eval env (Branch (cond, trueb, falseb)) k = eval env cond (branch_cont env trueb falseb k)
|
|
| eval env (Var idx) k = k (unpack_recursion (env_lookup (idx, env)))
|
|
| eval env (Lambda t) k = k (Closure (env, t))
|
|
| eval env (App (lhs, rhs)) k = eval env lhs (app_cont env rhs k)
|
|
| eval env (BuiltinApp (oper, lhs, rhs)) k = eval env lhs (builtin_app_cont env oper rhs k)
|
|
| eval env (Fix body) k =
|
|
let val self = ref Loop
|
|
in eval (env_push_ref (self, env)) body (fix_cont self k)
|
|
end
|
|
|
|
| eval env (Reset body) k =
|
|
(* The identity is what makes the continuation delimited!
|
|
We don't capture the full program continuation, but just the chunk
|
|
inside the reset block
|
|
*)
|
|
k (eval env body identity)
|
|
|
|
| eval env (Shift body) k = app_cont2 env body k (Continuation k)
|
|
|
|
and branch_cont env trueb _ k (BoolV true) = eval env trueb k
|
|
| branch_cont env _ falseb k (BoolV false) = eval env falseb k
|
|
| branch_cont _ _ _ _ _ = raise Stuck "If conditional is not a boolean"
|
|
|
|
and app_cont env rhs k (Closure (benv, body)) = eval env rhs (app_cont2 benv body k)
|
|
(* Observe how in this clause the continuation k is discarded! We are following a different path! *)
|
|
| app_cont env rhs _ (Continuation capt_k) = eval env rhs (invoke_continuation capt_k)
|
|
| app_cont _ _ _ _ = raise Stuck "Left hand side of application is not a function nor continuation"
|
|
|
|
and app_cont2 env body k arg = eval (env_push_value (arg, env)) body k
|
|
and invoke_continuation capt_k arg = capt_k arg
|
|
|
|
and builtin_app_cont env oper rhs k (IntV n1) = eval env rhs (builtin_app_cont2 n1 oper k)
|
|
| builtin_app_cont _ _ _ _ _ = raise Stuck "Builtin op left argument is not an int"
|
|
and builtin_app_cont2 n1 Sum k (IntV n2) = k (IntV (n1 + n2))
|
|
| builtin_app_cont2 n1 Sub k (IntV n2) = k (IntV (n1 - n2))
|
|
| builtin_app_cont2 n1 LessThan k (IntV n2) = k (BoolV (n1 < n2))
|
|
| builtin_app_cont2 n1 Equal k (IntV n2) = k (BoolV (n1 = n2))
|
|
| builtin_app_cont2 _ _ _ _ = raise Stuck "Builtin op riht argument is not an int"
|
|
|
|
and fix_cont self k v =
|
|
let val _ = self := v
|
|
in k v
|
|
end
|
|
|
|
fun evaluate term = eval empty_env term identity
|
|
end
|