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

/**This file contains the proof that the polyhedra of the
   torus partition actually cover.*/

public class ProofCompact1 implements Runnable {
    int halt;
    Manager M;

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

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

    public void run() {
	System.out.println("START");
	checkPlatinum();
	checkConvex();
	checkDisjoint();
	checkCover();
	System.out.println("END");
    }


    /**COVERING TEST**/

    public  void checkCover() {
	for(int k=0;k<10;++k) checkCover(k);
    }


    public  void checkCover(int k) {
	int total=0;
	System.out.print("cover test: "+k+" ");
	GoldenPolyWedge[] ALL=polyList(k);
	for(int i=0;i<ALL.length;++i) {
	    GoldenPolyWedge P=ALL[i];
	    for(int j=0;j<P.count;++j) {
	       GoldenComplex z=new GoldenComplex(P.z[j%P.count]);
	       boolean test1=onBdy(z);
	    
	       if(test1==false) {
		   GoldenComplex[] L1=PolyCover.neighbors(0,z,ALL);
		   GoldenComplex[] L2=PolyCover.neighbors(1,z,ALL);
	           boolean test2=PolyCover.matchFold(z,L1,L2);  
	           if(test2==false) {
		       ++total;
		   }
	       }
	    }
	}
	if(total>0) failMessage();
	System.out.println("end");
    }

    public  GoldenPolyhedron[] polyList() {
	int total=0;
	GoldenPolyhedron[] LIST=new GoldenPolyhedron[64];
	for(int i=0;i<64;++i) {
	    LIST[i]=DataPartition.getGoldenPolyhedron(i);
	}
	return(LIST);
    }

    public  GoldenPolyWedge[] polyList(int k) {
	GoldenPolyhedron[] LIST=polyList();
	GoldenReal[] LIST2=DataPartitionRaw.getHeight();
        LIST2=GoldenReal.interlace(LIST2);
	GoldenReal HEIGHT=LIST2[k];
	GoldenPolyWedge[] LIST3=new GoldenPolyWedge[64];
	int total=0;
	for(int i=0;i<64;++i) {
	   GoldenPolyWedge Q=GoldenPolyCombinatorics.intersect(LIST[i],HEIGHT);
	   if(Q!=null) {
	       LIST3[total]=new GoldenPolyWedge(Q);
	       ++total;
	   }
	}
	GoldenPolyWedge[] LIST4=new GoldenPolyWedge[total];
	for(int i=0;i<total;++i) LIST4[i]=new GoldenPolyWedge(LIST3[i]);
	return(LIST4);
    }


    public  boolean onBdy(GoldenComplex z) {
	/*top*/
	if(GoldenReal.equals(z.y,new GoldenReal(2,0))==true) return(true);
	/*bottom*/
	if(GoldenReal.equals(z.y,new GoldenReal(0,0))==true) return(true);
	/*left*/
	GoldenComplex w1=new GoldenComplex(new GoldenReal(3,-2),new GoldenReal(0,0));
	GoldenComplex w2=new GoldenComplex(new GoldenReal(-3,2),new GoldenReal(2,0));
	boolean test=GoldenComplex.isBetween(z,w1,w2);
	if(test==true) return(true);
	/*right*/
	w1=new GoldenComplex(new GoldenReal(5,-2),new GoldenReal(0,0));
	w2=new GoldenComplex(new GoldenReal(-1,2),new GoldenReal(2,0));
	test=GoldenComplex.isBetween(z,w1,w2);
	if(test==true) return(true);
	return(false);
    }


    /**DISJOINTNESS TEST**/

    public void checkDisjoint() {
	int total=0;
	System.out.print("disjoint test:   ");
	GoldenPolyhedron[] LIST=polyList();
	for(int i=0;i<LIST.length;++i) {
	  for(int j=i+1;j<LIST.length;++j) {
	      GoldenPolyhedron P1=LIST[i];
	      GoldenPolyhedron P2=LIST[j];
	      boolean test=disjoint(P1,P2);
	      if(test==false) ++total;
	  }
	}
	System.out.println("end");
	if(total>0) failMessage();
    }

    /**This routine returns true if it can prove that the two polyhedra
       have disjoint interiors. **/

    public  boolean disjoint(GoldenPolyhedron P1,GoldenPolyhedron P2) {
	if(disjoint1(P1,P2)==true) return(true);
	return(false);
    }

    public  boolean disjoint1(GoldenPolyhedron P1,GoldenPolyhedron P2) {
	int n1=P1.count;
	int n2=P2.count;
	GoldenVector[] W=new GoldenVector[4];
	for(int i1=0;i1<n1;++i1) {
	    for(int i2=i1+1;i2<n1;++i2) {
  	       for(int j1=0;j1<n2;++j1) {
	          for(int j2=j1+1;j2<n2;++j2) {
		      int[] u={i1,i2,j1,j2};
 	              W[0]=new GoldenVector(P1.V[u[0]]);
	              W[1]=new GoldenVector(P1.V[u[1]]);
	              W[2]=new GoldenVector(P2.V[u[2]]);
	              W[3]=new GoldenVector(P2.V[u[3]]);
	              GoldenVector X1=GoldenVector.minus(W[0],W[1]);
	              GoldenVector X2=GoldenVector.minus(W[2],W[3]);
	              GoldenVector DIR1=GoldenVector.cross(X1,X2);
                      GoldenVector DIR2=DIR1.negate();
                      boolean test=separate(P1,P2,DIR1);
	              if(test==true) return(true);
                      test=separate(P1,P2,DIR2);
	              if(test==true) return(true);
		  }
	       }
	    }
	}
	return(false);
    }

