
/* lambda.q: an implementation of the lambda calculus
   $Id: lambda.q,v 1.3 2007/09/26 23:03:26 agraef Exp $ */

/* This file is part of the Q programming system.

   The Q programming system is free software; you can redistribute it and/or
   modify it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   The Q programming system is distributed in the hope that it will be
   useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program; if not, write to the Free Software
   Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. */

/* This is the old lambda module from Q <= 7.0, slightly revised so that it
   can coexist with the built-in lambda function in Q 7.1 and later.

   Note that this module is _not_ part of the standard prelude any more. Most
   applications will want to use the new builtin lambda which is more
   efficient and versatile, and also has some nice syntactic sugar. However,
   if you have legacy code which depends on the old lambda module then you
   should be able to make it work with the help of this module. Moreover, this
   script also demonstrates how lambdas can be implemented in terms of the
   combinatorial calculus. Or you can use it to just play with the combinators
   themselves.

   If you want, you can even replace the builtin lambda with the one provided
   by this module. To these ends, just uncomment the line reading "::lambda =
   lambda;" below and then import this module in your script. You can also
   install this module on the Q path and add it to the standard prelude by
   adding the line "include lambda;" to prelude.q. This will give you pretty
   much the same implementation of lambda as in previous releases, with the
   added benefit that you can use the syntactic sugar for lambdas provided by
   Q 7.1 and later. (Doing this is *not* recommended, however, since it will
   make your installation incompatible with a standard Q installation.)  */

/* The implementation is based on the combinatorial calculus as described,
   e.g., in M.C. Henson: "Elements of Functional Languages", Blackwell
   Scientific Publications, Oxford, 1987. Some care is needed, though, to
   make the calculus work with lambdas involving special forms and operations
   with side-effects. Furthermore, the calculus is extended to handle pattern
   matching and to perform lambda substitutions in lists and tuples in an
   efficient manner.

   The size of a compiled lambda is O(M*N^2) for a pattern of size M and a
   lambda expression of size N, which should be efficient enough for most
   practical purposes, as long as you avoid huge expressions in the lambda
   body.

   Note that this implementation suffers from some limitations which the new
   built-in lambda doesn't have: it doesn't handle non-linear patterns and the
   anonymous variable, and it won't perform any "call-by-need" pattern
   matching. Otherwise it should be a drop-in replacement for the builtin
   lambda function. */

include stdlib;

/* The lambda expression type. */

public type Lambda : ::Lambda = special lambda X Y;

lambdax (lambda X Y)	= '~(lambda X Y);

/* Uncomment this to override the builtin lambda function with the one
   provided by this module. */

//::lambda = lambda;

/* combinator symbols (standard mode) */

public special _I ~X, _K X ~Y, _S X Y ~Z, _SL X Y ~Z, _ST X Y ~Z, _A X ~Y,
  _L X ~Y, _T X ~Y, _B X Y ~Z, _BL X Y ~Z, _BT X Y ~Z, _C X Y ~Z, _CL X Y ~Z,
  _CT X Y ~Z;

public special _H X ~Y, _HL X ~Y, _HT X ~Y, _HK X Y ~Z;

/* special mode combinators (same as above, but inhibit argument evaluation) */

public special __I X, __K X Y, __S X Y Z, __SL X Y Z, __ST X Y Z, __A X Y,
  __L X Y, __T X Y, __B X Y Z, __BL X Y Z, __BT X Y Z, __C X Y Z, __CL X Y Z,
  __CT X Y Z;

public special __H X Y, __HL X Y, __HT X Y, __HK X Y Z;

/* lambda: *******************************************************************/

special c X Y, b X Y, s X Y;
special _c X Y, _b X Y, _s X Y;
special v ~Xs X;

lambda X Y		= catch fail (v [] X||c X Y);

/* Only linear patterns are allowed. We check this using a left-to-right depth
   first traversal of the pattern, raising an exception if any variable occurs
   (at least) twice. */

