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

import awt.*;
import java.awt.*;
import java.util.Vector;
import java.util.Enumeration;
import gve.calc.formula.*;
import gve.calc.formula.Boolean;

public class Proof extends Tabular {
	
 Worden verondersteld iets van de vorm `a |- b' te bevatten 
	private Part sequent[];
	
 Worden verondersteld iets van de vorm `A', `C1(1)' of `R(3,4)' te bevatten 
	private Part because[];
	private byte linestatus[];	// PENDING: move this out of the Model and into the ProofView

	static final byte DUNNO = 0;
	static final byte OKAY = 1;
	static final byte BAD = 2;

	public static final int SEQUENT=0;
	public static final int BECAUSE=1;

	public Proof(Part firstSequent) {
		sequent = new Part[1]; sequent[0] = firstSequent; firstSequent.setParent(this);
		because = new Part[1]; because[0] = new Identifier(""); because[0].setParent(this);
		linestatus = new byte[1];
	}

	
 Only used by read() and clone() 
	private Proof() {}

	public Object clone() {
		Proof result = new Proof();
		result.sequent = new Part[sequent.length];
		result.because = new Part[because.length];
		result.linestatus = new byte[linestatus.length];
		for (int i = sequent.length-1; i>=0; i--) {
			result.sequent[i] = (Part)sequent[i].clone();
			result.sequent[i].setParent(result);
			result.because[i] = (Part)because[i].clone();
			result.because[i].setParent(result);
		}
		System.arraycopy(linestatus,0,result.linestatus,0,linestatus.length);
		return result;
	}

	public int getHeight() { return sequent.length; }
	public int getWidth() { return 2; }

	public void setLineStatus(int line,byte status) {
		if (isComment(line)) status = DUNNO;	// Comments are not marked in any way
		linestatus[line] = status;
		MVC.changed(this,new RepaintRequest(new Integer(line)));
	}

	public byte getLineStatus(int line) { return linestatus[line]; }

	public Part elementAt(int i,int j) {
		switch(j) {
		case SEQUENT: return sequent[i];
		case BECAUSE: return because[i];
		default: throw new ArrayIndexOutOfBoundsException("invalid column "+j);
		}
	}

	public void setElementAt(int i,int j,Part el) {
		switch(j) {
		case SEQUENT: sequent[i] = el; el.setParent(this); break;
		case BECAUSE: because[i] = el; el.setParent(this); break;
		}
	}

	public void removeRow(int pos) {
		sequent = removeRow(sequent,pos);
		because = removeRow(because,pos);
		for (int i = 0; i < because.length; i++) {
			// verwijzingen naar regelnummers die veranderen aanpassen
			Part cause = because[i];
			while (cause instanceof OperatorSpace) {
				OperatorSpace spat = (OperatorSpace)cause;
				cause = spat.right;
			}
			if (cause instanceof Brackets) {
				Brackets brack = (Brackets)cause;
				CommaEnumerator prems = new CommaEnumerator(brack.getChild());
				while (prems.hasMoreElements()) {
					Part lijnnr = prems.nextPart();
					if (!(lijnnr instanceof Identifier)) continue;
					Identifier lijnident = (Identifier)lijnnr;
					int lijn = Integer.parseInt(lijnident.getString());
					if (lijn > pos) lijnident.setString(""+(lijn - 1));
				}
			}
		}
		byte [] newstatus = new byte[sequent.length];
		for (int i = pos-1; i>=0; i--) newstatus[i] = linestatus[i];
		for (int i = linestatus.length-1; i>pos; i--) newstatus[i-1] = linestatus[i];
		linestatus = newstatus;
		super.removeRow(pos);
	}

	public void insertRow(int pos) {
		sequent = insertRow(sequent,pos);
		because = insertRow(because,pos);
		// Adjust line number references
		for (int i = 0; i < because.length; i++) {
			Part cause = because[i];
			while (cause instanceof OperatorSpace) {
				OperatorSpace spat = (OperatorSpace)cause;
				cause = spat.right;
			}
			if (cause instanceof Brackets) {
				Brackets brack = (Brackets)cause;
				CommaEnumerator prems = new CommaEnumerator(brack.getChild());
				while (prems.hasMoreElements()) {
					Part lijnnr = prems.nextPart();
					if (!(lijnnr instanceof Identifier)) continue;
					Identifier lijnident = (Identifier)lijnnr;
					int lijn = Integer.parseInt(lijnident.getString());
					if (lijn > pos) lijnident.setString(""+(lijn + 1));
				}
			}
		}
		byte [] newstatus = new byte[sequent.length];
		for (int i = pos-1; i>=0; i--) newstatus[i] = linestatus[i];
		for (int i = linestatus.length-1; i>=pos; i--) newstatus[i+1] = linestatus[i];
		linestatus = newstatus;
		super.insertRow(pos);
	}

	public boolean isComment(int lineno) {
		if (!isEmpty(because[lineno])) return false;
		if (sequent[lineno] instanceof StringPart) return true;
		return false;
	}

	
 Returns null if all symbols inside p have a type. Else returns a symbol that has no type 
	private String checktypes(Part p,Matcher m) {
		if (Part.isEmpty(p)) return null;
		if (p instanceof Identifier) {
			String str = ((Identifier)p).getString();
			if (m.isFunction(str)) return null;
			if (m.getTomatchType(str) != null) return null;
			try { new Double(str); } catch (NumberFormatException exc) { return str; }
			return null;
		}
		int i = 0;
		while (true) {
			Part child = p.getChild(i++);
			if (child == null) return null;
			String check = checktypes(child,m);
			if (check != null) return check;
		}
	}

	
 Throws a ProofInvalidException when the proof line is bad.
	  When the proof line is ok, matched symbols are addded to the VariableStore. 
	public void vfyline(int lineno,VariableStore store) throws ProofInvalidException {
		if (isEmpty(because[lineno])) {	// Blank line, or declaration
			if (isEmpty(sequent[lineno])) return;	// blank line
			if (sequent[lineno] instanceof OperatorSpace) {	// declaration
				OperatorSpace spat = (OperatorSpace)sequent[lineno];
				if (!(spat.right instanceof Identifier))
					throw new ProofInvalidException("Invalid variable name in declaration");
				if (!(spat.left instanceof Identifier))
					throw new ProofInvalidException("Invalid type in declaration");
				String typ = ((Identifier)spat.left).getString();
				if (typ.equals("List") || typ.equals("Var") || typ.equals("Term") || typ.equals("Pred") || typ.equals("Formula") || typ.equals("Const"))
					return;
				throw new ProofInvalidException("Unknown type `"+typ+"' in declaration");
			}
			if (isComment(lineno)) return;
			if (sequent[lineno] instanceof OperatorModel)
				throw new ProofInvalidException("No rule given to explain this line");
			throw new ProofInvalidException("Invalid line");
		}
		if (because[lineno] instanceof Identifier) {
			String cause = ((Identifier)because[lineno]).getString();
			if (cause.equals("prem")) return;
			if (cause.equals("arg")) return;
		}
		// Welke regel beweert deze lijn te gebruiken?
		String rulename;
		int [] premissen = null;	// bevat regelnummers
		int paramcount = 0;	// aantal opgegeven parameters
		if (because[lineno] instanceof OperatorSpace) {
			OperatorSpace spat = (OperatorSpace)because[lineno];
			if (spat.left instanceof Identifier) {
				rulename = ((Identifier)spat.left).getString();
				// Eventueel parameters
				while (spat.right instanceof OperatorSpace) {
					spat = (OperatorSpace)spat.right;
					paramcount++;
				}
				// Lijst regelnummers premissen opstellen
				if (spat.right instanceof Brackets) {
					Brackets brack = (Brackets)spat.right;
					CommaEnumerator prems = new CommaEnumerator(brack.getChild());
					Vector premvector = new Vector();
					while (prems.hasMoreElements()) {
						Part lijnnr = prems.nextPart();
						if (!(lijnnr instanceof Identifier)) continue;
						premvector.addElement(((Identifier)lijnnr).getString());
						int nr = Integer.parseInt(((Identifier)lijnnr).getString());
						if (nr < 1) throw new ProofInvalidException(
							lijnnr,"Regelnummer kleiner dan 1");
						if (nr > lineno) throw new ProofInvalidException(
							lijnnr,"Lijn gebruikt een verdere lijn");
						if (nr > because.length) throw new ProofInvalidException(
							lijnnr,"Lijn bestaat niet");
					}
					premissen = new int[premvector.size()];
					for (int i = premvector.size()-1; i>=0; i--) {
						// premissen[] bevat interne regelnummers (begint vanaf 0)
						premissen[i] = Integer.parseInt((String)premvector.elementAt(i)) - 1;
						if (debuglevel>=10) System.out.println("---premisse "+premissen[i]);
					}
				} else if (spat.right instanceof Identifier) {
					// Rule without premisses but with arguments (so the "because"
					// column reads "rulename arg")
					paramcount++;
				}
			} else
				throw new ProofInvalidException("Invalid justification syntax");
		} else if (because[lineno] instanceof Identifier) {
			rulename = ((Identifier)because[lineno]).getString();
		} else throw new ProofInvalidException("Invalid justification syntax");
		// Opzoeken in rules
		Proof rule;
		{	Part p = store.load(rulename);
			if (p == null) throw new ProofInvalidException("Object "+rulename+" does not exist");
			if (p instanceof Proof) rule = (Proof)p;
			else throw new ProofInvalidException("No proof in "+rulename);
		}
		if (rule == null) throw new ProofInvalidException("There is no "+rulename+" rule");
		rule = (Proof)rule.clone();
		// Controleren of de lijn voldoet aan de regel
		if (debuglevel>=10) System.out.println("Checking");
		Matcher matcher = new Matcher();
		StandardFunctions.registerFunctions(matcher.getEvaluator());
		// types bepalen van alle symbolen uit de bewijsregel
		for (int i = rule.getHeight()-1; i>=0; i--) {
			{	Part cause = rule.elementAt(i,BECAUSE);
				if (!(cause instanceof Identifier)) continue;
				String causestr = ((Identifier)cause).getString();
				if (! (causestr.equals("") || causestr.equals("arg")) ) continue;
			}
			Part seq = rule.elementAt(i,SEQUENT);
			if (!(seq instanceof OperatorSpace)) continue;
			OperatorSpace declar = (OperatorSpace)seq;
			if (!(declar.right instanceof Identifier)) continue;
			Identifier varname = (Identifier)declar.right;
			matcher.setPatternType(varname.getString(),declar.left);
		}
		// types bepalen van alle symbolen uit het bewijs
		for (int i = 0; i < lineno; i++) {
			if (!Part.isEmpty(because[i])) {
				// Only empty or "arg" in the right column indicates a variable
				if (!(because[i] instanceof Identifier)) continue;
				String cause = ((Identifier)because[i]).getString();
				if (!(cause.equals("arg"))) continue;
			}
			Part seq = sequent[i];
			if (!(seq instanceof OperatorSpace)) continue;
			OperatorSpace declar = (OperatorSpace)seq;
			if (!(declar.right instanceof Identifier)) continue;
			Identifier varname = (Identifier)declar.right;
//System.out.println(varname.getString()); declar.left.dump();
			matcher.setTomatchType(varname.getString(),declar.left);			
		}
		// Controleer of alle symbolen een type hebben
		{	String bad = checktypes(sequent[lineno],matcher);
			if (bad != null) throw new ProofInvalidException("Symbol "+bad+" has no type");
		}
		// Match parameters van de bewijsregel (bv de t en x uit "S t x")
		{
			// Implementation: "arg" in "because" column
			int ruleline = -1;	// search in rule for "arg" lines
			Part paramvalues = null;
			if (paramcount > 0) paramvalues = because[lineno];
			for (int matchparam=0; matchparam<paramcount; matchparam++) {
				paramvalues = ((OperatorSpace)paramvalues).right;
				// search next "arg" line
				while (true) {
					ruleline++;
					if (ruleline >= rule.getHeight())
						throw new ProofInvalidException("Too many arguments given");
					Part p = rule.elementAt(ruleline,BECAUSE);
					if (p instanceof Identifier && ((Identifier)p).getString().equals("arg"))
						break;
				}
				// found "arg" line at line "ruleline"
				Part declaration = rule.elementAt(ruleline,SEQUENT);
				if (!(declaration instanceof OperatorSpace))
					throw new ProofInvalidException("Line "+(ruleline+1)+" of "+rulename+" is not a symbol declaration");
				if (!(((OperatorSpace)declaration).right instanceof Identifier))
					throw new ProofInvalidException("Line "+(ruleline+1)+" of "+rulename+" is not a declaration");
				Identifier symbol = (Identifier)((OperatorSpace)declaration).right;
				Part argval;
				if (paramvalues instanceof OperatorSpace) argval = ((OperatorSpace)paramvalues).left;
				else argval = paramvalues;
				boolean success = matcher.match(argval,symbol);
				if (!success)
					throw new ProofInvalidException("Cannot match arg "+symbol.getString());
				matcher.setMatchedValue(symbol.getString(),Brackets.unbracket(argval));
			}
			// Check if we have enough parameters for the proof
			while (true) {
				ruleline++;
				if (ruleline >= rule.getHeight()) break;	// Okay, we got them all
				Part p = rule.elementAt(ruleline,BECAUSE);
				if (p instanceof Identifier && ((Identifier)p).getString().equals("arg"))
					throw new ProofInvalidException("Not enough arguments supplied");
			}
		}
		// PENDING: conclusie van rule beter bepalen (gebruikt nu gewoon laatste regel)
		// Quick partial match
		if (!matcher.qmatch(sequent[lineno],rule.elementAt(rule.getHeight()-1,SEQUENT)))
			throw new ProofInvalidException("Cannot match conclusions");
		// PENDING: quick match of the premisses
		//	(is this possible??? Possibly only when there's only one premisse?)

		// Full match
		ProofLinesMatched plm = new ProofLinesMatched(matcher,this,premissen,rule,
			new LineMatched(sequent[lineno],rule.elementAt(rule.getHeight()-1,SEQUENT)));
		boolean success = plm.match();
		if (!success)
			throw new ProofInvalidException(plm.status,"Cannot match");
	}

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

	public static Part read(java.io.BufferedReader r) throws java.io.IOException,
			ClassNotFoundException,NoSuchMethodException,
			java.lang.reflect.InvocationTargetException,IllegalAccessException {
if (debuglevel>=10) System.out.println("Reading");
		int height = Integer.parseInt(r.readLine());
		Proof result = new Proof();
		result.sequent = new Part[height];
		result.because = new Part[height];
		result.linestatus = new byte[height];
		// Backward compatibility stuff: ignore Uneditables, since now we don't
		// store line number labels any more. Historical note: very old versions used
		// Identifiers, not Uneditables, to store the line numbers; these files we cannot
		// read any more with this version. The change between these obsolete formats
		// took place sometween march and july 2000.
		int width = result.getWidth();
		for (int i = 0; i < height; i++) {
			for (int j = 0; j < width; j++) {
				Part p = Part.read(r);
//System.out.println(i+","+j+"\t"+p);
				if (p instanceof Uneditable) {	// Ignore Uneditables
					j--;
					continue;
				}
				result.setElementAt(i,j,p);
			}
		}
		// The next line is what we really mean
		// Remove compat stuff and restore this line in the future.
		// result.readTable(r);
		return result;
	}

	public void modified(Part child) {
//System.out.println("modified "+child);
		Point p = whichOffspring(child);
		if (p == null) return;
		// If a line is modified, remove red or green rectangle
		setLineStatus(p.y,DUNNO);
	}

	public Component createView(FormulaView view) {
		return new ProofView(this,view);
	}

	public void saveLatex(java.io.BufferedWriter w) throws java.io.IOException {
		w.write("\\begin{array}{lrcll}");
		w.newLine();
		int h = getHeight();
		for (int i = 0; i < h; i++) {
			w.write((i+1)+"&");
			Part seq = elementAt(i,0);	// sequent
			if (seq instanceof OperatorModel) {
				OperatorModel model = (OperatorModel)seq;
				model.left.saveLatex(w);
				w.write("&");
				model.saveOperatorLatex(w);
				w.write("&");
				model.right.saveLatex(w);
			} else {
				w.write("\\multicolumn{3}{c}{");
				seq.saveLatex(w);
				w.write("}");
			}
			w.write("&");
			elementAt(i,1).saveLatex(w);
			w.write("\\\\");
			w.newLine();
		}
		w.write("\\end{array}");
		w.newLine();
	}
}

class LineMatched implements Matched {
	private Part tomatch,pattern;
	
	public LineMatched(Part tomatch,Part pattern) {
		this.tomatch = tomatch;
		this.pattern = pattern;
	}

	public boolean foundMatch(Matcher m) {
		return m.match(tomatch,pattern);
	}
}

 PENDING: backtrace ??? 
class ProofLinesMatched implements Matched {
	private Matcher matcher;
	private Proof proof,rule;
	private int [] prems;
	private Matched matched;
	/* no of next line of the rule to check */
	private int linecount = 0;
	public ProofSuccess status = new ProofSuccess();

	
 match lines of the proof proof with
	  lines having numbers in prem[] of rule
	  marked with "prem"
	  For each match of all those, call m.foundMatch().
	 
	public ProofLinesMatched(Matcher matcher,Proof proof,int []prem,Proof rule,Matched m) {
		this.matcher = matcher;
		this.proof = proof;
		this.prems = prem;
		this.rule = rule;
		matched = m;
	}

	public boolean match() {
		return foundMatch(matcher);
	}

	/* Check if matched doesn't contain identifiers
	 * of type List or Term */
	private boolean checkForLists(Part matched,Matcher m) {
		if (matched instanceof Identifier) {
			Part typ = m.getTomatchType(((Identifier)matched).getString());
			if (typ instanceof Identifier) {
				String typstr = ((Identifier)typ).getString();
				if (typstr.equals("List")) return false;
				if (typstr.equals("Term")) return false;
			}
		}
		int count = 0;
		while (true) {
			Part child = matched.getChild(count);
			if (child == null) return true;	// done
			if (!checkForLists(child,m)) return false;
			count++;
		}
	}

	
 Creates an Evaluator where symbols of the proof are defined
	  This is important for functions acting on unknowns.
	  E.g., suppose we have to match a line of the rule "Ltx = subst(t,x,L)"
	  and L matches to "L1,x=t" where L1 is an unknown List.
	  Then "subst(t,x,L)" becomes "subst(t,x,(L1,x=t))" which must *not* be
	  evaluated as "{L1,t=t}" but as "subst(t,x,L1) union {t=t} 
	private Evaluator makeEvaluator(Matcher m) {
		Evaluator eval = new MultiEvaluator();
		StandardFunctions.registerFunctions(eval);
		Enumeration enum = m.tomatchSymbols();
		while (enum.hasMoreElements()) {
			String symbol = (String)enum.nextElement();
			// Define symbol with itself as value
			// PENDING: define it as "unknown variable of type t"?
			eval.defineVariable(symbol,new Identifier(symbol));
System.out.println("defining "+symbol);
		}
		return eval;
	}

	
 Returns true if all identifiers in pattern are matched
	  to a value *and* those values are not of type List
	  This code is heavily inspired on Matcher.isKnown() 
	private boolean isFullyKnown(Part pattern,Matcher m) {
		if (pattern instanceof Identifier) {
			String patstr = ((Identifier)pattern).getString();
			Part val = m.getMatchedValue(patstr);
			if (val == null) return false;
			Part typ = m.getPatternType(patstr);
			// Note: if the rule has a "List L", and "L" is somewhere inside pattern,
			// check the type of the *thing L is matched to*. It's equally possible
			// that L is matched to a term, in which case we should return true!
			if (typ instanceof Identifier) {
				String typstr = ((Identifier)typ).getString();
				if (typstr.equals("List")) {
					// Check type of the thing this List is matched to, since it's
					// equally possible that L is matched to a few terms, in which case we
					// should return true!
					return checkForLists(val,m);
				}
			}
			return true;
		}
		if (pattern instanceof OperatorSpace) {
			// Maybe it's a known function
			OperatorSpace spat = (OperatorSpace)pattern;
			if (spat.left instanceof Identifier) {
				Identifier fnam = (Identifier)spat.left;
				if (m.isFunction(fnam.getString()))
					return isFullyKnown(spat.right,m);
			}
		}
		int count = 0;
		while (true) {
			Part child = pattern.getChild(count);
			if (child == null) return true;	// done
			if (!isFullyKnown(child,m)) return false;
			count++;
		}
	}

