package gve.calc.formula;

import java.awt.*;

public class OperatorQuantor extends PrefixUnaryOp {
	private boolean kind;

	public static final boolean EXISTS = false;
	public static final boolean FORALL = true;

	public String getName() {
		return kind ? "forall" : "exists";
	}

	public int getPri() { return 800; }

	public boolean getKind() { return kind; }

	public OperatorQuantor(String name,Part ch) {
		super(ch);
		switch(name.charAt(0)) {
		case 'e': kind = EXISTS; break;
		case 'f': kind = FORALL; break;
		default: throw new Error("Bad quantor name "+name);
		}
	}

	OperatorQuantor(boolean kind,Part ch) {
		super(ch);
		this.kind = kind;
	}

	public void write(java.io.Writer w) throws java.io.IOException {
		super.write(w);
		w.write(kind+"\n");
	}

	public static Part read(java.io.BufferedReader r) throws java.io.IOException,
			ClassNotFoundException,NoSuchMethodException,
			java.lang.reflect.InvocationTargetException,IllegalAccessException{
		Part child = Part.read(r);
		String line = r.readLine();
		boolean kind = java.lang.Boolean.valueOf(line).booleanValue();
		return new OperatorQuantor(kind,child);
	}

	public boolean same(Object o) {
		if (o instanceof OperatorQuantor) {
			OperatorQuantor quantor = (OperatorQuantor)o;
			return quantor.kind==kind && quantor.child.same(child);
		}
		return false;
	}

	public Component createView(FormulaView view) {
		return new PrefixUnaryOpView(this,view,new OperatorQuantorSymbolView(kind,getName()));
	}

	public void saveOperatorLatex(java.io.BufferedWriter w) throws java.io.IOException {
		if (kind == EXISTS) w.write("\\exists");
		else if (kind == FORALL) w.write("\\forall");
	}
}

class OperatorQuantorSymbolView extends TextSymbolView {
	private boolean kind;
	public OperatorQuantorSymbolView(boolean kind,String str) {
		super(str);
		this.kind = kind;
	}

	public Dimension getSymbolSize() {
		FontMetrics metrics = getFontMetrics(getFont());
		int opWidth = metrics.charWidth(kind ? 'A' : 'E');
		return new Dimension(opWidth,metrics.getHeight());
	}

	public void paintSymbol(Graphics g) {
		FontMetrics metrics = g.getFontMetrics();
		int ascent = metrics.getAscent();
		int opWidth = metrics.charWidth(kind ? 'A' : 'E');
		if (kind == OperatorQuantor.EXISTS) paintExists(g,opWidth,ascent);
		else if (kind == OperatorQuantor.FORALL) paintForall(g,opWidth,ascent);
	}

	
 Paint inside pixels [0,w-1] x [0,h-1] 
	private void paintExists(Graphics g,int w,int h) {
		w--; h--;	// Makes calculations easier
		g.drawLine(0,h,w,h);
		g.drawLine(w,h,w,0);
		g.drawLine(w,0,0,0);
		g.drawLine(w/2,h/2,w,h/2);		
	}

	private void paintForall(Graphics g,int w,int h) {
		w--; h--;
		g.drawLine(0,0,w/2,h);
		g.drawLine(w/2,h,w,0);
		g.drawLine(w/4,h/2,w*3/4,h/2);
	}
}