/* lambda.q: an implementation of the lambda calculus
   $Id: lambda.q,v 1.4 2004/02/20 02:01:15 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 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. */

include stdlib;

/* The lambda expression type. Create appropriate subtypes for other types of
   constructs which translate into lambdas and must be expanded recursively.
   These types must all provide an implementation of the lambdax function
   which returns an equivalent quoted lambda term, or throws an exception if
   the expression fails to expand properly. The latter case will cause the
   entire lambda expression to fail. */

public type Lambda = special lambda X Y;

public special lambdax X;

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

/* 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) ~(s X Z) if isspecial Y;
			= _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) ~(_s X Z) if isspecial Y;
			= __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;

/* translate a special argument expression (no recursive lambda expansion) */

s X Y			= _HK X Y if not isvar X;
s X X			= _I;
s X (Y Z)		= _S ~(s X Y) ~(s X Z);
s X [Y|Z]		= _SL ~(s X Y) ~(s X Z);
s X (Y|Z)		= _ST ~(s X Y) ~(s X Z);
s X Y			= _K Y otherwise;

_s X Y			= __HK X Y if not isvar X;
_s X X			= __I;
_s X (Y Z)		= __S ~(_s X Y) ~(_s X Z);
_s X [Y|Z]		= __SL ~(_s X Y) ~(_s X Z);
_s X (Y|Z)		= __ST ~(_s X Y) ~(_s X Z);
_s X Y			= __K Y otherwise;

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

/* This admittedly looks terrible, but with the exception of various
   extensions and the "saturated combinator expansion" kludge it is a fairly
   straightforward implementation of the standard combinator calculus
   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 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;