package euler;

import java.util.Calendar;
import java.util.Date;
import java.util.Hashtable;
import java.util.SimpleTimeZone;
import java.util.StringTokenizer;

public class BuiltinManager {

	private Hashtable _builtins = new Hashtable();

	private static final Object LOCK = new Object();
	private static BuiltinManager instance = null;

	private BuiltinManager() {
		_builtins.put(Euler.EclashesWith, new Object());
		_builtins.put(Euler.Etuple, new Object());
		_builtins.put(Euler.LOGdtlit, new Object());
		_builtins.put(Euler.LOGequalTo, new Object());
		_builtins.put(Euler.LOGimplies, new Object());
		_builtins.put(Euler.LOGincludes, new Object());
		_builtins.put(Euler.LOGnotEqualTo, new Object());
		_builtins.put(Euler.LOGnotImplies, new Object());
		_builtins.put(Euler.LOGnotIncludes, new Object());
		_builtins.put(Euler.LOGracine, new Object());
		_builtins.put(Euler.LOGsemantics, new Object());
		_builtins.put(Euler.LOGuri, new Object());
		_builtins.put(Euler.MATHabsoluteValue, new Object());
		_builtins.put(Euler.MATHatan2, new Object());
		_builtins.put(Euler.MATHcos, new Object());
		_builtins.put(Euler.MATHcosh, new Object());
		_builtins.put(Euler.MATHdegrees, new Object());
		_builtins.put(Euler.MATHdifference, new Object());
		_builtins.put(Euler.MATHequalTo, new Object());
		_builtins.put(Euler.MATHexponentiation, new Object());
		_builtins.put(Euler.MATHgreaterThan, new Object());
		_builtins.put(Euler.MATHintegerQuotient, new Object());
		_builtins.put(Euler.MATHlessThan, new Object());
		_builtins.put(Euler.MATHmemberCount, new Object());
		_builtins.put(Euler.MATHnegation, new Object());
		_builtins.put(Euler.MATHnotEqualTo, new Object());
		_builtins.put(Euler.MATHnotGreaterThan, new Object());
		_builtins.put(Euler.MATHnotLessThan, new Object());
		_builtins.put(Euler.MATHproduct, new Object());
		_builtins.put(Euler.MATHproofCount, new Object());
		_builtins.put(Euler.MATHquotient, new Object());
		_builtins.put(Euler.MATHremainder, new Object());
		_builtins.put(Euler.MATHrounded, new Object());
		_builtins.put(Euler.MATHsin, new Object());
		_builtins.put(Euler.MATHsinh, new Object());
		_builtins.put(Euler.MATHsum, new Object());
		_builtins.put(Euler.MATHtan, new Object());
		_builtins.put(Euler.MATHtanh, new Object());
		_builtins.put(Euler.STRconcatenation, new Object());
		_builtins.put(Euler.STRcontains, new Object());
		_builtins.put(Euler.STRcontainsIgnoringCase, new Object());
		_builtins.put(Euler.STRendsWith, new Object());
		_builtins.put(Euler.STRequalIgnoringCase, new Object());
		_builtins.put(Euler.STRgreaterThan, new Object());
		_builtins.put(Euler.STRlessThan, new Object());
		_builtins.put(Euler.STRmatches, new Object());
		_builtins.put(Euler.STRnotEqualIgnoringCase, new Object());
		_builtins.put(Euler.STRnotGreaterThan, new Object());
		_builtins.put(Euler.STRnotLessThan, new Object());
		_builtins.put(Euler.STRnotMatches, new Object());
		_builtins.put(Euler.STRstartsWith, new Object());
		_builtins.put(Euler.TIMEgmTime, new Object());
		_builtins.put(Euler.TIMEinSeconds, new Object());
	}

	public static BuiltinManager getInstance() {
		synchronized (LOCK) {
			if (instance == null) {
				instance = new BuiltinManager();
			}
		}
		return instance;
	}

	public void registerBuiltin(String s) {
		// TODO
	}

