Next: Inversion and Invert Up: New features in LEGO Version 1.3 Previous: Induction

LEGO Version 1.3: Infix

Introduction of a new infix operator is via a Configure declaration, for
example

Configure Infix + left 7;

asserts that + is an infix operator which is left associative with
precedence 7 (as per usual, higher numbers mean tighter binding). 

This causes the expression

a + b

to be parsed as 

op+ a b

Pretty-printing reverses the above process for infix-declared operators
applied to exactly two arguments.


Example:
--------

Lego> Configure Infix + left 5;
Infix + left 5
Lego> [A:Type][a:A][op+:A->A->A];
decl  A : Type
decl  a : A
decl  op+ : A->A->A
  (* time= 0.0  gc= 0.0  sys= 0.010000 *)
Lego> a+(a+a); 
value = a + (a + a)
type  = A


Notes
-----

To maintain backward compatibility, the operators \/ and /\ are
aliased to "or" and "and" respectively, rather than op\/ and op/\.
They should work exactly as before (once you've got lib_logic loaded).

Built-in infix operators have a higher precedence than any user-defined
ones.

In Configure declarations, associativity (left or right) and the
precedence (1-9) are mandatory unless the operator is one of +,-,*, or
/, in which case in the absence of user-supplied associativity and
precedence defaults will be used.

The syntactic class of infix operators is currently 

+  -  /  *  <<  >>  /\  \/  |-  ::  &word @word

where word is one or more alphabetic characters. 


How 'alpha' is alpha?
---------------------

Eventually the syntactic class for infix operators will be expanded to
something a bit more rational (suggestions welcome), and the mechanism
for precedence and associativity defaults will be extended to use
those of the first character of the new operator. 
[Did I already do this? - djs]