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

/**This class contains the proof that the compactification map is
well defined on all of the polyhedra of the compactification.  It is
the only place where we use the lift to 4 dimensions.  The proof here
is half of the verification of the Compactification Theorem.  The other
half consists in checking that the polyhedra we have listed really
do form a partition of the torus.*/


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

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



    public void run() {
	for(int i=0;i<64;++i) {
	    boolean test=checkPoly(i);  
            int[] e=sequencePoly(i);
	    System.out.print(i+" "+test+"   ");
	    for(int k=1;k<=8;++k) System.out.print(e[k]+" ");
	    System.out.println("");
	}
    }

    public boolean checkPoly(int i) {
	for(int j=0;j<4;++j) {
	  GoldenPolyhedron GP=DataPartition.getGoldenPolyhedron(i);
	  GoldenPolytope GX=I(j,GP);
	  int[] e=sequencePoly(i);

	  for(int k=1;k<=8;++k) {
	     boolean test=checkSqueezed(e[k],k,GX);
	     if(test==false) return(false);
	     GX=tilde_EGuided(e[k],k,GX);
	  }
	}
	return(true);
    }

    /**This routine uses floating point arithmetic to compute
       a certain sequence associated to each polyhedron.  We do this
       by tracking the centroid of the lifted polytope.  It actually
       doesn't matter how we compute this sequence.  Once we have it,
       we feed it into our rigorous verifier.*/

   public int[] sequencePoly(int i) {	
	Polyhedron P=DataPartition.getPolyhedron(i);
	Polytope X=Compactify.I(0,P);
	Vector4 V=X.getCenter();
	int[] u=Compactify.determineSequence(V);
	return(u);
   }


    /**Now for all the supporting routines**/


    /**The piecewise affine maps of R^4**/

    public static GoldenPolytope tilde_EGuided(int e,int j,GoldenPolytope X) {
	GoldenPolytope Y=new GoldenPolytope();
	Y.count=X.count;
	for(int i=0;i<X.count;++i) Y.V[i]=tilde_EGuided(e,j,X.V[i]);
	return(Y);
    }

    public static GoldenVector4 tilde_EGuided(int e,int j,GoldenVector4 V) {
	return(GoldenVector4.plus(linear(j%4,V),translateGuided(e,j%4,V)));
    }

    public static GoldenVector4 linear(int q,GoldenVector4 V) {
	double p=GoldenRatio.phi(1);
	GoldenReal a0=new GoldenReal(0,0);
	GoldenReal a1=new GoldenReal(1,0);
	GoldenReal a2=new GoldenReal(2,0);
	GoldenReal a3=new GoldenReal(-1,0);
	GoldenReal a4=new GoldenReal(1,-1);
	GoldenReal a5=new GoldenReal(-1,1);
	GoldenReal a6=new GoldenReal(0,1);
	GoldenReal a7=new GoldenReal(0,-1);

	GoldenReal[][] m0={{a1,a0,a0,a0},{a0,a1,a0,a0},{a5,a0,a0,a0},{a0,a0,a0,a1}};
	GoldenReal[][] m1={{a1,a0,a0,a0},{a0,a1,a0,a0},{a0,a4,a1,a1},{a0,a5,a0,a0}};
	GoldenReal[][] m2={{a1,a0,a0,a0},{a0,a1,a0,a0},{a0,a0,a1,a0},{a3,a5,a6,a0}};
	GoldenReal[][] m3={{a6,a3,a3,a6},{a5,a0,a3,a6},{a4,a1,a2,a7},{a4,a1,a1,a4}};
	GoldenReal[][][] m={m0,m1,m2,m3};
	GoldenVector4 W=new GoldenVector4(a0,a0,a0,a0);
	for(int i=0;i<4;++i) {
	    for(int j=0;j<4;++j) W.x[i]=GoldenReal.plus(W.x[i],GoldenReal.times(m[q][i][j],V.x[j]));
	}
	return(W);
    }

    /**In this routine, the integer e plays the role of the determiner*/

    public static GoldenVector4 translateGuided(int e,int k,GoldenVector4 V) {
	GoldenReal d=new GoldenReal(e,0);
	GoldenReal d0=GoldenReal.times(d,new GoldenReal(0,1));
	GoldenReal d1=GoldenReal.times(d,new GoldenReal(0,-1));
	GoldenReal O=new GoldenReal(0,0);
	if(k==0) return(new GoldenVector4(O,O,d1,O));
	if(k==1) return(new GoldenVector4(O,O,d0,d1));
	if(k==2) return(new GoldenVector4(O,O,O,d1));
	if(k==3) return(new GoldenVector4(d1,d1,d0,d0));
	return(null);
    }


    /**THE BASIC AFFINE MAP**/

    /**These maps are not used in the proof.  They are included
       for the sake of comparison both with the floating point
       versions and with the "guided versions" that are used in
       the proof.  See sanity check 1.8**/


    public static GoldenPolytope tilde_E(int j,GoldenPolytope X) {
	GoldenPolytope Y=new GoldenPolytope();
	Y.count=X.count;
	for(int i=0;i<X.count;++i) Y.V[i]=tilde_E(j,X.V[i]);
	return(Y);
    }

    public static GoldenVector4 tilde_E(int j,GoldenVector4 V) {
	return(GoldenVector4.plus(linear(j%4,V),translate(j%4,V)));
    }

    public static GoldenVector4 translate(int k,GoldenVector4 V) {
	GoldenReal d=determine(k,V);
	d=d.floor(4);
	GoldenReal d0=GoldenReal.times(d,new GoldenReal(0,1));
	GoldenReal d1=GoldenReal.times(d,new GoldenReal(0,-1));
	GoldenReal O=new GoldenReal(0,0);
	if(k==0) return(new GoldenVector4(O,O,d1,O));
	if(k==1) return(new GoldenVector4(O,O,d0,d1));
	if(k==2) return(new GoldenVector4(O,O,O,d1));
	if(k==3) return(new GoldenVector4(d1,d1,d0,d0));
	return(null);
    }



    /**THE AFFINE LIFT*/

    public static GoldenVector4 I(int k,GoldenVector V) {
	System.out.println(k);
	GoldenReal f0=new GoldenReal(0,0);
	GoldenReal f1=new GoldenReal(2,0);
	GoldenReal f2=new GoldenReal(-2,2);
	GoldenReal f3=new GoldenReal(-4,2);
	GoldenReal[] f={f0,f1,f2,f3};
	GoldenReal g1=f[k];
	GoldenReal g2=new GoldenReal(-g1.a[0],-g1.a[1]);
	GoldenVector4 W1=I(V);
	GoldenVector4 W2=new GoldenVector4(f0,f0,g2,g1);
	GoldenVector4 W3=GoldenVector4.plus(W1,W2);
	return(W3);
    }


    public static GoldenVector4 I(GoldenVector V) {
	GoldenReal a0=new GoldenReal(0,0);
	GoldenReal a1=new GoldenReal(1,0);
	GoldenReal a2=new GoldenReal(2,0);
	GoldenReal p1=new GoldenReal(-1,1); // 1/phi
	GoldenReal p2=new GoldenReal(1,-1); // -1/phi
	GoldenReal u=GoldenReal.minus(V.x[0],a1);
	GoldenReal v=GoldenReal.minus(GoldenReal.times(a2,V.x[1]),a1);
	GoldenReal w=new GoldenReal(V.x[2]);
	GoldenReal[] a={GoldenReal.plus(v,w),GoldenReal.plus(v,w),u,u};
	GoldenReal[] b={w,GoldenReal.minus(a0,w),GoldenReal.times(w,p1),GoldenReal.times(w,p2)};
	GoldenReal[] c=new GoldenReal[4];
	for(int i=0;i<4;++i) c[i]=GoldenReal.plus(a[i],b[i]);
	GoldenVector4 W=new GoldenVector4(c);
	return(W);

    }

    /**applies the affine lift to each vector of P**/

    public static GoldenPolytope I(int k,GoldenPolyhedron P) {
	GoldenPolytope X=new GoldenPolytope();
	X.count=P.count;
	for(int i=0;i<P.count;++i) {
	    X.V[i]=I(P.V[i]);
	}
	return(X);
    }




    /**CHECKING THE ITINERARIES*/


    public static GoldenReal determine(int k,GoldenVector4 V) {
	GoldenReal[] x=V.toComponents();
	GoldenReal d=new GoldenReal(0,0);
	GoldenReal a=new GoldenReal(2,1);
	if(k%4==0)  d=GoldenReal.plus(x[0],new GoldenReal(1,0));
	if(k%4==1)  d=GoldenReal.plus(x[1],new GoldenReal(1,0));
	if(k%4==2)  d=GoldenReal.plus(GoldenReal.plus(x[1],x[2]),a);
        if(k%4==3)  d=GoldenReal.plus(GoldenReal.plus(x[0],x[3]),a);
	return(d);
    }

    /**This computes the kth determiner d for V and checks that 
       e <= d <= e+4**/

    public static boolean checkSqueezed(int e,int k,GoldenVector4 V) {
	GoldenReal d=determine(k,V);
	d=GoldenReal.minus(d,new GoldenReal(e,0));
	GoldenReal a0=new GoldenReal(0,0);
	GoldenReal a4=new GoldenReal(4,0);
	if(GoldenReal.equals(d,a0)==true) return(true);
	if(GoldenReal.equals(d,a4)==true) return(true);
	if(d.isPositive()==false) return(false);
	d=GoldenReal.minus(a4,d);
	if(d.isPositive()==false) return(false);
	return(true);
    }

    /**This makes the determiner check for each vertex of X.*/

    public static boolean checkSqueezed(int e,int k,GoldenPolytope X) {
	for(int i=0;i<X.count;++i) {
	    if(checkSqueezed(e,k,X.V[i])==false) return(false);
	}
	return(true);
    }


}