102 lines
2.5 KiB
Standard ML
102 lines
2.5 KiB
Standard ML
structure StringKey : ORD_KEY = struct
|
|
type ord_key = string
|
|
val compare = String.compare
|
|
end
|
|
|
|
structure StringSet : ORD_SET = RedBlackSetFn (StringKey)
|
|
|
|
|
|
type var = string
|
|
|
|
(* Type of valid expressions *)
|
|
datatype Term = Var of var
|
|
| App of Term * Term
|
|
| Abs of var * Term
|
|
|
|
(* Used for alpha reduction *)
|
|
fun freshvar (Var x) = Var (x ^ "'")
|
|
|
|
val egVar = Var "x"
|
|
val egApp = App (egVar, egVar)
|
|
val egAbs = Abs ("x", egVar) (* λx. x *)
|
|
val egAbs2 = Abs ("x", App (egVar, Var "y")) (* λx. x y *)
|
|
|
|
(* Only variable names, not Var objects, are used *)
|
|
fun freevars exp =
|
|
let
|
|
fun freehelper (Var x) = StringSet.singleton x
|
|
| freehelper (App (t1, t2)) = StringSet.union(freehelper t1, freehelper t2)
|
|
| freehelper (Abs (x, t)) =
|
|
StringSet.difference(freehelper(t), StringSet.singleton(x))
|
|
in
|
|
StringSet.listItems (freehelper exp)
|
|
end
|
|
|
|
fun boundvars exp =
|
|
let
|
|
fun boundhelper (Var x) = StringSet.empty
|
|
| boundhelper (App (t1, t2)) = StringSet.union(boundhelper t1, boundhelper t2)
|
|
| boundhelper (Abs (x, t)) = StringSet.union(StringSet.singleton x, boundhelper t)
|
|
in
|
|
StringSet.listItems (boundhelper exp)
|
|
end
|
|
|
|
fun allvars exp =
|
|
let
|
|
fun allhelper (Var x) = StringSet.singleton x
|
|
| allhelper (App (t1, t2)) = StringSet.union(allhelper t1, allhelper t2)
|
|
| allhelper (Abs (x, t)) = StringSet.union(StringSet.singleton x, allhelper t)
|
|
in
|
|
StringSet.listItems (allhelper exp)
|
|
end
|
|
|
|
(* v is string (ie, var) *)
|
|
fun freshvar (v, t) = if StringSet.member(freevars t, v) then
|
|
freshvar(v ^ "'", t)
|
|
else v
|
|
|
|
fun alphared (s, Abs (v, t)) = let
|
|
val nvar = fresh (v, t)
|
|
in
|
|
Abs (nv, subst(v, nv, t))
|
|
|
|
|
|
(*
|
|
- subst ("x", Var "z", Var "x");
|
|
val it = Var "z" : Term
|
|
*)
|
|
|
|
|
|
(*
|
|
fun subst (x, s, Orig as (Var a)) = if x = a then s
|
|
else Orig
|
|
| subst (x, s, App (t1, t2)) = App (subst (x, s, t1), subst (x, s, t2))
|
|
| subst (x, s, Orig as (Abs v, t)) = if x = v then Orig
|
|
else if StringSet.member(freevars t, v) then subst (x, s, (alphared (s, Orig)))
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
| freevars (Abs (x, e)) = StringSet.difference(freevars(e), StringSet.singleton(x))
|
|
*)
|
|
|
|
(*
|
|
| freevars (Abs (x, e)) =
|
|
let
|
|
val b = StringSet.singleton(x)
|
|
in
|
|
StringSet.difference(freevars(e), b)
|
|
end;
|
|
*)
|