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


    /**This class contains routines which help with the
       rigorous verification routines in the files
       VerifyTile
       VerifyRenorm
       VerifyReduction
    **/

public class VerifySupport  {

    /**THE COMPACTIFICATION MAP**/


    /**This is the basic map into the torus.  Everything is
       scaled by 2 to avoid leaving the ring Z[phi].**/


    public static GoldenVector theta(GoldenComplex z) {
	GoldenReal A=new GoldenReal(-3,2);
	GoldenReal B=new GoldenReal(-1,1);
	GoldenReal ONE=new GoldenReal(1,0);
	GoldenReal x=GoldenReal.plus(ONE,GoldenReal.times(z.x,B));
	GoldenReal y=GoldenReal.plus(ONE,GoldenReal.minus(z.x,z.y));
	x.a[0]=x.a[0]*2;
	x.a[1]=x.a[1]*2;
	GoldenReal t=GoldenReal.times(new GoldenReal(2,0),z.y);
	GoldenVector V=new GoldenVector(x,y,t);
	V=fundamentalDomain(V);
	return(V);
    }

    public static GoldenPolyhedron theta(GoldenPolyWedge W) {
	GoldenPolyhedron P=new GoldenPolyhedron();
	P.count=W.count;
	for(int i=0;i<P.count;++i) P.V[i]=theta(W.z[i]);
	return(P);
    }


    /**starts with an arbitrary vector and moves it to the
       fundamental domain.  The fundamental domain here is
       the fundamental domain in the floating point case
       scaled by a factor of 2. */

    public static GoldenVector fundamentalDomain(GoldenVector V) {
	GoldenReal x0=new GoldenReal(V.x[0]);
	GoldenReal x1=new GoldenReal(V.x[1]);
	x0=x0.dec(4);
	x1=x1.dec(4);
	GoldenReal t=functional(x0,x1);
	if(t.isPositiveOrZero()==false) x0.a[0]=x0.a[0]+4;
	GoldenReal FOUR=new GoldenReal(4,0);
	if(GoldenReal.isLess(FOUR,t)==true) x0.a[0]=x0.a[0]-4;
	GoldenReal r=V.x[2].dec(4);
	GoldenVector W=new GoldenVector(x0,x1,r);
	return(W);
    }

    public static GoldenReal functional(GoldenReal x,GoldenReal y) {
	GoldenReal A=new GoldenReal(-3,2);
	GoldenReal t=GoldenReal.minus(x,GoldenReal.times(A,y));
	t=GoldenReal.plus(A,t);
	t=GoldenReal.plus(A,t);
	return(t);
    }




    /**THE END RESULT OF THE DYNAMICS**/

    /**The relevant power of the polyhedron exchange map acts
       as a translation on P.  This routine gets the translation
       vector. When we actually use this vector, we mod out by
       the lattice (4Z)^3.**/

    public static GoldenVector getTotalMove(int[] I) {
	GoldenVector W=new GoldenVector(0,0,0,0,0,0);
	for(int i=0;i<I.length;++i) {
	     GoldenVector V=DataPartition.getMoveGolden(I[i]);
	     W=GoldenVector.plus(W,V);
	}
	W=W.scale(new GoldenReal(2,0));
	return(W);
    }

    public static GoldenVector getTotalMoveInverse(int[] I) {
	GoldenVector W=new GoldenVector(0,0,0,0,0,0);
	GoldenVector G=getTotalMove(I);
	G=GoldenVector.minus(W,G);
	return(G);
    }


    /**These routines do the same thing, without scaling.**/

    public static GoldenVector getTotalMoveRaw(int[] I) {
	GoldenVector W=new GoldenVector(0,0,0,0,0,0);
	for(int i=0;i<I.length;++i) {
	     GoldenVector V=DataPartition.getMoveGolden(I[i]);
	     W=GoldenVector.plus(W,V);
	}
	return(W);
    }

