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


/*This file does calculation 1*/


public class ProofCalc1 {


    public static void main(Manager M) {
	for(int i=0;i<8;++i) M.C.MESSAGE[i]="";
	M.C.MESSAGE[0]="calc 1 start";
	M.C.MESSAGE[1]="computing pairs";
	M.C.repaint();
	int[][] t=overlapList();
	verify(t,M);
    }

    /*This tests the calculation 1 identity on a grid of
      points fine enough to hit every region*/

    public static void verify(int[][] t,Manager M) {

	int count=0;
	int[] LIST=new int[t.length];
	for(int i=0;i<t.length;++i) LIST[i]=-1;

	LongPolyhedron P=DataPartitionExtra.domainF1();
	for(int k=105;k<420;k=k+10) {
	    for(int i=-840;i<840;i=i+20) {
		for(int j=-420;j<420;j=j+20) {
		    LongVector W=new LongVector(i,j,k);
		    for(int q=0;q<t.length;++q) {
	              LongPolyhedron Q1=DataPartition.imagePoly(t[q][0]);
		      LongPolyhedron Q2=DataPartition.alphaPoly(t[q][1]);
		      boolean test1=LongPolyCombinatorics.insideStrict(W,Q1);
		      boolean test2=LongPolyCombinatorics.insideStrict(W,Q2);
		      if((test1==true)&&(test2==true)) {
			  if(onList(q,LIST,count)==false) {
			      LIST[count]=q;
			      ++count;
			      boolean test=checkIdentity(W);
			      Integer COUNT=new Integer(count);
			      M.C.MESSAGE[2]=COUNT.toString()+" out of 48";
			      if(count==48) M.C.MESSAGE[3]="finishing loop";
			      M.C.repaint();
			      if(test==false) throw new ProofException("calc 1 fails");
			  }
		      }
		    }
		}
	    }
	}
	if(count<t.length) throw new ProofException("not all hit");
	M.C.MESSAGE[4]="calc 1 done";
	M.C.repaint();
    }


    public static boolean onList(int k,int[] LIST,int count) {
	for(int i=0;i<count;++i) {
	    if(k==LIST[i]) return(true);
	}
	return(false);
    }

    /*This checks the main identity*/
    public static boolean checkIdentity(LongVector W) {
        LongVector W1=ProofSupport.F2(W);
        LongVector W2=ProofSupport.alpha(W);
	W2=ProofSupport.F1(W2);
	W2=ProofSupport.alpha(W2);
	LongVector W3=LongVector.minus(W1,W2);
	long dot=LongVector.dot(W3,W3);
	if(dot==0) return(true);
	return(false);
    }





    /**This generates the list of pairs of polyhedra from
       the F^{-1} partition and the alpha F alpha partition
       which are not disjoint*/

    public static int[][] overlapList() {
	int[][] t=new int[100][2];
	int count=0;
	for(int i=0;i<32;++i) {
	    for(int j=0;j<32;++j) {
		LongPolyhedron P=DataPartition.imagePoly(i);
		LongPolyhedron Q=DataPartition.alphaPoly(j);
	        boolean test=LongPolyCombinatorics.separate(10,P,Q);
		if(test==false) {
		    t[count][0]=i;
		    t[count][1]=j;
		    ++count;
		}
	    }
	}
	int[][] u=new int[count][2];
	for(int i=0;i<count;++i) u[i]=t[i];
	return(u);
    }



}