	private boolean matchPrem(Part pattern,Matcher m) {
		if (pattern instanceof OperatorModel &&
			((OperatorModel)pattern).getKind()==OperatorModel.ASSERTION) {
			if (prems == null) return false;
			for (int i = prems.length-1; i>=0; i--) {
				linecount++;
				Matcher fallback = m;
				m = new FallbackMatcher(m);
				boolean success = m.match(proof.elementAt(prems[i],Proof.SEQUENT),pattern,this);
				m = fallback;
				linecount--;
				if (success)	// recursive match succeeded
					return true;
				// if recursive match didn't succeed, try the other "prem"-marked lines ...
			}
			return false;
		}
		// A premisse can also be something like "not(x=y)"
		// In this case, we replace the symbols by their values and evaluate.
		// Used in a.o. the "VarVar" and "SubL1" rules
//System.out.println("Proof: matchPrem()");
//pattern.dump();
		if (m.isKnown(pattern)) {
			// Check a condition, e.g. "not(x in freevar(L) )"
/*			if (!isFullyKnown(pattern,m)) {
				// If L is matched to a "List M", then we cannot
				// decide this by evaluate()ing, but we have to match
				// the formula just like a regular premisse
				// PENDING: regression test: load "Gx" rule, change last line (5,6) -> (5)  => should fail
				for (int i = prems.length-1; i>=0; i--) {
					linecount++;
					Matcher fallback = m;
					m = new FallbackMatcher(m);
					boolean success = m.match(proof.elementAt(prems[i],Proof.SEQUENT),pattern,this);
					m = fallback;
					linecount--;
System.out.println("matched "+success+" with "); proof.elementAt(prems[i],Proof.SEQUENT).dump();
					if (success)	// recursive match succeeded
						return true;
					// if recursive match didn't succeed, try the other "prem"-marked lines ...
				}
				return false;
			}*/
			// Check if it evaluates to true
			Evaluator eval = new MultiEvaluator();
			StandardFunctions.registerFunctions(eval);
			Part value = m.fillinSymbols(pattern).evaluate(eval);
//System.out.println("Evaluated to "+value);
			if (value instanceof Boolean && ((Boolean)value).getBooleanValue()) {
				linecount++;
				boolean success = foundMatch(m);
				linecount--;
				return success;
			}
			return false;
		}
		return false;
	}

