import java.applet.Applet;
import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import java.awt.geom.*;
import java.math.*;

/**This contains the proof of 3 statements:

1. The pinwheel map is defined on
   the interior of each pinwheel tile.

2. The pinwheel map is not defined on any essential edge of a pinwheel 
   tile. By essential, we mean an edge that is not contained in the
   boundary of the main strip.

3. The pinwheel map is defined and the identity on the interior of
any inessential edge.**/


public class ProofPinwheel2 implements Runnable {
    int halt;
    Manager M;
    GoldenReal[][] h=new GoldenReal[4][3];
    GoldenComplex[] v=new GoldenComplex[4];


public ProofPinwheel2(Manager MM) {
    this.M=MM;
}


    public void failMessage() {
	throw new ProofException("ProofPinwheel2");
    }


    public void run() {
	System.out.println("START");
	System.out.print("start defined test 2  --  ");
	PinwheelMap PIN=new PinwheelMap();
	setPinwheel();
	int total=DataPinwheel.COUNT();
	for(int i=0;i<total;++i) {
	    boolean test=testPinwheel(i);
	    if(test==false) failMessage();
	}
	System.out.println("end");

	System.out.print("start undefined 2 test  --  ");
	for(int i=0;i<total;++i) {
	    boolean test=testPinwheelUndefined(i);
	    if(test==false) failMessage();
	}
	System.out.println("end");
	System.out.println("END");
    }


    /**This tests the pinwheel map on a pinwheel tile.**/

    public boolean testPinwheel(int i) {
	PinwheelMap PIN=new PinwheelMap();
	Complex z=ProofPinwheel1.center(i);
	int[] list=PIN.mapSpectrum(z);
	GoldenPolyWedge P=DataPinwheel.returnPoly(i);
	for(int j=0;j<P.count;++j) {
	    GoldenComplex w=new GoldenComplex(P.z[j]);
	    boolean test=testVertex(w,list);
	    if(test==false) return(false);
	}
	return(true);
    }


    /**vertex test: This returns true if the itinerary given as list
       weakly describes the pinwheel map applied to z. That is,
       the list describes the map spectrum for arbitrarily small
       perturbations of z**/

    public boolean testVertex(GoldenComplex z,int[] list) {
	GoldenComplex w=new GoldenComplex(z);
	for(int i=1;i<9;++i) {
	    w=doMap(i,list[i],w);
	    boolean test=weakStrip(i,w);
	    if(test==false) return(false);
	}
	return(true);
    }



    /**This tests the pinwheel map is nowhere defined on the boundary of the
       pinwheel tile.**/

    public boolean testPinwheelUndefined(int i) {
	PinwheelMap PIN=new PinwheelMap();
	Complex z=ProofPinwheel1.center(i);
	int[] list=PIN.mapSpectrum(z);
	GoldenPolyWedge P=DataPinwheel.returnPoly(i);
	for(int j=0;j<P.count;++j) {
	    int j1=j;
	    int j2=(j+1)%P.count;
	    GoldenComplex w1=new GoldenComplex(P.z[j1]);
	    GoldenComplex w2=new GoldenComplex(P.z[j2]);
	    boolean hor=specialEdge(w1,w2);
	    boolean test=false;
	    if(hor==false) test=testEdgeUndefined(w1,w2,list);
	    if(hor==true) test=testEdgeIdentity(w1,w2,list);
	    if(test==false) return(false);
	}
	return(true);
    }

    /**This tests if the edge is completely contained in the
       boundary of the main strip**/

    public boolean specialEdge(GoldenComplex w1,GoldenComplex w2) {
	GoldenReal y1=w1.y;
	GoldenReal y2=w2.y;
	if((y1.a[0]==2)&&(y1.a[1]==0)&&(y2.a[0]==2)&&(y2.a[1]==0)) return(true);
	if((y1.a[0]==-2)&&(y1.a[1]==0)&&(y2.a[0]==-2)&&(y2.a[1]==0)) return(true);
	return(false);
    }


    /**This tests that the map is defined and the identity on an edge.
       It only is applied to edges in the boundary of the main strip.
       We check that the first and last points differ by (0,4k) for some integer k.
       What is going on is that we are applying the map pi_8...pi_1 instead
       of the full pinwheel map g pi_8...pi_1.  The map g simply adjusts the
       second coordinate by some 4k until the point lies in the main strip.*/


