Try and Implement delconts

.gitignore

@@ -0,0 +1,2 @@
+benchmarks.sh
+telescope

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 _) = "<closure>"
+    | 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 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

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 _) = "<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

main.sml

@@ -1,86 +1,4 @@
-(* Lambda term (encoded using de bruijn indices), booleans and delimited continuations *)
+open LambdaCal
-
-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 _) = "<closure>"
-  | pretty_print_value (BoolV b) = Bool.toString b
-  | pretty_print_value (IntV n) = Int64.toString n
-  | pretty_print_value Loop = "<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 "<infinite loop>"
-  | 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)
-
 (* 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
+exception InvalidAlgo
-val _ = print (pretty_print_value (evaluate term))
-val _ = print "\n"
 
+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"

telescope.mlb

@@ -0,0 +1,4 @@
+$(SML_LIB)/basis/basis.mlb
+lambda_calculus.sml
+lambda_calculus_delconts.sml
+main.sml