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, 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 ( a);