v Xs (X Y)		= v (v Xs X) Y;
v Xs [X|Y]		= v (v Xs X) Y;
v Xs (X|Y)		= v (v Xs X) Y;
v Xs X			= Xs if not isvar X;
			= throw 'X if any (eq 'X) Xs;
			= ['X|Xs] otherwise;

/* There are two sets of compilation functions which generate code using the
   standard and the special mode combinators, respectively. This is needed to
   prevent premature evaluation of matched special subterms inside the lambda
   argument. Switching from standard to special compilation mode happens only
   in the first rule below (watch out for the _c on the rhs). */

c (X Y) Z		= _H ~(c X ~(_c Y Z));
c [X|Y] Z		= _HL ~(c X ~(c Y Z));
c (X|Y) Z		= _HT ~(c X ~(c Y Z));
c X Y			= _HK X Y if not isvar X;
			= b X Y otherwise;

_c (X Y) Z		= _H ~(_c X ~(_c Y Z));
_c [X|Y] Z		= _HL ~(_c X ~(_c Y Z));
_c (X|Y) Z		= _HT ~(_c X ~(_c Y Z));
_c X Y			= __HK X Y if not isvar X;
			= _b X Y otherwise;

/* translate a basic lambda expression (X = lambda variable) */

b X Y: ::Lambda		= b X `(lambdax Y);

b X X			= _I;
b X (Y Z)		= _S ~(b X Y) ~(b X Z);
b X [Y|Z]		= _SL ~(b X Y) ~(b X Z);
b X (Y|Z)		= _ST ~(b X Y) ~(b X Z);
b X Y			= _K Y otherwise;

_b X Y: ::Lambda	= _b X `(lambdax Y);

_b X X			= __I;
_b X (Y Z)		= __S ~(_b X Y) ~(_b X Z);
_b X [Y|Z]		= __SL ~(_b X Y) ~(_b X Z);
_b X (Y|Z)		= __ST ~(_b X Y) ~(_b X Z);
_b X Y			= __K Y otherwise;

/* combinator rules: *********************************************************/

/* Besides various extensions and the "saturated combinator expansion" kludge
   this is a fairly straightforward implementation of the standard combinator
   calculus as discussed in Henson 1987.

   Extensions to the standard calculus are:

   - Special form combinators, and an explicit function application combinator
     (_A). This is necessary to prevent premature evaluation of the lambda
     body.

   - Separate combinators for constructing lists (_?L) and tuples (_?T).
     Required for an efficient implementation of lambda substitutions in lists
     and tuples. Without this, combinator term sizes explode much too easily.

   - Additional matching combinators (_H?). These are the basic functions
     required to match an argument against a pattern and extract the component
     values.

   - Two alternative combinator sets, "standard" (_*) and "special" (__*).
     The standard mode combinators evaluate their argument, which is the
     normal behaviour, while the special mode combinators protect the argument
     in order to prevent premature evaluation of special subterms extracted
     from the lambda argument. */

special a ~X Y, x X;

/* standard mode combinator definitions: */

_I X			= X;
_K X _			= X;

_S X Y Z		= a (X Z) (Y Z);
_SL X Y Z		= [X Z|Y Z];
_ST X Y Z		= (X Z|Y Z);

_A X Y			= X Y;
_L X Y			= [X|Y];
_T X Y			= (X|Y);

_B X Y Z		= a X (Y Z);
_BL X Y Z		= [X|Y Z];
_BT X Y Z		= (X|Y Z);

_C X Y Z		= X Z Y;
_CL X Y Z		= [X Z|Y];
_CT X Y Z		= (X Z|Y);

_H X (Y Z)		= X Y Z;
_HL X [Y|Z]		= X Y Z;
_HT X (Y|Z)		= X Y Z;
_HK X Y X		= Y;

/* same for special mode */

__I X			= X;
__K X _			= X;

__S X Y Z		= a (X Z) (Y Z);
__SL X Y Z		= [X Z|Y Z];
__ST X Y Z		= (X Z|Y Z);

__A X Y			= X Y;
__L X Y			= [X|Y];
__T X Y			= (X|Y);

__B X Y Z		= a X (Y Z);
__BL X Y Z		= [X|Y Z];
__BT X Y Z		= (X|Y Z);

__C X Y Z		= X Z Y;
__CL X Y Z		= [X Z|Y];
__CT X Y Z		= (X Z|Y);

__H X (Y Z)		= X Y Z;
__HL X [Y|Z]		= X Y Z;
__HT X (Y|Z)		= X Y Z;
__HK X Y X		= Y;

/* "Saturated combinator expansion" kludge: This is used to force expansion of
   saturated combinators in special form arguments distributed by the _S and
   _B combinators. */

a X Y			= X Y if not isspecial X;
			= X `(x Y) otherwise;

x (_I X)		= 'X;
x (_K X _)		= 'X;
x (_S X Y Z)		= '(`(x (X Z)) `(x (Y Z)));
x (_SL X Y Z)		= '[`(x (X Z))|`(x (Y Z))];
x (_ST X Y Z)		= '(`(x (X Z))|`(x (Y Z)));
x (_A X Y)		= '(X Y);
x (_L X Y)		= '[X|Y];
x (_T X Y)		= '(X|Y);
x (_B X Y Z)		= '(X `(x (Y Z)));
x (_BL X Y Z)		= '[X|`(x (Y Z))];
x (_BT X Y Z)		= '(X|`(x (Y Z)));
x (_C X Y Z)		= '(`(x (X Z)) Y);
x (_CL X Y Z)		= '[`(x (X Z))|Y];
x (_CT X Y Z)		= '(`(x (X Z))|Y);

