/*  Copyright (C) Stephen Lee 2008 .  
 *  Email:stephen@tachyos.org  
 *  This program 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 of the License, or
 *  (at your option) any later version.
 *  
 *  This program 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., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
*/

package godel;

import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import javax.swing.*;
//import javax.swing.plaf.basic.BasicArrowButton;
import java.math.*;
import java.util.*;
import java.io.*;
import javax.swing.event.*;
import java.net.*;

/**This applet implements the conversion of a function (expressed as a computer program) into an arithmetical formula.
 * This is the program which carries out the most important part of this Gödel's incompleteness theorem project.
 * It works very much like a compiler, you input a program written in a programming language, and it tranforms this program into another form. In this case, rather than producing executable output, 
 * it expresses the program in terms of the Gödel number of an arithmetical formula.
 * @author Stephen Lee*/
public class Godel3 extends Applet implements ActionListener,CaretListener{
	
private static final long serialVersionUID = 1L; 

/** Haskell file loaded automatically*/
String lfile="godel2";

/** List of identifiers  */
class IdList extends ArrayList {
private static final long serialVersionUID = 1L;
/** Shrinks list of strings
 * @param s New length of list
 */
void  shrinkTo(int s){removeRange(s,size());}
}

/** new arithmetic variable
 * @return int form of new variable 
 */	
int newV(){
return vbase++;}	

/** Holds an encoded representation of an expression */
class TExpr{
 /** Encoded representation of expression*/
 BigInteger value;
 /** Type of expression 1:integer,2:Duple,3:List,4:Boolean */
 int type;

