Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* $Id: mixmod.ml.txt,v 1.1 2005/02/24 01:45:32 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))