package gve.calc.logic;

import awt.*;
import java.awt.*;
import gve.calc.formula.*;

 Model theory operators 
public class OperatorModel extends InfixBinaryOp {
	private byte kind;

	public static final byte ASSERTION=0;	// single turnstyle
	public static final byte MODELS=1;	// double turnstyle
	public static final byte TRIANGLE=2;

	public String getName() {
		return kind==ASSERTION ? "|-" :
			kind==MODELS ? "|=" :
			kind==TRIANGLE ? "|>" : "*ERROR*";
	}

	public int getPri() { return 400; }

	public int getKind() { return kind; }

	
 This constructor supposes the name is valid.
	  Only a very minimal sanity check is made. 
	public OperatorModel(String name,Part l,Part r) {
		super(l,r);
		switch(name.charAt(1)) {
		case '-': kind = ASSERTION; break;
		case '=': kind = MODELS; break;
		case '>': kind = TRIANGLE; break;
		default: throw new Error("Bad quantor name "+name);
		}
	}

	public OperatorModel(byte kind,Part l,Part r) {
		super(l,r);
		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 left = Part.read(r);
		Part right = Part.read(r);
		String line = r.readLine();
		byte kind = (byte)Integer.parseInt(line);
		return new OperatorModel(kind,left,right);
	}

	public Part evaluate(Evaluator ev) {
		return new OperatorModel(kind,left.evaluate(ev),right.evaluate(ev));
	}

	public boolean same(Object o) {
		if (!(o instanceof OperatorModel)) return false;
		OperatorModel obj = (OperatorModel)o;
		return kind==obj.kind && left.same(obj.left) && right.same(obj.right);
	}

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

	public void saveOperatorLatex(java.io.BufferedWriter w) throws java.io.IOException {
		switch (kind) {
		case ASSERTION:
			w.write("\\vdash");
			break;
		case MODELS:
			w.write("\\models");
			break;
		case TRIANGLE:
			w.write("\\rhd");
			break;
		}
	}
}

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

	public Dimension getSymbolSize() {
		FontMetrics metrics = getFontMetrics(getFont());
		return new Dimension(metrics.charWidth(' ')+1,metrics.getHeight());
	}

	public void paintSymbol(Graphics g) {
		int spatWidth = g.getFontMetrics().charWidth(' ');
		int mBase = g.getFontMetrics().getAscent();
		int opWidth = spatWidth;
		if (kind == OperatorModel.ASSERTION) paintAssertion(g,opWidth,mBase);
		else if (kind == OperatorModel.MODELS) paintModels(g,opWidth,mBase);
		else if (kind == OperatorModel.TRIANGLE) paintTriangle(g,opWidth,mBase);
	}

	private void paintAssertion(Graphics g,int w,int h) {
		h--;
		g.drawLine(0,0,0,h);
		g.drawLine(0,h/2,w,h/2);
	}

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

	private void paintTriangle(Graphics g,int w,int h) {
		h--;
		g.drawLine(0,0,0,h);
		g.drawLine(0,h,w,h/2);
		g.drawLine(w,h/2,0,0);
	}
}