-- LambdaCalc.russell
open <*
T: type ~ proc[T->T] ,
TRUE: T ~ lambda x:T in lambda y:T in x ni ni ,
FALSE: T ~ lambda x:T in lambda y:T in y ni ni ,
ZERO: T ~ lambda x:T in lambda y:T in y ni ni ,
ID: T ~ lambda x:T in x ni ,
printBoolValue: proc[T->[]] ~ lambda f:T in
open <
putTrue: T ~ lambda x:T in putString<stream~stdout,string~"TRUE">; x ni ,
putFalse: T ~ lambda x:T in putString<stream~stdout,string~"FALSE">; x ni
> in
(((f putTrue) putFalse) ID)
ni
ni ,
printNatValue: proc[T->[]] ~ lambda f:T in
open ref[integer.val] | integer in
open < sum ~ new<> > in
assign<lhs~sum, rhs~0>;
((f lambda x:T in assign<lhs~sum, rhs~+<a~valOf sum, b~1>>; x ni) ID);
putString<stream~stdout, string~toString (valOf sum)>;
putString<stream~stdout, string~"\n">
ni
ni
ni
*> in
open <*
suc: T ~ lambda n:T in lambda s:T in lambda z:T in s (n s z) ni ni ni ,
fromInteger: func[ integer.val->T ] ~ lambda n: integer.val in
if (integer.leq<a~n,b~0>)?t => ZERO else suc(fromInteger(integer.-<a~n,b~1>)) fi ni ,
plus: T ~ lambda n:T in lambda m:T in ((n suc) m) ni ni ,
times: T ~ lambda n:T in lambda m:T in ((n (plus m)) ZERO) ni ni ,
exp: T ~ lambda n:T in lambda m:T in ((m (times n)) (suc ZERO)) ni ni
*> in
printNatValue( (exp (fromInteger 2))(fromInteger 3) )
ni
ni