	public boolean isBuiltin(String s) {
		return _builtins.get(s) != null;
	}

	public boolean applyBuiltin(Euler er, Euler goal, Stack stack, int tab, StringBuffer pp, StringBuffer pc) {
		Parser np = new Parser();
		boolean not = false;
		try {
			if (goal.verb == Euler.STRconcatenation) {
				Euler el = goal.subj.deref();
				StringBuffer sb = new StringBuffer("\"");
				while (el.getFirst() != null) {
					sb.append(er.getLit(el.getFirst().deref()));
					el = el.getRest();
				}
				sb.append("\"");
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRequalIgnoringCase) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.toLowerCase().equals(ov.toLowerCase())) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRnotEqualIgnoringCase) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (!sv.toLowerCase().equals(ov.toLowerCase())) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRgreaterThan) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.compareTo(ov) > 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRnotGreaterThan) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.compareTo(ov) <= 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRlessThan) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.compareTo(ov) < 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRnotLessThan) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.compareTo(ov) >= 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRstartsWith) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.startsWith(ov)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRendsWith) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.endsWith(ov)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRcontains) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.indexOf(ov) != -1) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRmatches) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.matches(ov)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRnotMatches) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (!sv.matches(ov)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.STRcontainsIgnoringCase) {
				String sv = er.getLit(goal.subj.deref());
				String ov = er.getLit(goal.obj.deref());
				if (sv.toLowerCase().indexOf(ov.toLowerCase()) != -1) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.STRkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.TIMEgmTime && goal.subj.deref().verb.equals("\"\"")) {
				er.obj = np.parse('"' + er.now() + '"');
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.TIMEkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.TIMEinSeconds) {
				StringTokenizer st = new StringTokenizer(er.getLit(goal.subj.deref()), "+-:.TZ");
				int ye = Integer.parseInt(st.nextToken());
				int mo = Integer.parseInt(st.nextToken());
				int da = Integer.parseInt(st.nextToken());
				int ho = Integer.parseInt(st.nextToken());
				int mi = Integer.parseInt(st.nextToken());
				int se = Integer.parseInt(st.nextToken());
				SimpleTimeZone t = new SimpleTimeZone(0, "UTC");
				Calendar c = Calendar.getInstance(t);
				c.set(ye, mo - 1, da, ho, mi, se);
				er.obj = np.parse(Long.toString(c.getTimeInMillis() / 1000));
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.TIMEkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHsum) {
				Euler el = goal.subj.deref();
				double d = 0;
				while (el.getFirst() != null) {
					d += new Double(er.getLit(el.getFirst().deref())).doubleValue();
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(er.nat(goal.subj.deref(), d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHdifference) {
				Euler el = goal.subj.deref();
				double d = new Double(er.getLit(el.getFirst().deref())).doubleValue();
				el = el.getRest();
				while (el.getFirst() != null) {
					d -= new Double(er.getLit(el.getFirst().deref())).doubleValue();
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(er.nat(goal.subj.deref(), d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHproduct) {
				Euler el = goal.subj.deref();
				double d = 1;
				while (el.getFirst() != null) {
					d *= new Double(er.getLit(el.getFirst().deref())).doubleValue();
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(er.nat(goal.subj.deref(), d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHquotient) {
				Euler el = goal.subj.deref();
				double d = new Double(er.getLit(el.getFirst().deref())).doubleValue();
				el = el.getRest();
				while (el.getFirst() != null) {
					d /= new Double(er.getLit(el.getFirst().deref())).doubleValue();
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(d);
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHintegerQuotient) {
				Euler el = goal.subj.deref();
				double d = new Double(er.getLit(el.getFirst().deref())).doubleValue();
				el = el.getRest();
				while (el.getFirst() != null) {
					d /= new Double(er.getLit(el.getFirst().deref())).doubleValue();
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(Integer.toString((int) d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHremainder) {
				Euler el = goal.subj.deref();
				double d = new Double(er.getLit(el.getFirst().deref())).doubleValue();
				el = el.getRest();
				while (el.getFirst() != null) {
					d %= new Double(er.getLit(el.getFirst().deref())).doubleValue();
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(er.nat(goal.subj.deref(), d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHnegation && goal.subj.bound) {
				double d = new Double(er.getLit(goal.subj.deref())).doubleValue();
				StringBuffer sb = new StringBuffer().append(er.nat(goal.subj.deref(), -d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHabsoluteValue) {
				double d = new Double(er.getLit(goal.subj.deref())).doubleValue();
				StringBuffer sb = new StringBuffer().append(er.nat(goal.subj.deref(), d < 0 ? -d : d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHrounded) {
				double d = new Double(er.getLit(goal.subj.deref())).doubleValue();
				StringBuffer sb = new StringBuffer().append(Math.round(d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHexponentiation) {
				Euler el = goal.subj.deref();
				double d = new Double(er.getLit(el.getFirst().deref())).doubleValue();
				el = el.getRest();
				while (el.getFirst() != null) {
					d = Math.pow(d, new Double(er.getLit(el.getFirst().deref())).doubleValue());
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(er.nat(goal.subj.deref(), d));
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHatan2) {
				Euler el = goal.subj.deref();
				double d = new Double(er.getLit(el.getFirst().deref())).doubleValue();
				el = el.getRest();
				while (el.getFirst() != null) {
					d = Math.atan(d / new Double(er.getLit(el.getFirst().deref())).doubleValue());
					el = el.getRest();
				}
				StringBuffer sb = new StringBuffer().append(d);
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHcos) {
				if (goal.subj.deref().bound) {
					double d = new Double(er.getLit(goal.subj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(Math.cos(d));
					er.obj = np.parse(sb.toString());
					if (goal.obj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else if (goal.obj.deref().bound) {
					double d = new Double(er.getLit(goal.obj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(Math.acos(d));
					er.obj = np.parse(sb.toString());
					if (goal.subj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else
					not = true;
			} else if (goal.verb == Euler.MATHdegrees) {
				if (goal.subj.deref().bound) {
					double d = new Double(er.getLit(goal.subj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(d * 180 / Math.PI);
					er.obj = np.parse(sb.toString());
					if (goal.obj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else if (goal.obj.deref().bound) {
					double d = new Double(er.getLit(goal.obj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(d * Math.PI / 180);
					er.obj = np.parse(sb.toString());
					if (goal.subj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else
					not = true;
			} else if (goal.verb == Euler.MATHsin) {
				if (goal.subj.deref().bound) {
					double d = new Double(er.getLit(goal.subj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(Math.sin(d));
					er.obj = np.parse(sb.toString());
					if (goal.obj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else if (goal.obj.deref().bound) {
					double d = new Double(er.getLit(goal.obj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(Math.asin(d));
					er.obj = np.parse(sb.toString());
					if (goal.subj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else
					not = true;
			} else if (goal.verb == Euler.MATHtan) {
				if (goal.subj.deref().bound) {
					double d = new Double(er.getLit(goal.subj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(Math.tan(d));
					er.obj = np.parse(sb.toString());
					if (goal.obj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else if (goal.obj.deref().bound) {
					double d = new Double(er.getLit(goal.obj.deref())).doubleValue();
					StringBuffer sb = new StringBuffer().append(Math.atan(d));
					er.obj = np.parse(sb.toString());
					if (goal.subj.unify(er.obj, er, stack)) {
						pp.append('\n');
						for (int i = tab; i > 0; i--)
							pp.append(' ');
						pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
						if (tab == 0)
							pc.append(goal).append('\n');
					} else
						not = true;
				} else
					not = true;
			} else if (goal.verb == Euler.MATHgreaterThan) {
				if (er.mathCompare(goal) > 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHnotGreaterThan) {
				if (er.mathCompare(goal) <= 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHlessThan) {
				if (er.mathCompare(goal) < 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHnotLessThan) {
				if (er.mathCompare(goal) >= 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHequalTo) {
				if (er.mathCompare(goal) == 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHnotEqualTo) {
				if (er.mathCompare(goal) != 0) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHmemberCount) {
				int n = 0;
				Euler el = goal.subj.deref();
				StringBuffer sb = new StringBuffer();
				if (el.getRest() != null) {
					while (el.getFirst() != null) {
						n++;
						el = el.getRest();
					}
					sb.append(n);
				} else {
					boolean ot = Configuration.getInstance().getThink();
					Configuration.getInstance().setThink(true);
					er.proof("data:," + el + " " + Euler.RDFSmember + " ?X. ");
					Configuration.getInstance().setThink(ot);
					sb.append(er.conc.size());
				}
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.MATHproofCount) {
				boolean ot = Configuration.getInstance().getThink();
				Configuration.getInstance().setThink(true);
				String p = er.proof(er.toURI(goal.subj));
				Configuration.getInstance().setThink(ot);
				StringBuffer sb = new StringBuffer().append(er.conc.size());
				er.obj = np.parse(sb.toString());
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.MATHkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGdtlit) {
				er.obj = np.parse("^^");
				er.obj.subj = goal.subj.deref().getFirst();
				er.obj.obj = goal.subj.deref().getRest().getFirst();
				if (goal.obj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGequalTo) {
				if (goal.subj.deref().verb == goal.obj.deref().verb) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGnotEqualTo) {
				if (goal.subj.deref().verb != goal.obj.deref().verb) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGincludes) {
				Euler e = new Euler();
				er.ext.engine++;
				e.ext = new EulerExt();
				e.ext.se = true;
				if (goal.subj.deref().getFirst() != null) {
					Euler el = goal.subj.deref();
					while (el.getFirst() != null) {
						e.load(er.toURI(el.getFirst().deref()));
						el = el.getRest();
					}
				} else
					e.load(er.toURI(goal.subj.deref()));
				String p = e.proof(er.toURI(goal.obj.deref()));
				if (p.indexOf("# Proof found") != -1) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGnotIncludes) {
				Euler e = new Euler();
				er.ext.engine++;
				e.ext = new EulerExt();
				e.ext.se = true;
				if (goal.subj.deref().getFirst() != null) {
					Euler el = goal.subj.deref();
					while (el.getFirst() != null) {
						e.load(er.toURI(el.getFirst().deref()));
						el = el.getRest();
					}
				} else
					e.load(er.toURI(goal.subj.deref()));
				String p = e.proof(er.toURI(goal.obj.deref()));
				if (p.indexOf("# Proof found") == -1) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGsemantics) {
				Euler e = np.parse(false, "^^");
				e.subj = goal.subj.deref().copy();
				e.obj = np.parse(false, Euler.LOGsemantics);
				if (goal.obj.deref().unify(e, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGracine) {
				String gsv = goal.subj.deref().verb;
				Euler el = goal.subj.deref();
				if (gsv.indexOf('#') != -1)
					el = np.parse((gsv.substring(0, gsv.indexOf('#')) + '>'));
				if (goal.obj.deref().unify(el, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGuri) {
				String gsv = goal.subj.deref().verb;
				Euler el = np.parse('"' + (gsv.substring(1, gsv.length() - 1) + '"'));
				if (gsv.charAt(0) == '<' && gsv.charAt(gsv.length() - 1) == '>' && goal.obj.deref().unify(el, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.LOGkb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			} else if (goal.verb == Euler.LOGimplies) {
				Euler e = er;
				boolean ot = Configuration.getInstance().getThink();
				if (goal.subj.subj == null || goal.subj.verb == "^^" || goal.subj.verb == "!") {
					e = new Euler();
					er.ext.engine++;
					Euler el = goal.subj.deref();
					while (el.getFirst() != null) {
						if (el.getFirst().getFirst() != null)
							Configuration.getInstance().setThink(true);
						else
							e.load(er.toURI(el.getFirst().deref()));
						el = el.getRest();
					}
				}
				e.prepare();
				StringBuffer sb = new StringBuffer();
				if (goal.obj.toString().indexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null)
					sb.append("[ r:test ").append(
							goal.subj.getFirst().verb == "!" ? goal.subj.getFirst().subj : goal.subj.getFirst()).append(";")
							.append(" r:begins \"").append(er.now()).append("\"^^xsd:dateTime; r:ends \"");
				String p = null;
				p = e.proof(er.toURI(goal.obj));
				boolean pass = p.indexOf("# No proof found") == -1;
				pp.append('\n');
				for (int i = tab; i > 0; i--)
					pp.append(' ');
				pp.append(p);
				if (tab == 0)
					pc.append(p).append('\n');
				if (goal.obj.toString().indexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null) {
					sb.append(er.now()).append("\"^^xsd:dateTime; r:system :euler; ").append("a ").append(
							pass ? "r:PassingRun" : "r:UndecidedRun, r:IncompleteRun").append(", r:TestRun].");
					System.err.println(sb);
				}
				Configuration.getInstance().setThink(ot);
			} else if (goal.verb == Euler.LOGnotImplies) {
				Euler e = er;
				long om = Configuration.getInstance().getSteps();
				if (Configuration.getInstance().getSteps() != -1)
					Configuration.getInstance().setSteps(Configuration.getInstance().getSteps() / 20);
				if (goal.subj.subj == null || goal.subj.verb == "^^" || goal.subj.verb == "!") {
					e = new Euler();
					er.ext.engine++;
					Euler el = goal.subj.deref();
					while (el.getFirst() != null) {
						e.load(er.toURI(el.getFirst().deref()));
						el = el.getRest();
					}
				}
				e.prepare();
				StringBuffer sb = new StringBuffer();
				if (goal.obj.toString().indexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null)
					sb.append("[ r:test ").append(
							goal.subj.getFirst().verb == "!" ? goal.subj.getFirst().subj : goal.subj.getFirst()).append(";")
							.append(" r:begins \"").append(er.now()).append("\"^^xsd:dateTime; r:ends \"");
				String p = null;
				if (goal.obj.verb == Euler.Eevidence)
					p = e.proof(er.toURI(goal.obj.subj));
				else
					p = e.proof(er.toURI(goal.obj));
				boolean fail = p.indexOf("# Proof found") != -1;
				pp.append('\n');
				for (int i = tab; i > 0; i--)
					pp.append(' ');
				pp.append(p);
				if (tab == 0)
					pc.append(p).append('\n');
				if (goal.obj.toString().indexOf("Manifest") == -1 && goal.subj.deref().getFirst() != null) {
					sb.append(er.now()).append("\"^^xsd:dateTime; r:system :euler; ").append("a ").append(
							fail ? "r:FailingRun" : "r:UndecidedRun, r:IncompleteRun").append(", r:TestRun].");
					System.err.println(sb);
				}
				Configuration.getInstance().setSteps(om);
			} else if (goal.verb == Euler.EclashesWith && goal.subj.deref().subj != null
					&& Datatype.clash(goal.obj.deref().verb, goal.subj.deref().subj.verb)) {
				pp.append('\n');
				for (int i = tab; i > 0; i--)
					pp.append(' ');
				pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.Ekb);
				if (tab == 0)
					pc.append(goal).append('\n');
			} else if (goal.verb == Euler.Etuple) {
				String s = goal.obj.toString();
				if (!Euler.tuples.contains(s))
					Euler.tuples.addElement(s);
				er.obj = np.parse("_:e" + Euler.tuples.indexOf(s) + "_");
				if (goal.subj.unify(er.obj, er, stack)) {
					pp.append('\n');
					for (int i = tab; i > 0; i--)
						pp.append(' ');
					pp.append('{').append(goal).insert(pp.length() - 2, "} e:evidence ").insert(pp.length() - 2, Euler.Ekb);
					if (tab == 0)
						pc.append(goal).append('\n');
				} else
					not = true;
			}
		} catch (NumberFormatException exc) {
			not = true;
		} catch (Throwable exc) {
			exc.printStackTrace();
			not = true;
		}
		return not;
	}
}