/*  Copyright (C) Stephen Lee 2007 .  
 *  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.util.*;
import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import javax.swing.*;
import javax.swing.plaf.basic.BasicArrowButton;

import java.math.*;

/**This is an applet to implement a Gödel numbering scheme.
 *  It translates between formal arithmetic statements and positive integers.
 *  For further information see <a href='http://www.tachyos.org/godel/Godel_applet1.html'>G&ouml;del numbering applet</a>*/
public class godel1 extends Applet implements KeyListener,ActionListener {

private static final long serialVersionUID = 1L; 
public godel1(){}

Font cf1;
/** Text Area for aritmetic formulae*/
JTextArea txta=new JTextArea();
/**Text Area for Godel Numbers */
JTextArea numed=new JTextArea();

//Label lab1=new Label();
String strin;
/** Current position in text*/
int pos;
/** Value of (G&ouml;del) number entered.
 *  This is the input bitstream*/
BigInteger numin;

/** Set when end of input number reached */
boolean endflg;
/** Output text as HTML */
boolean html;
/** Press to convert from G&ouml;del numbers to arithmetic formulae*/
BasicArrowButton but1 =new BasicArrowButton(SwingConstants.NORTH);
/** Press to convert from arithmetic formulae to G&ouml;del numbers*/
BasicArrowButton but2 =new BasicArrowButton(SwingConstants.SOUTH);
final BigInteger THREE=BigInteger.valueOf(3);
final BigInteger FOUR=BigInteger.valueOf(4);
/** Thrown if text input is not valid */
Error InvInp=new Error("Invalid Input");
/** check if Godel numbers are to be in binary*/
JCheckBox binar=new JCheckBox("binary");
/** Check to wrap number rather than having multiple numbers*/
JCheckBox twrap=new JCheckBox("text-wrap");
/** Check to generate output in the form of HTML (doesn't work for input)*/
JCheckBox ohtml=new JCheckBox("html out");
/** radix - swapped between 10 and 2 */
int radx=10;
/** counter which is used to put regular nbsp's into html, to help with wrapping*/
int spct=0;


public void keyPressed(KeyEvent e) {}
public void keyReleased(KeyEvent e) {}

/** replace alt_A with &forall; and &gt; with &rArr;*/
public void keyTyped(KeyEvent e) {
char c= e.getKeyChar();
int m=e.getModifiers();	
if ((m&InputEvent.ALT_MASK)>0){	
    if (Character.toUpperCase(c)=='A')txta.replaceSelection("\u2200");    
    else if (c=='>')txta.replaceSelection("\u21D2");    
	e.consume();}}

/** react to up and down buttons, and binary and text-wrap checkbox changes */ 
public void actionPerformed(ActionEvent e) {
    int rado;
    StringTokenizer tok;
String res;
String ac=e.getActionCommand();
try{
if (ac=="down"){
  html=ohtml.isSelected();
  txta.setText(""); 
  tok=new StringTokenizer(numed.getText(),"\n"); 
  while (tok.hasMoreTokens()){
    numin=new BigInteger(tok.nextToken(),radx);
    res=wff();
    if (numin.compareTo(BigInteger.ONE)!=0) res="ERROR ("+res+")";
    txta.append(res+"\n");}}
else if (ac=="up"){ 
	tok=new StringTokenizer(txta.getText(),"\n"); 
	  numed.setText("");
	  while (tok.hasMoreTokens()){
    strin=tok.nextToken();
    pos=0;
    numin=parse1();
    /*n=numin.bitLength();
    numin=numin.clearBit(n-1);*/
    numed.append(numin.toString(radx)+"\n");}}
else if (ac=="binary"){
     tok=new StringTokenizer(numed.getText(),"\n"); 
     numed.setText("");
     rado=radx;
	 radx=12-radx;
     while (tok.hasMoreTokens()){
       BigInteger pc=new BigInteger( tok.nextToken(),rado);
	   numed.append(pc.toString(radx)+"\n");}
	}
else if (ac=="text-wrap"){
  numed.setLineWrap(twrap.isSelected());
}
} catch (Error ii){JOptionPane.showMessageDialog(null, "Input not valid");}
}

/**Set up applet */
public void init() {
 setLayout(null);
 setBackground(new Color(230,240,240));
// cf1=new Font("Lucida Sans Unicode",Font.PLAIN,14);
 cf1=new Font("",Font.PLAIN,14);
// add(numed);
// numed.setBounds(10,10,200,20);
 add(but1);
 but1.setBounds(10,275,40,20);
 but1.setFont(cf1);
 add(but2);
 but2.setBounds(60,275,40,20);
 JScrollPane scroll1 = new JScrollPane(txta);
 add(scroll1);
 JScrollPane scroll2 = new JScrollPane(numed);
 add(scroll2);
 txta.setFont(cf1);
 scroll1.setBounds(10,300,600,250);
 scroll2.setBounds(10,20,600,250);
 txta.addKeyListener(this);
 txta.setLineWrap(true);
 but2.addActionListener(this);
 but1.addActionListener(this);
 but1.getModel().setActionCommand("up");
 but2.getModel().setActionCommand("down");
 //add(lab1);
 //lab1.setBounds(110,275,500,20);
 add(binar);
 binar.setBounds(10, 5, 60, 15);
 binar.addActionListener(this);
 add(twrap);
 twrap.setBounds(80, 5, 80, 15);
 twrap.addActionListener(this);
 add(ohtml);
 ohtml.setBounds(170, 5, 90, 15);
}
//--------------------------------
/** Get 2 bits of input bitstream */
int get2(){
endflg=(numin.signum()==0);
int result=numin.and(THREE).intValue();
numin=numin.shiftRight(2);
return result;
}

/** Get variable from input bitstream
 * @return variable in text form
 */
String getvar(){
    int num,n;
    String sn;
 num=0;
 do {n=get2(); if (n<3)num=3*num+n+1;}while (n<3&&!endflg);
 if (num>=3) sn=String.valueOf(num/3);else sn="";
 return String.valueOf((char)('x'+num%3))+sn;}
 
/** Get term from input bitstream
 * @return term in text form
 */
String term(int p){
String res; int q=2;
boolean isvar=!numin.testBit(0);
numin=numin.shiftRight(1);
if (isvar)return getvar();
else switch (get2()){
 case 0:res="0";break;
 case 1:res= term(q)+"\'";break;
 case 2:q=0;res=term(q)+"+ "+term(q);break;
 default:q=1;res=term(1)+"*"+term(1);}
if (p>q)return "("+(html&&spct++%9==0?"&nbsp; ":" ")+res+")"; else return res;
}

/** Get formula from input bitstream
 * @return formula in text form
 */
String wff(){
 switch (get2()){
 case 0:return term(0)+"="+term(0);
 case 1:return (html?"&not;":"¬")+wff();
 case 2:return "("+wff()+(html?"&rArr;":"\u21D2")+wff()+")";
 case 3:return (html?"&forall;":"\u2200")+getvar()+" "+wff();}
 return "";
}
//--------------------------------------
/** Gets next character from text */
char nxtch(){
if(pos>=strin.length()) 
 throw InvInp;
while (strin.charAt(pos)==' ') pos+=1 ;
return strin.charAt(pos++);
}

/** checks whether current character matches a given one
 * @param c the character to match
 * @return true for a match
 */
boolean chkch(char c){
 while (pos<strin.length()&&strin.charAt(pos)==' ')pos++;
  if(pos>=strin.length()||strin.charAt(pos)!=c)return false;
 pos++;return true;
}

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

/** Translates a text variable into a bitstream form
 * @param c - the initial letter of the variable
 * @return bitstream form of variable
 */
BigInteger getvarn(char c){
    BigInteger num=THREE;
    int n ;
 n=0;   
 while (pos<strin.length()&&Character.isDigit(strin.charAt(pos))){
  n*=10;n+=Character.digit(strin.charAt(pos),10); pos++;}
 n=n*3+(int)(c-'x');
 while (n>0){n--;
  num=num.multiply(FOUR).add(BigInteger.valueOf(n%3));
  n/=3;}
 return num.setBit(num.bitLength());}

/** Applies a unary operator to a term or formula.
 * Also used for operator part of binary operators.
 * @param op code for operator ' 5,&not; 1 
 * @param x1 code for input term or formula
 * @return code for resulting term or formula
 */
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)); 	
}
//-------------------

