/*	Copyright (C) 2000, 2001, Geert Vernaeve. All Rights Reserved.	*/
package gve.calc.logic;

import java.awt.*;
import java.awt.event.*;
import java.util.Enumeration;
import awt.*;
import awt.Button;
import gve.calc.formula.*;
import gve.calc.formula.Part;
import gve.calc.formula.HasCursorPos;

public class ProofView extends TabularView implements CreatesPopup {
	public ProofView(Proof model,FormulaView view) {
		super(model,view);
		int h = model.getHeight();
		int w = model.getWidth() + 1;
		for (int i = 0; i < h; i++) {
			// We use CursorPosLabels because they implement HasBaseline.
			add(new CursorPosLabel(""+(i+1)),i*w);
		}
		TabularLayout layout = (TabularLayout)getLayout();
		layout.HSPACE=20;
		layout.setCols(model.getWidth() + 1);
	}

	public void updateView(Object with) {
		if (with instanceof RepaintRequest) {
			// Actually only need to repaint 1 line ...
			repaint();
		} else super.updateView(with);
		checkLineNumbers();
	}

	
 Since the View has a column that does not correspond to a column of
	  the Model, we have to manage that column ourselves by supplying
	  our own addRow() and remRow() routines. 
	public void addRow(int row) {
		FormulaView view = FormulaView.get(this);
		Proof model = (Proof)getModel();
		int w = model.getWidth() + 1;
		add(new CursorPosLabel(""+(row+1)),row * w);
		for (int j = 0; j < model.getWidth(); j++)
			add(view.getView(model.elementAt(row,j)),j+1 + w * row);
		TabularLayout layout = (TabularLayout)getLayout();
		layout.setRows(model.getHeight());
	}

	public void remRow(int row) {
		Proof model = (Proof)getModel();
		int w = model.getWidth() + 1;
		for (int j = model.getWidth(); j>=0; j--)
			remove (j + w * row);
		TabularLayout layout = (TabularLayout)getLayout();
		layout.setRows(model.getHeight());		
	}

	
 The line number labels of the proof are not part of the Part tree,
	  since Parts want to be as economically as possible.
	  This method checks if the labels are still showing the correct
	  line numbers. 
	private void checkLineNumbers() {
		Proof model = (Proof)getModel();
		int h = model.getHeight();
		int w = model.getWidth() + 1;
		for (int i = h-1; i>=0; i--) {
			Component comp = getComponent(i*w);
			if (!(comp instanceof CursorPosLabel)) continue;
			CursorPosLabel lab = (CursorPosLabel)comp;
			String shouldbe = ""+(i+1);
			String str = lab.getText();
			if (str.equals(shouldbe)) continue;	// label is OK
			lab.setText(shouldbe);
			lab.invalidate();
		}
	}

	public void paint(Graphics g) {
		Proof proof = (Proof)getModel();
		int h = proof.getHeight();
		Dimension siz = getSize();
		int y = 0;
		int xoffset = 0;
		if (getCursorPos() == Somewhere_LEFT)
			xoffset = g.getFontMetrics().charWidth(' ');
		TabularLayout layout = (TabularLayout)getLayout();
		Color col = g.getColor();
		for (int i = 0; i < h; i++) {
			int rowheight =  layout.getRowHeight(this,i);
			switch (proof.getLineStatus(i)) {
			case Proof.DUNNO: break;
			case Proof.OKAY: g.setColor(Color.green);
				g.drawRect(xoffset,y,siz.width-xoffset-1,rowheight-1);
				break;
			case Proof.BAD: g.setColor(Color.red);
				g.drawRect(xoffset,y,siz.width-xoffset-1,rowheight-1);
				break;
			}
			y += layout.VSPACE + rowheight;
		}
		g.setColor(col);
		super.paint(g);
	}

	public Component createPopup(int x,int y) {
		Button b;
		FormulaView view = FormulaView.get(this);
		ProofViewListener listen = new ProofViewListener(this,y);
		Container cont = new Panel();
		cont.setLayout(new GridPackLayout(0,1));
		cont.add(b = new Button("Insert line"));
		b.addActionListener(listen);
		cont.add(b = new Button("Verify line"));
		b.addActionListener(listen);
		cont.add(b = new Button("Verify proof"));
		b.addActionListener(listen);
		MenuButton mb;
		cont.add(mb = new MenuButton("Rules",this,MenuButton.RIGHT));
		mb.add(b = new Button("prem"));
		b.addActionListener(listen);
		Part rules = view.getVar("rules");
		if (rules instanceof Brackets) {
			Brackets rulez = (Brackets)rules;
			if (rulez.getKind() == Brackets.CURLY) {
				CommaEnumerator enum = new CommaEnumerator(rulez.getChild());
				while (enum.hasMoreElements()) {
					Part p = enum.nextPart();
					if (!(p instanceof ProofRule)) continue;
					ProofRule rule = (ProofRule)p;
					String label = rule.getName();
					int nargs = rule.getParamCount();
					if (nargs > 0) label += " / "+nargs;
					mb.add(b = new Button(label));
					b.addActionListener(listen);
				}
			}
		}
		LoadRules.addLoadButtons(mb.popup,view);
		mb.pack();
		return cont;
	}

