lib/browser/GraphBrowser/Spline.java
author blanchet
Wed, 04 Aug 2010 23:27:27 +0200
changeset 38195 a8cef06e0480
parent 33686 8e33ca8832b1
child 50473 ca4088bf8365
permissions -rw-r--r--
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     1
/***************************************************************************
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     2
  Title:      GraphBrowser/Spline.java
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     3
  Author:     Stefan Berghofer, TU Muenchen
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     4
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     5
  This class is used for drawing spline curves (which are not yet
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     6
  supported by the Java AWT).
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     7
***************************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     8
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     9
package GraphBrowser;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    10
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    11
import java.awt.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    12
import java.util.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    13
import java.io.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    14
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    15
class SplineSection {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    16
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    17
	/*** Section of a spline function ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    18
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    19
	double x_b,x_c,x_d;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    20
	double y_b,y_c,y_d;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    21
	int dx,dy;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    22
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
	public SplineSection(double xb,double xc,double xd,
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    24
		double yb,double yc,double yd,int dx2,int dy2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    25
		x_b=xb;x_c=xc;x_d=xd;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    26
		y_b=yb;y_c=yc;y_d=yd;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    27
		dx=dx2;dy=dy2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    28
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    29
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    30
	public Point draw(Graphics g,Point s) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    31
		double m;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    32
		int s_x,s_y,e_x=0,e_y=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
		int x,y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    34
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    35
		s_x=s.x;s_y=s.y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    36
		if (dx>=dy) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    37
			if (dx==0) return s;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    38
			m=1/((double)dx);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    39
			for (x=0;x<dx;x++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    40
				e_x=(int)(Math.round((x_b*x*m+x_c)*x*m+x_d));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    41
				e_y=(int)(Math.round((y_b*x*m+y_c)*x*m+y_d));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    42
				g.drawLine(s_x,s_y,e_x,e_y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    43
				s_x=e_x;s_y=e_y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    44
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    45
		} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    46
			m=1/((double)dy);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    47
			for (y=0;y<dy;y++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    48
				e_x=(int)(Math.round((x_b*y*m+x_c)*y*m+x_d));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    49
				e_y=(int)(Math.round((y_b*y*m+y_c)*y*m+y_d));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    50
				g.drawLine(s_x,s_y,e_x,e_y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    51
				s_x=e_x;s_y=e_y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    52
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    53
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    54
		return new Point(e_x,e_y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    55
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    56
}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    57
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    58
public class Spline {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    59
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    60
	Vector sections;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    61
	Vector points;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    62
	Point start,end;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    63
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    64
	public Spline(Vector pts) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    65
		int i;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    66
		double d0,d1,d2,d3;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    67
		Point p0,p1,p2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    68
		SplineSection s;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    69
		
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    70
		start=(Point)(pts.firstElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    71
		end=(Point)(pts.lastElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    72
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    73
		sections=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    74
		for (i=1;i<=pts.size()-4;i+=3) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
			p0=(Point)(pts.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
			p1=(Point)(pts.elementAt(i+1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    77
			p2=(Point)(pts.elementAt(i+2));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    78
			s=new SplineSection(
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    79
				(double)(p2.x-2*p1.x+p0.x),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    80
				2.0*(p1.x-p0.x),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    81
				(double)(p0.x),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    82
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
				(double)(p2.y-2*p1.y+p0.y),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    84
				2.0*(p1.y-p0.y),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    85
				(double)(p0.y),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    86
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    87
				Math.abs(p2.x-p0.x),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    88
				Math.abs(p2.y-p0.y)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    89
			);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    90
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    91
			sections.addElement(s);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    92
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    93
		points=pts;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    94
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    95
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    96
	public void draw(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    97
		Enumeration e1=sections.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    98
		Point p=start;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    99
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   100
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   101
			p=((SplineSection)(e1.nextElement())).draw(g,p);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   102
		g.drawLine(p.x,p.y,end.x,end.y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   103
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   104
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   105
	public void PS(PrintWriter p) {
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   106
		Point p0,p1,p2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   107
		int i;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   108
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   109
		p.println("n "+start.x+" "+start.y+" m");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   110
		for (i=1;i<=points.size()-4;i+=3) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   111
			p0=(Point)(points.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   112
			p1=(Point)(points.elementAt(i+1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   113
			p2=(Point)(points.elementAt(i+2));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   114
			p.println(p0.x+" "+p0.y+" l");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   115
			p.println(p0.x+" "+p0.y+" "+p1.x+" "+p1.y+" "+p2.x+" "+p2.y+" c");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   116
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   117
		p.println(end.x+" "+end.y+" l s");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   118
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   119
}