Skip to content

Instantly share code, notes, and snippets.

@eldesh

eldesh/gist:5714388

Last active Dec 18, 2015
Embed
What would you like to do?
De Bruijn変換をStandardMLで実装
(*
* (* 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
-
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment