De Bruijn変換をStandardMLで実装

gistfile1.ml

(*
 * (* debruijn.cm *)
 * Group
 * is
 *   $/basis.cm
 *   debrujn.sml
 *)

(**
 * De Bruijn変換
 * http://www.geocities.jp/sanpukoubou/SanpuKouron/debrujn.pdf
 *
 *)

structure Lambda =
struct
  datatype t = Num of int
             | Var of string
             | Lam of string * t
             | App of t * t
             | Let of string * t * t
             | Letrec of string * t * t

  fun toString (Num x) = concat["Num(", Int.toString x, ")"]
    | toString (Var id) = concat["Var(", id, ")"]
    | toString (Lam (v,e)) = concat["fn ", v, " => ", toString e]
    | toString (App (e1,e2)) = concat["(", toString e1, " ", toString e2, ")"]
    | toString (Let (id,e1,e2)) = concat["let val ", id, " = ", toString e1, " in ", toString e2, " end"]
    | toString (Letrec (id,e1,e2)) = concat["letrec val ", id, " = ", toString e1, " in ", toString e2, " end"]

end
(**
 (* λx.x(λy.x y (λz.x y z)) *)
 - val expr =
 L.Lam("x"
   , L.App(L.Var "x"
       , L.Lam ("y"
           , L.App(L.Var "x"
               , L.App(L.Var "y"
                   , L.Lam ("z"
                       , L.App(L.Var "x"
                           , L.App(L.Var "y"
                               , L.Var "z"))))))));
 - pp $ L.toString $ expr
 fn x => (Var(x) fn y => (Var(x) (Var(y) fn z => (Var(x) (Var(y) Var(z))))))
 *)

structure DeBruijn =
struct
  datatype t = Num of int
             | L of int
             | Fn of t
             | App of t * t
             | Let of t * t
             | Letrec of t * t

  fun toString (Num x) = concat["Num(", Int.toString x, ")"]
    | toString (L n)   = concat["L(", Int.toString n, ")"]
    | toString (Fn e)  = concat["fn ", toString e]
    | toString (App (e1,e2)) = concat["(", toString e1, " ", toString e2 ,")"]
    | toString (Let (e1,e2)) = concat["let ", toString e1, " in ", toString e2, " end"]
    | toString (Letrec (e1,e2)) = concat["letrec ", toString e1, " in ", toString e2, " end"]

  local structure E = Lambda
  in
  fun getindex i [] v = raise Fail (concat["getindex ", Int.toString i])
    | getindex i (v'::vs) v = if v' = v then i
                              else getindex (i+1) vs v
  fun index_var vs expr =
    case expr
      of E.Num x => Num x
       | E.Var id => let val i = getindex 0 vs id
                     in L i end
       | E.Lam (v,e) => let val e' = index_var (v::vs) e
                        in Fn e' end
       | E.App (e1,e2) => let val e'1 = index_var vs e1
                              val e'2 = index_var vs e2
                          in App (e'1, e'2) end
       | E.Let (v,e1,e2) => let val e1' = index_var vs e1
                                val e2' = index_var (v::vs) e2
                            in Let (e1',e2') end
       | E.Letrec (v,e1,e2) => let val e1' = index_var (v::vs) e1
                                   val e2' = index_var (v::vs) e2
                               in Letrec (e1',e2') end

  fun translate expr = index_var [] expr
  end

end
(**
 (* λ.0 (λ.1 0 (λ.2 1 0)) *)
 - val expr =
 L.Lam("x"
     , L.App(L.Var "x"
         , L.Lam ("y"
             , L.App(L.Var "x"
                 , L.App(L.Var "y"
                     , L.Lam ("z"
                         , L.App(L.Var"x"
                             , L.App(L.Var"y", L.Var "z"))))))));
 - pp $ L.toString $ expr;
 fn x => (Var(x) fn y => (Var(x) (Var(y) fn z => (Var(x) (Var(y) Var(z))))))
 val it = () : unit
 -
 *)