From f6c861d5a1456b29ef7c2fe9dab1f835c71cb20a Mon Sep 17 00:00:00 2001 From: Francesco Magliocca Date: Wed, 6 Apr 2022 22:10:05 +0200 Subject: [PATCH] Try and Implement delconts --- .gitignore | 2 + lambda_calculus.sml | 82 ++++++++++++++++++++++++++ lambda_calculus_delconts.sml | 106 +++++++++++++++++++++++++++++++++ main.sml | 110 +++++++---------------------------- telescope.mlb | 4 ++ 5 files changed, 216 insertions(+), 88 deletions(-) create mode 100644 .gitignore create mode 100644 lambda_calculus.sml create mode 100644 lambda_calculus_delconts.sml create mode 100644 telescope.mlb diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..af82b0f --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +benchmarks.sh +telescope diff --git a/lambda_calculus.sml b/lambda_calculus.sml new file mode 100644 index 0000000..0a26898 --- /dev/null +++ b/lambda_calculus.sml @@ -0,0 +1,82 @@ +structure LambdaCal = struct + (* Lambda term (encoded using de bruijn indices), booleans *) + 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 + and builtin_op = Sum | Sub | LessThan | Equal + + (* Value, the result of a computation *) + datatype value = + Closure of env * term + | 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 _) = "" + | pretty_print_value (BoolV b) = Bool.toString b + | pretty_print_value (IntV n) = Int64.toString n + | pretty_print_value 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 "" + | unpack_recursion x = x + + fun eval (_, Bool b) = BoolV b + | eval (_, Int i) = IntV i + | eval (env, Branch (cond, trueb, falseb)) = eval_branch (env, eval (env, cond), trueb, falseb) + | eval (env, Var idx) = unpack_recursion (env_lookup (idx, env)) + + | eval (env, Lambda t) = Closure (env, t) + | eval (env, App (lhs, rhs)) = eval_app (env, eval (env, lhs), eval (env, rhs)) + | eval (env, BuiltinApp (oper, lhs, rhs)) = eval_builtin (oper, eval (env, lhs), eval (env, rhs)) + | eval (env, Fix body) = eval_fix (env, body) + + and eval_branch (env, BoolV true, trueb, _) = eval (env, trueb) + | eval_branch (env, BoolV false, _, falseb) = eval (env, falseb) + | eval_branch _ = raise Stuck "Condition is not a boolean" + + and eval_app (env, Closure (cEnv, body), arg) = eval (env_push_value (arg, cEnv), body) + | eval_app _= raise Stuck "Left term in application is not a lambda" + + and eval_builtin (Sum, IntV n1, IntV n2) = IntV (n1 + n2) + | eval_builtin (Sub, IntV n1, IntV n2) = IntV (n1 - n2) + | eval_builtin (LessThan, IntV n1, IntV n2) = BoolV (n1 < n2) + | eval_builtin (Equal, IntV n1, IntV n2) = BoolV (n1 = n2) + | eval_builtin _ = raise Stuck "Argument of builtin op is not integer" + + and eval_fix (env, body) = + let + (* Step 1. Augment the body with an infinite loop variable *) + val self = ref Loop + val new_env = env_push_ref (self, env) + val result = eval (new_env, body) + (* Here we tie the knot and assign self to the result of the evaluation *) + val _ = self := result + in + result + end + + fun evaluate t = eval (empty_env, t) +end diff --git a/lambda_calculus_delconts.sml b/lambda_calculus_delconts.sml new file mode 100644 index 0000000..755f1a3 --- /dev/null +++ b/lambda_calculus_delconts.sml @@ -0,0 +1,106 @@ +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 _) = "" + | pretty_print_value (Continuation _) = "" + | pretty_print_value (BoolV b) = Bool.toString b + | pretty_print_value (IntV n) = Int64.toString n + | pretty_print_value 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 "" + | 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 diff --git a/main.sml b/main.sml index 5737b0b..d9f3caa 100644 --- a/main.sml +++ b/main.sml @@ -1,86 +1,4 @@ -(* Lambda term (encoded using de bruijn indices), booleans and delimited continuations *) - -datatype builtin_op = Sum | Sub | LessThan | Equal - -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 - -(* Value, the result of a computation *) -datatype value = - Closure of env * term - | 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 _) = "" - | pretty_print_value (BoolV b) = Bool.toString b - | pretty_print_value (IntV n) = Int64.toString n - | pretty_print_value Loop = "" - - -exception UnboundVar - -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) - -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 "" - | unpack_recursion x = x - -fun eval (_, Bool b) = BoolV b - | eval (_, Int i) = IntV i - | eval (env, Branch (cond, trueb, falseb)) = eval_branch (env, eval (env, cond), trueb, falseb) - | eval (env, Var idx) = unpack_recursion (env_lookup (idx, env)) - | eval (env, Lambda t) = Closure (env, t) - | eval (env, App (lhs, rhs)) = eval_app (env, eval (env, lhs), eval (env, rhs)) - | eval (env, BuiltinApp (oper, lhs, rhs)) = eval_builtin (oper, eval (env, lhs), eval (env, rhs)) - | eval (env, Fix body) = eval_fix (env, body) - -and eval_branch (env, BoolV true, trueb, _) = eval (env, trueb) - | eval_branch (env, BoolV false, _, falseb) = eval (env, falseb) - | eval_branch _ = raise Stuck "Condition is not a boolean" - -and eval_app (env, Closure (cEnv, body), arg) = eval (env_push_value (arg, cEnv), body) - | eval_app _= raise Stuck "Left term in application is not a lambda" - -and eval_builtin (Sum, IntV n1, IntV n2) = IntV (n1 + n2) - | eval_builtin (Sub, IntV n1, IntV n2) = IntV (n1 - n2) - | eval_builtin (LessThan, IntV n1, IntV n2) = BoolV (n1 < n2) - | eval_builtin (Equal, IntV n1, IntV n2) = BoolV (n1 = n2) - | eval_builtin _ = raise Stuck "Argument of builtin op is not integer" - -and eval_fix (env, body) = - let - (* Step 1. Augment the body with an infinite loop variable *) - val self = ref Loop - val new_env = env_push_ref (self, env) - val result = eval (new_env, body) - (* Here we tie the knot and assign self to the result of the evaluation *) - val _ = self := result - in - result - end - - -fun evaluate term = eval (empty_env, term) - +open LambdaCal (* 1. Can we implement recursion in terms of shift and reduce? Re recursion is an effect *) (* The term i want to define is: @@ -93,12 +11,14 @@ fix (\. (\. if $0 = 0 then 0 else $0 + $1 ($0 - 1))) val args = CommandLine.arguments() val input_string = hd args val input_number = valOf (Int64.fromString input_string) +val func_name = hd (tl args) +val method_name = hd (tl (tl args)) local val cond = BuiltinApp (Equal, Var 0, Int 0) fun decrement x = BuiltinApp (Sub, x, Int 1) fun add x y = BuiltinApp (Sum, x, y) - val branch = Branch (cond, Int 0, add (Var 0) (App (Var 1, decrement (Var 0)))) + val branch = Branch (cond, Int 0, add (Int 1) (App (Var 1, decrement (Var 0)))) in fun sum input_number = App (Fix (Lambda branch), Int input_number) end @@ -120,7 +40,6 @@ in fun iter_sum input_number = App (App (Fix (Lambda (Lambda branch)), Int 0), Int input_number) end - (* The term i want to define is: fix (\fib. (\x. if x < 2 then x else fib (x - 1) + fib (x - 2))) @@ -138,7 +57,22 @@ in fun fib input_number = App (Fix (Lambda branch), Int input_number) end -val term = sum input_number -val _ = print (pretty_print_value (evaluate term)) -val _ = print "\n" +exception InvalidAlgo +val algo = case func_name of + "sum" => sum + | "fib" => fib + | "iter_sum" => iter_sum + | _ => raise InvalidAlgo + +val term = algo input_number +val timer = Timer.startCPUTimer() +val _ = LambdaCal.pretty_print_value (LambdaCal.evaluate term) +val _ = print ((Int64.toString input_number) ^ " ") +val {usr, sys} = Timer.checkCPUTimer timer +val tot = Time.+ (usr, sys) + +fun showMs t = Time.toString t + +val _ = print (showMs tot) +val _ = print "\n" diff --git a/telescope.mlb b/telescope.mlb new file mode 100644 index 0000000..7cce208 --- /dev/null +++ b/telescope.mlb @@ -0,0 +1,4 @@ +$(SML_LIB)/basis/basis.mlb +lambda_calculus.sml +lambda_calculus_delconts.sml +main.sml