    public static GoldenVector getTotalMoveInverseRaw(int[] I) {
	GoldenVector W=new GoldenVector(0,0,0,0,0,0);
	GoldenVector G=getTotalMoveRaw(I);
	G=GoldenVector.minus(W,G);
	return(G);
    }




    /**THE RENORMALIZATION MAP**/


    public static int indexA(int[] L,GoldenVector V) {
	for(int branch=0;branch<4;++branch) {
	    if(insideA(L[0],L[1],branch,V,false)==true) return(branch);
	}
	throw(new ProofException("VerifySupport: indexA"));
    }

    public static GoldenVector mapAtoB(int[] L,GoldenVector V) {
	int test2=indexA(L,V);
	GoldenVector W=AtoB(L[0],L[1],test2,V);
	return(W);
    }

    /**Here the the map from A to B, guided by the integer index.
       In our rigorous verification scheme, all vectors are doubled.
       So, to get the index, we need to scale V in half.  Also, when
       we get the integer data for the affine map, we need to double
       the translation part.**/

    public static GoldenVector AtoB(int LA,int LB,int branch,GoldenVector V) {
       int[] AFF=DataRenormRaw.getAffine(LA,LB,branch);
       for(int i=2;i<8;++i) AFF[i]=2*AFF[i];  //doubling the translation part
       GoldenVector W=GoldenVector.affineInverse(AFF,V);
       return(W);
    }





    /**These get the partition characteristics of the
       polygon.  Any point in the polygon has the
       same characteristics.**/

    public static int[] getCharA(GoldenPolyWedge P) {
	GoldenComplex z=P.cheapInterior();
	return(Characteristics.getCharA(z.y.dec(2)));
    }

    public static int getCharB(GoldenPolyWedge P) {
	GoldenComplex z=P.cheapInterior();
	return(Characteristics.getCharB(z.y.dec(2)));
    }





    /**CONTAINMENT IN THE A-RENORM SET**/


    /**tests if a vector is inside the A-renorm set.**/

    public static boolean insideA(GoldenVector V,int[] L) {
	return(insideA(V,L,false));
    }

    public static boolean insideA(GoldenVector V,int[] L,boolean BOUNDARY) {
	for(int i=0;i<4;++i) {
	    if(insideA(L[0],L[1],i,V,BOUNDARY)==true) return(true);
	}
	return(false);
    }


    /**The vector V is scaled up by a factor of 2 from what it would
       be in the floating point case.  If the boolean variable
       bdy is true, then we also check for containment in the
       boundary**/

    public static boolean insideA(int LA,int LB,int branch,GoldenVector V,boolean BOUNDARY) {
	boolean bdy=false;
	GoldenPolyhedron P=DataRenorm.getGoldenA(LA,LB,branch);
	int[] N=DataRenormRaw.polyNormal(LB,branch);
	int[] A=DataRenormRaw.faceAnchor(LB,branch);
	for(int i=0;i<A.length;++i) {
	   GoldenVector gn=DataPartition.getNormal(N[i]);
	   GoldenVector p0=P.V[A[i]];
	   p0=p0.scale(new GoldenReal(2,0));
	   GoldenReal test=GoldenVector.dot(gn,GoldenVector.minus(p0,V));
	   if(test.isPositiveOrZero()==false) return(false); 
           if(test.isZero()==true) bdy=true;
	}
	if(BOUNDARY==false) return(true);
	return(bdy);
    }



    /**CONTAINMENT IN THE B-RENORM SET**/


  /**tests if a vector is inside the B-renorm set.**/


    public static boolean insideB(GoldenVector V,int L) {
	return(insideB(V,L,false));
    }

    public static boolean insideB(GoldenVector V,int L,boolean BOUNDARY) {
	for(int i=0;i<4;++i) {
	    if(insideB(L,i,V,BOUNDARY)==true) return(true);
	}
	return(false);
    }

