// Krivine's Abstract Machine For Lambda Terms plus Integer Constants

/* 
  This (very) abstract machine reduces a lambda term to *weak head normal
  form*.  Essentially, we do not descend down into a lambda-abstraction
  until the lambda-abstraction is applied to a term.  The machine also
  uses *call-by-name* as opposed to the more usual call-by-value.  This
  means that arguments are not evaluated before they're passed to the 
  lambda term/function.

  Formally, a machine consists of a STACK.  A STACK is a list of CLOSURES.
  A CLOSURE is of the form (t,Env) where t is a lambda term and Env is
  a list of BINDINGS. A BINDING is of the form (x,CLOSURE) where x is a 
  variable represented by a string.  One of the nice aspects of this 
  machine is that alpha-conversion is not required during reduction.  
  It is only needed when we wish to print the result.

  The machine is initialized with <(t,null)> where t is the term to
  be computed, then transitions as follows:

  <(x,Env)::S> ==> <Env(x)::S>
  <((app A B),Env)::S> ==> <(A,Env)::(B,Env)::S>
  <((lambda x.B,Env)::Cl::S) ==> <(B,(x,Cl)::Env)::S>
  else S ==> S

  Here, :: represents list cons and Env(x) searching for the binding of
  x in Env.  Env is used in a stack-like manner so the top binding for x
  is returned.
*/

import java.util.ArrayList;
import java.io.*;

interface term   // abstract type of all lambda terms
{
    <T> T accept(tvisitor<T> v); // for visitor pattern
}

class abs implements term  // lambda vname.body
{
  String vname;
  term body;   
    public abs(String v,term b) {body=b; vname=v;}
    public <T> T accept(tvisitor<T> v) {return v.visit(this);}
    public String toString() {return "lambda "+vname+"."+body;}
}

class app implements term  // applications (a b)
{
   term a;
   term b;
    public app(term x, term y) {a=x; b=y;}
    public <T> T accept(tvisitor<T> v) {return v.visit(this);}
    public String toString() { return "("+a+" "+b+")"; }
}

class var implements term  // a variable represented by a string
{
   String name;
    public var(String v) {name=v;}
    public <T> T accept(tvisitor<T> v) {return v.visit(this);}
    public String toString() {return name;}
}

class iconst implements term  // integer constant
{
    int val;
    public iconst(int x) {val=x;}
    public <T> T accept(tvisitor<T> v) {return v.visit(this);}
    public String toString() {return ""+val;}
}

interface tvisitor<T>   // generic visitor 
{
    T visit(abs x);
    T visit(app x);
    T visit(var x);
    T visit(iconst x);
}

// sample term: new abs("x",new abs("y",new var("x"))); 

/* implements Krivine's abstract machine: */
class Closure
{
    public term t;
    public Binding env;
    public Closure(term a, Binding b)
    {t=a; env=b;}
}

// we use our own implementation of linked list to improve memory
// management (no need to clone ArrayList):
class Binding
{
    public var v;
    public Closure cl;
    public Binding(var x, Closure y) {v=x; cl=y;}
    public Binding(var x, Closure y, Binding b) {v=x; cl=y; Rest=b;}
    public Binding Rest;
}

class Stack
{
    Closure Cl;
    Stack Rest;
    public Stack(Closure x, Stack y) {Cl=x; Rest=y;}

    // combines what remains on the stack into one term, apply
    // suspended substitutions using suber visitor:
    public term flatten() 
    {
	suber sb = new suber(Cl.env);
	term t = Cl.t.accept(sb);
	for(Stack i=this.Rest;i!=null;i=i.Rest)
	    {   sb.CE = i.Cl.env;
		t = new app(t, i.Cl.t.accept(sb));
	    }
	return t;
    }
}//stack

// static substitutions (no reduction - will alpha convert)
class suber implements tvisitor<term>
{
    public static int cx =0; // variable counter for alpha conversion
    public Binding CE;
    public suber(Binding e) {CE=e;}
    public term visit(iconst x) { return x; }
    public term visit(var x)
    {
	Closure cl = cutvisitor.lookup(x.name,CE);
	if (cl==null) return x;
	else return cl.t.accept(new suber(cl.env));
    }
    
    public term visit(app P)
    {
	return new app(P.a.accept(this),P.b.accept(this));
    }
    
    public term visit(abs A)
    {
	// alpha convert the abstraction:
	String aname =A.vname+cx; cx++;
	Closure foraname = new Closure(new var(aname),null);
	Binding CE2 = new Binding(new var(A.vname),foraname,CE);
	return new abs(aname, A.body.accept(new suber(CE2)));
    }
}//suber

// The following visitor executes the machine:
class cutvisitor implements tvisitor<Object> 
{
    public static Closure lookup(String name, Binding CE)
    {
	for(Binding i=CE;i!=null;i=i.Rest)
	    {   
		if (i.v.name.equals(name)) return i.cl; 
	    }
	return null;
    }//lookup

    public Binding CE; // current closure of term
    public kam machine;
    public boolean stop = false;

    public Object visit(var v)
    {
	Closure C = lookup(v.name,CE);
	if (C==null) stop = true;
	else machine.S = new Stack(C,machine.S.Rest);
	return null;
    }
    public Object visit(iconst x)
    { stop=true; return null;}
    public Object visit(app P)
    {
	machine.S = new Stack(new Closure(P.a,CE), new Stack(new Closure(P.b,CE),machine.S.Rest));
	return null;
    }
    public Object visit(abs A)
    {
	if (machine.S.Rest==null) {stop=true; return null;}
	Closure C = machine.S.Rest.Cl;
	CE = new Binding(new var(A.vname),C,CE);
	machine.S = new Stack(new Closure(A.body,CE),machine.S.Rest.Rest);
	return null;
    }
    
}//cut visitor

public class kam  // main instances of machine
{
    public Stack S;
    public Binding Defs=null; // global defs, used as base for Stack
    // Defs will be set by parser
    public term run(term t) // evaluate single term
    {
	S = new Stack(new Closure(t,Defs),null);
	cutvisitor beta = new cutvisitor();
	beta.machine = this;
	while (!beta.stop)
	    {
		beta.CE = S.Cl.env;
		S.Cl.t.accept(beta);
	    }  
	return S.flatten();
    }//run

    public term run(ArrayList<term> Ts) // evaluate each term in a list
    {
	term last=null;
	for(term t:Ts) 
	    { 
		last=run(t);  
		System.out.println(last);
		suber.cx=0; // reset variable counter
	    }
	return last;
    }
    
    public static void main(String[] args) throws Exception
    {
	kam machine = new kam();  
	Mylambdapluslexer lxr = new Mylambdapluslexer(new FileReader(args[0]));
	lambdaplusparser parserp = new lambdaplusparser(lxr);	
	parserp.setup(machine);
	ArrayList<term> Ts = parserp.parse();
	machine.run(Ts);
    }//main
}//kam