[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Daniel C. Wang]

This is a multi-part message in MIME format.
--------------090607040003080506040707
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit

Attached is SML file that sketchs how to do the interoperation expressed as 
a source to source translation of code to be linked into the interpter.

It deals with recursive polymorphic structures.
Each coercion between the generic and hosted representation is constant time.

--------------090607040003080506040707
Content-Type: text/plain;
 name="eval.sml"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline;
 filename="eval.sml"

(* Generic Interpreter *)
structure Eval =
  struct
    type var = string
    datatype exp =
      Val of value
    | App of exp * exp
    | Lam of var * exp
    | Var of var
    and value =
      I of int
    | P of value * value
    | F of value -> value
    | A of unit -> value (* abstract value *) (* using thunk to simulate existential type *)

    fun empty _ = raise (Fail "not found")
    fun bind (env,x,v) y =
      if x = y then v else env y
    fun eval env (Val (A av)) = (av ())
      | eval env (Val v) = v
      | eval env (App(e1,e2)) =
      (case (eval env e1,eval env e2) of
	 (F f,v) => f v
       | _ => raise (Fail "bad app"))
      | eval env (Lam (x,e)) =
	 (F (fn v => eval (bind (env,x,v)) e))
      | eval env (Var x) = (env x)
  end

(* Polymorphic Input source program to be linked into interpret *)
structure Lst =
  struct
    datatype 'a list = Nil | Cons of ('a * 'a list)

    fun length Nil = 0
      | length (Cons(_,xs)) = 1 + length xs

    fun sum Nil = 0
      | sum (Cons(x,xs)) = x + sum xs

    fun mkLst 0 = Nil
      | mkLst n = (Cons(n,mkLst (n-1)))
  end

(* Produced via type-directed source translation of input source. *)
structure Lst =
  struct
    (* generic abstract interface *)
    datatype ('a,'b) listF =
      Nil
    | Cons of ('a * 'b)
      
    fun lengthF unwrap Nil =  0
      | lengthF unwrap (Cons(_,b)) = 1 + lengthF unwrap (unwrap b)
      
    fun sumF unwrap Nil = 0
      | sumF unwrap (Cons(x,xs)) = x + sumF unwrap (unwrap xs)
      
    fun mkLstF wrap 0 = wrap Nil
      | mkLstF wrap n = wrap (Cons(n,mkLstF wrap (n-1)))

  (* exported to the normal compiled "host" SML code that never interacts with our interpret *)
    datatype 'a list = Fix of ('a,'a list) listF
    fun length (Fix x) = lengthF (fn Fix x => x) x
    fun sum (Fix x) = sumF (fn Fix x => x) x
    fun mkLst x = mkLstF Fix x
  end

(* generated automatically *)	 
structure InitEnv :> sig
  val init_env : Eval.var -> Eval.value
end =
  struct
    open Lst
    open Eval
    (* each coercion is constant time *)
    fun wrapLst wrap Nil = I 0
      | wrapLst wrap (Cons(x,xs)) = P(wrap x,xs)

    fun unwrapLst unwrap (I 0) = Nil
      | unwrapLst unwrap (P(x,xs)) = Cons(unwrap x,xs)
      | unwrapLst unwrap (A av) = unwrapLst unwrap (av())
      | unwrapLst unwrap _ = raise (Fail "bad list")

    fun wrapInt i = I i
    fun unwrapInt (I i) = i
      | unwrapInt (A av) = unwrapInt (av ())
      | unwrapInt _ = raise (Fail "bad int")

    fun id x = x
    val interp_length = F (fn x => wrapInt (lengthF (unwrapLst id) (unwrapLst id x)))
    val interp_sum = F (fn x => wrapInt (sumF (unwrapLst unwrapInt) (unwrapLst unwrapInt x)))
    val interp_mkLst = F (fn x => (mkLstF (wrapLst wrapInt) (unwrapInt x)))

    (* coerce a native host list to an interp list *)
    fun interpLst wrap (Fix Nil) = (I 0)
      | interpLst wrap (Fix (Cons(x,xs))) = (P(wrap x,A (fn () => interpLst wrap xs)))

    fun bind_lst xs = List.foldl (fn ((x,v),env) => bind (env,x,v)) empty xs
    val init_env = 
     bind_lst [("length",interp_length),
	       ("sum",interp_sum),
	       ("mkLst",interp_mkLst),
	       ("l",interpLst wrapInt (mkLst 10))]
  end

structure Example =
  struct
    open Eval
    val prog1 = App(Var "length",Var "l")
    val prog2 = App(Var "sum",Var "l")
    val prog3 = App(Var "length",App(Var "mkLst",Val (I 10)))
    val prog4 = App(Var "sum",App(Var "mkLst",Val (I 10)))
    fun run p = Eval.eval InitEnv.init_env p
end
--------------090607040003080506040707--