    public static boolean insideB(int LB,int branch,GoldenVector V,boolean BOUNDARY) {
	boolean bdy=false;
	GoldenPolyhedron P=DataRenorm.getGoldenB(LB,branch);
	int[] N=DataRenormRaw.polyNormal(LB,branch);
	int[] A=DataRenormRaw.faceAnchor(LB,branch);
	for(int i=0;i<A.length;++i) {
           GoldenVector gn=DataPartition.getNormal(N[i]);
	   GoldenVector p0=P.V[A[i]];
	   p0=p0.scale(new GoldenReal(2,0));
	   GoldenReal test=GoldenVector.dot(gn,GoldenVector.minus(p0,V));
	   if(test.isPositiveOrZero()==false) return(false);   
           if(test.isZero()==true) bdy=true;
	}
	if(BOUNDARY==false) return(true);
	return(bdy);
    }

    /**When the third coordinate of the vector is [0]=[4], there
       is a question of which one to pick.  We find guide the
       correct choice by considering the floating point value of
       the center of mass of the polyhedron.  The variable high
       is true iff this value exceeds 1. **/

    /**scaling a polyhedron**/

    public static GoldenPolyhedron scale2(GoldenPolyhedron P) {
	GoldenReal r=new GoldenReal(2,0);
	GoldenPolyhedron Q=new GoldenPolyhedron();
	Q.count=P.count;
	for(int i=0;i<P.count;++i) Q.V[i]=P.V[i].scale(r);
	return(Q);
    }


    /**FLOATING POINT ROUTINES:  These routines use floating
       point arithmetic to achieve their ends. However, the results
       of these calculations are then fed into the exact arithmetic
       programs and rigorously checked to be correct.**/


    public static int[] getItinerary(GoldenPolyhedron P,int length) {
	Polyhedron Q=P.toPolyhedron();
	Vector V=Q.getCenter();	
        int[] I=PolyhedronExchange.itinerary(V,length);
	return(I);
    }

    public static int[] getItinerary(GoldenPolyWedge P,int length) {
	PolyWedge Q=P.toPolyWedge();
	Complex z=Q.getCenter();
	return(getItinerary(z,length));
    }

    public static int[] getItinerary(Complex z,int length) {
	Vector V=TorusMap.theta(z);
	int[] I=PolyhedronExchange.itinerary(V,length);
	return(I);
    }

    public static int[] getItineraryInverse(GoldenPolyWedge P,int length) {
	PolyWedge Q=P.toPolyWedge();
	Complex z=Q.getCenter();
	return(getItineraryInverse(z,length));
    }

    public static int[] getItineraryInverse(Complex z,int length) {
	Vector V=TorusMap.theta(z);
	int[] I=PolyhedronExchange.itineraryInverse(V,length);
	return(I);
    }

    /*This routine specifically gets the chain itinerary for the
      renorm tile specified by the arguments.*/

  public static int[] itineraryChain(int a_or_b,int LA,int LB,int branch,int k) {
	Polyhedron P=new Polyhedron();
	int direction=0;
	if((a_or_b==1)&&(LA%2==0)) direction=1;
	boolean direct=true;
	boolean A_OR_B=true;
	if(a_or_b==1) A_OR_B=false;
	if(direction==1) direct=false;
	if(a_or_b==0) P=DataRenormReturn.getA(LA,LB,branch,k,direction);
	if(a_or_b==1) P=DataRenormReturn.getB(LB,branch,k,direction);
	Vector V=P.getCenter();
	return(itineraryAB(V,A_OR_B,direct,true));
  }


    /**This routine starts with a point and computes the itinerary of the
       dynamics, until the point reaches the renorm set.  The routine
       returns null if the number of iterates exceeds 799. The longest
       chain length is 703, so a failure indicates that the point is periodic.
       
       -- A_OR_B controls whether we test for the A renorm set or the B renorm set.
   
       -- forward controls whether we consider the forwards or backwards iterates

       -- FORCEMOVE controls whether we allow the possibility of 0 iterates. This
          is only relevent if the point starts out in the renorm set.

    **/

