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

namespace Eulersharp
{

  using System;
  using System.Collections;
  using System.IO;
  using System.Runtime.CompilerServices;
  using System.Text;
  using Eulersharp.Output;

  /// <summary>
  /// This class contains methods for launching the euler backward chaining reasoner
  /// </summary>

  public class EulerRunner 
  {
    /// <summary>Main method invoked via <code>Euler</code></summary>
    /// <param name="args">command line arguments</param>

    [STAThread]
    public static void Main(string[] args) 
    {
      if (args.Length == 0 || args[0].EndsWith("-help")) {
        Console.Error.WriteLine("Version: " + Configuration.GetInstance().Version);
        Console.Error.WriteLine("Usage: Euler [--step count] [--debug] [--trace] axiom ... [--nope] [--think] [--filter|--query] lemma");
      }
      else 
      {
        try 
        {
          TextWriter outp = Console.Out;
          outp.WriteLine(doProof(args));
          if (outp != Console.Out) outp.Close();
        }
        catch (Exception e) 
        {
          Console.Error.WriteLine(e);
        }
      }
    }

    /// <summary>This method generates a proof based on the given arguments</summary>

    [MethodImpl(MethodImplOptions.Synchronized)]
    public static String doProof(String[] args) 
    {
      try 
      {
        Euler e = new Euler();
        Parser np = new Parser();
        int n = args.Length - 1;
        String c = e.toURI(np.Parse('<' + args[n] + '>'));
        for (int j = 0; j < n; j++) 
        {
          if (args[j].EndsWith("-think")) Configuration.GetInstance().Think = true;
          else if (args[j].EndsWith("-nope")) Configuration.GetInstance().ProofExplanation = false;
          else if (args[j].EndsWith("-step")) Configuration.GetInstance().Steps = Int64.Parse(args[++j]);
          else if (args[j].EndsWith("-local")) Configuration.GetInstance().RunLocal = true;
          else if (args[j].EndsWith("-debug")) StdOutputter.GetInstance().setLogLevel(Outputter.LOGLEVEL.FINE);
          else if (args[j].EndsWith("-trace")) StdOutputter.GetInstance().setLogLevel(Outputter.LOGLEVEL.FINER);
          else if (!args[j].StartsWith("-")) e.Load(e.toURI(np.Parse('<' + args[j] + '>')));
          else if (args[j].EndsWith("-graph")) {
            Euler el = new Euler();
            el.Load(e.toURI(np.Parse('<' + args[++j] + '>')));
            StringBuilder sb = new StringBuilder("data:,");
            for (IEnumerator en = (IEnumerator) el.ext.ns.Keys.GetEnumerator(); en.MoveNext(); ) {
              Object nsx = en.Current;
              sb.Append("@prefix ").Append(nsx).Append(' ').Append(el.ext.ns[nsx]).Append(".\n");
            }
            String s = el.ext.baseURI;
            while (el.near != null) {
              sb.Append('{').Append(el.near).Append("} q:source <").Append(s).Append(">.\n");
              el = el.near;
            }
            e.Load(sb.ToString());
          }
          else if (args[j].EndsWith("-filter") || args[j].EndsWith("-query")) {
            Euler el = new Euler();
            el.uid = -1;
            el.Load(e.toURI(np.Parse('<' + args[++j] + '>')));
            StringBuilder sb = new StringBuilder("data:,");
            for (IEnumerator en = (IEnumerator) el.ext.ns.Keys.GetEnumerator(); en.MoveNext(); ) {
              Object nsx = en.Current;
              sb.Append("@prefix ").Append(nsx).Append(' ').Append(el.ext.ns[nsx]).Append(".\n");
            }
            while (el.near != null) {
              if (el.near.verb == Euler.LOGimplies) {
                for (Euler er = el.near.obj; er != null; er = er.near) {
                  sb.Append('{');
                  for (Euler ee = el.near.subj; ee != null; ee = ee.near) {
                    e.rewrite(false, ee, np);
                    bnp(ee);
                    sb.Append(ee);
                  }
                  sb.Append(sfg(el.near.subj, er));
                  sb.Append("} => {_:").Append(el.near.uid).Append(' ').Append(Euler.Qselect).Append(" {");
                  e.rewrite(false, er, np);
                  bnc(er);
                  sb.Append(er).Append("}}. \n");
                }
                el = el.near;
              }
              else if (el.near.verb == Euler.Qselect && el.near.near.verb == Euler.Qwhere) {
                for (Euler er = el.near.obj; er != null; er = er.near) {
                  sb.Append('{');
                  for (Euler ee = el.near.near.obj; ee != null; ee = ee.near) {
                    e.rewrite(false, ee, np);
                    bnp(ee);
                    sb.Append(ee);
                  }
                  sb.Append(sfg(el.near.near.obj, er));
                  sb.Append("} => {").Append(el.near.subj).Append(' ').Append(Euler.Qselect).Append(" {");
                  e.rewrite(false, er, np);
                  bnc(er);
                  sb.Append(er).Append("}}. ");
                }
                el = el.near.near;
              }
	      else if (el.near.verb.Equals("WHERE")) {
		if (!el.near.obj.verb.Equals("")) {
		  Euler et = new Euler();
		  et.subj = el.near.obj;
		  el.near.obj = et;
		}
		for (Euler er = el.near.subj; er != null; er = er.near) {
		  for (Euler ev = el.near.obj; ev != null; ev = ev.near) {
		    sb.Append('{');
		    for (Euler ee = ev.subj; ee != null; ee = ee.near) {
		      e.rewrite(false, ee, np);
                      bnp(ee);
		      sb.Append(ee);
		    }
                    sb.Append(sfg(ev.subj, er));
		    sb.Append("} => {_:e").Append(el.near.subj.uid).Append(' ').Append(Euler.Qselect).Append(" {");
		    e.rewrite(false, er, np);
                    bnc(er);
		    sb.Append(er).Append("}}. \n");
		  }
		}
		el = el.near;
	      }
              else el = el.near;
            }
            c = sb.ToString();
            e.Load(c);
	    e.ext.loaded.Add('<' + e.toURI(np.Parse('<' + args[j] + '>')) + '>');
          }
        }
        e.Prepare();
        String p = e.Proof(c);
        if (!Configuration.GetInstance().ProofExplanation) {
          Euler el = new Euler();
          el.uid = -1;
          el.Load("data:," + p);
          StringBuilder sb = new StringBuilder();
          for (IEnumerator enr = (IEnumerator) el.ext.ns.Keys.GetEnumerator(); enr.MoveNext(); ) {
            Object nsx = enr.Current;
            sb.Append("@prefix ").Append(nsx).Append(' ').Append(el.ext.ns[nsx]).Append(".\n");
          }
          sb.Append('\n');
          for (Euler eu = el; eu.near != null; eu = eu.near) {
            if (eu.near.verb == Euler.Qselect) {
              Euler en = eu.near.near;
              eu.near = eu.near.obj;
              eu.near.near = en;
            }
          }
          while (el.near != null) {
            Euler eu = el.near.near;
            while (eu != null) {
              if (eu.unify(el.near, e, null)) break;
              eu = eu.near;
            }
            if (eu == null && el.near.cverb != "vv") sb.Append(el.near).Append('\n');
            el = el.near;
          }
          p = sb.ToString();
        }
        Configuration.GetInstance().Think = false;
        Configuration.GetInstance().ProofExplanation = true;
        Configuration.GetInstance().Steps = -1;
        Configuration.GetInstance().RunLocal = false;
        return p;
      }
      catch (Exception e) 
      {
        Console.Error.WriteLine(e);
        return null;
      }
    }

