package gve.calc.logic;

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

public final class LogicFunctions implements Function {
	public LogicFunctions() {}

	public Part call(String funcname,Part args,Evaluator eval) {
		if (funcname.equals("freevar"))
			return new Brackets(freevar(args),Brackets.CURLY);
		else if (funcname.equals("subst")) {
			args = Brackets.unbracket(args);
			if (args instanceof OperatorComma) {
				Part arg1 = ((OperatorComma)args).left;
				args = ((OperatorComma)args).right;
				if (args instanceof OperatorComma) {
					Part arg2 = ((OperatorComma)args).left;
					Part arg3 = ((OperatorComma)args).right;
					arg3 = (Part)arg3.clone();	// substitute on a clone of the input formula
					if (arg2 instanceof Identifier)
						return subst(arg1,((Identifier)arg2).getString(),arg3);
				}
			}
		}
		return null;
	}

	
 Replace all *free* occurrences of a variable in a formula by a term
	  PENDING: rotate inserted terms! 
	public static final Part subst(Part term,String varname,Part formula) {
		Formula f = new Formula(formula);
		subst(term,varname,f);
		return f.getRootPart();
	}

	public static final void subst(Part term,String varname,Formula f) {
		subst(term,varname,f,f.getRootPart(),new Hashtable());
	}

	public static final void subst(Part term,String varname,Formula f,Part p,Hashtable gebonden) {
		if (p instanceof Identifier) {
			Identifier ident = (Identifier)p;
			if (gebonden.get(ident.getString()) != null)
				// deze variabele is gebonden
				return;
			if (ident.getString().equals(varname)) f.replace(p,(Part)term.clone());
			else f.replace(p,(Identifier)p.clone());
			return;
		}
		if (p instanceof OperatorQuantor) {
			OperatorQuantor quantor = (OperatorQuantor)p;
			if (quantor.child instanceof OperatorColon) {
				// quantor met gebonden variabele
				OperatorColon colon = (OperatorColon)quantor.child;
				Part varpart = colon.left;
				// Either Qvar:formula  or  Qvar in set:formula
				if (varpart instanceof OperatorSet && ((OperatorSet)varpart).getKind()==OperatorSet.IN)
					varpart = ((OperatorSet)varpart).left;
				// Name of bounded var is in varpart now
				if (varpart instanceof Identifier) {
					String varnam = ((Identifier)varpart).getString();
					gebonden.put(varnam,varnam);
					Part result = freevar(colon.right,gebonden);
					subst(term,varname,f,colon.right,gebonden);
					gebonden.remove(varnam);
				}
			}
			return;
		}
		// Default case
		for (int i = 0; ;i++) {
			Part child = p.getChild(i);
			if (child == null) break;
			subst(term,varname,f,child,gebonden);
		}
	}

	
 Return a formula containing comma-delimited list of free variables inside
	  a formula 
	public static final Part freevar(Part p) {
		return freevar(p,new Hashtable());
	}

	private static Part freevar(Part p,Hashtable gebonden) {
		if (p instanceof Identifier) {
			Identifier ident = (Identifier)p;
			if (gebonden.get(ident.getString()) != null)
				// deze variabele is gebonden
				return new Identifier("");
			if (ident.isNumeric()) return new Identifier("");	// numerieke constante telt niet mee
			return (Part)p.clone();
		}
		if (p instanceof OperatorQuantor) {
			OperatorQuantor quantor = (OperatorQuantor)p;
			if (quantor.child instanceof OperatorColon) {
				// quantor met gebonden variabele
				OperatorColon colon = (OperatorColon)quantor.child;
				Part varpart = colon.left;
				// Either Qvar:formula  or  Qvar in set:formula
				if (varpart instanceof OperatorSet && ((OperatorSet)varpart).getKind()==OperatorSet.IN)
					varpart = ((OperatorSet)varpart).left;
				// Name of bounded var is in varpart now
				if (varpart instanceof Identifier) {
					String varname = ((Identifier)varpart).getString();
					gebonden.put(varname,varname);
					Part result = freevar(colon.right,gebonden);
					gebonden.remove(varname);
					return result;
				}
			}
		}
		// Default case: freevars of p is union of freevars of all children of p
		Part result = null;
		for (int i = 0; ;i++) {
			Part child = p.getChild(i);
			if (child == null) break;
			Part fv = freevar(child,gebonden);
			if (fv instanceof Identifier) {
				Identifier fvIdent = (Identifier)fv;
				if (fvIdent.getString().equals("")) continue;	// fv is empty
				// fv is one element; add to front of result
				if (result == null) result = fv;
				else result = new OperatorComma(fv,result);
			} else if (fv instanceof OperatorComma) {
				OperatorComma comma = (OperatorComma)fv;
				if (result == null) result = comma;
				else {
					// Add result to end of fv
					OperatorComma scan = comma;
					while (true) {
						if (scan.right instanceof OperatorComma)
							scan = (OperatorComma)scan.right;
						else {
							scan.right = new OperatorComma(scan.right,result);
							scan.right.setParent(scan);
							result = fv;
							break;
						}
					}
				}
			}
		}
		if (result == null) return new Identifier("");
		else return result;
	}
}