    public static int[] itineraryAB(GoldenPolyWedge P,boolean a_or_b,boolean forward,boolean FORCEMOVE) {
	PolyWedge Q=P.toPolyWedge();
	Complex z=Q.getCenter();
	Vector V=TorusMap.theta(z);
	return(itineraryAB(V,a_or_b,forward,FORCEMOVE));
    }



    public static int[] itineraryAB(Vector V0,boolean a_or_b,boolean forward,boolean FORCEMOVE) {

	boolean inside=false;
	int total=0;
	int type=-1;
	int[] LIST=new int[800];
	Vector V=new Vector(V0);


	/**We first check if the vector actually lies in the renorm set**/
        if(a_or_b==true) inside=DataRenorm.insideA(V);
        if(a_or_b==false) inside=DataRenorm.insideB(V);
	if((FORCEMOVE==false)&&(inside==true)) {
	   int[] ZERO=new int[0];
	   return(ZERO);
	}
	inside=false;


	while((total<799)&&(inside==false)) {

	    if(forward==true) {
	      type=PolyhedronExchange.classify(V);
	      LIST[total]=type; 
	      ++total;
              V=PolyhedronExchange.doDynamicsPlus(V,type);
	    }

	    if(forward==false) {
	      type=PolyhedronExchange.classifyInverse(V);
	      LIST[total]=type;  
	      ++total;
              V=PolyhedronExchange.doDynamicsMinus(V,type);
	    }

            if(a_or_b==true) inside=DataRenorm.insideA(V);
            if(a_or_b==false) inside=DataRenorm.insideB(V);
	}

	if(total>798) return(null);  //doesn't hit the renorm set
	int[] LIST2=new int[total];
	for(int i=0;i<total;++i) LIST2[i]=LIST[i];
	return(LIST2);
    }



    /**The polyhedron P here has NOT been scaled up by a factor of 2.**/

    public static GoldenPolyhedron fundamentalDomain(GoldenPolyhedron P) {
	GoldenVector V1=P.cheapInterior();
	V1=V1.scale(new GoldenReal(2,0));
        GoldenVector V2=fundamentalDomain(V1);
	GoldenVector V3=GoldenVector.minus(V2,V1);
	boolean fail=false;
	for(int i=0;i<3;++i) {
	    for(int j=0;j<2;++j) {
		if(V3.x[i].a[j]%2!=0) throw(new ProofException("fundamentalDomain"));
		V3.x[i].a[j]=V3.x[i].a[j]/2;
	    }
	}

	P=P.translate(V3);
	GoldenPolyhedron X=new GoldenPolyhedron(P);
	return(X);
    }

    /**This finds the point in the chain that lies in the A renorm set.**/

    public static GoldenComplex getChainStart(GoldenComplex z1) {
	Complex w1=z1.toComplex();
	Complex w2=StripRenorm.inside(w1,false,false,true);
	GoldenComplex z2=new GoldenComplex(w2,20,.00000001);
	return(z2);
    }

    /**This finds the point p=(x,y) in the A-chain that minimizes |x|**/


    public static GoldenComplex getMinimizeA(GoldenComplex z1) {
	Complex w1=z1.toComplex();
	Complex w2=StripRenorm.inside(w1,false,false,true);
	Complex w3=StripRenorm.minimizeA(w2);
	GoldenComplex z3=new GoldenComplex(w3,20,.00000001);
	return(z3);
    }

    /**This finds the point p=(x,y) in the B-chain that minimizes |x|**/

    public static GoldenComplex getMinimizeB(int[] L,GoldenComplex z1) {
	Complex w1=z1.toComplex();
	boolean reverse=false;
        if(L[0]%2==0) reverse=true;
        Complex w2=StripRenorm.inside(w1,false,false,true); 
        Complex w3=StripRenorm.renorm(w2,reverse);
	GoldenComplex z3=new GoldenComplex(w3,20,.00000001);
	return(z3);
    }

}