Copyright (C) 2000, 2001, Geert Vernaeve. All Rights Reserved.
  Created 3-Dec-2000. 
package test;

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

 Regression tests. 
public class Test {
	public static void main(String [] args) {
		gve.calc.formula.StandardOperators.registerStandardOps();
		StackWindow calc = new StackWindow(null);
		StackCanvas canvas = calc.getCanvas();

		boolean result;
		result = test1(canvas);
		print(1,result);

		result = test2(canvas);
		print(2,result);
		
		result = test3(canvas);
		print(3,result);

		result = test4(canvas);
		print(4,result);

// Commented out because this tests the experimental Stack class ...
//		result = test5(canvas);
//		print(5,result);

		print (6,test6(canvas));
		print (7,test7(canvas));
		print (8,test8(canvas));		
		print (9,test9(canvas));

		testProof(canvas,"propctest");
		testProof(canvas,"propcctest",29);

		testProof(canvas,"A"); testProof(canvas,"C"); testProof(canvas,"C1");
		testProof(canvas,"C2"); testProof(canvas,"R"); testProof(canvas,"X");

		testProof(canvas,"bewijs1"); testProof(canvas,"bewijs2"); testProof(canvas,"bewijs3");

		testProof(canvas,"ZeBe"); testProof(canvas,"ZeOn"); testProof(canvas,"NN1");
		testProof(canvas,"NN2"); testProof(canvas,"SN"); testProof(canvas,"CoPo1");
		testProof(canvas,"CoPo2"); testProof(canvas,"CoPo3"); testProof(canvas,"CoPo4");
		testProof(canvas,"XQ1"); testProof(canvas,"AEx"); testProof(canvas,"AEx2");
		testProof(canvas,"CCo"); testProof(canvas,"AnDc"); testProof(canvas,"AnU");
		testProof(canvas,"UU"); testProof(canvas,"XQ2"); testProof(canvas,"NX");

		testProof(canvas,"D"); testProof(canvas,"D1"); testProof(canvas,"D2");
		testProof(canvas,"I"); testProof(canvas,"I1");

		testProof(canvas,"I2"); testProof(canvas,"XQ3"); testProof(canvas,"DEl");
		testProof(canvas,"IEl"); testProof(canvas,"MP"); testProof(canvas,"KeRe");
		testProof(canvas,"ZeIm"); testProof(canvas,"UD"); testProof(canvas,"DCo");
		testProof(canvas,"DAs1"); testProof(canvas,"DAs2");

		// Base rules for predicate calculus
		testProof(canvas,"G"); testProof(canvas,"Gx"); testProof(canvas,"Stx");
		testProof(canvas,"E"); testProof(canvas,"Etx");

		// Derived predicate rules
		testProof(canvas,"GGx"); testProof(canvas,"ExGxt"); testProof(canvas,"SGxy");
		testProof(canvas,"AvGxy");

		testProof(canvas,"ESy"); testProof(canvas,"ET");

		testProof(canvas,"ECnx"); testProof(canvas,"EAnx"); testProof(canvas,"GPx");
		testProof(canvas,"ExPxt"); testProof(canvas,"SPxy"); testProof(canvas,"AvPxy");

		testProof(canvas,"predtest");

		testProof(canvas,"subtest");

		// Simple prop calculus
		testProof(canvas,"oef1"); testProof(canvas,"oef2");

		// Heavy predicate stuff
		testProof(canvas,"oef31"); testProof(canvas,"oef31b"); testProof(canvas,"oef371");
		testProof(canvas,"oef372"); testProof(canvas,"oef373"); testProof(canvas,"oef373b");
		testProof(canvas,"oef374");

		// The "most important" substitution calculus rules
		testProof(canvas,"SubL1"); testProof(canvas,"FreeG2"); testProof(canvas,"FreeNil");
		testProof(canvas,"FreeList"); testProof(canvas,"FreeG"); testProof(canvas,"SubL2");
		testProof(canvas,"SubL4"); testProof(canvas,"SubList2"); testProof(canvas,"SubG1");
		testProof(canvas,"VarVar"); testProof(canvas,"FV1"); testProof(canvas,"SubG2");
		testProof(canvas,"SubConst"); testProof(canvas,"SubTerm"); testProof(canvas,"SubList");
		testProof(canvas,"SubEq"); testProof(canvas,"SubPred"); testProof(canvas,"SubVar");

		stats();

//		System.exit(0);
	}

	static int passed = 0, failed = 0;

	static void print(int testno,boolean result) {
		System.out.println("Test "+testno+" "+(result ? "PASS" : "FAIL"));
		if (result) passed++; else failed++;
	}

	static void stats() {
		System.out.println((passed+failed)+" tests, passed "+passed+", failed "+failed);
		try {
			java.io.FileWriter fw = new java.io.FileWriter("testlog",true);
			fw.write(new java.util.Date().toString());
			fw.write("\n");
			fw.write("total "+(passed+failed)+" passed "+passed+" failed "+failed+"\n");
			fw.close();
		} catch (java.io.IOException exc) {}
	}

	static boolean test1(StackCanvas canvas) {
		System.out.println("test 1 (2-mar-2000)");
		// Test: type "notx", split with a space in "not x"
		// and check that no superfluous space has been generated
		// (same as "forallx" in the debug report)
		Formula f;
		Part shouldbe = new OperatorNot(new Identifier("x"));
		canvas.push(f = new Formula("notx"));
		canvas.setActiveFormula(0);
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.keydn(KeydnListener.Key_RIGHT);
		view.keydn(KeydnListener.Key_RIGHT);
		view.keydn(KeydnListener.Key_RIGHT);
		view.keydn(' ');
		Part p = f.getRootPart();
		boolean result;
		if (p.same(shouldbe)) {
			result = true;
		} else {
			p.dump();
			shouldbe.dump();
			result = false;
		}
		canvas.pop();
		return result;
	}

	static boolean test2(StackCanvas canvas) {
		System.out.println("test 2 (28-feb-2000)");
		// 6-dec-2000: not really the same bug as 28-feb-2000 but
		// when typing a space to change "xsubseteq y" into "x subseteq y",
		// the formula is OK but a NullPointerException is thrown in IdentifierView.splitme()
		// and moreover, the cursor part still is the "subseteq" Identifier (which
		// has been replaced by an OperatorSet).
		Formula f;
		Part shouldbe = new OperatorSet("subseteq",new Identifier("x"),new Identifier("y"));
		Identifier critical = new Identifier("xsubseteq");
		canvas.push(f = new Formula(new OperatorSpace(critical,new Identifier("y"))));
		canvas.setActiveFormula(0);
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(critical,1);
		boolean result = true;
		try {
			view.keydn(' ');
		} catch (Exception exc) {
			exc.printStackTrace();
			result = false;
		}
		Part p = f.getRootPart();
		if (!p.same(shouldbe)) {
			p.dump();
			shouldbe.dump();
			result = false;
		}
		canvas.pop();
		return result;
	}

	static boolean test3(StackCanvas canvas) {
		System.out.println("test 3 (6-dec-2000)");
		// type "x y", set cursor at the left of the space, type another
		// space => crash
		Formula f;
		Part shouldbe = new OperatorSpace(new Identifier("x"),new Identifier("y"));
		Part critical = new OperatorSpace(new Identifier("x"),new Identifier("y"));
		canvas.push(f = new Formula(critical));
		canvas.setActiveFormula(0);
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(critical,0);
		boolean result = true;
		try {
			view.keydn(' ');
		} catch (Exception exc) {
			exc.printStackTrace();
			result = false;
		}
		Part p = f.getRootPart();
		if (!p.same(shouldbe)) {
			p.dump();
			shouldbe.dump();
			result = false;
		}
		canvas.pop();
		return result;
	}

	static boolean test4(StackCanvas canvas) {
		System.out.println("test 4 (10-dec-2000)");
		// type "gve*C x" where "*" is the cursor, then type "."
		// Cause: OperatorSpace.recognizeOp() returned always
		// "true" in this case so the split of ".C" was not performed
		// since Identifier.splitme() thought that an identifier was
		// already recognized
		Formula f;
		Part shouldbe = new OperatorSpace(
			new OperatorDot(new Identifier("gve"),new Identifier("C")),
			new Identifier("x"));
		Part critical = new Identifier("gveC");
		canvas.push(f = new Formula(new OperatorSpace(critical,new Identifier("x"))));
		canvas.setActiveFormula(0);
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(critical,3);
		boolean result = true;
		try {
			view.keydn('.');
		} catch (Exception exc) {
			exc.printStackTrace();
			result = false;
		}
		Part p = f.getRootPart();
		if (!p.same(shouldbe)) {
			p.dump();
			shouldbe.dump();
			result = false;
		}
		Part cp = view.getCursorPart();
		// PENDING: cursor should be at pos 0 of "C" identifier
		if (!(cp instanceof Identifier)) {
			System.out.println("Cursor not on OperatorDot");
			result = false;
		} else {
			Identifier cpIdent = (Identifier)cp;
			if (!cpIdent.getString().equals("C")) {
				System.out.println("Cursor not on C but on "+cpIdent.getString());
				result = false;
			}
			//// BUG IS IN InfixBinaryOp:96
			// Before: cursor is at "C", pos 0;
			// After: cursor is at OperatorDot
			int cpos = ((HasCursorPos)view.getCursorComp()).getCursorPos();
			if (cpos != 0) {
				System.out.println("CursorPos is "+cpos+", not 0");
				result = false;
			}
		}
		canvas.pop();
		return result;
	}
	