/**  Applies a binary operator to a pair of terms or formulae.
 * 
 * @param x1 first term or formula
 * @param op code for binary operator
 * @param x2 second term or formula
 * @return code for resulting term or formula
 */
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);
}

/**Handles lowest level items in expression
 * zero, variables and (expression)
 * @return code for item.
 */
BigInteger parse6(){
BigInteger cur=BigInteger.ZERO;
 char c=nxtch();
 if (c=='0')return BigInteger.valueOf(9);
 if (c>='x'&c<='z')return getvarn(c).shiftLeft(1);
 if (c=='('){cur=parse1();chkchv(')');return cur;}
 throw InvInp;
}

/** Handles successor operator
 * @return code for term
 */
BigInteger parse5(){
 BigInteger cur=parse6();
 while(chkch('\''))cur=unop(5,cur);
 return cur;}

/** Handles multiplication 
 * @return code for term
 */
BigInteger parse4(){
    BigInteger cur;
 cur=parse5();
 while (chkch('*'))cur=binop(cur,7,parse5());
 return cur;}

/** HAndles addition 
 * @return code for term
 */
BigInteger parse3(){
    BigInteger cur;
 cur=parse4();
 while (chkch('+'))cur=binop(cur,6,parse4());
 return cur;
}
 
/** Handles &forall;,&not; and equality
 * @return code for formula
 */
BigInteger parse2(){
    BigInteger cur;
 if (chkch('\u2200')){return binop(getvarn(nxtch()),3,parse2());}
 if (chkch('¬')) return unop(1,parse2());
 cur=parse3();
 if (chkch('='))return binop(cur,0,parse3());
 return cur;}
 
/** Main routine for parsing strin
 * Handles &rArr;
 * &rArr; is right associative A&rArr;B&rArr;C means A&rArr;(B&rArr;C)
 * @return code for formula
 */
BigInteger parse1(){
	 BigInteger cur;
 cur=parse2();
 if (chkch('\u21D2'))return binop(cur,2,parse1());
 return cur;
}

 
public String getAppletInfo() {
 return "Godel number";
}

}