/*  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.awt.datatransfer.*;
import java.math.*;
/**This is an applet to implement a numerical encoding of arithmetical proofs.
 * Such an encoding is required in the proof of Gödel's incompleteness theorem.
 * It uses the axiom system describes in <a href='http://www.tachyos.org/godel/proof.html'>A proof system for arithmetic</a>
 *  For further information see <a href='http://www.tachyos.org/godel/Godel_applet2.html'>G&ouml;del numbering applet</a>
 * @author Stephen Lee */
public class Godel2 extends Applet implements ActionListener,MouseListener {

private static final long serialVersionUID = 1L; 

//Representation of an expression as a BigInteger always includes an extra leaing bit.
public Godel2(){}
Font cf1;
/** Text area for Godel number of proof */
JTextArea prnum=new JTextArea();
/** Text area for Godel numbers of lines of proof */
JTextArea plines=new JTextArea();
//Label lab1=new Label();
/** Set when end of proof number reached */
boolean endflg;
/** Press button to generate proof lines from proof number */
BasicArrowButton but2 =new BasicArrowButton(SwingConstants.SOUTH);
final BigInteger THREE=BigInteger.valueOf(3);
final BigInteger FOUR=BigInteger.valueOf(4);
//final BigInteger LARGE=new BigInteger("9444732965739290427391");
/**Stack of bound variables 
 * vstack,vlist,vsp and vlp are not currently used*/
int[] vstack=new int[20];
/** List of bound variables relevant to current term*/
int[] vlist=new int[44];
/** Stack pointer for vstack */
int vsp;
/** Count for vlist */
int vlp;
/** int form of variable in Ax4 or Ind axioms 
 * Will be replaced by Termx*/
long varep;
/** replacement term for varep */
BigInteger Termx;

/** Godel numbers of integer axioms */
BigInteger[] IntAx={new BigInteger("57459223650"),
  new BigInteger("205311074"),new BigInteger("6545"),
  new BigInteger("207818546"),new BigInteger("12756"),
  new BigInteger("833340372"),new BigInteger("2524"),
  new BigInteger("7276970972")};
/** Store for Godel numbers of lines of proof */
BigInteger line[]=new BigInteger[200];
/** Current line number for lines of proof */
int curlin;
/** Holds G&ouml;del number of proof (bitstream)*/
BigInteger Proofin;
/** Holds bitstream number to be parsed */
BigInteger Source;
/** */
JCheckBox binar=new JCheckBox("binary",false);
/** Radix for proof number input (10 or 2)*/
int radx=10;

/** respond to down button or change of proof number radix */
public void actionPerformed(ActionEvent e) {
String ac=e.getActionCommand();
try{
if (ac=="down"){
  plines.setText("");
//  Proofin=new BigInteger("11100001001101011000111101000100111000000000111100000100111010000000111011011110000000101101100100101110101100101100000100101110101100100010110010111011100001011011000001100011111001000001110010000001110110111100000001011011110001011000110001000100101110101111001011010100001101111100010000111010001111010010110100000011000101001111010000001100010100111100000000111010100011101100101110111000001100000101100101110100100010010111010111100001011011010110001111100101011100110001111011000001100011000111110001011001011101110010110010001101111100100011011111000110110010010011111000101101001000111100001100100101110101100110000010010111010010001011110000101100001011000111111010011101100100111100001111001100110001100010001001011101110010001011101111110010111010101001111000111010100001011110010010111100011111100001110100010011110000011010111100001100110100,00111000010110000011100011111101000110110000011110001101010111100001111010100001011110010110001101010111100001111010100001011110010011011101111100010011100100001111010100110110001111000110001101100000011110000011010000001111011000001101100011000110000101111110111010001111010110000011010110001011000110001011011010010000111101011111001001011001111100111010100111101011000110100011101010010110110100101100011101011111100001010001111000111000000111101011000001101000111010100101100000111010100101101100001011011100011111011100001111010110000011010110001011000110001000111010111001000011110111",2);
  Proofin=new BigInteger(prnum.getText(),radx);
  proves();
  /*for (int i=1;i<curlin;i++)plines.append(line[i].toString()+"\n")*/;}
else if (ac=="binary")try{
 String	prtxt=prnum.getText();
 if (prtxt.length()>0){
 BigInteger pc=new BigInteger(prtxt ,radx);
 prnum.setText(pc.toString(12-radx));}}
 finally {radx=12-radx;}
} catch (Error ii){JOptionPane.showMessageDialog(null, "Input not valid");}
}

/** Paste into upper (proof number) text area  on right mouse click */
public void mouseClicked(MouseEvent me) {
try{	
if (me.getButton()==MouseEvent.BUTTON3)
	prnum.setText((String)Toolkit.getDefaultToolkit().getSystemClipboard().getContents(null).getTransferData(
				         DataFlavor.stringFlavor));
}catch(Exception e){} 
}

public void mouseEntered(MouseEvent arg0) {}
public void mouseExited(MouseEvent arg0) {}
public void mousePressed(MouseEvent arg0) {}
public void mouseReleased(MouseEvent arg0) {}

/** 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(plines);
// plines.setBounds(10,10,200,20);
 add(but2);
 but2.setBounds(60,275,40,20);
 JScrollPane scroll1 = new JScrollPane(prnum);
 add(scroll1);
 JScrollPane scroll2 = new JScrollPane(plines);
 add(scroll2);
 prnum.setFont(cf1);
 scroll1.setBounds(10,20,600,250);
 scroll2.setBounds(10,300,600,250);
 add(binar);
 binar.setBounds(10, 5, 60, 15);
 binar.addActionListener(this);
 prnum.setLineWrap(true);
 but2.addActionListener(this);
 but2.getModel().setActionCommand("down");
 //add(lab1);
 //lab1.setBounds(110,275,240,20);
 prnum.addMouseListener(this);
}
/** get 2 bits from bitstream */
int get2(){
	endflg=(Source.signum()==0);
	int result=Source.and(THREE).intValue();
	Source=Source.shiftRight(2);
	return result;
	}

/*int get4(){
int result=Source.and(THREE).intValue();
	Source=Source.shiftRight(4);
return result;
	}*/

/** Get int from bitstream */
long getint(){
long n,res=0;
do {n=get2(); if (n<3)res=3*res+n+1;}while (n<3&&!endflg);
return res;
}

/** Gets variable from input bitstream
 * @param stk - set if variable is to be put on stack
 * @return bitstream form of variable
 */
BigInteger Sgetvar(boolean stk){
int varg=(int)getint();
if (stk) {vstack[vsp++]=varg;}
if (varg==varep){
  for (int i=0;i<vsp;i++) vlist[vlp++]=vstack[i]; 
  return Termx;}
else return Varb(varg).shiftLeft(1);
}

/** 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)); 	
}

/** Encodes the result of a binary operator
 * @param X1 first term or formula
 * @param op code for operator
 * @param X2 second term or formula
 * @return code for operator result
 */
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);
}