    public  boolean separate(GoldenPolyhedron P1,GoldenPolyhedron P2,GoldenVector DIR) {
	if(DIR.isZero()==true) return(false);

	for(int i=0;i<4;++i) {
	    for(int j=0;j<4;++j) {
		GoldenReal r1=GoldenVector.dot(P1.V[i],DIR);
		GoldenReal r2=GoldenVector.dot(P2.V[j],DIR);
		GoldenReal r3=GoldenReal.minus(r1,r2);
		if(r3.isPositiveOrZero()==false) return(false);
	    }
	}
	return(true);
    }





    /**PLATINUM TEST**/

    /**We call an edge of a polyhedron platinum if it intersects every
       Z[phi] horizontal slice in a point whose coords are in Z[phi].
       We call a golden polyhedron platinum if all its non-horizontal edges
       are golden.  Just for fun, we verify that all the polyhedra in
       our partition are platinum.**/
       

    public void checkPlatinum() {
	System.out.print("platinum test: ");
	GoldenPolyhedron[] LIST=polyList();
	int total=0;
	for(int i=0;i<LIST.length;++i) {
	    boolean test=testPlatinum(LIST[i]);
	    if(test==false) ++total;
	}
	if(total>0) failMessage();
	System.out.println("end");
    }


    public  boolean testPlatinum(GoldenPolyhedron P) {
	int[][] LIST=GoldenPolyCombinatorics.edgeList(P);
	for(int a=0;a<LIST.length;++a) {
	    int i=LIST[a][0];
	    int j=LIST[a][1];
	    boolean test1=GoldenPolyCombinatorics.edge(P,i,j);
	    boolean test2=testPlatinum(P,i,j);
	    if((test1==true)&&(test2==false)) return(false);
	}
	return(true);
    }

    public  boolean testPlatinum(GoldenPolyhedron P,int i,int j) {
	GoldenVector[] V={P.V[i],P.V[j]};
	return(testPlatinum(V));
    }

    public  boolean testPlatinum(GoldenVector[] V) {
	Vector V1=V[0].toVector();
	Vector V2=V[1].toVector();
	double d=V2.x[2]-V1.x[2];
	if(Math.abs(d)<.0000001) return(true);
	double x1=(V2.x[0]-V1.x[0])/d;
	double x2=(V1.x[2]*V2.x[0]-V2.x[2]*V1.x[0])/d;
	double y1=(V2.x[1]-V1.x[1])/d;
	double y2=(V1.x[2]*V2.x[1]-V2.x[2]*V1.x[1])/d;

	double[] Y={x1,x2,y1,y2};
	for(int i=0;i<4;++i) {
	   int[] rr=GoldenRatio.recognize(Y[i],500);
	   if(Math.abs(rr[0])>50) return(false);
	   if(Math.abs(rr[1])>50) return(false);
	}
	return(true);
    }



    /**CONVEXITY TEST**/

    public void checkConvex() {
	System.out.print("convex test: ");
	int total=0;
	for(int i=0;i<64;++i) {
	    GoldenPolyhedron P=DataPartition.getGoldenPolyhedron(i);
	    boolean test=convex(P,2);
	    if(test==false) ++total;
	}
	if(total>0) failMessage();
	System.out.println("end");
    }

    /**This is a test for strict convexity at a vertex.
       We dot the vertex and all the others with one of the
       first (2L+1)^6 GoldenVectors and verify that the given
       vertex has the largest dot product in at least one case.
       Taking L=2 works for our purposes.*/

    public  boolean convex(GoldenPolyhedron P,int L) {
	for(int i=0;i<P.count;++i) {
	    if(extreme(P,P.V[i],L)==false) failMessage();
	}
	return(true);
    }


    /**Tests if a vertex is an extreme point of the polyhedron*/
    public  boolean extreme(GoldenPolyhedron P,GoldenVector X,int L) {
	for(int i1=-L;i1<=L;++i1) {
	for(int i2=-L;i2<=L;++i2) {
	for(int i3=-L;i3<=L;++i3) {
	for(int i4=-L;i4<=L;++i4) {
	for(int i5=-L;i5<=L;++i5) {
	for(int i6=-L;i6<=L;++i6) {
	    int[] A={i1,i2,i3,i4,i5,i6};
	    GoldenVector DIR=new GoldenVector(A);
	    if(DIR.isZero()==true) return(false);
	    boolean test=GoldenPolyCombinatorics.extreme(P,0,X,DIR);
	    if(test==true) return(true);
	}}}}}}
	failMessage();
	return(false);
     }



}