x (__I X)		= 'X;
x (__K X _)		= 'X;
x (__S X Y Z)		= '(`(x (X Z)) `(x (Y Z)));
x (__SL X Y Z)		= '[`(x (X Z))|`(x (Y Z))];
x (__ST X Y Z)		= '(`(x (X Z))|`(x (Y Z)));
x (__A X Y)		= '(X Y);
x (__L X Y)		= '[X|Y];
x (__T X Y)		= '(X|Y);
x (__B X Y Z)		= '(X `(x (Y Z)));
x (__BL X Y Z)		= '[X|`(x (Y Z))];
x (__BT X Y Z)		= '(X|`(x (Y Z)));
x (__C X Y Z)		= '(`(x (X Z)) Y);
x (__CL X Y Z)		= '[`(x (X Z))|Y];
x (__CT X Y Z)		= '(`(x (X Z))|Y);

x X			= 'X otherwise;

/* optimization rules: */

/* These rules *must* be in the given order. In particular, the rules for
   removing superflous applications (_A) nested in the _S? combinators must
   come before the rules producing the _B? and _C? combinators, to take
   effect. */

_S (_K X) (_K Y)	= _K (X Y);
_S (_K X) _I		= _A X;
_S (_A X) Y		= _S X Y;
_S X (_A Y)		= _S X Y;
_S (_K X) Y		= _B X Y;
_S X (_K Y)		= _C X Y;

_SL (_K X) (_K Y)	= _K [X|Y];
_SL (_K X) _I		= _L X;
_SL (_A X) Y		= _SL X Y;
_SL X (_A Y)		= _SL X Y;
_SL (_K X) Y		= _BL X Y;
_SL X (_K Y)		= _CL X Y;

_ST (_K X) (_K Y)	= _K (X|Y);
_ST (_K X) _I		= _T X;
_ST (_A X) Y		= _ST X Y;
_ST X (_A Y)		= _ST X Y;
_ST (_K X) Y		= _BT X Y;
_ST X (_K Y)		= _CT X Y;

__S (__K X) (__K Y)	= __K (X Y);
__S (__K X) __I		= __A X;
__S (__A X) Y		= __S X Y;
__S X (__A Y)		= __S X Y;
__S (__K X) Y		= __B X Y;
__S X (__K Y)		= __C X Y;

__SL (__K X) (__K Y)	= __K [X|Y];
__SL (__K X) __I	= __L X;
__SL (__A X) Y		= __SL X Y;
__SL X (__A Y)		= __SL X Y;
__SL (__K X) Y		= __BL X Y;
__SL X (__K Y)		= __CL X Y;

__ST (__K X) (__K Y)	= __K (X|Y);
__ST (__K X) __I	= __T X;
__ST (__A X) Y		= __ST X Y;
__ST X (__A Y)		= __ST X Y;
__ST (__K X) Y		= __BT X Y;
__ST X (__K Y)		= __CT X Y;
