// $Id: BuiltinManager.cs 1295 2007-05-11 16:52:51Z josd $

namespace Eulersharp
{

  using System;
  using System.Collections;
  using System.Globalization;
  using System.Text;
  using System.Text.RegularExpressions;
  using System.Xml;
  
  using Eulersharp;

  /// <summary>
  /// This classes manages all builtins. Built in methods or plugin methods can be 
  /// registered and applyed by er manager.
  /// </summary>
  public class BuiltinManager 
  {

    #region Declarations

    private static object LOCK = new object();
    private static BuiltinManager instance = null;

    private Hashtable _builtins = new Hashtable();

    #endregion

    #region Constructor

    /// <summary>
    /// This method constructs an instance of the builtin manager class. This
    /// constructor is private because er class is a singleton. The only
    /// instance of er class should be retrieved via the getInstance() method. 
    /// </summary>
    private BuiltinManager() 
    {
      _builtins[Euler.EclashesWith] = new Object();
      _builtins[Euler.Etuple] = new Object();
      _builtins[Euler.LOGdtlit] = new Object();
      _builtins[Euler.LOGequalTo] = new Object();
      _builtins[Euler.LOGimplies] = new Object();
      _builtins[Euler.LOGincludes] = new Object();
      _builtins[Euler.LOGnotEqualTo] = new Object();
      _builtins[Euler.LOGnotImplies] = new Object();
      _builtins[Euler.LOGnotIncludes] = new Object();
      _builtins[Euler.LOGracine] = new Object();
      _builtins[Euler.LOGsemantics] = new Object();
      _builtins[Euler.LOGuri] = new Object();
      _builtins[Euler.MATHabsoluteValue] = new Object();
      _builtins[Euler.MATHatan2] = new Object();
      _builtins[Euler.MATHcos] = new Object();
      _builtins[Euler.MATHcosh] = new Object();
      _builtins[Euler.MATHdegrees] = new Object();
      _builtins[Euler.MATHdifference] = new Object();
      _builtins[Euler.MATHequalTo] = new Object();
      _builtins[Euler.MATHexponentiation] = new Object();
      _builtins[Euler.MATHgreaterThan] = new Object();
      _builtins[Euler.MATHintegerQuotient] = new Object();
      _builtins[Euler.MATHlessThan] = new Object();
      _builtins[Euler.MATHmemberCount] = new Object();
      _builtins[Euler.MATHnegation] = new Object();
      _builtins[Euler.MATHnotEqualTo] = new Object();
      _builtins[Euler.MATHnotGreaterThan] = new Object();
      _builtins[Euler.MATHnotLessThan] = new Object();
      _builtins[Euler.MATHproduct] = new Object();
      _builtins[Euler.MATHproofCount] = new Object();
      _builtins[Euler.MATHquotient] = new Object();
      _builtins[Euler.MATHremainder] = new Object();
      _builtins[Euler.MATHrounded] = new Object();
      _builtins[Euler.MATHsin] = new Object();
      _builtins[Euler.MATHsinh] = new Object();
      _builtins[Euler.MATHsum] = new Object();
      _builtins[Euler.MATHtan] = new Object();
      _builtins[Euler.MATHtanh] = new Object();
      _builtins[Euler.STRconcatenation] = new Object();
      _builtins[Euler.STRcontains] = new Object();
      _builtins[Euler.STRcontainsIgnoringCase] = new Object();
      _builtins[Euler.STRendsWith] = new Object();
      _builtins[Euler.STRequalIgnoringCase] = new Object();
      _builtins[Euler.STRgreaterThan] = new Object();
      _builtins[Euler.STRlessThan] = new Object();
      _builtins[Euler.STRmatches] = new Object();
      _builtins[Euler.STRnotEqualIgnoringCase] = new Object();
      _builtins[Euler.STRnotGreaterThan] = new Object();
      _builtins[Euler.STRnotLessThan] = new Object();
      _builtins[Euler.STRnotMatches] = new Object();
      _builtins[Euler.STRstartsWith] = new Object();
      _builtins[Euler.TIMEgmTime] = new Object();
      _builtins[Euler.TIMEinSeconds] = new Object();
    }

    /// <summary>
    /// This class acts as a singleton. getInstance() returns the only instance of
    /// er class.
    /// </summary>
    /// <returns>the only instance of er class</returns>
    public static BuiltinManager GetInstance() 
    {
      lock(LOCK)
      {
        if (instance == null) 
        {
          instance = new BuiltinManager();
        }
        return instance;
      }
    }

    #endregion

    #region Public methods

    /// <summary>
    /// This method registers a builtin.
    /// </summary>
    /// <param name="s">The name of the builtin</param>
    public void RegisterBuiltin(string s) 
    {
      // TODO
    }

    /// <summary>
    /// This method checks if builtin.
    /// </summary>
    /// <param name="s">The name of the builtin</param>
    public bool IsBuiltin(string s) 
    {
      return _builtins[s] != null;
    }

    /// <summary>
    /// This method applies a builtin
    /// </summary>
    /// <param name="er">proof engine</param>
    /// <param name="goal">builtin to be proved</param>
    /// <param name="stack">proof stack</param>
    /// <param name="tab">proof depth</param>
    /// <param name="pp">partial proof</param>
    /// <param name="pc">compact proof</param>
    public bool ApplyBuiltin(Euler er, Euler goal, Stack stack, int tab, StringBuilder pp, StringBuilder pc)
    {
      Parser np = new Parser();
      bool not = false;
      try {
        if (goal.verb == Euler.STRconcatenation) {
          Euler el = goal.subj.deref();
          StringBuilder sb = new StringBuilder("\"");
          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.ToLower().Equals(ov.ToLower())) 
          {
            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.ToLower().Equals(ov.ToLower())) 
          {
            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.STRcontainsIgnoringCase) {
          String sv = er.getLit(goal.subj.deref());
          String ov = er.getLit(goal.obj.deref());
          if (sv.ToLower().IndexOf(ov.ToLower()) != -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());
          Match m = Regex.Match(sv, ov);
          if (m.Success && m.Value.Equals(sv)) {
            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());
          Match m = Regex.Match(sv, ov);
          if (!(m.Success && m.Value.Equals(sv))) {
            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) {
          er.obj = np.Parse(new StringBuilder().Append(XmlConvert.ToDateTime(er.getLit(goal.subj.deref())).Ticks/10000000L-62135600400L).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.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 += Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().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 = Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
          el = el.getRest();
          while (el.getFirst() != null) {
            d -= Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().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 *= Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().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 = Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
          el = el.near.obj;
          while (el.getFirst() != null) {
            d /= Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().Append(d.ToString(NumberFormatInfo.InvariantInfo));
          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 = Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
          el = el.near.obj;
          while (el.getFirst() != null) {
            d /= Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().Append(((int)d).ToString(NumberFormatInfo.InvariantInfo));
          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 = Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
          el = el.getRest();
          while (el.getFirst() != null) {
            d %= Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().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 = Double.Parse(er.getLit(goal.subj.deref()), NumberFormatInfo.InvariantInfo);
          StringBuilder sb = new StringBuilder().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 = Double.Parse(er.getLit(goal.subj.deref()), NumberFormatInfo.InvariantInfo);
          StringBuilder sb = new StringBuilder().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 = Double.Parse(er.getLit(goal.subj.deref()), NumberFormatInfo.InvariantInfo);
          StringBuilder sb = new StringBuilder().Append(Math.Round(d).ToString(NumberFormatInfo.InvariantInfo));
          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 = (double) Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
          el = el.getRest();
          while (el.getFirst() != null) {
            d = Math.Pow(d, (double) Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo));
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().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 = (double) Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo);
          el = el.getRest();
          while (el.getFirst() != null) {
            d = Math.Atan(d/(double) Double.Parse(er.getLit(el.getFirst().deref()), NumberFormatInfo.InvariantInfo));
            el = el.getRest();
          }
          StringBuilder sb = new StringBuilder().Append(d.ToString(NumberFormatInfo.InvariantInfo));
          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 = Double.Parse(er.getLit(goal.subj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append(Math.Cos(d).ToString(NumberFormatInfo.InvariantInfo));
            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 = Double.Parse(er.getLit(goal.obj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append(Math.Acos(d).ToString(NumberFormatInfo.InvariantInfo));
            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 = Double.Parse(er.getLit(goal.subj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append((d*180/Math.PI).ToString(NumberFormatInfo.InvariantInfo));
            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 = Double.Parse(er.getLit(goal.obj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append((d*Math.PI/180).ToString(NumberFormatInfo.InvariantInfo));
            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 = Double.Parse(er.getLit(goal.subj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append(Math.Sin(d).ToString(NumberFormatInfo.InvariantInfo));
            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 = Double.Parse(er.getLit(goal.obj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append(Math.Asin(d).ToString(NumberFormatInfo.InvariantInfo));
            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 = Double.Parse(er.getLit(goal.subj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append(Math.Tan(d).ToString(NumberFormatInfo.InvariantInfo));
            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 = Double.Parse(er.getLit(goal.obj.deref()), NumberFormatInfo.InvariantInfo);
            StringBuilder sb = new StringBuilder().Append(Math.Atan(d).ToString(NumberFormatInfo.InvariantInfo));
            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();
          StringBuilder sb = new StringBuilder();
          if (el.getRest() != null) {
            while (el.getFirst() != null) {
              n++;
              el = el.getRest();
            }
            sb.Append(n);
          }
          else {
            bool ot = Configuration.GetInstance().Think;
            Configuration.GetInstance().Think = true;
            er.Proof("data:," + el + " " + Euler.RDFSmember + " ?X. ");
            Configuration.GetInstance().Think = ot;
            sb.Append(Euler.conc.Count);
          }
          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) {
          bool ot = Configuration.GetInstance().Think;
          Configuration.GetInstance().Think = true;
          String p = er.Proof(er.toURI(goal.subj));
          Configuration.GetInstance().Think = ot;
          StringBuilder sb = new StringBuilder().Append(Euler.conc.Count);
          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 - 2) + '"'));
          if (gsv[0] == '<' && gsv[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;
          bool ot = Configuration.GetInstance().Think;
          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().Think = true;
              else e.Load(er.toURI(el.getFirst().deref()));
              el = el.getRest();
            }
          }
          e.Prepare();
	  StringBuilder sb = new StringBuilder();
          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));
          bool 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 :eulersharp; ")
              .Append("a ").Append(pass?"r:PassingRun":"r:UndecidedRun, r:IncompleteRun").Append(", r:TestRun].");
	    Console.Error.WriteLine(sb);
	  }
          Configuration.GetInstance().Think = ot;
        }
        else if (goal.verb == Euler.LOGnotImplies) {
          Euler e = er;
          long om = Configuration.GetInstance().Steps;
          if (Configuration.GetInstance().Steps != -1) Configuration.GetInstance().Steps = Configuration.GetInstance().Steps/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) {
              if (el.getFirst().getFirst() != null) Configuration.GetInstance().Think = true;
              else e.Load(er.toURI(el.getFirst().deref()));
              el = el.getRest();
            }
          }
          e.Prepare();
	  StringBuilder sb = new StringBuilder();
          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));
          bool 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 :eulersharp; ")
              .Append("a ").Append(fail?"r:FailingRun":"r:UndecidedRun, r:IncompleteRun").Append(", r:TestRun].");
	    Console.Error.WriteLine(sb);
	  }
          Configuration.GetInstance().Steps = 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.Add(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 (FormatException) {
        not = true;
      }
      catch (Exception exc) {
        Console.Error.WriteLine(exc);
        not = true;
      }
      return not;
    }

    #endregion
  }
}