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

import java.util.Hashtable;
import java.util.Enumeration;
import gve.calc.formula.*;

//PENDING: should do Brackets.unbracket() at strategic places

 A Matcher is a repository for symbol values and types.
  Using this information, it can match expressions to patterns. 
public class Matcher {
	
 symbols to match -> matched value 
	private Evaluator matches = new SingleEvaluator();

	
 keys: symbol (String); values: type of this symbol (Part)
	  patternTypes contains symbol types of the pattern;
	  tomatchTypes contains symbol types of the part tree to match. 
	private Hashtable patternTypes = new Hashtable();
	private Hashtable tomatchTypes = new Hashtable();

	public Matcher() {}

	
 Creates a deep optimized copy of m.
	  Deep: later changes on m do not affect the new Matcher
	  Optimized: if m is a recursive matcher (e.g. a FallbackMatcher),
	  the new Matcher is flattened
	  Caveat emptor: type info of undefined symbols is *not* preserved in the new Matcher.
	  Pattern types are also lost. 
	public Matcher(Matcher m) {
		Enumeration enum;
/*		enum = m.tomatchSymbols();
		while (enum.hasMoreElements()) {
			String symbol = (String)enum.nextElement();
			Part val = m.getMatchedValue(symbol);
			if (val != null) setMatchedValue(symbol,val);
			Part ttype = m.getTomatchType(symbol);
			if (ttype != null) setTomatchType(symbol,ttype);
		}*/
		// PENDING: copy type info also
//System.out.println("---matcher");
		enum = m.matchedSymbols();
		while (enum.hasMoreElements()) {
			String symbol = (String)enum.nextElement();
			Part val = m.getMatchedValue(symbol);
			if (val != null) setMatchedValue(symbol,val);
//System.out.println(symbol);
//val.dump();
		}
	}

	public Evaluator getEvaluator() { return matches; }

	public Object clone() {
		Matcher result = new Matcher();
		result.matches = (SingleEvaluator)matches.clone();
		result.patternTypes = (Hashtable)patternTypes.clone();
		result.tomatchTypes = (Hashtable)tomatchTypes.clone();
		return result;
	}

	public void setPatternType(String symbol,Part typ) { patternTypes.put(symbol,typ); }
	public void setTomatchType(String symbol,Part typ) { tomatchTypes.put(symbol,typ); }

	public Part getPatternType(String symbol) { return (Part)patternTypes.get(symbol); }
	public Part getPatternType(Identifier symbol) { return (Part)patternTypes.get(symbol.getString()); }
	public Part getTomatchType(String symbol) { return (Part)tomatchTypes.get(symbol); }
	public Part getTomatchType(Identifier symbol) { return (Part)tomatchTypes.get(symbol.getString()); }

	public Part getMatchedValue(String symbol) { return matches.getValue(symbol); }
	public void setMatchedValue(String symbol,Part value) {
		matches.defineVariable(symbol,value);
	}
	public void undefineMatch(String symbol) { matches.undefVariable(symbol); }

	public Enumeration tomatchSymbols() { return tomatchTypes.keys(); }
	public Enumeration matchedSymbols() { return matches.variables(); }

	protected boolean isFunction(String fname) { return matches.isFunction(fname); }

