AĻOLI

The lambda contribution

We present here a simple application using the lambda calculus written with Aļoli. The contribution starts with three description files:
  1. lambda.metal for the definition of the abstract syntax,
  2. lambda-std.ppml for the definition of the prettyprinting,
  3. lambda.g for the definition of the parser.
We then give a first example of how to use only the metal and the ppml secification to visualize trees. Then we propose a second example that makes us of the parser we have defined. All the files that are described here are in the contrib directory of the Aļoli distribution. In order to be able to run the examples below make sure that your classpath variable is properly set. It must contain both the path to the directory contrib plus the standard path to the Aļoli distribution. If for example Aļoli is installed under the directory /net, we have 
CLASSPATH:=/net/aioli/contrib/:/net/aioli/classes:$CLASSPATH

Metal

Because Aļoli uses a package convention to be able to retrieve automatically formalism definition, the metal definition has to be done in the lang/lambda subdirectory. The formalism is defined in the lambda.metal file. We define a lambda calculus with an abstraction, an application, variables and boolean constants: 
formalism of lambda is
      VAR ::= var;
      TOP  ::= true false app VAR abs;
      true  ->  ;
      false  -> ;
      app  -> TOP TOP ;
      abs  -> VAR TOP ;
      var  -> implemented as STRING ;
end
To compile this file we first need to produce an intermediate java code. It is done using the metal compiler

java aioli.metal.Compile lambda.metal

It creates a file formalism.java that we can compile as a standard java file:

javac formalism.java

We get as lambdaected the corresponding class file formalism.class. If you have any problem in completing the previous two steps, either you are using an old version of java (<1.1) or your CLASSPATH is not properly set.

Ppml

Aļoli uses a package convention to retrieve automatically prettyprinters. The ppml definition of lambda must be put inside the lang/lambda subdirectory. We write the standard prettyprinter of lambda in the lambda-std.ppml file. We use the class names var kw to leave the possibity of setting later different graphical attribut (color and fonts) to the corresponding subboxes: 
prettyprinter std of lambda is

*x!0 -> "...";

app(*x, *y) -> [<h 0> "(" [<h 1>  *x *y ] ")"];

abs(*x, *y) -> [<h 0> "(" [<h 1> "lambda"  
                             [<h 0> in class = var : *x "."]
                             *y]  ")"];

var *x -> identitypp(*x);

true() -> in class = kw : "True";

false() -> in class = kw : "False";

end prettyprinter
To compile a specification we follow the same steps than for metal but this time using the ppml compiler. We first produce intermediate java sources:

java aioli.ppml.Compile lambda-std.ppml

We get two java files BBstd.java et PPstd.java. We then simply need to compile the latter: 

javac PPstd.java

Cette fois on a deux fichiers base_std.java et pp_std.java. Il suffit de compiler le second pour compiler aussi le premier:

javac pp_std.java

An example without parser

Vtp implements a very simple protocol to transfer tree structures. So eventhough we don't have yet a parser for lambda we can already build applications that manipulates lambda term. Our first example is a program that visualizes lambda terms. It is described in the file test.java: 

package lambda;

import java.io.*;
import java.awt.Frame;
import java.awt.Container;
import aioli.vtp.*;
import aioli.variable.*;
import aioli.gfxobj.*;

public final class test extends Frame {

  public static void main(String[] theArgs) {
    new test(theArgs[0]);
  }
  public test(String file) {
    try {
      Tree tree = Proto.readTree(new FileInputStream(file));
      Variable var = new Variable(tree);
      System.out.println(tree.toString());
      Ctedit ct = new Ctedit(var,"std");
      add(ct.getComponent());
      setSize(600,400);
      setTitle("Lambda");
      setVisible(true); 
      ct.setStyle("DEFAULT","times-17","black","white");
      ct.setStyle("kw","times-17-i",null,null);
      ct.setStyle("var",null,"blue",null);
      ct.redraw(120,20);
    }
    catch (FileNotFoundException e) {}
  }
}
We first compile this file:

