package gve.calc.formula;

import awt.*;
import java.awt.*;
import awt.Button;
import java.awt.event.*;
import gve.calc.logic.TableauPart;
import gve.calc.logic.OperatorModel;

public class OperatorBooleanView extends InfixBinaryOpView implements ActionListener {
	public OperatorBooleanView(OperatorBoolean model,FormulaView view,Component operatorView) {
		super(model,view,operatorView);
	}

	public Component createPopup(int x,int y) {
		OperatorBoolean model = (OperatorBoolean)getModel();
		Button b;
		byte kind = model.getKind();
		Container cont = new Panel();
		cont.setLayout(new GridPackLayout(0,1));
		boolean empty = true;
		// is this the main operator of a formula on the left/right of a |> operator?
		if (kind == OperatorBoolean.AND) {
			Part p = (Part)getModel();
			while (p.parent instanceof OperatorComma) p = p.parent;
			if (p.parent instanceof OperatorModel
				&& ((OperatorModel)p.parent).getKind()==OperatorModel.TRIANGLE
				&& !TableauPart.hasReduction(p.parent)) {
				cont.add(b = new Button("Reduce in tableau"));
				empty = false;
				b.addActionListener(this);
			}
		} else if (kind==OperatorBoolean.OR || kind==OperatorBoolean.IMPLIES) {
			/* PENDING: check if the parent is OperatorModel and has no reduction ... */
			cont.add(b = new Button("Rewrite with not/and"));
			empty = false;
			b.addActionListener(this);
		}
		if (!empty) return cont;
		return null;
	}

	public void actionPerformed(ActionEvent evt) {
		String cmd = evt.getActionCommand();
		OperatorBoolean operator = (OperatorBoolean)getModel();
		FormulaView view = FormulaView.get(this);
		Formula f = view.getFormula();
		if (cmd.equals("Rewrite with not/and")) {
			Identifier dummy = new Identifier("");
			switch(operator.getKind()) {
			case OperatorBoolean.OR:	// a or b == not(not a¬ b)
			    {	f.replace(operator,dummy);
				Part left = operator.left, right = operator.right;
				int notpri = new OperatorNot(new Identifier("")).getDownPri();
				if (left instanceof InfixBinaryOp && ((InfixBinaryOp)left).getPri()<notpri)
					left = new Brackets(left);
				if (right instanceof InfixBinaryOp && ((InfixBinaryOp)right).getPri()<notpri)
					right = new Brackets(right);
				f.replace(dummy,new OperatorNot(new Brackets(
					new OperatorBoolean("&",new OperatorNot(left),new OperatorNot(right))
				)));
			    }
				break;
			case OperatorBoolean.IMPLIES:	// a=>b == not a or b == not(a & not b)
			    {	f.replace(operator,dummy);
			    	// STRANGE: if we don't clone the left Part, the syntax tree comes out OK,
				// but it's not shown: the user sees "not(¬ rightpart)" !!
				Part left = (Part)operator.left.clone(), right = operator.right;
				int notpri = new OperatorNot(new Identifier("")).getDownPri();
				int andLpri = ((OperatorBoolean)getModel()).getLeftPri();
				if (left instanceof InfixBinaryOp && ((InfixBinaryOp)left).getPri()<andLpri)
					left = new Brackets(left);
				if (right instanceof InfixBinaryOp && ((InfixBinaryOp)right).getPri()<notpri)
					right = new Brackets(right);
				f.replace(dummy,new OperatorNot(new Brackets(
					new OperatorBoolean("&",left,new OperatorNot(right))
				)));
			    }
				break;
			}
		} else if (cmd.equals("Reduce in tableau") && operator.getKind()==OperatorBoolean.AND) {
			Part p = operator;
			while (p.parent instanceof OperatorComma) p = p.parent;
			if (p.parent instanceof OperatorModel && ((OperatorModel)p.parent).getKind()==OperatorModel.TRIANGLE) {
				OperatorModel mod = (OperatorModel)p.parent;
				if (p == mod.right) {	// Reduceren aan rechterkant
					// Add double branch
					Identifier dummy = new Identifier("");
					Part rightlist,leftlist;
					OperatorModel leftbranch = new OperatorModel("|>",(Part)mod.left.clone(),
						leftlist=OperatorComma.copyListExcept(mod.right,operator));
					OperatorModel rightbranch = new OperatorModel("|>",(Part)mod.left.clone(),
						rightlist=OperatorComma.copyListExcept(mod.right,operator));
					f.replace(mod,new TableauPart(dummy,leftbranch,rightbranch));
					f.replace(dummy,mod);
					OperatorComma.addToFrontOfList(f,leftlist,(Part)operator.left.clone());
					OperatorComma.addToFrontOfList(f,rightlist,(Part)operator.right.clone());
				} else if (p == mod.left) {	// operator staat links
					Identifier dummy = new Identifier("");
					OperatorModel newmod = new OperatorModel("|>",dummy,(Part)mod.right.clone());
					{	// Add branch
						Identifier dummy2 = new Identifier("");
						f.replace(mod,new TableauPart(dummy2,newmod));
						f.replace(dummy2,mod);
					}
					if (mod.left instanceof OperatorComma) {
						OperatorComma comma = (OperatorComma)mod.left;
						f.replace(dummy,comma.copyListExcept(operator));
						OperatorComma.addToFrontOfList(f,newmod.left,(Part)operator.right.clone());
						OperatorComma.addToFrontOfList(f,newmod.left,(Part)operator.left.clone());
					} else {
						f.replace(dummy,new OperatorComma((Part)operator.left.clone(),(Part)operator.right.clone()));
					}
				}
			}
		}
	}
}