	// From here on, use of matches, patternTypes and tomatchTypes directly is forbidden
	// (use the member functions)

	
 Checks if tomatch matches the pattern 
	public boolean match(Part tomatch,Part pattern) {
		return matchImpl(tomatch,pattern,new AlwaysTrue());
	}

	
 Returns true if all identifiers in pattern are matched to a value. 
	public boolean isKnown(Part pattern) {
		if (pattern instanceof Identifier) {
			Part val = getMatchedValue(((Identifier)pattern).getString());
			if (val == null) return false;
			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 (isFunction(fnam.getString()))
					return isKnown(spat.right);
			}
		}
		int count = 0;
		while (true) {
			Part child = pattern.getChild(count);
			if (child == null) return true;	// done
			if (!isKnown(child)) return false;	// child contains unmatched identifier
			count++;
		}
	}

	
 Takes a pattern; returns a copy of the pattern where all symbols
	  are replaced with their values. 
	public Part fillinSymbols(Part pattern) {
		if (pattern instanceof Identifier) {
			Part val = getMatchedValue(((Identifier)pattern).getString());
			if (val != null) return (Part)val.clone();
			else return (Part)pattern.clone();
		} else {
			Part result = (Part)pattern.clone();
			replaceSymbols(result);
			return result;
		}
	}

	private void replaceSymbols(Part p) {
		int i = 0;
		while (true) {
			Part child = p.getChild(i++);
			if (child == null) return;
			if (child instanceof Identifier) {
				Part val = getMatchedValue(((Identifier)child).getString());
				if (val != null) {
					p.replaceChild(child,(Part)val.clone());
				}
			} else {
				replaceSymbols(child);
			}
		}
	}

	
 E.g.: match ("x,y,z|-y","L |- a")
	  Calls action.foundMatch() for each match found, until
	  action.foundMatch() returns true (and then the result of match() is also true).
	  When no match is found, or on each match action.foundMatch() returned false,
	  the result of foundMatch() is false.
	  When this method returns, no variable values are modified. 
	public boolean match(Part tomatch,Part pattern,Matched action) {
	 	if (action == null) action = new AlwaysTrue();
		return matchImpl(tomatch,pattern,action);
	}

	
 This method assumes that action!=null 
	private boolean matchImpl(Part tomatch,Part pattern,Matched action) {
//System.out.println("***match tomatch"); tomatch.dump();
//System.out.println("***match pattern"); pattern.dump();
		tomatch = Brackets.unbracket(tomatch);
		pattern = Brackets.unbracket(pattern);
		if (pattern instanceof Identifier) {	// Match one symbol to tomatch
			if (Part.isEmpty(pattern) && Part.isEmpty(tomatch))
				return action.foundMatch(this);
			Part typ = getPatternType((Identifier)pattern);
			String symbolname = ((Identifier)pattern).getString();
			if (typ == null) {
				// e.g. match "freevar(x)" to "freevar(x)"
				// => match "freevar" to "freevar"; this symbol has of course no type
				// but still must return a successful match
				if (isFunction(symbolname)) {
					if (tomatch instanceof Identifier && ((Identifier)tomatch).getString().equals(symbolname))
						return action.foundMatch(this);
					return false;
				}
			}
			{	Part val = getMatchedValue(symbolname);
				if (val != null) {	// Match known symbol
					if (val.same(tomatch)) {
						return action.foundMatch(this);
					}
					return false;
				}
			}
			if (!(typ instanceof Identifier))	// We don't handle compound types yet
				return false;
			// Try to match a currently unmatched symbol
			String typename = ((Identifier)typ).getString();
			if (typename.equals("List")) {
				setMatchedValue(symbolname,tomatch);
				boolean result = action.foundMatch(this);
				undefineMatch(symbolname);
				return result;
			} else if (typename.equals("Term") || typename.equals("Formula")) {
				if (tomatch instanceof OperatorComma) return false;
				// if tomatch is a single identifier, check if its type is not List
				if (tomatch instanceof Identifier) {
					Part tmTyp = getTomatchType((Identifier)tomatch);
					if (tmTyp instanceof Identifier) {
						String tmt = ((Identifier)tmTyp).getString();
						if (tmt.equals("List")) return false;
					}
				}
				setMatchedValue(symbolname,tomatch);
				boolean result = action.foundMatch(this);
				undefineMatch(symbolname);
				return result;
			} else if (typename.equals("Var")) {
				if (tomatch instanceof Identifier) {
					Part tmTyp = getTomatchType((Identifier)tomatch);
					if (tmTyp instanceof Identifier) {
						String tmt = ((Identifier)tmTyp).getString();
						if (!(tmt.equals("Var"))) return false;
					}
					setMatchedValue(symbolname,tomatch);
					boolean result = action.foundMatch(this);
					undefineMatch(symbolname);
					return result;
				} else return false;	
			}
			return false;
		} else if (pattern instanceof OperatorModel) {
			if (!(tomatch instanceof OperatorModel)) return false;
			// Match left child with an OperatorCommaMatched (i.e., consider it as a
			// list where "a,b" = "b,a"
			// and right child in the classic way
/*			boolean result;
			result = new OperatorCommaMatched(((OperatorModel)tomatch).left,
				((OperatorModel)pattern).left,new AlwaysTrue(),this).match();
			if (!result) return false;
			return match(((OperatorModel)tomatch).right,
				((OperatorModel)pattern).right,action);*/
			return new OperatorModelMatched((OperatorModel)tomatch,(OperatorModel)pattern,action).foundMatch(this);
//		} else if (pattern instanceof OperatorComma) {
//			return new OperatorCommaMatched(tomatch,pattern,action,this).match();
		} else if (tomatch instanceof Operator && pattern instanceof Operator
			&& tomatch.getClass().getName().equals(pattern.getClass().getName())
			&& ((Operator)tomatch).getName().equals(((Operator)pattern).getName())) {
			// Default action for operators: match two like operators
			// Recursively match all children
			return new MultipleMatched(Part.getChildren(tomatch),Part.getChildren(pattern),
				action,this).match();
		}
		return false;
	}

	
 Do a quick, partial match
	  If this method returns false, no partial match was found (so don't even
	  think about finding a full match() ...
	  This method does not sport a Matched action argument
	  like match() because quick matches never need to backtrack 
	public boolean qmatch(Part tomatch,Part pattern) {
		tomatch = Brackets.unbracket(tomatch);
		pattern = Brackets.unbracket(pattern);
		if (pattern instanceof Identifier) {	// Match one symbol to tomatch
			if (Part.isEmpty(pattern) && Part.isEmpty(tomatch))
				return true;
			Part typ = getPatternType((Identifier)pattern);
			String symbolname = ((Identifier)pattern).getString();
			if (typ == null) {
				if (isFunction(symbolname)) {
					if (tomatch instanceof Identifier && ((Identifier)tomatch).getString().equals(symbolname))
						return true;
					return false;
				}
			}
			if (!(typ instanceof Identifier))	// We don't handle compound types yet
				return false;
			{	Part val = getMatchedValue(symbolname);
				if (val != null) {	// Match known symbol
					if (val.same(tomatch)) return true;
					// We know that pattern *has to* match to val,
					// and here we find that it also has to match tomatch
					return false;	// A match will never be possible!
				}
			}
			// Try to match a currently unmatched symbol
			String typename = ((Identifier)typ).getString();
			if (typename.equals("List")) {
				setMatchedValue(symbolname,tomatch);
				return true;
			} else if (typename.equals("Term") || typename.equals("Formula")) {
				if (!(tomatch instanceof OperatorComma)) {
					if (tomatch instanceof Identifier) {
						Part tmTyp = getTomatchType((Identifier)tomatch);
						if (tmTyp instanceof Identifier) {
							String tmt = ((Identifier)tmTyp).getString();
							if (tmt.equals("List")) return false;
						}
					}
					setMatchedValue(symbolname,tomatch);
					return true;
				} else return false;
			} else if (typename.equals("Pred")) {
				if (tomatch instanceof Identifier) {
					setMatchedValue(symbolname,tomatch);
					return true;
				} else return false;
			} else if (typename.equals("Var")) {
				if (tomatch instanceof Identifier) {
					Part tmTyp = getTomatchType((Identifier)tomatch);
					if (tmTyp instanceof Identifier) {
						String tmt = ((Identifier)tmTyp).getString();
						if (!(tmt.equals("Var"))) return false;
					}
					setMatchedValue(symbolname,tomatch);
					return true;
				} else return false;
			} else if (typename.equals("Const")) {
				if (tomatch instanceof Identifier) {
					Part tmTyp = getTomatchType((Identifier)tomatch);
					if (tmTyp instanceof Identifier) {
						String tmt = ((Identifier)tmTyp).getString();
						if (!(tmt.equals("Const"))) return false;
					}
					setMatchedValue(symbolname,tomatch);
					return true;
				} else return false;
			}
			return false;
		} else if (pattern instanceof OperatorModel) {
			if (!(tomatch instanceof OperatorModel)) return false;
			OperatorModel patModel = (OperatorModel)pattern;
			OperatorModel tomModel = (OperatorModel)tomatch;
			if (!patModel.getName().equals(tomModel.getName())) return false;
			// check right argument
			if (!(qmatch(tomModel.right,patModel.right))) return false;
			// check left argument; we only can check if it is not an OperatorComma
			if (patModel.left instanceof OperatorComma) return true;
			return qmatch(tomModel.left,patModel.left);
//		} else if (pattern instanceof OperatorComma) {
			// A match may still be possible, but that we cannot decide quickly
//			return true;
		} else if (tomatch instanceof Operator && pattern instanceof Operator
			&& tomatch.getClass().getName().equals(pattern.getClass().getName())
			&& ((Operator)tomatch).getName().equals(((Operator)pattern).getName())) {
			// Default action for operators: match two like operators
			// Recursively match all children
			int count = 0;
			while (true) {
				Part chTomatch = tomatch.getChild(count);
				Part chPattern = pattern.getChild(count);
				if (chTomatch == null) break;
				if (!qmatch(chTomatch,chPattern)) return false;
				count++;
			}
			return true;
		}
		return false;
	}

	public void dump() {
		matches.dump();
	}
}