/** gets a term from the proof bitstream
 * @return encoded form of term
 */
BigInteger Sterm(){
boolean isvar=!Source.testBit(0);
Source=Source.shiftRight(1);
if (isvar)return Sgetvar(false);
else switch (get2()){
 case 0:return BigInteger.valueOf(9);
 case 1:return Unop(5,Sterm());
 case 2:return Binop(Sterm(),6,Sterm());
 default:return Binop(Sterm(),7,Sterm());}
}

/**Gets a formula from the proof bitstream
 * @return encoded form of formula
 */
BigInteger Swff(){BigInteger T1;
switch (get2()){
 case 0: return Binop(Sterm(),0,Sterm());
 case 1: return Unop(1,Swff());
 case 2:return Binop(Swff(),2,Swff());
 default: { T1=Binop(Sgetvar(true),3,Swff());vsp--;return T1;}
}
}

/** Gets low order bits of a number
 * @param x Input number
 * @param n Number of bits  
 * @return Low order n bits of x
 */
BigInteger LowOrder(BigInteger x,int n){
return x.and(BigInteger.ONE.shiftLeft(n).subtract(BigInteger.ONE));
}

/**Converts int form of a variable bitstream form. 
 * The terminator is included,
 * but the starting 3 must be added separately if needed.
 * @param V  Variable in int form
 * @return Variable coded as a BigInteger
 */
BigInteger Varb(long V){
long n=V;
BigInteger Num=BigInteger.valueOf(7);
while (n>0){n--; 
 Num=Num.multiply(FOUR).add(BigInteger.valueOf(n%3));
 n/=3;}
return Num;
}

/** Gets previously established formula from line number
 * 1st bit 1 -> next 4 bits define number of axiom
 * 1st bit 0 -> encoded line number of proof follows
 * @return encoded form of formula
 */
BigInteger Glin(){
int l;
boolean isax=Source.testBit(0);
Source=Source.shiftRight(1);
if (isax){
  l=Source.and(BigInteger.valueOf(15)).intValue();
  Source=Source.shiftRight(4);
  return IntAx[l-1];}
else return line[(int)getint()];
}

/** Axiom 1: WF1&rArr;(WF2&rArr;WF1)
 * Gets two formulae
 * @return resulting line of proof
 */
BigInteger Ax1(){
BigInteger WF1=Swff();
BigInteger WF2=Swff();
BigInteger t=Binop(WF2,2,WF1);
return Binop(WF1,2,t);
}
/** Axiom 2: (WF1&rArr;(WF2&rArr;WF3))&rArr;((WF1&rArr;WF2)&rArr;(WF1&rArr;WF3))
 * Gets three formulae
 * @return resulting line of proof
 */
