use "ParsePrint.ML";
(*** Lambda-terms ***)
signature LAMBDA =
sig
datatype term = Free of string
| Bound of string
| Int of int
| Op of string
| Abs of string*term
| Apply of term*term
val abstract: string -> term -> term
val inst: (string * term) list -> term -> term
end;
functor LambdaFUN(Basic: BASIC) : LAMBDA =
struct
local open Basic in
datatype term = Free of string
| Bound of string
| Int of int
| Op of string
| Abs of string*term
| Apply of term*term;
(*Convert occurrences of b to bound index i in a term*)
fun abstract b (Free a) = if a=b then Bound(a) else Free a
| abstract b (Bound j) = Bound j
| abstract b (Abs(a,t)) = Abs(a, abstract b t)
| abstract b (Apply(t,u)) = Apply(abstract b t, abstract b u);
(*Substitution for free variables*)
fun member x [] = false
|member x (y::ys) = (x=y) orelse (member x ys);
fun isop x = member x ["I","K","S","B","C","Y","CONS","HD","TL","+",
"ADD","MUL","SUB","DIV",
"IF","EQ","AND","OR","NOT","PR","PAR","SET"];
fun isnum str =
let
fun forall [] p = true
|forall (x::xs) p = (p x) andalso (forall xs p);
in
forall (explode str)
(fn ch => member ch ["0","1","2","3","4","5","6","7","8","9"])
end;
fun mkint "" num = num
|mkint str num =
let val dig =hd(explode str);
val rest=implode(tl(explode str));
in
mkint rest (10*num + (if dig="0" then 0
else if dig="1" then 1
else if dig="2" then 2
else if dig="3" then 3
else if dig="4" then 4
else if dig="5" then 5
else if dig="6" then 6
else if dig="7" then 7
else if dig="8" then 8
else 9))
end;
fun inst env (Free a) = if (isnum a) then Int(mkint a 0)
else if (isop a) then Op(a)
else (inst env (lookup(env,a))
handle Lookup => Free a)
| inst env (Bound i) = Bound i
| inst env (Abs(a,t)) = Abs(a, inst env t)
| inst env (Apply(t1,t2)) = Apply(inst env t1, inst env t2);
end
end;
(*** Parsing of lambda terms ***)
signature PARSELAM =
sig
type term
val abslist: string list * term -> term
val applylist: term * term list -> term
val read: string -> term
end;
functor ParseLamFUN (structure Parse: PARSE
and Lambda: LAMBDA) : PARSELAM =
struct
local open Parse open Lambda in
type term = term;
(*Abstraction over several free variables*)
fun abslist([], t) = t
| abslist(b::bs, t) = Abs(b, abstract b (abslist(bs, t)));
(*Application of t to several terms*)
fun applylist(t, []) = t
| applylist(t, u::us) = applylist(Apply(t,u), us);
fun makelambda ((((_,b),bs),_),t) = abslist(b::bs,t)
(*term/atom distinction prevents left recursion; grammar is ambiguous*)
fun term toks =
( $"%" -- id -- repeat id -- $"." -- term >> makelambda
|| atom -- repeat atom >> applylist
) toks
and atom toks =
( id >> Free
|| $"(" -- term -- $")" >> (#2 o #1)
) toks;
val read = reader term;
end
end;
(******** SHORT DEMONSTRATIONS ********)
structure Basic = BasicFUN();
structure LamKey =
struct val alphas = []
and symbols = ["(", ")", "'", "->"]
end;
structure LamLex = LexicalFUN (structure Basic=Basic and Keyword=LamKey);
structure Parse = ParseFUN(LamLex);
structure Lambda = LambdaFUN(Basic);
structure ParseLam = ParseLamFUN (structure Parse=Parse and Lambda=Lambda);
open Basic; open Lambda;
val stdenv = map (fn (a,b) => (a, ParseLam.read b))
[ (*booleans*)
("true", "%x y.x"), ("false", "%x y.y"),
("if", "%p x y. p x y"),
(*ordered pairs*)
("pair", "%x y f.f x y"),
("fst", "%p.p true"), ("snd", "%p.p false"),
(*natural numbers*)
("suc", "%n f x. n f (f x)"),
("iszero", "%n. n (%x.false) true"),
("0", "%f x. x"), ("1", "suc 0"),
("2", "suc 1"), ("3", "suc 2"),
("4", "suc 3"), ("5", "suc 4"),
("6", "suc 5"), ("7", "suc 6"),
("8", "suc 7"), ("9", "suc 8"),
("add", "%m n f x. m f (n f x)"),
("mult", "%m n f. m (n f)"),
("expt", "%m n f x. n m f x"),
("prefn", "%f p. pair (f (fst p)) (fst p)"),
("pre", "%n f x. snd (n (prefn f) (pair x x))"),
("sub", "%m n. n pre m"),
(*lists*)
("nil", "%z.z"),
("cons", "%x y. pair false (pair x y)"),
("null", "fst"),
("hd", "%z. fst(snd z)"), ("tl", "%z. snd(snd z)"),
(*recursion for call-by-name*)
("YN", "%f. (%x.f(x x))(%x.f(x x))"),
("fact", "YN (%g n. if (iszero n) 1 (mult n (g (pre n))))"),
("append", "YN (%g z w. if (null z) w (cons (hd z) (g (tl z) w)))"),
("inflist", "YN (%z. cons MORE z)"),
(*recursion for call-by-value*)
("YV", "%f. (%x.f(%y.x x y)) (%x.f(%y.x x y))"),
("factV", "YV (%g n. (if (iszero n) (%y.1) (%y.mult n (g (pre n))))y)") ];
fun read a = inst stdenv (ParseLam.read a);