class AlwaysTrue implements Matched {
	public AlwaysTrue() {}
	
	public boolean foundMatch(Matcher m) {
		return true;
	}
}

class OperatorModelMatched implements Matched {
	private int count = 0;
	private OperatorModel tomatch,pattern;
	private Matched action;	// action to perform if a match is found

	public OperatorModelMatched(OperatorModel tomatch,OperatorModel pattern,Matched action) {
		this.tomatch = tomatch;
		this.pattern = pattern;
		this.action = action;
//System.out.println("CREATE "+this);
	}

	public boolean foundMatch(Matcher m) {
		// Match left child with an OperatorCommaMatched (i.e., consider it as a
		// list where "a,b" = "b,a"
		// and right child in the classic way
		count++;
//System.out.println("FOUNDMATCH enter "+count+" "+this);
		boolean result = false;
		switch (count) {
			case 1:
				if (pattern.left instanceof OperatorComma)
					result = new OperatorCommaMatched(tomatch.left,pattern.left,this,m).match();
				else
					result = m.match(tomatch.left,pattern.left,this);
				break;
			case 2:
				result = m.match(tomatch.right,pattern.right,this);
				break;	
			case 3: result = action.foundMatch(m);
				break;
			default: System.out.println("***OperatorModelMatched: this cannot happen.");
		}
//System.out.println("FOUNDMATCH leave "+count+" "+this);
		count--;
		return result;
	}
}

 Matcher for OperatorComma patterns
  WARNING: probably malfunctioning on patterns that are not OperatorComma!
 	(e.g. tomatch = "L", pattern = "", this probably always matches successfully 
class OperatorCommaMatched implements Matched {
	private Matched action;
	private Part[] tomatch;
	private Part[] pattern;
	private int count = 0;
	private Matcher matcher;

	public OperatorCommaMatched(Part tomatch,Part pattern,Matched action,Matcher m) {
		this(tomatch,OperatorComma.chopCommas(pattern),action,m);
	}

	public OperatorCommaMatched(Part tomatch,Part []pat,Matched action,Matcher m) {
		this.tomatch = OperatorComma.chopCommas(tomatch);
		if (this.tomatch.length > 32)
			// We use an int to hold bit flags about tomatch[] ...
			throw new Error("Expression to match is too complex");
		// First the Terms (easier to match), then the rest
		pattern = new Part[pat.length];
		int filldown = 0;	// index of next Term to write (fills up from 0 to higher values)
		int fillup = pat.length-1;	// index of next non-Term to write (fills up from pat.length-1 to lower values)
		for (int i = pat.length-1; i >= 0; i--) {
			if (pat[i] instanceof Identifier) {
				Part typ = m.getPatternType((Identifier)pat[i]);
				if (typ instanceof Identifier) {
					if (((Identifier)typ).getString().equals("List")) {
						pattern[fillup--] = pat[i];
						continue;
					}
				}
			}
			pattern[filldown++] = pat[i];
		}
		this.action = action;
		matcher = m;
	}

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

	
 Returns a bit pattern:
	  bit i is set => tomatch[i] has not been matched
	  bit i is clear => tomatch[i] has been matched by some pattern[j]
	 				for some j != except 
	private int checkmatch(int except) {
		int mustmatch = (1<<tomatch.length)-1;
		for (int j = 0; j < pattern.length; j++) {
			if (j == except) continue;
			if (mustmatch == 0) return 0;
			Part val = matcher.fillinSymbols(pattern[j]);
			CommaEnumerator enum = new CommaEnumerator(val);
			while (enum.hasMoreElements()) {
				Part p = enum.nextPart();
				for (int i = tomatch.length-1; i>=0; i--) {
					if (tomatch[i].same(p)) mustmatch &= ~(1<<i);
				}
			}
		}
		return mustmatch;
	}

	
 Idem as checkmatch(int), but consider *all* pattern[j]'s 
	private int checkmatch() { return checkmatch(-1); }

	
 Strategy: First match all Terms. This is relatively inexpensive, since
	  we only have to try to match each Term to each element of tomatch[].
	  Then, match all Lists. Note that all elements of tomatch[] that weren't
	  matched to an Identifier earlier on, have to be matched with the Lists.
	  The only thing we don't know is which of those Identifiers has to be matched
	  to which of the Lists (except when there's only one List involved) and
	  which of the already matched Terms have to be added to the Lists ...
	 
	public boolean foundMatch(Matcher m) {
		// Try to match pattern[count].
		if (count == pattern.length) {	// done
			if (checkmatch() == 0)	// OK, the whole tomatch[] has been matched
				return action.foundMatch(m);
			return false;
		}
		count++;	// make this Matched ready for the recursion
		try {
			Part pat = pattern[count-1];
			if (pat instanceof Identifier) {
				Part typ = m.getPatternType((Identifier)pat);
				if (!(typ instanceof Identifier)) return false;	// no support for complex types yet
				String t = ((Identifier)typ).getString();
				if (t.equals("Term") || t.equals("Formula")) {
					// A term can match with any of the tomatch[] elements so try each one
					for (int i = tomatch.length-1; i>=0; i--) {
						boolean result = m.match(tomatch[i],pat,this);
						if (result)
							// everything matched recursively
							return true;
						// either pat did not match tomatch[i], or this.foundMatch() returned false
						// so continue the search
					}
					return false;
				} else if (t.equals("List")) {
					// A List can match with any *subset* of tomatch[] so try each one (expensive!)
					String symbolName = ((Identifier)pat).getString();
					{	Part val = m.getMatchedValue(symbolName);
						if (val != null) {
							// Check if the elements in val are in tomatch[]
							CommaEnumerator enum = new CommaEnumerator(val);
							while (enum.hasMoreElements()) {
								Part p = enum.nextPart();
								boolean found = false;
								for (int i = tomatch.length-1; i>=0; i--) {
									if (tomatch[i].same(p)) {
										found = true;
										break;
									}
								}
								if (!found) return false;	// cannot match
							}
							// All symbols in val are in tomatch[] so we have a successful match
							return foundMatch(m);	// continue the search
						}
					}
					// Try to match the List to various suitable subsets of tomatch[]
					// Each bit of mustmatch corresponds to a tomatch[] element:
					// bit i is clear => tomatch[i] may or may not be in the List
					// but i is set => tomatch[i] must be included in the List
					int mustmatch = 0;
					// Is this the last unmatched List ?
					boolean lastchance = true;
					for (int i = count; i < pattern.length; i++) {
						Part val = m.getMatchedValue(((Identifier)pattern[i]).getString());
						if (val != null) {
							lastchance = false;	// we still have an unmatched list left
							break;
						}
					}
					if (lastchance) {
						// Check which tomatch[i] are already matched by part of the pattern
						mustmatch = checkmatch(count-1);
					}
					for (int mask = (1<<tomatch.length)-1; mask>=0; mask--) {
						if ((mask & mustmatch) != mustmatch)
							// We *must* match all entries marked in mustmatch
							continue;
						Part trythis = null;
						int bitmask = 1;
						for (int i = 0; i<tomatch.length; i++,bitmask<<=1) {
							if ((mask & bitmask) == 0) continue;	// not in mask
							// add tomatch[i] to trythis
							if (trythis == null) trythis = (Part)tomatch[i].clone();
							else trythis = new OperatorComma(trythis,(Part)tomatch[i].clone());
						}
						if (trythis == null) trythis = new Identifier();	// empty list
						m.setMatchedValue(symbolName,trythis);
						boolean result = foundMatch(m);
						m.undefineMatch(symbolName);
						if (result) return true;	// We found a match!
						// no match found; keep trying
					}
					return false;
				} else return false;
			} else if (pat instanceof Operator) {
				// Try to match pat with each corresponding element of tomatch[]
				for (int i = tomatch.length-1; i>=0; i--) {
					boolean result = m.match(tomatch[i],pat,this);
					if (result) return true;
				}
				return false;
			}
		} finally {
			count--;
		}
		return false;
	}
}