   public boolean testEdgeIdentity(GoldenComplex z1,GoldenComplex z2,int[] list) {
       boolean test1=testEdgeUndefined(z1,z2,list);
       if(test1==true) return(false);
	GoldenComplex w1=new GoldenComplex(z1);
	GoldenComplex w2=new GoldenComplex(z2);
	for(int i=1;i<9;++i) {
	    w1=doMap(i,list[i],w1);
	    w2=doMap(i,list[i],w2);
	}
	if(GoldenReal.equals(w1.x,z1.x)==false) return(false);
	if(GoldenReal.equals(w2.x,z2.x)==false) return(false);
	long q1=z1.y.a[0]-w1.y.a[0];
	long q2=z2.y.a[0]-w2.y.a[0];
	q1=(q1+100)%4;
	q2=(q2+100)%4;
	if(q1!=0) return(false);
	if(q2!=0) return(false);
	if(w1.y.a[1]!=0) return(false);
	if(w2.y.a[1]!=0) return(false);
        return(true);
   }


    /**edge test:  This checks that a given edge is mapped by the pinwheel map
       into the boundary of a strip.  We ignore the edges that start out in the
       line y=0. These are not edges of the tiles, but rather artifacts of the
       way we produce the tiles.**/

    public boolean testEdgeUndefined(GoldenComplex z1,GoldenComplex z2,int[] list) {
	if((z1.y.isZero()==true)&&(z2.y.isZero()==true)) return(true);  //y=0 case
	GoldenComplex w1=new GoldenComplex(z1);
	GoldenComplex w2=new GoldenComplex(z2);
	boolean test2=false;
	for(int i=1;i<9;++i) {
	    w1=doMap(i,list[i],w1);
	    w2=doMap(i,list[i],w2);
	    boolean test=bdyStrip(i,w1,w2);
	    if(test==true) return(true);
	}
	return(false);
    }




    /**This sets the data used for the strip maps.
       One difference between the data here and in
       the class PinwheelMap.java is that we don't
       divide the h[i][j] by 4.  We want to keep it
       so that these numbers belong to Z[phi]. To
       account for this, the test that a given point
       lies in the relevant strip is that the relevant
       linear functional evaluates to something in [0,4]
       rather than something in [0,1].**/

    public void setPinwheel() {	
        v[0]=new GoldenComplex(-2,0,-2,0);
	v[1]=new GoldenComplex(0,0,4,0);
	v[2]=new GoldenComplex(-2,0,2,0);
	v[3]=new GoldenComplex(4,-4,0,0);

	h[0][0]=new GoldenReal(-1,0);
	h[0][1]=new GoldenReal(-1,0);
	h[0][2]=new GoldenReal(+3,0);

	h[1][0]=new GoldenReal(-1,0);
	h[1][1]=new GoldenReal(+1,0);
	h[1][2]=new GoldenReal(+3,0);

	h[2][0]=new GoldenReal(0,-1);
	h[2][1]=new GoldenReal(2,-1);
	h[2][2]=new GoldenReal(2,-1);

	h[3][0]=new GoldenReal(0,-1);
	h[3][1]=new GoldenReal(-2,1);
	h[3][2]=new GoldenReal(2,-1);
    }

    /**tests if z is inside the jth strip**/

    public boolean weakStrip(int j,GoldenComplex z) {
	GoldenReal d=applyFunctional(j,z);
	GoldenReal e=GoldenReal.minus(new GoldenReal(4,0),d);
	if((d.a[0]==0)&&(d.a[1]==0)) return(true);
	if((e.a[0]==0)&&(e.a[1]==0)) return(true);
	if(d.isPositive()==false) return(false);
	if(e.isPositive()==false) return(false);
	return(true);
    }

    /**tests if z1 and z2 lie in same the boundary of the strip.**/

    public boolean bdyStrip(int j,GoldenComplex z1,GoldenComplex z2) {
	GoldenReal d=applyFunctional(j,z1);
	GoldenReal e=applyFunctional(j,z2);
	boolean test1=((d.a[0]==0)&&(d.a[1]==0));
	boolean test2=((e.a[0]==0)&&(d.a[1]==0));
	boolean test3=((d.a[0]==4)&&(d.a[1]==0));
	boolean test4=((e.a[0]==4)&&(d.a[1]==0));
        if((test1==true)&&(test2==true)) return(true);
        if((test3==true)&&(test4==true)) return(true);
	return(false);
    }





    public GoldenReal applyFunctional(int j,GoldenComplex z) {
	GoldenReal[] d=new GoldenReal[3];
	d[0]=GoldenReal.times(h[j%4][0],z.x);
	d[1]=GoldenReal.times(h[j%4][1],z.y);
	d[2]=GoldenReal.plus(h[j%4][2],GoldenReal.plus(d[0],d[1]));
	return(d[2]);
    }





    /**This does the basic map.  
       j is the strip index
       k is the number of steps.**/

    public GoldenComplex doMap(int j,int k,GoldenComplex z){
        GoldenComplex K=new GoldenComplex(k,0,0,0);
        GoldenComplex w=GoldenComplex.plus(z,GoldenComplex.times(K,v[j%4]));
        return(w);
    }

}