 TExpr(BigInteger v,int t){
value=v;type=t;}}

/** Holds information about Haskell function  */
class Funinfo {
/** Type of function 1:integer,2:Duple,3:List,4:Boolean */
int type;
/** ∃ Nf x<Nf ⇒ f(x)=&beta(Yf,Zf,x) */
int Nf,Yf,Zf;
/** functions which this one depends upon */
BitSet dependsOn;
Funinfo(int typ){
dependsOn=new BitSet();
type=typ;
Nf=newV();
Yf=newV();
Zf=newV();}
/** ∀ Nf,Yf,Zf (code) */
BigInteger fvars(BigInteger code){
BigInteger result=falll(Zf,code);
result=falll(Yf,result);
result=falll(Nf,result);
return result;}

/** &beta;<sub>f</sup>(x)=&beta;(X<sub>f</sup>,Y<sub>f</sup>,x)*/
BigInteger beta(int vp,int vx){
int v1,cs,es,vs;
cs=Csp;es=Esp;vs=VarList.size();
//if (vin==0)v1=newV();else v1=vin;
v1=newV();
BigInteger V1=varb(v1);
Estore[Esp++]=v1;
addcond(binop(V1,0,unop(5,binop(unop(5,varb(vp)),7,varb(Zf)))));
addcond(exists(locv,binop(varb(Yf),0,binop(varb(vx),6,binop(Vloc,7,V1)))));
addcond(exists(locv,binop(V1,0,binop(varb(vx),6,unop(5,Vloc)))));
return resconds(cs,es,vs);}}


/** counter for int form of variables */
int vbase;
/** Store for information about functions*/
Funinfo[] finfo=new Funinfo[50];
/** number of functions without a name
 * 2 i.e. !! and (:) */
int nonf;//=0;
/* int form of a variable for general use &exist; x1 (...)*/
final int locv=3;

/** list of numbers of functions used in code */
int[] deplist=new int[50];
/** Reserved words */
String[] reswords={"if","case","let","module","where","import","Integer","then","else",
     "div","mod","in","of"};
/** 2 character tokens */
char[][] tokens={{':',':'},{'-','>'},{'!','!'},{'=','='},{'/','='},{'<','='},{'>','='},{'|','|'},{'&','&'}};
/** Function names */
IdList FunList=new IdList();
/**Haskell variable names */
IdList VarList=new IdList();
/** Reserved words in List form */
java.util.List ResList;//=new ArrayList();
/** Store for code of functions*/
BigInteger[] Fstore=new BigInteger[150];
/** Store for coded conditions */
BigInteger[] Cstore=new BigInteger[150];
/** Store for variables which need &exist; condition before current piece of code */
int[] Estore=new int[150];

/** Store for info about Haskell variables
 * Match position in VarList.  Stores (int form)*8)+type */
int[] Varstore=new int[200];

/** Press to encode statement of the form y=f(x) for a function f */
JButton but3 = new JButton("y=*f*(x)");
/** Press to encode statement of the form &sigma;<sub>1</sub> */
JButton but4 = new JButton("\u03C3\u2081");
/** Press to encode statement of the form &sigma;<sub>2</sub> */
JButton but5 = new JButton("\u03C3\u2082");
/** Edit area for name of function for y=f(x) encoding */
JTextField fedit=new JTextField();
/** Text area for output of G&ouml;del number of G&ouml;del statement */
JTextArea prnum=new JTextArea();
/** Text area for input of Haskell code */
JTextArea plines=new JTextArea();
/** Holds the Haskell code */
String strin;
/** Current position in strin */
int pos;
/** Counter for deplist */
int fdct;
/** Stack pointer for CStore */
int Csp;
/** Stack pointer for EStore */
int Esp;
/** General compilation error */
Error InvInp=new Error("Invalid Input");
/** More specific type Error */
Error TypeErr=new Error("Type Error");
final BigInteger THREE=BigInteger.valueOf(3);
final BigInteger FOUR=BigInteger.valueOf(4);
final BigInteger ZERO=BigInteger.ZERO;
/** Encoded form of predefined functions */
BigInteger predefs;
//BigInteger todo=ZERO;
//TExpr todox=new TExpr(ZERO,0);

/** Coded form of zero */
final BigInteger c0=BigInteger.valueOf(9);//
/** coded form of variable x1 (locv) */
final BigInteger Vloc=BigInteger.valueOf(60);//111100
/** coded form of first variable (x) */
final BigInteger Z0=BigInteger.valueOf(14);//1110 =varb(0) - but I'll probably change this
/** int form of first variable (x) */
final int z0=0;

/** info for function currently being compiled */
Funinfo finf;
/** Set of function nos. for which dependency calculation has started */
BitSet dep1=new BitSet();
/** Set of function nos. for which dependency calculation has finished */
BitSet dep2=new BitSet();

	
/** Initalise applet */
public void init() {
ResList=Arrays.asList(reswords);
setLayout(null);
setBackground(new Color(230,240,240));
add(fedit);
fedit.setBounds(10,275,100,20);
fedit.setText(lfile);
add(but3);
but3.setBounds(120,275,80,20);
add(but4);
but4.setBounds(240,275,50,20);
add(but5);
but5.setBounds(300,275,50,20);
JScrollPane scroll1 = new JScrollPane(plines);
add(scroll1);
JScrollPane scroll2 = new JScrollPane(prnum);
add(scroll2);
scroll1.setBounds(10,20,600,250);
scroll2.setBounds(10,300,600,250);
prnum.setLineWrap(true);
plines.addCaretListener(this);
but3.addActionListener(this);
but4.addActionListener(this);
but5.addActionListener(this);
but3.getModel().setActionCommand("fx");
but4.getModel().setActionCommand("sig1");
but5.getModel().setActionCommand("sig2");
try{
  URL url1=new URL("http://www.tachyos.org/godel/"+lfile+".hs");
  BufferedReader in = new BufferedReader(new InputStreamReader(url1.openConnection().getInputStream()));
  String s;
  while ((s= in.readLine()) != null) plines.append(s+"\n");}
catch (FileNotFoundException r1){}
catch (IOException r2){};
}
	
/** Reset caret colour after it's turned red to show an error */
public void caretUpdate(CaretEvent e){
plines.setSelectionColor(Color.BLACK);}
	
/** Code for #t1=#t2*/
BigInteger iseq(BigInteger t1,BigInteger t2){
return binop(t1,0,t2);}

/** &forall; #v #t1 */
BigInteger falll(int v,BigInteger t1){
return binop(varb0(v),3,t1);}

/** #v&lt;N<sub>f</sub>*/
void paramcond(int v,int fno){
addcond(lessthan(varb(v),varb(finfo[fno].Nf)));}

/** #t1&lt;#t2 */
BigInteger lessthan(BigInteger t1,BigInteger t2){
return exists(locv,iseq(binop(t1,6,unop(5,varb(locv))),t2));}

/** ¬(&forall;z (z=num(n)&rArr;¬#n)*/
BigInteger diag(BigInteger n){
 return nott( falll(2,impp(iseq(varb(2), num (n)), nott (n))));}

/** &exist; #v #T */
BigInteger exists(int v,BigInteger T){
return nott(binop(varb0(v),3,nott(T)));}

/** &sigma;<sub>&phi;</sub> */
BigInteger sigma(BigInteger phi){
int diag=FunList.indexOf("diag");
 BigInteger n=nott( falll(2,impp(finfo[diag].beta(0,2), nott (phi))));
 return diag(n);}

/** produces the code for predefined list operators (:),(!!) and functions length and tail */ 
void predefines(){
int[] v=new int[9];
int x,y,n,i,es,cs,vs;
cs=Csp;es=Esp;vs=VarList.size();
x=newV();y=newV();n=newV();
for (i=0;i<9;i++) v[i]=newV();
BigInteger res;
finfo[0]=new Funinfo(0331);//(:)::Integer->[Integer]->[Integer];
finfo[1]=new Funinfo(0311);//(!!)::[Integer]->Integer->Integer;
nonf=2;
FunList.add("length");
FunList.add("tail");
finfo[2]=new Funinfo(013);//length::[Integer]->Integer;
finfo[3]=new Funinfo(033);//tail::[Integer]->[Integer];
for (i=2;i<=8;i++)Estore[Esp++]=v[i];
for (i=3;i<=5;i++) paramcond(v[i],1);
paramcond(v[6],2);
addcond(finfo[0].beta(v[1],v[2]));
addcond(iseq(J(varb(v[2]),c0),varb(v[3])));
addcond(iseq(J(varb(v[2]),unop(5,varb(n))),varb(v[4])));
addcond(iseq(J(varb(y),varb(n)),varb(v[5])));
addcond(iseq(Z0,BigInteger.valueOf(9)));//z0=0
addcond(finfo[1].beta(v[4],v[6]));
addcond(finfo[1].beta(v[4],v[5]));
addcond(finfo[1].beta(v[3],x));
addcond(finfo[2].beta(v[2],v[7]));
addcond(iseq(varb(v[8]),unop(5,varb(v[7]))));
addcond(finfo[2].beta(y,v[8]));
addcond(finfo[2].beta(z0,z0));
addcond(finfo[3].beta(v[2], y));
res=resconds(cs,es,vs);
paramcond(x,0);
paramcond(y,0);
paramcond(n,0);
predefs=resconds(cs,es,vs);
res=impp(predefs,res);
res=falll(n,res);res=falll(x,res);
predefs=falll(y,res);}

/** Recursively calculates which functions a function depends upon 
 * f may be recursively defined, but mutual recursion is not allowed
 * @param f index of function
 */
void calcdep(int f){
if (dep1.get(f))throw InvInp;
dep1.set(f);
for(int i=finfo[f].dependsOn.nextSetBit(0); i>=0; i=finfo[f].dependsOn.nextSetBit(i+1)) 
  if (i!=f&&!dep2.get(i)) calcdep(i);
dep2.set(f);
deplist[fdct++]=f;}

/** Calculates which functions a function depends upon, using calcdep 
 * @param f index of function
 */
void calcdeps(int f){
fdct=0;
dep1.clear();dep2.clear();
calcdep(f);
}

/** compiles the functions defined in the plines edit,  */
void fcompile(){
FunList.clear();VarList.clear();
pos=0;vbase=6;itype=0;
strin=plines.getText();
predefines();
parse1();
}

BigInteger funcround(BigInteger fcode){
int d;
BigInteger res =nott(fcode);
for (int i=0;i<fdct;i++){
  d=deplist[i];
  if (d>=4) res=binop(Fstore[d-nonf],2,res);}
res=binop(predefs,2,res);
for (int i=0;i<fdct;i++){
  d=deplist[i];
  res=finfo[d].fvars(res);}
return nott(res);
}

BigInteger yisfx(String fname){
fcompile();
int f=FunList.indexOf(fname);
calcdeps(f+nonf);
BigInteger code=finfo[f+nonf].beta(0,1);//y=*f*(x)
return funcround(code);
}

/** responds to button press */
public void actionPerformed(ActionEvent e) {
String ac=e.getActionCommand();
String fname;
BigInteger result=ZERO;
BigInteger phi;
 try{
if (ac=="fx"){
    fname=plines.getSelectedText();
    if (fname==null||fname.length()==0)fname=fedit.getText(); 
    else fedit.setText(fname);
    result=yisfx(fname);
  }
  else if (ac=="sig1"){
    fcompile();
    int proof=FunList.indexOf("proof");
    calcdeps(proof+nonf);
    phi=falll(2,nott(finfo[proof+nonf].beta(0, 2)));
    result=funcround(sigma(phi));
  }
  else if (ac=="sig2"){
    fcompile();
    int proofsearch=FunList.indexOf("proofsearch");
    calcdeps(proofsearch+nonf);
    phi=falll(2,nott(finfo[proofsearch+nonf].beta(z0, 2)));
    result=funcround(sigma(phi));
    
  }
	} catch (Error ii){
		plines.requestFocus();
		plines.setSelectionStart(pos);
		plines.setSelectionEnd(pos+1);
		plines.setSelectionColor(Color.RED);
		JOptionPane.showMessageDialog(null, ii.getMessage());}
prnum.setText(result.toString());
/*prnum.setText("");
for (int c=0;c<FunList.size();c++){
  prnum.append("<br>"+Integer.toString(c+nonf)+":"+FunList.get(c)+"::");
  for (int i=0;i<FunList.size();i++)
    if (finfo[c+nonf].dependsOn.get(i+nonf))prnum.append(FunList.get(i)+",");
  prnum.append("\n");}//*/
}
/** Bitstream forms of 0-3 (0,0',0'',0''')*/
BigInteger[] numc={BigInteger.valueOf(011),BigInteger.valueOf(0113),BigInteger.valueOf(01133),BigInteger.valueOf(011333)};
/** Encodes a number as an arithmetic expression */
BigInteger num(BigInteger x){
if (x.compareTo(THREE)>=0) 
  return binop(binop(num(x=x.divide(THREE)),7,numc[3]),6,numc[x.mod(THREE).intValue()]);
return numc[x.intValue()];}

//--------------------------------------

/** moves pos to the first non-whitespace character */
void skipsps(){
while (pos<strin.length()&&Character.isWhitespace(curch=strin.charAt(pos)))pos++; 
}

/** Type of current item */
int itype;
/** current character */
char curch;
/** current item if it is an integer */
BigInteger curnum;
/** current item if it is an identifier */
String curword;
/** current item if it is a token */
int curtok;

/** Gets item from input text.   */
void getitem(){
StringBuffer sbuf=new StringBuffer();
if (itype>0)return;
while (pos<strin.length()&&Character.isWhitespace(curch=strin.charAt(pos)))pos++; 
if (Character.isDigit(curch)){
  do {sbuf.append(curch);pos++;curch=strin.charAt(pos);}
  while (Character.isDigit(curch));
  curnum=new BigInteger(sbuf.toString());itype=3;
  return; }
if (Character.isLetter(curch) ){
  do {sbuf.append(curch);pos++;curch=strin.charAt(pos);}
  while (Character.isLetterOrDigit(curch)||curch=='\'');
  curword=sbuf.toString();
  itype=4;return;}
for (int i=0;i<9;i++)
  if (curch==tokens[i][0]&&strin.charAt(pos+1)==tokens[i][1]){
   pos+=2;curtok=i;itype=2;return;}
itype=1;pos++;
}

/** Requires a word, that is an identifier or reserved word */
void getword(){
getitem();
if (itype!=4)throw InvInp;
itype=0;
}

/** Checks whether the current item is a single character matching c*/
boolean chkch(char c){
getitem();
boolean res=(itype==1&&curch==c);
if (res) itype=0;
return res;
}

/** Checks whether the current item is a single character in S.
 * @param S characters considered
 * @return The index of the character in S if found, otherwise -1
 */
int chkchS (String S){
getitem();
if (pos>=strin.length()||itype!=1) return -1;
int res=S.indexOf(curch);
if (res>=0)itype=0;
return res;
}

/** requires the current item to be a single character matching c
 * @param c the character to match
 */
void chkchv(char c){
if (!chkch(c))
	 throw InvInp;
}

/**Checks whether the current item is a 2 character token number t*/
void chktokv(int t){
getitem();
if (itype!=2||curtok!=t) throw InvInp;
itype=0;
}
/** Encodes the result of the unary operator */
BigInteger unop(int op,BigInteger x1){
int shft;
if (op>=4){op=2*op-7;shft=3;} 
else shft=2;
return x1.shiftLeft(shft).add(BigInteger.valueOf(op));  
}
/** Encodes the result of a binary operator */
BigInteger binop(BigInteger x1,int op,BigInteger x2){
int n2=x1.bitLength();
 BigInteger t=x2.shiftLeft(n2-1).add(x1.clearBit(n2-1));
 return unop(op,t);
}

/** #A &rArr; #B */
BigInteger impp (BigInteger A,BigInteger B){
return binop(A,2,B);	
}

/**Function calls, variables, numbers,[], (expr),duples */
TExpr expr10(){ 
TExpr t,t1;
int id,tk,p,r;
BigInteger res=ZERO;
getitem();
if (itype==4){
  itype=0;
  id=FunList.lastIndexOf(curword);
  if (id<0) id=FunList.lastIndexOf(curword+'\'');
  if (id>=0){
    finf.dependsOn.set(id+nonf);
	  tk=finfo[id+nonf].type;
	  t=expr10();
    //v=parameter and f v and v<Nf
    if (t.type!=tk%8) throw TypeErr;
	  res=t.value;
	  tk/=8;
	  while (tk>8){
		  t1=expr10();
		  if (t1.type!=tk%8) throw TypeErr;
		  res=J(res,t1.value);
		  tk/=8;}
    p=newV();
    r=newV();
    Estore[Esp++]=p;Estore[Esp++]=r;
    addcond(iseq(varb(p),res));
    addcond(finfo[id+nonf].beta(p,r));
	  return new TExpr(varb(r),tk);}
  id=VarList.lastIndexOf(curword);
  if (id>=0){
    return new TExpr(varb(Varstore[id]/8),Varstore[id]%8);}
  if (curword.equals("fromInteger")||curword.equals("toInteger")) return expr2(0);
  throw InvInp;}
if (itype==3){itype=0;return new TExpr(num(curnum),1);}
if (chkch('[')){chkchv(']');
  return new TExpr(BigInteger.valueOf(9),3);}
chkchv('(');
t=expr2(0);
if (chkch(',')){	  
  t1=expr2(0);
  if (t.type!=1||t1.type!=1)throw TypeErr; 
  t=new TExpr(J(t.value,t1.value),2);}
chkchv(')');
return t;}

/** !! operator */
TExpr expr9(){
	int p,r;
	TExpr t1=expr10();
  getitem();
	while (itype==2&&curtok==2){
  itype=0;
	TExpr ind=expr10();
  if (t1.type!=3||ind.type!=1) throw TypeErr;
  p=newV();r=newV();
  Estore[Esp++]=p;Estore[Esp++]=r;
  addcond(binop(varb(p),0,J(t1.value,ind.value)));
  addcond(finfo[1].beta(p,r));
	t1.value=varb(r);
  t1.type=1;	}
	return t1;
}

/**  * #0, `div` #1, `mod` #2 */
int mulop(){ 
int a=chkchS("*`");
if (a==1){
  getword();
  a=ResList.indexOf(curword)-8;// 1 or 2
  itype=0;chkchv('`');
  if ((a+1)/2!=1) throw InvInp;}
return a;
}

/** *, `div`, `mod` */
TExpr expr7(){ 
int op,v1,v2;
TExpr t1=expr9();
while ((op=mulop())>=0){
  TExpr t2=expr9();
  if (t1.type!=1||t2.type!=1)throw TypeErr;
  if (op==0)  t1.value=binop(t1.value,7,t2.value);
  else {v1=newV();v2=newV();
    Estore[Esp++]=v1;Estore[Esp++]=v2;
    addcond(iseq(t1.value,binop(binop(varb(v1),7,t2.value),6,varb(v2))));
    addcond(lessthan(varb(v2),t2.value));
    if (op==1)t1.value=varb(v1);
    else t1.value=varb(v2);}}
return t1;
}

/** + and - */
TExpr expr6(){
int op, v;
TExpr t1=expr7();
while ((op=chkchS("+-"))>=0){
  TExpr t2=expr7();
  if (t1.type!=1||t2.type!=1)throw TypeErr;
  if (op==0) t1.value=binop(t1.value,6,t2.value);
  else{v=newV();
    Estore[Esp++]=v;
    addcond(binop(binop(varb(v),6,t2.value),0,t1.value));
    t1.value=varb(v);}} 
return t1;}

//* (:) operator*/
TExpr expr5(){
TExpr t1=expr6();
if (!chkch(':')) return t1;
TExpr t2=expr5();
if ((t1.type!=1)||(t2.type!=3)) throw InvInp;
int p=newV();int r=newV();
Estore[Esp++]=r;Estore[Esp++]=p;
addcond(binop(varb(p),0,J(t1.value,t2.value)));
addcond(finfo[0].beta(p,r));
t2.value=varb(r);
return t2;
}


/** Encode ¬#A */
BigInteger nott(BigInteger A){
  if (A.and(THREE).compareTo(BigInteger.ONE)==0)return A.shiftRight(2);
	return A.shiftLeft(2).add(BigInteger.ONE);
}

/** Add a condition to the list*/
void addcond(BigInteger A){
Cstore[Csp++]=A;	
}
/** &exist; variables (&and; Conditions) */
BigInteger resconds(int csb,int esb,int vsb){
int i;
BigInteger res=Cstore[csb];
for (i=csb+1;i<Csp;i++)res=nott(impp(Cstore[i],nott(res)));  
for (i=esb;i<Esp;i++)res=exists(Estore[i],res);
VarList.shrinkTo(vsb);
Csp=csb;Esp=esb;
return res;
}
/**relational operators */
TExpr expr4(){

TExpr b=expr5();
int t=chkchS("<>");
if (t<0&&itype==2){if (curtok>=3&&curtok<=6) t=curtok-1;}
if (t>=0){
itype=0;
TExpr b1=expr5();  
if (b.type!=1||b1.type!=1)throw TypeErr;
switch (t){
	case 0:b.value=lessthan(b.value,b1.value);break; //<
	case 1:b.value=lessthan(b1.value,b.value);break;//>
	case 2:b.value=iseq(b.value,b1.value);break;// ==
	case 3:b.value= nott( iseq(b.value,b1.value));break;// /=
  case 4:b.value=nott(lessthan(b1.value,b.value));break;// <=
  case 5:b.value=nott(lessthan(b.value,b1.value));break;// >=
  }
b.type=4;
}
return b;}

/** && operator*/
TExpr expr3(){
TExpr b=expr4();
getitem();
if (itype==2&&curtok==8){
  itype=0;
  TExpr t=expr3();
  if (b.type!=4||t.type!=4)throw TypeErr;
  b.value= nott(impp(b.value,nott(t.value)));}
return b;}


/** if, case and let and || operator */
TExpr expr2(int vareq){ 
int varn,item,d1,d2,typ,c,csb,esb,vsb;
TExpr t1,t2,tb;
BigInteger res;
getitem();
if (itype==4){
  item=ResList.indexOf(curword);
  if (item>=0) switch (item) {
  case 0://if 
    itype=0;
    if (vareq==0) varn=newV(); else varn=vareq;
    tb=expr2(0);
    if (tb.type!=4)throw TypeErr;
    getword();
    if (ResList.indexOf(curword)!=7) throw InvInp;
    t1=expr2(varn);
    res=impp(tb.value,t1.value);
    getitem();
    if (itype==4&&ResList.indexOf(curword)==8){
      itype=0;
      t2=expr2(varn);
      if (t1.type!=t2.type)throw TypeErr;
      res=nott(impp(res,nott(impp(nott(tb.value),t2.value))));    }
    if (vareq==0){addcond(res);res=varb(varn);}
    return new TExpr(res,t1.type);
  case 1://case
    itype=0;typ=0;esb=Esp;csb=Csp;vsb=VarList.size();
    if (vareq==0) varn=newV(); else varn=vareq;
    int vcase=newV();
    Estore[Esp++]=vcase;
    tb=expr2(vcase); addcond(tb.value);
    chkResv(12); chkchv('{');
    BigInteger union=ZERO;
    while (!chkch('}')){
      if (chkch('_')){t1=new TExpr(nott(union),3);}
      else {t1=expr2(vcase);
        if (union.intValue()==0)union=t1.value; else union=impp(nott(union),t1.value);}
      chktokv(1);
      t2=expr2(varn);
      addcond(impp(t1.value,t2.value));
      if (typ==0)typ=t2.type;
      else if (typ!=t2.type)throw TypeErr; 
      chkchv(';');}  
    res=resconds(csb,esb,vsb);
    if (vareq==0){addcond(res);res=varb(varn);}
    return new TExpr(res,typ);
  case 2://let
  int vs=VarList.size(); 
  itype=0;chkchv('{');
  do {
    if (chkch('}'))break;
    if (chkch('(')){
      d1=makesym(1);chkchv(',');
      d2=makesym(1);chkchv(')');
      chkchv('=');
      t1=expr2(0);
      if (t1.type!=2)throw TypeErr;
      addcond(binop(J(varb(d1),varb(d2)),0,t1.value));}
    else {getword();
      VarList.add(curword);
      d1=newV();
      int id=VarList.size()-1;
      chkchv('=');
      t1=expr2(d1);
      Varstore[id]=8*d1+t1.type;}
    c=chkchS(";}");
    if (c<0)throw InvInp;
    }while (c==0);
  chkResv(11);
  t1=expr2(vareq);
  VarList.shrinkTo(vs);
  return t1;
  }}
t1=expr3();
getitem();
if (itype==2&&curtok==7){
  t2=expr2(0);
  if (t1.type!=4||t2.type!=4)throw TypeErr;
  t1.value=impp(nott(t1.value),t2.value);}
if (vareq>0)t1.value=iseq(t1.value,varb(vareq));
return t1;
}

/** Requires current item to be 'Integer' reserved word */ 
void chkIntv(){
getitem();
if (itype!=4||ResList.indexOf(curword)!=6)throw InvInp;
itype=0;
}

/** Gets type descriptor.
 * Type will be based on Integer */
int getType(){
int res=1;
getitem();
if (chkch('[')) res=3;
else if (chkch('('))res=2;
chkIntv();
if (res==3)chkchv(']');
else if (res==2){
  chkchv(',');chkIntv();chkchv(')');}
return res;
}

/** Deals with the definition part of a function (which must be present)*/
void DefFn(String name){
int mult=1;
FunList.add(name);
int id=FunList.size()-1;
int ftyp=0;
chktokv(0);
do {itype=0;ftyp=ftyp+mult*getType();mult*=8;getitem();} while (itype==2&&curtok==1);
finfo[id+nonf]=new Funinfo(ftyp);
chkchv(';');
}

/** Defines the current identifier to be a variable of a given type
 * @param type 
 * @return int representation of variable
 */

int makesym(int type){
getword();
VarList.add(curword);
int id=VarList.size()-1;
int v=newV();
Varstore[id]=8*v+type;
return v;
}

/** 
 * @param n - an int representation of an arithmetic variable 
 * @return the bitstream representation of the variable
 */
BigInteger varb0(int n){
BigInteger num=THREE;
while (n>0){n--;
num=num.multiply(FOUR).add(BigInteger.valueOf(n%3));
n/=3;}
return num.setBit(num.bitLength());}

/**
 * @param n - an int representation of an arithmetic variable 
 * @return the bitstream representation of the variable with last bit 0 (signifying a variable)
 */
BigInteger varb(int n){
return varb0(n).shiftLeft(1);}

/**J is a 1 to 1 functio combining two integers into one 
 * @param t1 1st term
 * @param t2 2nd term
 * @return representation of (t1+t2)^2+t1+1
 */
BigInteger J(BigInteger t1,BigInteger t2){
BigInteger res;
res=binop(t1,6,t2);
res=binop(res,7,res);
res=binop(res,6,t1);
return binop(res,6,BigInteger.valueOf(75));
}

/** Combines n integer variables into one integer 
 * @param vs int representation of variables
 * @param n number of variables
 * @return values combined using J function
 */
BigInteger Jn(int[]  vs,int n){
BigInteger res=varb(vs[0]);
for (int i=1;i<n;i++) res=J(res,varb(vs[i]));
return res;
}

/** Creates (if needed) a variable equal to a given term
 * @param Term 
 * @return int form of variable equal to Term
 */
BigInteger vform(BigInteger Term){
if (!Term.testBit(0)) return Term;
BigInteger v=varb(newV());
addcond(binop(Term,0,v));
return v;
}
	
/** Processes body of a function
 * @param id function identifier
 * @return code for function
 */
BigInteger DoFun(int id){
	int[] ptyps=new int[4];
	int[] pvars=new int[4];
int ftyp,vp,vres,vs,es,cs,n=0,j=0;
TExpr resx;
BigInteger res,pcond;
finf=finfo[id+nonf];
ftyp=finf.type;
while (ftyp>7){ptyps[n++]=ftyp%8;ftyp=ftyp/8;}
for (j=0;j<n;j++)pvars[j]=makesym(ptyps[j]);
es=Esp;cs=Csp;vs=VarList.size();
vp=newV(); vres=newV();
Estore[Esp++]=vres;
addcond(finf.beta(vp,vres));
chkchv('=');
resx=expr2(vres);
if (resx.type!=ftyp)throw TypeErr;
chkchv(';');
addcond(resx.value);
res=resconds(cs,es,vs);
addcond(lessthan(varb(vp),varb(finf.Nf)));
addcond(iseq(varb(vp),Jn(pvars,n)));
pcond=resconds(cs,es,vs);
res=impp(pcond,res);
for (j=0;j<n;j++)res=falll(pvars[j],res);
VarList.shrinkTo(vs);
return falll(vp,res);	
}

/** Ensures that current word is a given reserved word
 * @param i Number of reserved word required
 */
void chkResv(int i){
getitem();
if (itype!=4||ResList.indexOf(curword)!=i) throw InvInp;
itype=0;
}

/** Parses program in strin */
void parse1(){
chkResv(3);//Module
getword();//name
chkResv(4);//where
chkchv('{');
getitem();
if((itype==4&&ResList.indexOf(curword)==5)){//import
  itype=0;
	do getword(); while (chkch('.'));
	chkchv(';');}
while (!chkch('}')){
  getword();
	int id=FunList.lastIndexOf(curword);
	if (id<0) DefFn(curword);
  else Fstore[id]=DoFun(id);}
for (int c=0;c<FunList.size();c++)
  prnum.append(FunList.get(c)+","+((Fstore[c]==null)?0:1)+"\n");
}
	
}