BigInteger Ax2(){
BigInteger WF1=Swff();
BigInteger WF2=Swff();
BigInteger WF3=Swff();
BigInteger T=Binop(WF1,2,WF2);
BigInteger T1= Binop(WF1,2,WF3);
T1=Binop(T,2,T1);
T=Binop(WF2,2,WF3);
T=Binop(WF1,2,T);
return Binop(T,2,T1);
}
/** Axiom 3 (¬WF2&rArr;¬WF1)&rArr;((¬WF2&rArr;WF1)&rArr;WF2)
 * Gets two formulae
 * @return resulting line of proof
 */

BigInteger Ax3(){
BigInteger WF1=Swff();
BigInteger WF2=Swff();
BigInteger T1=Unop(1,WF2);
BigInteger T=Binop(T1,2,Unop(1,WF1));
T1=Binop(T1,2,WF1);
T1=Binop(T1,2,WF2);
return Binop(T,2,T1);}

/** Axiom 4:&forall;V WF(V)&rArr;WF(T)
 * (T is a term free for V in WF)
 * Gets a variable, a term and a formula
 * @return resulting line of proof
 */
BigInteger Ax4(){
BigInteger rep;
long varx=getint();
Termx=Sterm();
BigInteger WF=Swff();
Proofin=Source;varep=varx;
Source=WF;rep=Swff();//replace
Source=Proofin;
//if (erflg) return BigInteger.ZERO;
WF=Binop(Varb(varx),3,WF);
return Binop(WF,2,rep);
}
/** Axiom 5: &forall;V(WF1&rArr;WF2)&rArr;(WF1&rArr;&forall;V WF2) 
 * (WF1 has no free occurence of V)
 * Gets a variable and two formulae
 * @return resulting line of proof
 */
BigInteger Ax5(){
long varx=getint();
BigInteger WF1=Swff();
BigInteger WF2=Swff();
BigInteger T=Binop(WF1,2,WF2);
T=Binop(Varb(varx),3,T);
BigInteger T1=Binop(Varb(varx),3,WF2);
T1=Binop(WF1,2,WF2);
return Binop(T,2,T1);
}

/** Modus Ponens: WF1,WF1 &rArr; WF2 |- WF2
 * Gets two formulae
 * @return resulting line of proof */
BigInteger MP(){
BigInteger Tres;
BigInteger WF1=Glin();
Tres=Glin();
Proofin=Source;
Source=Tres;
if (get2()!=2)Tres=BigInteger.ZERO;
if (WF1.compareTo(Swff())!=0)Tres=BigInteger.ZERO;
Tres=Swff();
Source=Proofin;
return Tres;
}

/** Generalisation: WF |- &forall;V WF 
 * Gets a variable and a formula
 * @return  resulting line of proof  */
BigInteger Gen(){
long varx=getint();
BigInteger WF1=Glin();
return Binop(Varb(varx),3,WF1);
}

/** Induction: WF(0) &rArr;((&forall;V (WF(V) &rArr; WF(V'))) &rArr; &forall;V WF(V))
 *  * Gets a variable and a formula
 * @return  resulting line of proof */
BigInteger Ind(){
long varx=getint();
BigInteger V=Varb(varx);
BigInteger WF=Swff();
Proofin=Source;
Termx=V.shiftLeft(4).add(THREE);//V'
Source=WF;varep=varx;BigInteger t1=Swff();//replace
t1=Binop(WF,2,t1);
t1=Binop(V,3,t1);
BigInteger t=Binop(V,3,WF);
t1=Binop(t1,2,t);
Source=WF;
Termx=BigInteger.valueOf(9); t=Swff();//0
Source=Proofin;
return Binop(t,2,t1);
}


/** Gets a line of a proof
 * @param c0 intial two bits - previously obtained
 * @return resulting line of proof  */
BigInteger proofline(int c0){
varep=-1;
switch (c0){
 case 1:switch (get2()){ //propositional axiom
  case 0:return Ax1();
  case 1:return Ax2();
  default:return Ax3();
 }
 case 2:switch (get2()){// predicate & induction
  case 0:return Ax4();
  case 1:return Ax5();
  default: return Ind();
 }
 default: switch (get2()){ //rules
  case 0:return MP();
  default:return Gen();
 }
}
}

/**Produces  G&ouml;del numbers of formulae of proof from G&ouml;del number of proof in Proofin */
void proves(){
int c0;
curlin=1;
Source=Proofin;
while ((c0=get2())>0) {
 line[curlin]=proofline(c0);
 plines.append(line[curlin].toString()+"\n");
  curlin++;
}}
 

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

}

/*
13977428729055444594
972062322
59137
231
*/