    static void bnp(Euler el) {
      if (el.subj != null) bnp(el.subj);
      if (el.cverb.StartsWith("_:")) el.cverb = "?P" + el.cverb.Substring(2);
      if (el.obj != null) bnp(el.obj);
    }

    static void bnc(Euler el) {
      if (el.subj != null) bnc(el.subj);
      if (el.cverb.StartsWith("_:")) el.cverb = "?C" + el.cverb.Substring(2);
      if (el.obj != null) bnc(el.obj);
    }

    static String sfg(Euler ev, Euler er) {
      StringBuilder sb = new StringBuilder();
      ArrayList wt = new ArrayList();
      ev.getX(true, wt);
      if (er.subj != null && er.subj.cverb != null && er.subj.cverb.StartsWith("_:")) {
        sb.Append("?C").Append(er.subj.cverb.Substring(2)).Append(" e:tuple (");
        for (IEnumerator e = wt.GetEnumerator(); e.MoveNext(); ) {
          String ne = (String)e.Current;
          if (ne.StartsWith("?")) sb.Append(ne).Append(' ');
        }
        sb.Append("). ");
      }
      if (er.obj != null && er.obj.cverb != null && er.obj.cverb.StartsWith("_:")) {
        sb.Append("?C").Append(er.obj.cverb.Substring(2)).Append(" e:tuple (");
        for (IEnumerator e = wt.GetEnumerator(); e.MoveNext(); ) {
          String ne = (String)e.Current;
          if (ne.StartsWith("?")) sb.Append(ne).Append(' ');
        }
        sb.Append("). ");
      }
      return(sb.ToString());
    }
  }
}