CC Machine in OCaml

(*                                                              -*- OCaml -*-
   [email protected]
   Released under the terms of the GNU Lesser General Public License.

   The CC Machine -- an ISWIM interpreter

   The specification of this eval_cc function comes from Felleisen & Flatt --
   Programming Languages and Lambda Calculi.

   See http://www.cs.uvm.edu/~dvanhorn/scheme/cc.scm for a Scheme version of
   this machine.

   TODO: Make delta and base types parameterizable.
*)

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
and 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 | Times | Exp
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 ->
	if f x then let (prefix, suffix) = recur rest in
	x::prefix, suffix
	else [], x::rest
  in
  recur ls
;;

(* delta : primop -> term list -> term *)
let delta op args =
  match args with
    Value(Base(Int x))::rest ->
      let y =
	match rest with
	| [Value(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) -> Value(Base b)
  | Value(Var y) ->
      if x=y then Value v
      else Value(Var y)
  | Value(Lambda(y,n)) ->
      if x=y then Value(Lambda(y,n))
      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))
;;


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

   The 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 ->
      delta o args, 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
;;

(* eval_cc : term -> result *)
let eval_cc 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)
;;


(*  ((lambda (x) x) ((lambda (x) x) 5))  *)
eval_cc (App (Value (Lambda ("x", Value (Var "x"))),
	      App (Value (Lambda ("x", Value (Var "x"))),
		   Value (Base (Int 5)))));;

(* - : result = Result (Int 5) *)