CC, SCC, CK, CEK Machines.

I've added the CEK machine to the list and refactored things into modules.

Coming soon: SECD machine, parser.

-d




(*                                                              -*- OCaml -*-
   Copyright (c) 2003 David Van Horn
   Licensed under the Academic Free License version 2.0

   The CC, CK and CEK Machines -- ISWIM interpreters
   [email protected]

   The specification of the Cc.eval, Ck.eval and Cek.eval functions come from
   Felleisen & Flatt -- Programming Languages and Lambda Calculi.

   TODO: Make delta and base types parameterizable.
*)

module Term =
  struct
    open List
    type term =
      | Value of value
      | App of term * term
      | AppPrim of primop * term list
    and value =
      | Base of base
      | Var of var
      | Lambda of var * term
    and var = string
    and base = Int of int | False | True
    and primop = Add1 | Sub1 | Plus | Minus
    and result = Result of base | Function

(*
   span : ('a -> bool) -> 'a list -> 'a list * 'a list
   An old scheme friend

   Span splits the list into the longest initial prefix whose elements all
   satisfy the predicate f, and the remaining tail. Cf. Olin Shivers's SRFI-1.
*)
    let span f ls =
      let rec recur = function
	| [] -> [], []
	| x::rest as l ->
	    if f x then let (prefix, suffix) = recur rest in
	    x::prefix, suffix
	    else [], l
      in
      recur ls
	
(* delta : primop -> base list -> term *)
    let delta op args =
      match args with
	Base(Int x)::rest ->
	  let y =
	    match rest with
	    | [Base(Int y)] -> y
	    | [] -> 1
	  in
	  let result =
	    match op with
	    | Add1 | Plus -> x+y
	    | Sub1 | Minus ->
		let sum = x-y in
		if sum <= 0 then 0 else sum
	  in
	  Value(Base (Int result))
	
    let is_value = function
      | Value v -> true
      | _ -> false
	    	
    let is_base = function
      | Value (Base b) -> true
      | _ -> false
	
(*
   gen_var : unit -> string

   Returns a fresh variable name of the form "zn" where n is an integer
   (so don't use variable of this form!).
*)
    let gen_var =
      let i = ref 0 in
      fun () ->
	i := !i+1;
	"z" ^ (string_of_int !i)
		
(*
   substitute : term -> var -> value -> term

   Substitutes v for x in m.
*)
    let rec substitute m x v =
      match m with
      | Value(Base b) -> m
      | Value(Var y) ->
	  if x=y then Value v
	  else m
      | Value(Lambda(y,n)) ->
	  if x=y then m
	  else let z = gen_var () in
	  Value(Lambda(z, (substitute (substitute n y (Var z)) x v)))
      | App(n,p) ->
	  App(substitute n x v, substitute p x v)
      | AppPrim(o, tlist) ->
	  AppPrim(o, (map (fun t -> substitute t x v) tlist))
	
  end

module Cc =
  struct
    open Term
    open List
    type context =
      | CEmptyHole
      | CInHole of context * context
      | CAppV of value * context
      | CAppE of context * term
      | CAppPrim of primop * value list * context * term list

(*
   cc : term * context -> term * context

   The CC Machine state transition function.
*)
(*
    let cc = function
      | App(m,n), e
	when not (is_value m) ->
	  m, CInHole(e, CAppE(CEmptyHole, n))
      | App(Value(v), m), e
	when not (is_value m) ->
	  m, CInHole(e, CAppV(v, CEmptyHole))
      | AppPrim(o, args), e
	when for_all is_base args ->
	  let blist = (map (fun (Value v) -> v) args) in
	  delta o blist, e
      | AppPrim(o, args), e ->
	  let (vlist, m::tlist) = span is_value args in
	  let vlist = map (fun (Value v) -> v) vlist in
	  m, CInHole(e, CAppPrim(o, vlist, CEmptyHole, tlist))
      | App(Value(Lambda(x,m)), Value v), e ->
	  substitute m x v, e
      | Value v, CInHole(e, CAppV(u, CEmptyHole)) ->
	  App(Value u, Value v), e
      | Value v, CInHole(e, CAppE(CEmptyHole, n)) ->
	  App(Value v, n), e
      | Value v, CInHole(e, CAppPrim(o, vlist, CEmptyHole, tlist)) ->
	  let vlist = map (fun x -> (Value x)) vlist in
	  AppPrim(o, vlist@[(Value v)]@tlist), e
*)

(*
   Simplified version of CC state transitions.
*)
    let cc = function
      | App(m,n), e ->
	  m, CInHole(e, CAppE(CEmptyHole, n))
      | AppPrim(o, m::tlist), e ->
	  m, CInHole(e, CAppPrim(o, [], CEmptyHole, tlist))
      | Value v, CInHole(e, CAppV(Lambda (x,m), CEmptyHole)) ->
	  substitute m x v, e
      |  Value v, CInHole(e, CAppE(CEmptyHole, n)) ->
	  n, CInHole(e, CAppV(v, CEmptyHole))
      | (Value b) as v, CInHole(e, CAppPrim(o, blist, CEmptyHole, []))
	when is_base v ->
	  delta o (blist@[b]), e
      | Value v, CInHole(e, CAppPrim(o, vlist, CEmptyHole, n::tlist)) ->
	  n, CInHole(e, CAppPrim(o, vlist@[v], CEmptyHole, tlist))
	
    let eval term =
      let rec loop = function
	| Value(Base b), CEmptyHole -> (Result b)
	| Value(Lambda (x,m)), CEmptyHole -> Function
	| term, context -> loop (cc (term, context))
      in
      loop (term, CEmptyHole)
  end

(* For use in the CK Machine *)
module Ck =
  struct
    open Term
    open List
    type kont =
      | Mt
      | Fun of value * kont
      | Arg of term * kont
      | Opd of value list * primop * term list * kont

(*
   ck : term * kont -> term * kont

   The CK Machine state transition function.
 *)
    let ck = function
      | App(m,n), k ->
	  m, Arg(n, k)
      | AppPrim(o, m::tlist), k ->
	  m, Opd([], o, tlist, k)
      | Value v, Fun(Lambda (x,m), k) ->
	  substitute m x v, k
      | Value v, Arg(n, k) ->
	  n, Fun(v, k)
      | Value(Base b), Opd(vlist, o, [], k)
	when for_all is_base (map (fun v -> (Value v)) vlist) ->
	  delta o (vlist@[(Base b)]), k
      | Value v, Opd(vlist, o, n::tlist, k) ->
	  n, Opd([v]@vlist, o, tlist, k)
	
    let eval term =
      let rec loop = function
	| Value(Base b), Mt -> (Result b)
	| Value(Lambda (x,m)), Mt -> Function
	| term, k -> loop (ck (term, k))
      in
      loop (term, Mt)	
  end

module Cek =
  struct
    open Term
    open List
    exception UnboundVariable
    type k =
      | Mt
      | Fun of value * environment * k
      | Arg of term * environment * k
      | Opd of (value * environment) list * primop * (term * environment) list * k
    and environment = EmptyEnv | Env of (term -> term * environment)

(* In the CEK machine we use environment update rather than substitution *)

(* environment -> term -> term * environment *)
    let environment_lookup e t =
      match e with
      | Env(f) -> f t
      | EmptyEnv -> raise UnboundVariable
	
(*  environment -> term -> term -> environment -> environment *)
    let environment_update e x t e' =
      Env (fun term ->
	if (term = x) then (t,e')
	else environment_lookup e term)

(*
   cek : (term * environment) * k -> (term * environment) * k

   The CEK Machine state transition function.
*)
    let cek = function
      | (App(m,n), e), k ->
	  (m, e), Arg(n, e, k)
      | (AppPrim(o, m::tlist), e), k ->
	  (m, e), Opd([], o, (map (fun t -> (t, e)) tlist), k)
      | (Value(Var _) as x, e), k ->
	  environment_lookup e x, k
      | ((Value _) as v, e), Fun(Lambda(x,m), e', k) ->
	  (m, environment_update e' (Value (Var x)) v e), k
      | (Value v, e), Arg(n, e', k) ->
	  (n, e'), Fun(v, e, k)
      | (Value(Base b), e), Opd(vclosures, o, [], k) ->
	  let blist = (map (function (v,e) -> v) vclosures) in
	  (delta o (blist@[(Base b)]), EmptyEnv), k
      | (Value v, e), Opd(vclosures, o, (n,e')::tclosures, k) ->
	  (n, e'), Opd((v,e)::vclosures, o, tclosures, k)
	
    let eval term =
      let rec loop = function
	| (Value(Base b), e), Mt -> (Result b)
	| (Value(Lambda (x,m)), e), Mt -> Function
	| (t, e), k -> loop (cek ((t, e), k))
      in
      loop ((term, EmptyEnv), Mt)
  end

;;

open Term;;

Cc.eval (App (Value (Lambda ("x", Value (Var "x"))),
	      App (Value (Lambda ("x", Value (Var "x"))),
		   Value (Base (Int 5)))))
;;

Ck.eval (App (Value (Lambda ("x", Value (Var "x"))),
	      App (Value (Lambda ("x", Value (Var "x"))),
		   Value (Base (Int 5)))))
;;
Cek.eval(App (Value (Lambda ("x", Value (Var "x"))),
	      App (Value (Lambda ("x", Value (Var "x"))),
		   Value (Base (Int 5)))))
;;
(* - : result = Result (Int 5) *)

Cc.eval (App (Value (Lambda ("x", AppPrim(Add1, [Value (Var "x")]))),
	      App (Value (Lambda ("x", Value (Var "x"))),
		   Value (Base (Int 5)))))
;;
Ck.eval (App (Value (Lambda ("x", AppPrim(Add1, [Value (Var "x")]))),
	      App (Value (Lambda ("x", Value (Var "x"))),
		   Value (Base (Int 5)))))
;;
Cek.eval (App (Value (Lambda ("x", AppPrim(Add1, [Value (Var "x")]))),
	       App (Value (Lambda ("x", Value (Var "x"))),
		    Value (Base (Int 5)))))
;;
(* - : result = Result (Int 6) *)

(*
   Useful for seeing how evaluation proceeds.
   #trace cc;;
*)