mixmod.ml

(* $Id: mixmod.ml,v 1.2 2004/04/02 06:32:00 garrigue Exp $ *)

(* Basic interfaces *)

(* The types involved in our recursion *)
module type ET = sig type exp end
(* The recursive operations on our our types *)
module type E =
  sig
    module T : ET
    val eval : (string * T.exp) list -> T.exp -> T.exp
  end
(* A functor building the type of the conversion module between two types *)
module CW(T : ET)(L : ET) = struct
  module type C = sig
    val inj : L.exp -> T.exp
    val proj : T.exp -> L.exp option
  end
end
(* The identity conversion module *)
module CF = struct
  let inj x = x
  let proj x = Some x
end

(* Variables are common to lambda and expr *)

module VarT = struct
  type exp = [`Var of string]
end
module Var(E : E)(C : CW(E.T)(VarT).C) =
  struct
    module T = VarT
    let eval sub (`Var s as v : T.exp) =
      try List.assoc s sub with Not_found -> C.inj v
  end

(* The lambda language: free variables, substitutions, and evaluation *)
let gensym = let n = ref 0 in fun () -> incr n; "_" ^ string_of_int !n

module LamT(T : ET) = struct
  type exp = [VarT.exp | `Abs of string * T.exp | `App of T.exp * T.exp]
end
module Lam(E : E)(C : CW(E.T)(LamT(E.T)).C) =
  struct
    module T = LamT(E.T)
    module CVar = struct
      type t = VarT.exp
      (* All conversion modules use the same code, but we need to
         know the concrete types to build our coercions *)
      let inj = (C.inj :> t -> _)
      let proj x = match C.proj x with
        Some #t as y -> y
      | _ -> None
    end
    module LVar = Var(E)(CVar)

    let eval subst : T.exp -> E.T.exp = function
        #CVar.t as v -> LVar.eval subst v
      | `App(l1, l2) ->
          let l2' = E.eval subst l2 in
          let l1' = E.eval subst l1 in
          begin match C.proj l1' with
            Some (`Abs (s, body)) ->
              E.eval [s,l2'] body
          | _ ->
              C.inj (`App (l1', l2'))
          end
      | `Abs(s, l1) ->
          let s' = gensym () in
          C.inj (`Abs(s', E.eval ((s,C.inj (`Var s'))::subst) l1))
  end

module rec LamF : E with module T = LamT(LamF.T) = Lam(LamF)(CF)
let e1 = LamF.eval [] (`App(`Abs("x",`Var"x"), `Var"y"));;

(* The expr language of arithmetic expressions *)

module ExprT(T : ET) = struct
  type exp =
      [ `Var of string | `Num of int
      | `Add of T.exp * T.exp | `Mult of T.exp * T.exp]
end

module Expr(E : E)(C : CW(E.T)(ExprT(E.T)).C) =
  struct
    module T = ExprT(E.T)
    module CVar = struct
      type t = VarT.exp
      let inj = (C.inj :> t -> _)
      let proj x = match C.proj x with
        Some #t as y -> y
      | _ -> None
    end
    module LVar = Var(E)(CVar)

    let map f : T.exp -> T.exp = function
        #CVar.t | `Num _ as e -> e
      | `Add(e1, e2) -> `Add (f e1, f e2)
      | `Mult(e1, e2) -> `Mult (f e1, f e2)

    let eval subst (e : T.exp) =
      let e' = map (E.eval subst) e in
      let e'' = C.inj e' in
      match e' with
        #CVar.t as v -> LVar.eval subst v
      | `Add(e1, e2) ->
          begin match C.proj e1, C.proj e2 with
            Some(`Num m), Some (`Num n) -> C.inj (`Num (m+n))
          | _ -> e''
          end
      | `Mult(e1, e2) ->
          begin match C.proj e1, C.proj e2 with
            Some(`Num m), Some (`Num n) -> C.inj (`Num (m*n))
          | _ -> e''
          end
      | _ -> e''
  end

module rec ExprF : E with module T = ExprT(ExprF.T) = Expr(ExprF)(CF)
let e2 = ExprF.eval [] (`Add(`Mult(`Num 3, `Num 2), `Var"x"));;

(* The lexpr language, reunion of lambda and expr *)

module LExprT(T : ET) = struct
  type exp = [ LamT(T).exp | ExprT(T).exp ]
end
module LExpr(E : E)(C : CW(E.T)(LExprT(E.T)).C) =
  struct
    module T = LExprT(E.T)
    module CLam = struct
      type t = LamT(E.T).exp
      let inj = (C.inj :> t -> _)
      let proj x = match C.proj x with
        Some #t as y -> y
      | _ -> None
    end
    module SLam = Lam(E)(CLam)
    module CExpr = struct
      type t = ExprT(E.T).exp
      let inj = (C.inj :> t -> _)
      let proj x = match C.proj x with
        Some #t as y -> y
      | _ -> None
    end
    module SExpr = Expr(E)(CExpr)

    let eval subst = function
        #CLam.t as x -> SLam.eval subst x
      | #CExpr.t as x -> SExpr.eval subst x
  end

module rec LExprF : E with module T = LExprT(LExprF.T) = LExpr(LExprF)(CF)
let e3 =
  LExprF.eval [] (`Add(`App(`Abs("x",`Mult(`Var"x",`Var"x")),`Num 2), `Num 5))