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: mixmod2.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 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 = string
end
module Var(E : E)(C : CW(E.T)(VarT).C) =
struct
module T = VarT
let eval sub s =
try List.assoc s sub with Not_found -> C.inj s
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 = Var of 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)
open T
module CVar = struct
let inj x = C.inj (Var x)
let proj x = match C.proj x with Some (Var y) -> Some y | _ -> None
end
module LVar = Var(E)(CVar)
let eval subst = function
Var 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)
open LamF.T
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 VarT.exp | 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)
open T
module CVar = struct
let inj x = C.inj (Var x)
let proj x = match C.proj x with Some (Var y) -> Some y | _ -> None
end
module LVar = Var(E)(CVar)
let map f = function
Var _ | Num _ as e -> e
| Add(e1, e2) -> Add (f e1, f e2)
| Mult(e1, e2) -> Mult (f e1, f e2)
let eval subst e =
let e' = map (E.eval subst) e in
let e'' = C.inj e' in
match e' with
Var 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)
open ExprF.T
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 = Lam of LamT(T).exp | Expr of ExprT(T).exp
end
module LExpr(E : E)(C : CW(E.T)(LExprT(E.T)).C) =
struct
module T = LExprT(E.T)
open T
module CLam = struct
let inj x = C.inj (Lam x)
let proj x = match C.proj x with Some (Lam y) -> Some y | _ -> None
end
module SLam = Lam(E)(CLam)
module CExpr = struct
let inj x = C.inj (Expr x)
let proj x = match C.proj x with Some (Expr y) -> Some y | _ -> None
end
module SExpr = Expr(E)(CExpr)
let eval subst = function
Lam x -> SLam.eval subst x
| Expr x -> SExpr.eval subst x
end
module rec LExprF : E with module T = LExprT(LExprF.T) = LExpr(LExprF)(CF)
open LExprF.T
module LamTF = LamT(LExprF.T)
open LamTF
module ExprTF = ExprT(LExprF.T)
open ExprTF
let e3 =
LExprF.eval []
(Expr(Add(Lam(App(Lam(Abs("x",Expr(Mult(Expr(Var"x"),Expr(Var"x"))))),
Expr(Num 2))),
Expr(Num 5))))