	public boolean keydn(int key) {
		Proof proof = (Proof)getModel();
		FormulaView view = FormulaView.get(this);
		if (key == Key_BS) {
			Point p = proof.whichOffspring(view.getCursorPart());
			if (p == null) return super.keydn(key);
			if (Part.isEmpty(proof.elementAt(p.y,Proof.SEQUENT)) && Part.isEmpty(proof.elementAt(p.y,Proof.BECAUSE))) {
				proof.removeRow(p.y);
				view.setCursorPart(proof.elementAt(p.y>0 ? p.y-1 : 0,p.x==1 ? Proof.SEQUENT : Proof.BECAUSE));
				return true;
			}
		}
		if (key != '\n') return super.keydn(key);
		int child;
		{	Point p = proof.whichOffspring(view.getCursorPart());
			if (p == null) return super.keydn(key);
			child = p.y;
		}
		if (child == proof.getHeight()) return super.keydn(key);	// uh?
		proof.insertRow(child+1);
/*		Identifier left = new Identifier();
		OperatorModel fresh = new OperatorModel(OperatorModel.ASSERTION,left,new Identifier(""));
		// Note that we cannot call directly "proof.setElementAt()"
		// because that would not update the view's Component tree
		Formula f = FormulaView.get(this).getFormula();
		f.replace(proof.elementAt(child+1,Proof.SEQUENT),fresh);
		view.setCursorPart(left);
*/		view.setCursorPart(proof.elementAt(child+1,Proof.SEQUENT));
		return true;
	}
}

class ProofViewListener implements ActionListener {
	ProofView proofview;
	int ypos;

	public ProofViewListener(ProofView view,int y) {
		proofview = view;
		ypos = y;
	}

	
 lineno is internal line number (so the first line has number 0) 
	private void oops(int lineno,String title,Exception exc) {
		SimpleDialog dialog = new SimpleDialog(proofview,title,false);
		dialog.addText(exc.toString());
		dialog.addButton("OK");
		Proof proof = (Proof)proofview.getModel();
		Part rule = proof.elementAt(lineno,Proof.BECAUSE);
		String rulename = null;
		if (rule instanceof OperatorSpace) {
			OperatorSpace spat = (OperatorSpace)rule;
			rule = spat.left;
		}
		if (rule instanceof Identifier) rulename = ((Identifier)rule).getString();
		if (!rulename.equals("arg") && !rulename.equals("prem")) {
			Button b;
			dialog.addComp(b = new Button("Show rule "+rulename));
			b.addActionListener(this);
		}
		if (exc instanceof ProofInvalidException) {
			ProofInvalidException proofexc = (ProofInvalidException)exc;
			if (proofexc.status != null && proofexc.status.bestLine >= 0) {
				dialog.addComp(new ProofSuccessButton(rulename,proofexc.status,"Show best match"));
			}
		}

//		dialog.addComp(LoadRules.createLoadButton(
//			dialog,MenuButton.DOWN,FormulaView.get(proofview)));
		dialog.getResult();	// display dialog
	}