	private boolean matchEq(OperatorEquality eq,Matcher m) {
		if (!(eq.getName().equals("="))) return false;
		// Match an expression of type X=bla
		// where X is an unmacthed symbol and bla a fully matched expression
		if (eq.left instanceof Identifier) {
			Identifier varname = (Identifier)eq.left;
System.out.println("Proof: matchEq");
			if (m.getMatchedValue(varname.getString())==null && m.isKnown(eq.right)) {
				if(isFullyKnown(eq.right,m)) {
					Evaluator eval = new MultiEvaluator();
					StandardFunctions.registerFunctions(eval);
					Part value = m.fillinSymbols(eq.right).evaluate(eval);
					m.setMatchedValue(varname.getString(),value);
					linecount++;
					boolean result = foundMatch(m);
					linecount--;
					// PENDING: backtrack: restore old matched value
					return result;
				}
				// e.g. matchEq('Ltx = subst(t,x,L)',...)
				// where L matches "L1,x=x" and L1 is a List ...
				if (eq.right instanceof OperatorSpace) {
					// PENDING: the better solution is to build in type information
					// in Evaluator objects (so they become Matchers in fact?)
					// and then let the freevar() routine act accordingly on Lists
					System.out.println("not fully known, evaluates to: ");
					m.fillinSymbols(eq.right).evaluate(makeEvaluator(m)).dump();
					
				}
				return false;
			}
		}
		return false;
	}