javac test.java

To run an example, we just need to create a file proto.txt that contains valid construction using the protocol, so for example: 

a
lambda$var
x
n
lambda$true
0
n
lambda$abs
2
e
Now the command

java lambda.test proto.txt

creates a window:

window snapshot

Antlr

The next step is to write a parser for Lambda. Here is the simple definition of the parser: 
expression : ident | "True" | "False"
             | "("
                ( "lambda" ident "." expression
                | expression expression
                )
               ")"
        ;
ident: ("a".."z"|"A".."Z"|"_"|"$") ("a".."z"|"A".."Z"|"_"|"0".."9"|"$")*
For the moment there is no mechanism to retrieve parser, parser can belong to arbitrary packages. So we arbitrary decide to write the parser in the lambda subdirectory in the file lambda.g. Adding a header and vtp actions to the previous definition gives: 
header {package lambda;}

{
import java.io.*;
import aioli.vtp.*;}

class LambdaParser extends Parser;
options {
	tokenVocabulary=Lambda;
	vtpLanguage = "lambda";
} 

{
//class Main {
	public static Tree parse(InputStream ds) throws Exception {
		try {
		  LambdaLexer lexer = new LambdaLexer(ds);
		  LambdaParser parser = new LambdaParser(lexer);
		  return parser.expression();
		}
		catch(Exception e) {
			System.err.println("exception: "+e);
			throw e;   // so we can get stack trace
		}
	}
//}
}

expression
returns [Tree tr]
<< tr1 == *;tr2 == *;tr = *;>>
	: id1:IDENT
          <<tr = var *id1^;>>
          | "True"
	   <<tr= true();>>
          | "False"
	   <<tr= false();>>
          | LPAREN
            (  "lambda" id2:IDENT DOT tr1=expression
               <<tr=abs(var *id2^, *tr1);>>
             | tr1=expression tr2=expression
               <<tr=app(*tr1,*tr2);>>
            )
            RPAREN
	;




class LambdaLexer extends Lexer;

options {tokenVocabulary=Lambda;}


LPAREN :	'(' ;
RPAREN :	')' ;
DOT	:	'.';

// MISC STUFF 
WS	:	(' '
	|	'\t'
	|	'\n'  { newline(); }
	|	'\r')
		{ _ttype = Token.SKIP; }
	;


IDENT 
options { testLiterals=true;}
	:	
	('a'..'z'|'A'..'Z'|'_'|'$') ('a'..'z'|'A'..'Z'|'_'|'0'..'9'|'$')*
	;
To compile this file, we use the antlr tool: 
java antlr.Tool lambda.g
It produces several java files. The main file we need to compile is the LambdaParser: 
javac LambdaParser.java

An example using the parser

We can now define a new class test1 that makes use of the parser we have just defined: 

package lambda;

import java.io.*;
import java.awt.Frame;
import java.awt.Component;
import aioli.vtp.*;
import aioli.variable.*;
import aioli.gfxobj.*;

public final class test1 extends Frame {

  public static void main(String[] theArgs) {
    new test1(theArgs[0]);
  }
  public test1(String file) {
    try {
      Tree tree = LambdaParser.parse(new FileInputStream(file));
      Variable var = new Variable(tree);
      Ctedit ct = new Ctedit(var,"std");
      add(ct.getComponent());
      setSize(600,400);
      setTitle("Lambda");
      setVisible(true); 
      ct.setStyle("DEFAULT","times-17","black","white");
      ct.setStyle("kw","times-17-i",null,null);
      ct.setStyle("var",null,"blue",null);
      ct.redraw(120,20);
    }
    catch (FileNotFoundException e) {}
    catch (java.lang.Exception e) {}
  }
}
We compile the file: 
 javac test1.java

To run an example, we just need to create a file ex.lambda that contains a valid lambda expression: 

(lambda x . True)
Now the command

java lambda.test1 ex.lambda