	public void actionPerformed(ActionEvent evt) {
		String cmd = evt.getActionCommand();
		if (cmd.startsWith("Show rule ")) {
			cmd = cmd.substring(10);
			gve.calc.StackCanvas stack = gve.calc.StackWindow.createNew().getCanvas();
			Part p = stack.load(cmd);
			if (p == null) stack.push(new Formula(new StringPart("Unknown rule "+cmd)));
			else stack.push(new Formula(p));
			return;
		}
		Proof proof = (Proof)proofview.getModel();
		FormulaView fview = FormulaView.get(proofview);
		Formula formula = fview.getFormula();
		if (cmd.equals("Insert line")) {
			proofview.insertRowAtPixel(ypos);
		} else if (cmd.equals("Verify line")) {
			int lineno = ((TabularLayout)proofview.getLayout()).pixel2rowAt(ypos);
			boolean okay = true;
			try {proof.vfyline(lineno,fview.getVariableStore()); }
			catch (ProofInvalidException exc) {
				okay = false;
				if (exc.part != null)
					fview.setCursorPart(exc.part);
				if (Proof.debuglevel>=10) System.out.println(exc);
				oops(lineno,"Oops",exc);
			}
			proof.setLineStatus(lineno,okay ? Proof.OKAY : Proof.BAD);
		} else if (cmd.equals("Verify proof")) {
			int lines = proof.getHeight();
			for (int lineno = 0; lineno < lines; lineno++)
				proof.setLineStatus(lineno,Proof.DUNNO);
			for (int lineno = 0; lineno < lines; lineno++) {
				try { proof.vfyline(lineno,fview.getVariableStore()); }
				catch (ProofInvalidException exc) {
					proof.setLineStatus(lineno,Proof.BAD);
					if (exc.part != null)
						fview.setCursorPart(exc.part);
					if (Proof.debuglevel>=10) System.out.println(exc);
					oops(lineno,"Oops at line"+(lineno+1),exc);
					break;
				}
				proof.setLineStatus(lineno,Proof.OKAY);
			}
		} else {
			Object src = evt.getSource();
			if (!(src instanceof Component)) return;
			Component comp = (Component)src;
			comp = MenuButton.getParentMenuButton(comp);
			if (comp == null) return;
			if (((MenuButton)comp).getLabel().equals("Rules")) {
				String rulename;
//				int nargs = 0;
				{	// Process "rulename / #"
					int idx = cmd.indexOf(" / ");
					if (idx>= 0) {
						rulename = cmd.substring(0,idx);
//						nargs = Integer.parseInt(cmd.substring(idx+3));
					} else rulename = cmd;
				}
				int lineno = ((TabularLayout)proofview.getLayout()).pixel2rowAt(ypos);
				Part because = proof.elementAt(lineno,Proof.BECAUSE);
				Part ident = new Identifier(rulename);
				if (because instanceof Identifier) {
					formula.replace(because,ident);
				} else if (because instanceof OperatorSpace) {
					Part left = ((OperatorSpace)because).left;
					if (left instanceof Identifier)
						formula.replace(left,ident);
				} else return;
				fview.setCursorPart(ident,HasCursorPos.Somewhere_RIGHT);
			}
		}
	}
}

class ProofSuccessButton extends Button implements ActionListener {
	private ProofSuccess status;
	private String rulename;
	private Proof rule;

	public ProofSuccessButton(String rulename,ProofSuccess stat,String label) {
		super(label);
		status = stat;
		this.rulename = rulename;
		addActionListener(this);
	}
	
	public void actionPerformed(ActionEvent evt) {
		gve.calc.StackCanvas stack = gve.calc.StackWindow.createNew().getCanvas();
		stack.push(new Formula(new StringPart("Match succeeded up to line "+(status.bestLine+1))));
		Matrix mat = new Matrix(1,2);
		mat.setElementAt(0,0,new Identifier("Symbol"));
		mat.setElementAt(0,1,new Identifier("Match"));
		{	Matcher m = status.match;
			Enumeration enum = m.matchedSymbols();
			while (enum.hasMoreElements()) {
				String symbol = (String)enum.nextElement();
				Part val = m.getMatchedValue(symbol);
				if (val == null) continue;
				// This Part is already visible in the proof itself, so we have to clone
				// it if we want to show it in our window
				val = (Part)val.clone();
				mat.insertRow(1);
				mat.setElementAt(1,0,new Identifier(symbol));
				mat.setElementAt(1,1,val);
			}
		}
		stack.push(new Formula(mat));
		{	Part p = stack.load(rulename);
			if (p instanceof Proof) rule = (Proof)p;
		}
		if (rule != null) {
			mat = new Matrix(1,3);
			// Add prems
			for (int i = 0; i < rule.getHeight()-1; i++) {
				Part p = rule.elementAt(i,Proof.BECAUSE);
				if (!(p instanceof Identifier)) continue;
				String because = ((Identifier)p).getString();
//System.out.println(i+"\t"+because);
				if (!because.equals("prem")) continue;
				addLine(mat,i);
			}
			addLine(mat,rule.getHeight()-1);	// Add conclusion
			if (mat.getHeight() > 1) {
				mat.removeRow(0);
				FormulaView view = stack.push(new Formula(mat));
				StandardFunctions.registerFunctions(status.match.getEvaluator());
				for (int i = mat.getHeight()-1; i>=0; i--)
					colour(mat.elementAt(i,1),view);
			}
		}
	}

	private void colour(Part p,FormulaView view) {
		if (p instanceof Identifier) {
			String str = ((Identifier)p).getString();
			if (status.match.getMatchedValue(str) != null) return;
			if (status.match.isFunction(str)) return;
			view.getView(p).setBackground(Color.red);
			view.getView(p).setForeground(Color.white);
			return;
		}
		Part child;
		for (int count = 0; ; count++) {
			child = p.getChild(count);
			if (child == null) return;
			colour(child,view);
		}
	}

	
 Add a to-be-coulored-in line to the given matrix 
	private void addLine(Matrix mat,int lineno) {
		Formula f = new Formula(mat);
		int h = mat.getHeight();
		mat.insertRow(h);
		mat.setElementAt(h,0,new Identifier(""+(lineno+1)));
		Part p = rule.elementAt(lineno,Proof.SEQUENT);
		Part colour = (Part)p.clone();
		mat.setElementAt(h,1,colour);
		mat.setElementAt(h,2,rule.elementAt(lineno,Proof.BECAUSE));
	}
}