	static boolean test5(StackCanvas canvas) {
		System.out.println("test 5 (26-jan-2001)");
		// move cursor with cursor keys over Uneditable part
		// => null pointer exception
		// at gve.calc.formula.UneditableView.setCursorPos(UneditableView.java:18)
		// Cause: the UneditableView probably has been replaced
		// by another component by the time that setCursorPos() is
		// called, so its parent is null.
		// Fix: replaced "FormulaView.get(this).setCursorComp(null);"
		// with "return;".
		Formula f;
//		canvas.newObject("gve.calc.formula.Stack");
		Stack stack = new Stack();
		canvas.push(f = new Formula(stack));
		boolean result = true;
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(stack.elementAt(0));
		try {
			view.keydn(KeydnListener.Key_LEFT);
		} catch (NullPointerException exc) {
			exc.printStackTrace();
			result = false;
		}
		canvas.pop();
		return result;
	}

	static boolean test6(StackCanvas canvas) {
		// Type "a"; extend to "b,a" => result is "b ,a" where "b" and ",a" are two Identifiers!
		System.out.println("test 6 (6-feb-2001)");
		boolean result = true;
		Identifier ident = new Identifier("a");
		Formula f;
		canvas.push(f = new Formula(ident));
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(ident,HasCursorPos.Somewhere_LEFT);
		view.keydn('b');
		view.keydn(',');
		Part p = f.getRootPart();
		Part shouldbe = new OperatorComma(new Identifier("b"),new Identifier("a"));
		if (!p.same(shouldbe)) {
			p.dump();
			shouldbe.dump();
			result = false;
		}
		canvas.pop();
		return result;
	}

	static boolean test7(StackCanvas canvas) {
		// Type "a,b" and delete the comma
		System.out.println("test 7 (15-feb-2001)");
		OperatorComma comma = new OperatorComma(new Identifier("a"),new Identifier("b"));
		Formula f;
		canvas.push(f = new Formula(comma));
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(comma,HasCursorPos.Somewhere_MYRIGHT);
		view.keydn(KeydnListener.Key_BS);
		Part shouldbe = new Identifier("ab");
		Part root = f.getRootPart();
		boolean result = true;
		if (!root.same(shouldbe)) {
			root.dump();
			shouldbe.dump();
			result = false;		
		}
		canvas.pop();
		return result;
	}

	static boolean test8(StackCanvas canvas) {
		// Type "nomt x" and repair to "not x"
		System.out.println("test 8 (16-apr-2001)");

		Identifier nomt,iks;
		Part test = new OperatorSpace(nomt = new Identifier("nomt"),iks = new Identifier("x"));
		Formula f;
		canvas.push(f = new Formula(test));
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(nomt,3);
		view.keydn(KeydnListener.Key_BS);
		view.keydn(KeydnListener.Key_RIGHT);
		view.keydn(KeydnListener.Key_RIGHT);
		Part shouldbe = new OperatorNot(new Identifier("x"));
		Part root = f.getRootPart();
		boolean result = true;
		if (!root.same(shouldbe)) {
			root.dump();
			shouldbe.dump();
			result = false;		
		}
		Part cp = view.getCursorPart();
		if (cp != root  &&  cp != iks) {
			System.out.println("bad cursor part "+view.getCursorPart());
			result = false;
		}
		canvas.pop();
		return result;
	}

	static boolean test9(StackCanvas canvas) {
		// Type "not x" and change into "nomt x"
		System.out.println("test 9 (16-apr-2001)");

		Identifier nomt,iks;
		Part test = new OperatorNot(new Identifier("x"));
		Formula f;
		canvas.push(f = new Formula(test));
		FormulaView view = (FormulaView)canvas.getComponent(0);
		view.setCursorPart(test,2);
		view.keydn('m');
		Part shouldbe = new OperatorSpace(new Identifier("nomt"),new Identifier("x"));
		Part root = f.getRootPart();
		boolean result = true;
		if (!root.same(shouldbe)) {
			root.dump();
			shouldbe.dump();
			result = false;		
		}
		canvas.pop();
		return result;
	}

	static boolean testProof(StackCanvas canvas,String name) {
		return testProof(canvas,name,-1);
	}

	
 uptoline: e.g. 0 tests only first line, 1 only first two, etc
	static boolean testProof(StackCanvas canvas,String name,int uptoline) {
		System.out.println("Proof "+name);
		Proof proof = (Proof)canvas.load(name);
		int lines = proof.getHeight();
		boolean shouldfail = false;
		boolean ignore = false;
		boolean result = true;
		for (int lineno = 0; lineno < lines; lineno++) {
			if (proof.isComment(lineno)) {
				String comment = ((StringPart)proof.elementAt(lineno,Proof.SEQUENT)).getString();
				if (comment.equals("should fail")) shouldfail = true;
				if (comment.equals("pending")) ignore = true;
				continue;
			}
			try {
				proof.vfyline(lineno,(VariableStore)canvas);
				if (shouldfail) {
					System.out.println("line "+(lineno+1)+" should fail");
					result = false;
				}
			} catch (ProofInvalidException exc) {
				if (!shouldfail && !ignore) {
					System.out.println("oops at line "+(lineno+1)+exc);
					result = false;
				}
			}
			shouldfail = false; ignore = false;
			if (lineno == uptoline) break;
		}
		print(-1,result);
		return result;
	}
}