produces the same result than the example without parser:

window snapshot

We can refine this example by adding a button that shows where is the binder of a variable. The idea is to select a variable in the window and click on a button "Binder", the selection is then automatically moved to the binder of this variable. We first define in the class Binding a method that wlaks through the tree to find the binder 

package lambda;

import aioli.vtp.*;

public class Binding {

  public static Tree find(Tree tree) {
    // First check if it is a variable we are finding
    if (tree == null)
      return null;
    if ("lambda".equals(tree.formalism().name()) &&
	"var".equals(tree.operatorName())) {
      String nameVar = tree.atomValue().string();
      while (tree != null) {
	if ("abs".equals(tree.operatorName()) &&
            "var".equals(tree.down(1).operatorName()) &&
            nameVar.equals(tree.down(1).atomValue().string()))
	  return tree.down(1);
	tree = tree.up(1);
      }
    }
    return null;
  }
}
Then we use Awt libraries to define the button and the object that is listening to the event that are associated with the button. This is defined in the file BinderBut.java: 
package lambda;

import java.awt.*;
import java.awt.event.*;
import aioli.variable.Variable;
import aioli.vtp.Tree;

class BinderListener implements ActionListener {
  Variable _var;
  Tree _tree;
  Tree _old ;
  BinderListener(Variable var) {
    _var=var;
    _tree=null;
    _old =null;
  }
  public void actionPerformed(ActionEvent ae) {
    String str=((Button)(ae.getSource())).getLabel();
    Tree tree = _var.getCurrentTree();
    Tree res = Binding.find(tree);
    if (res != null)
      _var.updateCurrentSelection(res);
  }
}

public class  BinderBut  extends Panel {
  protected void makebutton(String name,
			    GridBagLayout gridbag,
			    GridBagConstraints c,
			    BinderListener el) {
    Button button = new Button(name);
    gridbag.setConstraints(button, c);
    button.addActionListener(el);
    add(button);
  }
        
   public  BinderBut(Variable var) {
     GridBagLayout g = new GridBagLayout();
     GridBagConstraints c = new GridBagConstraints();
     BinderListener el = new BinderListener(var);
     setLayout(g);
     c.fill = GridBagConstraints.BOTH;
     setLayout(g);
     c.weighty = 0.0;                  //reset to the default
     c.gridwidth = GridBagConstraints.REMAINDER; //end row
     c.gridheight = 1;               //reset to the default
     makebutton("Binder",g,c,el);
     c.weighty = 1.0;                  //reset to the default
     java.awt.Canvas cv = new java.awt.Canvas();
     g.setConstraints(cv, c);
     add(cv);
   }
}
We can now add the button to the window in a new test file test2.java 
package lambda;

import java.io.*;
import java.awt.Frame;
import java.awt.Component;
import aioli.vtp.*;
import aioli.variable.*;
import aioli.gfxobj.*;

public final class test2 extends Frame {

  public static void main(String[] theArgs) {
    new test2(theArgs[0]);
  }
  public test2(String file) {
    try {
      Tree tree = LambdaParser.parse(new FileInputStream(file));
      Variable var = new Variable(tree);
      Ctedit ct = new Ctedit(var,"std");
      add(ct.getComponent());
      add("West",new BinderBut(var));
      setSize(600,400);
      setTitle("Lambda");
      setVisible(true); 
      ct.setStyle("DEFAULT","times-17","black","white");
      ct.setStyle("kw","times-17-i",null,null);
      ct.setStyle("var",null,"blue",null);
      ct.redraw(120,20);
    }
    catch (FileNotFoundException e) {}
    catch (java.lang.Exception e) {}
  }
}
We compile the new test 
javac test2.java
and we run it with the file ex1.lambda that contains a lambda term with some variables: 
(lambda x . (lambda y . (y x)))
Running the command: 
java lambda.test2 ex1.lambda
selecting the second occurrence of x and clicking on the button Binder gives the expected result:

window snapshot