	public boolean foundMatch(Matcher m) {
		// Try to match next line of proof rule marked with "prem" with one of the
		// selected rules of the proof
		int found = 0;
//System.out.println("Trying to match line "+linecount);
//m.dump();
		// Search next line to process; when found, process it and recurse
		for (; ; linecount++) {
			status.record(linecount-1,m);
			if (linecount >= rule.getHeight()) // We're done!
				return matched.foundMatch(m);
			Part because = rule.elementAt(linecount,Proof.BECAUSE);
			if (!(because instanceof Identifier)) continue;
			String cause = ((Identifier)because).getString();
			if (cause.equals("prem")) {
				return matchPrem(rule.elementAt(linecount,Proof.SEQUENT),m);
//			} else if (cause.equals("arg")) {
//				;	// arg has already been pre-matched, do nothing (same as plain declarations)
			} else if (cause.equals("")) {
				// A declaration, comment or an assignment
				Part sequent = rule.elementAt(linecount,Proof.SEQUENT);
				if (sequent instanceof OperatorSpace) continue;	// declaration
				if (sequent instanceof StringPart) continue;	// comment
System.out.println("Proof: foundMatch()");
/*				if (m.isKnown(sequent)) {
					// Check a condition, e.g. "not( {x} in freevar(L) )"
					// PENDING: if L is matched to a "List M", then we cannot
					// decide this by evaluate()ing, but we have to match
					// the formula just like a regular premisse!
					Evaluator eval = new MultiEvaluator();
					StandardFunctions.registerFunctions(eval);
					Part value = m.fillinSymbols(sequent).evaluate(eval);
					if (value instanceof Boolean && ((Boolean)value).getBooleanValue()) {
						// Happens e.g. when the quick pre-match already matched
						// "atx" in something like "atx = subst(t,x,a)"
						linecount++;
						boolean result = foundMatch(m);
						linecount--;
						return result;
					}
					return false;
				} else if (sequent instanceof OperatorEquality) {
					return matchEq((OperatorEquality)sequent,m);
				} else*/ return false;	// Don't understand this line---PENDING: throw exception
			}
		}
	}
}