// $Id: Proof.cs 93 2003-07-01 07:28:40Z mdupont $

/*
EvalGoals, StackPop uses elrGoal

Call Overview
Proof::DoProof
      syno(elrGoal); 
--> EvalGoals
--> CallGoal --> TryCatch1 --> CheckImpliesFalse --> EulerProofWhile1 (elrEp)
			(stbldPv)	(stbldPv)	   --> ParseProof
						       --> EmitGoal(stbldPv)

				 --> EulerProofStep1   --> EulerProofStep2
				        (stbldPv)      --> Unify (*elrEp,stbldPv)
	           --> StackPop
rewrite --> copyAttributes
	--> rewriteHelper

*/
using System;
using System.Collections;
using System.IO;
using System.Net;
using System.Net.Sockets;
using System.Text;
using DotGNU.Rdf;

// now the rest is the implementation of the proof!
// class Proof -- the results of a proof

public class Proof : Euler
{
  //Euler elrG;
  //Euler elrLr;
  //Euler elrTs;
  //Euler elrTsb;
  //Hashtable hshtNs; // from parent
  //Hashtable hshtNsp;
  //Euler elrGoal;
  ArrayList vt;
  EStack stack;
  Euler Parent; // pointer to the parent object
  Euler elrB;
  Euler elrEl;
  Euler elrEp;
  Euler elrG ;
  Euler elrGd;
  Euler elrGn;
  Euler elrGoal;
  Euler elrGs;
  Euler elrLr;
  Euler elrN;
  Euler elrTe;
  Euler elrTs1;
  Euler elrTs2;
  Euler elrTs;
  Euler elrTsb;
  Euler[] vars;

  Hashtable hshtMto; // to table owl:FunctionalProperty properties
  //inherited  Hashtable hshtNsp; 
  Hashtable hshtOtm; // to table owl:InverseFunctionalProperty properties
  Hashtable hshtPct;
  Hashtable hshtDds; // to table log:definitiveDocument and Service properties
  Hashtable hshtYyn;

  Parser np;
  String cj;
  String uri; // base uri
  StringBuilder gen;
  StringBuilder nsp;
  StringBuilder pc;
  StringBuilder pp;
    //  StringBuilder proof;
  StringBuilder stbldGen;
  StringBuilder stbldPc;
  StringBuilder stbldPp;
    StringBuilder stbldProof;// was proof
  StringBuilder stbldPv;
  int tab;

// hash tables!
// temp
// to table log:definitiveDocument and Service properties
// to table owl:FunctionalProperty properties
// to table owl:InverseFunctionalProperty properties


public Proof(Euler parent,String uri,String u,String cj)
    {
      Console.Error.WriteLine("Proof constructor");

	Parent=parent;
	hshtSyn = Parent.hshtSyn;

	// stbldProof = new StringBuilder(4096);
	//	stbldNsp = new StringBuilder(256);
	stbldGen = new StringBuilder("data:,"); // line 338
	stbldPp = new StringBuilder(4096);
	

	stbldPc = new StringBuilder(4096);
	stbldPv = new StringBuilder(256);

	// hash tables!
	
	//	hshtPcct = new Hashtable();
	hshtNsp = new Hashtable(); 
	hshtYyn = new Hashtable();



	//hshtNs = new Hashtable();
	    // hshtNsp = new Hashtable();
	    //	    hshtSyn = new Hashtable();
	    //hshtMto = new Hashtable();
	    //	    hshtOtm = new Hashtable();
	    //	    hshtDds = new Hashtable();

	
	// to table owl:FunctionalProperty properties
	hshtMto = new Hashtable();
	
	// to table owl:InverseFunctionalProperty properties
	hshtOtm = new Hashtable();

	// to table log:definitiveDocument and Service properties
	hshtDds = new Hashtable();
	hshtPct = new Hashtable();

	elrB = null;
	elrEl = null;
	elrEp = null;
	elrG = null;
	elrGd = null;
	elrGn = null;
	elrGoal = new Euler();
	elrG = elrGoal;

	elrGs = null;

	elrLr = null;
	elrN = null;

// temp
	elrTe = null;
	elrTs = null;
	elrTs1 = null;
	elrTs2 = null;
	elrTsb = null;

	cj = fromWeb(uri);    u = parent.baseURI;
	vt = new ArrayList(); np = new Parser(cj, vt, this, u);
	      
	// created data
	if (hshtNs == null) {

     	    
	  //	    RegisterNamespaces();

	}
	
	stbldGen = new StringBuilder("data:,");

    }



    public String DoProof()
    {
    lock(this) {
      Console.Error.WriteLine("In DoProof");

      Console.Error.WriteLine("syno before syno(elrGoal);" + elrGoal );
      syno(elrGoal);
      Console.Error.WriteLine("syno after syno(elrGoal);" + elrGoal );

      String gener = stbldGen.ToString();

      if (!gener.Equals("data:,")) Load(gener); // like 380

      if (vt.Count > varmax) varmax = vt.Count;

      //      stbldNsps = new StringBuilder(256);

      if (Parent.hshtNs == null)
	{
	  EmitNamespaces(Parent.hshtNs);

	}
      
      tab = 0;
      vars = new Euler[varmax];
      elrLr = elrGoal.near; // line 391
      elrTs = null;
      elrTsb = null;
      stack = new EStack();

      // this controls the truth of this proof
      not = false;

      long istep = step;


      stbldProof = new StringBuilder(4096);

      // Line 407
      EmitHeader(stbldProof);


      if (loaded == null)
	{
	  stbldProof.Append("nothing");
	}
      else {
	  EmitSemanticsOpen(stbldProof);
	  EmitKeys(stbldProof);
	  EmitSemanticsClose(stbldProof);
      }

      stbldProof.Append('\n');
      stbldProof.Append('\n');

      int pn = stbldProof.Length;

      //      String temp = "TODO:Parent.stbldNsps"; //Parent.stbldNsps;
      stbldProof.Append(Parent.stbldNsps);

      int pns = stbldProof.Length;

      stbldProof.EnsureCapacity(stbldProof.Length * 2);

      Console.Error.WriteLine("In DoProof, proof so far is " + stbldProof);
      Console.Error.WriteLine("In DoProof, goal so far is " + elrGoal);

      Console.Error.WriteLine("In DoProof, before eval goals");
      EvalGoals(/*elrGoal,elrTs,vars,stack,stbldPp,stbldPc,elrLr*/);

      Console.Error.WriteLine("In DoProof, after eval goals");

      r.Call(step,elrGoal);

	if (elrGoal == null)
	{
	    Console.Error.WriteLine("elrGoal is null!");
//	    elrGoal = new Euler();
	}
	if (elrGn == null)
	{
	    Console.Error.WriteLine("elrGn is null!");
	    elrGn = new Euler();
	} 



      CurrentTime = DateTime.Now.Ticks;


      Euler elrEl; // elrEl is used by Unify , ParseProof, EulerProofWhile1, StackPop

      Console.Error.WriteLine("In While Loop " + elrGoal);
      while (true) {

	Console.Error.WriteLine("In CallGoal!");	
	if (elrGoal == null)
	{
	    Console.Error.WriteLine("elrGoal is null!");

	try {
	  CallGoal(pn /*elrGoal,,stbldProof,hshtPct,stbldPp,stbldPc,pns,istep,elrTs,stack,vars,elrLr, np, elrG, elrTsb, ref tab,  elrEl*/);
	  //	  elrGoal,pn,stbldProof,hshtPct,stbldPp,stbldPc,pns,istep,elrTs,stack,vars,elrLr)
	}
	catch (Exception e) {
	  Report.StackTrace(e.StackTrace);
	}
      }

    }
    }
    }

    //                  CallGoal(Euler,      int,    StringBuilder,      Hashtable,     StringBuilder,    StringBuilder,    int,     long,       Euler,    EStack, Euler[], Euler)'
    public virtual void CallGoal(int pn
				 /*				 Euler elrGoal, 
				 int pn,
				 StringBuilder stbldProof, 
				 Hashtable hshtPct, 
				 StringBuilder stbldPp, 
				 StringBuilder stbldPc, 
				 int pns, 
				 long istep, 
				 Euler elrTs, 
				 EStack stack, 
				 Euler[] vars,
				 Euler elrLr, 
				 Parser np, 
				 Euler elrG,
				 Euler elrTsb, 
				 ref int tab,
				 Euler elrEl
				 */
				 )
    {
      StringBuilder stbldPv = new StringBuilder(256);

	if (IfGoalNotNull(/*elrGoal,pn,hshtPct,stbldProof,pns , istep*/))

	    {
		not = false;
	    }

	Console.Error.WriteLine("In CallGoal!");	
	if (elrGoal == null)
	{
	    Console.Error.WriteLine("elrGoal is null!");
//	    elrGoal = new Euler();
	}
	if (elrGn == null)
	{
	    Console.Error.WriteLine("elrGn is null!");
	    elrGn = new Euler();
	} 


	
	TryCatch1(/*elrGoal,vars,
		  stack,stbldPp,istep, ref tab,
		  np, elrG, elrLr, elrTsb,stbldPc,*/
		  stbldPv
		  /*,
		  elrTs, 
		  elrEl*/);
	//    public virtual void  TryCatch1(Euler elrGoal, Euler[] vars, EStack stack, StringBuilder stbldPp, long istep, ref int tab, Parser np, Euler elrG, Euler elrLr, Euler elrTsb,StringBuilder stbldPc,  StringBuilder  stbldPv, Euler elrTs, Euler elrEl)

	
	if (trace) {
	    if (!not && elrGoal.verb != null) {
		r.Exit(step,elrGoal);
	    }
	    else if (!not && elrGoal.cverb != null) {
		r.Exit(elrGoal);
	    }
	    else if (not && elrGoal.verb != null) {
		r.Fail(step,elrGoal);
	    }
	    else if (not && elrGoal.cverb != null) {
		r.Fail(elrGoal);
	    }
	}


///*6F 0D 00 00 06 */ callvirt   instance void 'Euler'/*02000002*/::'ReportSteps'(class 'System'.'String'/*00000000*/, class 'Euler'/*02000002*/) /*0600000D*/
	ReportSteps(uri,elrGoal);

	if (elrGoal != null)
	  {
		Console.Error.WriteLine("elrGoal is advancing!");
		Console.Error.WriteLine(elrGoal);

		elrGoal = elrGoal.near; // same as line Euler.cs:425
	  }
	else
	  {
	    elrGoal = new Euler();
	    Console.Error.WriteLine("Goal is empty");
	  }

	
	if (trace && !not && elrGoal != null && elrGoal.verb != null)
	    r.Call(step,elrGoal);
	
	// Error Handling.. ?
	if (!not && elrGoal == null) {
	    stbldProof.Append(stbldPp);
	    stbldProof.Append("\n\n");
	    r.Continue();
	    // store this in the has
	    hshtPct[stbldPc.ToString()] = this;
	}
	
	//  public virtual void  StackPop(Euler elrGoal, Euler elrTs,Euler[] vars, EStack stack, StringBuilder stbldPp,	StringBuilder stbldPc ,Euler elrLr,ref int tab

	StackPop(
		 /*
		   elrGoal, elrTs,
		   vars,  stack,  stbldPp,
		   stbldPc ,
		   elrLr, tab
		 */
);
	
    }

	long istep;
    // step is called 
    public virtual void  TryCatch1(
				   /*Euler elrGoal, Euler[] vars, EStack stack, StringBuilder stbldPp, long istep, ref int tab, Parser np, Euler elrG, Euler elrLr, Euler elrTsb,StringBuilder stbldPc,  */
				   StringBuilder  stbldPv
				   /*, Euler elrTs, Euler elrEl*/)
    {

	Console.Error.WriteLine("in try catch");
	if (elrGoal == null)
	{
	    Console.Error.WriteLine("elrGoal is null!");
	    elrGoal = new Euler();
	}
	if (elrGn == null)
	{
	    Console.Error.WriteLine("elrGn is null!");
	    elrGn = new Euler();
	} 

	try {
	    if (elrGoal.varid != - 1 && elrGoal.subj != null && elrGoal.obj != null) {

	      Console.Error.WriteLine("varid ! -1");
	      elrGn = elrGoal.eval(vars, stack);

	      elrGoal.verb = elrGn.verb;
	      elrGoal.cverb = elrGn.cverb;

	    }

	    if (elrGoal.verb == null) {

	      Console.Error.WriteLine("emit implies");
		EmitImplies(/*stbldPp,elrGoal,stbldPc,ref tab*/);

	    }
	    else if (elrGoal.verb == "" && elrGoal.subj.obj == null) {  // @@ single

	      Console.Error.WriteLine("emit literal");

	      //(StringBuilder stbldPp, Euler elrGoal, ref int tab)
		EmitLiteral(/*stbldPp,elrGoal,ref tab*/);

	    }
	    else if (elrGoal.verb == Etrace) 
		{

		  Console.Error.WriteLine("report");
	// RECURSE : /* 6F 64 00 00 06     */ callvirt   instance void 'Report'/*0200000D*/::'ReportSteps'(int64, class 'System'.'String'/*00000000*/) /*06000064*/
		    r.Report(step,elrGoal);

		}

	    // LOGImplies match2 : is it implying a falshood! 
	    // implication needs falsehood!
	    // 
	    //    public virtual bool  CheckImpliesFalse(
	    /*
	      Euler elrGoal, Euler[] vars, EStack stack, Parser np, Euler elrG, StringBuilder stbldPp,  int tab,StringBuilder stbldPv
	    */
	    else if (CheckImpliesFalse(
				       /*
					 elrGoal, vars, stack, np, elrG, stbldPp, stbldPv,  tab
				       */
))
		{

		}

	    else {
		  Console.Error.WriteLine("deref goal");

		  if (elrGoal != null)
		    {
		      Euler elrGd = elrGoal.deref();
		      bool b = mstep == -1 || step-istep < mstep*(engine-eng);
		      bool c = mstep == -1 || step-istep < mstep*(engine-eng+1);
		      bool d = hshtDds[elrGoal.verb] != null;
		      
		      EulerProofStep1( 
				      /*elrG,uri,b,c,d,tab,elrLr,elrTsb,elrGoal,stbldPp,elrTs,elrGd,stbldPc,elrEl,stack,vars*/
	  );
		    }
		  else
		    {		  
		      Console.Error.WriteLine("goal is null!");

		    }
		  
	    }

	}
	catch (Exception exc) {
	    Report.StackTrace(exc.StackTrace);
	    not = true;
	}
    }


    public virtual bool  CheckImpliesFalse(/*
					     Euler elrGoal, Euler[] vars, EStack stack, Parser np, Euler elrG, StringBuilder stbldPp,  int tab,StringBuilder stbldPv, Euler elrTsb
					   */
)
    {
	if (elrGoal.verb == LOGimplies ||
	    elrGoal.obj != null && elrGoal.obj.verb != null && elrGoal.obj.verb == LOGFalsehood) 
	    { // IMPLIES FALSHOOD
		

		// elrGoal subj.
		if (elrGoal.subj.subj != null && elrGoal.subj.obj != null) 
		    {
			  
			if (elrGoal.subj.varid != - 1 && elrGoal.subj.refr != null) 
			    {
				Euler elrGs = elrGoal.subj.refr.eval(vars, stack);
				elrGoal.subj.verb = elrGs.verb;
				elrGoal.subj.cverb = elrGs.cverb;
			    }
			String rk = "";

			Euler elrEl = np.Parse(LOGFalsehood);

			EulerProofWhile1(/*elrG,elrGoal, elrEl,stack,vars,np,stbldPv*/);


			if (elrG == null) {
				
			    if (!stbldPv.ToString().StartsWith(LOGFalsehood)) {
				    
				Indent(stbldPp,tab);					
				EmitGoal(/*stbldPp,stbldPv, elrGoal, ref tab*/);
				/*
				  { stbldPv } elrGoal.cverb (elrGoal.obj | {elrGoal.obj })
				*/
				    
			    }
			}
			else 
			    {
				not = true; // we got a problem!
			    }
			    
		    } // elrGoal.subj.null

		
		else if (elrGoal.obj.unify(elrGoal.subj, this, stack) || 
			 elrGoal.subj.obj.verb == LOGFalsehood) 
		    {
			EmitGoal(/*stbldPp,stbldPv,elrGoal,ref tab*/);
			/* elrGoal.subj elrGoal.cverb elrGoal.obj	*/
		    }
		else not = true;
	    }
	return not;
    }

    public virtual void EulerProofWhile1(/*
					   Euler elrG, Euler elrGoal, Euler elrEl, EStack stack,Euler[] vars,  Parser np, StringBuilder stbldPv, Euler elrTsb
					 */)
    {
	elrG = elrGoal.subj;

	// CHAIN ON : 
	while (elrG != null) {
	
	    Euler elrGs = elrG.eval(vars, stack);
	    Euler elrEp = elrGoal.near;
	
	    while (elrEp != null) { // was line 1101

		if ( // was line 1102
		    elrEp.verb == null 
		    && 
		    elrGoal.obj.verb == LOGFalsehood 
		    && 
		    elrEp.obj.unify(elrGs, this, null)
		    ) // TODO: break if we are at the end?
		    break;
		elrEp = elrEp.near;// was line 1103
	    }

	    // here the Proof mechanism called, the results are parsed
	    elrEl = ParseProof("data:," + Parent.stbldNsps + elrG.ToString(),elrEl, elrG, np);
    
// 	    // this call could be wrong!
// 	    if (!Unify( ts, stbldPc,  stbldPp, elrGoal, stack, vars))
// 		{
// 		    break;
// 		}

	    elrG = elrG.near;
	
	

	} // end of while
    }

    public virtual void EmitGoal(/*StringBuilder stbldPp, Euler elrGoal, ref int tab*/)
    {
      if (stbldPp.Length > 0 && stbldPp[stbldPp.Length - 1] == '.') {
	stbldPp.Append('\n');
	Indent(stbldPp,tab);
      }
	 
      stbldPp.Append(elrGoal.subj);
      stbldPp.Append(' ');
      stbldPp.Append(elrGoal.cverb);
      stbldPp.Append(' ');
	 
      if (elrGoal.obj.subj != null) stbldPp.Append('{');
	 
      stbldPp.Append(elrGoal.obj);
	 
      if (elrGoal.obj.subj != null) {
	if (stbldPp[stbldPp.Length - 1] == '.') stbldPp[stbldPp.Length - 1] = '}';
	else stbldPp.Append('}');
      }
	 
      stbldPp.Append('.');

    }

    public virtual void EmitSubGoal(/*StringBuilder stbldPp, StringBuilder stbldPv, Euler elrGoal, ref int tab */ )
    {
	stbldPp.Append('{');
	stbldPp.Append(stbldPv);
	 
	if (stbldPp[stbldPp.Length - 1] == '.') stbldPp[stbldPp.Length - 1] = '}';
	else stbldPp.Append('}');
	 
	stbldPp.Append(' ');
	stbldPp.Append(elrGoal.cverb);
	 
	if (elrGoal.obj.subj == null && elrGoal.obj.obj == null) {
	    stbldPp.Append(' ');
	    stbldPp.Append(elrGoal.obj);
	}
	else {
	    stbldPp.Append('\n');
	     
	    Indent(stbldPp,tab);
	     
	    stbldPp.Append('{');
	    stbldPp.Append(elrGoal.obj);
	     
	    if (stbldPp[stbldPp.Length - 1] == '.') stbldPp[stbldPp.Length - 1] = '}';
	    else stbldPp.Append('}');
	}
	stbldPp.Append('.');
    }

    public bool Unify(Euler elrGoal, Euler elrG, Euler elrEl, Euler parent,  EStack stack,StringBuilder stbldPv, ref int tab ,StringBuilder stbldPp, Euler elrTsb)
    {
	if (
	    (elrG.unify(elrEl, parent, stack) && 
	     elrGoal.obj.verb != LOGFalsehood) || 
	    elrGoal.obj.unify(elrEl, this, stack)) 
	    {

		if (stbldPv.Length > 0 && stbldPv[stbldPv.Length - 1] == '.') 
		    {
			stbldPv.Append('\n');
			Indent(stbldPp,tab);
		    }

		// emit
		if (elrGoal.obj.verb == LOGFalsehood) 
		    stbldPv.Append(elrG);
		else 
		    stbldPv.Append(elrEl);
		return true;

	    }
	return false;
		
    }

 
   // part of a proof
   //    int step;
   bool not = false;
     
   bool CheckRules(bool b, bool d, Euler elrTs, Euler elrGd)
     {
       String ts_verb = elrTs.verb.ToString();
 
       if ( b && 
 	   (ts_verb == LOGimplies) && 
 	   (elrTs.obj.verb == elrGd.verb) &&		
 	   (
 	    !d 
 	    || 
 	    elrTs.subj.subj.verb.StartsWith(
 					    "<http://www.agfa.com/w3c/euler/log-rules#rule1d"
 					    )
 	    )
 	   )
 	{
 	  return true;
 	}
       return false;
     }


    public void skolem(bool otmp, Euler ex, Euler nr, Parser np, StringBuilder stbldGen) {
	if (ex.obj == null || ex.verb == "^^") return ;
	Euler elrEl = ex.copy();

	if (ex.subj == null) {
	    
	    elrEl.subj = np.Parse("_:" + nr.GetHashCode() + "_" + doc);
	}

	if (ex.subj != null && ex.subj.subj == null && ex.subj.obj != null)
	    {
		elrEl.subj = np.Parse("_:" + ex.subj.GetHashCode() + "_" + doc);
	    }

	if (ex.obj != null && ex.obj.subj == null && ex.obj.obj != null)
	    {
		elrEl.obj = np.Parse("_:" + ex.obj.GetHashCode() + "_" + doc);
	    }


	if (ex.subj == null && !otmp && hshtOtm[ex.verb] == null && ex.near == null
	    // TODO && ex.getFirst() == null
	    ) {

	    Console.Error.WriteLine("going to parse Elabel" + Elabel);

	    ex.near = np.Parse(Elabel);
	    ex.near.obj = np.Parse("_:" + nr.GetHashCode() + "_" + doc);
	}
	
	stbldGen.Append(elrEl);
	if (ex.subj != null) 
	    {
		// recurse
		skolem(otmp, ex.subj, ex.subj, np, stbldGen);
	    }

	if (ex.obj != null) {
	    // recurse
	    skolem(otmp, ex.obj, ex.obj, np, stbldGen);
	}

	if (ex.subj == null && ex.near != null && !ex.near.verb.Equals(Elabel))	    
	    {
		// recurse
		skolem(otmp || hshtOtm[ex.verb] != null, ex.near, nr, np, stbldGen);
	    }
	np.swap(ex);
    }
  
  

  



  public virtual Euler ParseProof(String u, Euler elrEl, Euler elrG, Parser np) {
    String rk = this.Proof("data:," + stbldNsps + elrG.ToString());
    ArrayList vt = new ArrayList();
    np = new Parser(rk, vt, this, u);
    elrEl = np.Parse();
    syno(elrEl);     
    return elrEl;
  }

  //                  Push(Euler,      Euler,     Euler,   StringBuilder,    StringBuilder, int)'
  public virtual void Push(
			   Euler n
/*Euler elrGoal, Euler elrTsb, Euler n, StringBuilder stbldPp, StringBuilder stbldPc, int tab,EStack stack*/) {
    r.Push(n);
	 
    stack.push(elrGoal, 0);
    stack.push(elrTsb, 0);
    stack.push(n, 0);
    stack.push(null, stbldPp.Length);
    stack.push(null, stbldPc.Length);
    stack.push(null, tab);
  }

  bool b; 
  bool c;
  bool d;
  public virtual Euler EulerProofStep2(Euler next
				       /*
					 bool b, bool c,bool d, Euler elrTs, Euler elrGd, Euler next*/) 
    {
      Euler use; // the return value

      while (next != null) {
	use = next;
	     
	// next
	if (
	    CheckRules(b,d,elrTs,elrGd)
	    )
	  {    
	    use = use.obj;
	    return use;
	  }	    	     
	if (c && 
	    !d && 
	    use.verb == elrGd.verb) 
	  {
	    return use;
	  }		
	else 
	  {
	    next = next.near;
	  }		   
	use = null;
      }
      return use;
    }
	
    
  public virtual void EulerProofStep1(
				      /*Euler elrG,String uri,bool b, bool c,bool d,int tab, Euler elrLr, Euler elrTsb, Euler elrGoal, StringBuilder stbldPp, Euler elrTs,Euler elrGd,StringBuilder stbldPc, Euler elrEl, EStack stack, Euler [] vars*/) 
    {		    

      Euler elrN;

      if (elrTs == null) {
	elrLr = this.near;
	elrTs = EulerProofStep2(elrLr ); ///*b,c,d,elrTs,elrGd,*/);
      }
      else if (elrTs != null) {

	Euler elrN = elrLr.near;
	elrTsb = null;
	elrN = EulerProofStep2(elrN);  // /*b,c,d,elrTs,elrGd*/
      }
	
      if (elrTsb != null) {
	  Push(elrN); // /*elrGoal,elrTsb,elrN,stbldPp,stbldPc,tab, stack*/ ELRTSB is important
      }
	

      ResetVars(vars); // from Euler.cs 1098
	
      // this is ok 
      Unify( /*elrTs, stbldPc,  stbldPp, elrGoal,  stack, vars, ref tab, elrTsb*/);
      //EulerProof.cs:348: no matching method for call to 
      //Unify(Euler, StringBuilder, StringBuilder, Euler, EStack, Euler[], int)'
      //public virtual void 
      //Unify(Euler , StringBuilder , StringBuilder , Euler,  EStack, Euler[] , ref tab)

    }

  public virtual void ResetVars(Euler[] vars)
    {
      // from Euler.cs 1098
      for (int i = 0; i < varmax; i++) vars[i] = null;
    }

    


  public virtual void EmitSyn(Hashtable hshtPct, StringBuilder proof)
    {

      IEnumerator sen = (IEnumerator) hshtSyn.Keys.GetEnumerator();

      while (sen.MoveNext()) {
	Object sne = sen.Current;
	
	if (sne.Equals(Parent.hshtSyn[sne])) continue;
	
	proof.Append(sne);
	proof.Append(' ');
	proof.Append(OWLsameAs);
	proof.Append(' ');
	proof.Append(Parent.hshtSyn[sne]);
	proof.Append(" .\n");
      }

      proof.Append('\n');
      proof.Append("# Proof found for ");
    }

   int pns;
   int pn;
    public virtual bool IfGoalNotNull(/*Euler elrGoal, int pn, Hashtable hshtPct, StringBuilder proof, int pns , long istep*/)
    {
	if (elrGoal == null) { // same as line 429

	CurrentTime = DateTime.Now.Ticks - CurrentTime;

	if (stbldProof == null)
	  {
	    Console.Error.WriteLine("Made a new stbldProof");

	    stbldProof = new StringBuilder();
	  }
	if (stbldProof.Length == pns) {
	  stbldProof.Length = pn;
	  stbldProof.Append("# No proof found for ");
	}
	else {
	  EmitSyn(hshtPct, stbldProof);
	}

	stbldProof.Append(uri );
	stbldProof.Append(" in ").Append(step-istep).Append(step-istep==1?" step":" steps");
	stbldProof.Append(" (").Append((step-istep)*10000000L/CurrentTime).Append(" steps/sec)"); // @@ 100ns
	stbldProof.Append(" using ").Append(engine-eng).Append(engine-eng==1?" engine":" engines");
	stbldProof.Append('\n');

	conc = hshtPct;

	return true;
      }
      return false;
    }

  public bool CheckLogForSome(Euler elrG)
    {
      return false;
    }

  public virtual void MainProofLoop(Euler elrG, Parser np, ArrayList vt, long query)
    {

      Console.Error.WriteLine("MainProofLoop()");

      // the main proof loop
      while (true) { // line 340

	Console.Error.WriteLine("before parse");

	if (np != null)
	  {
	    try {
	      Console.Error.WriteLine("MainProofLoop()before parse!");
	      elrG.near = np.Parse();
	      Console.Error.WriteLine("MainProofLoop()Goal :" + elrGoal);
	      Console.Error.WriteLine("MainProofLoop()G:" + elrG);
	      Console.Error.WriteLine("MainProofLoop()Near" + elrG.near);
	    }
	    catch
	      {
		Console.Error.WriteLine("Exception!");
	      }

	  }
	else
	  {
	    Console.Error.WriteLine("parser is null");
	  }



	Console.Error.WriteLine("after parse");

	if (elrG.near == null) {

	  Console.Error.WriteLine("Near is null");

	  break; // we dont have anything
	}
	else
	    {
		Console.Error.WriteLine("Parse results" +  elrG);
	    }

	while (elrG.near != null && elrG.near.verb != null) { // ok, we have a predicate
	

	  Console.Error.WriteLine("Near is not null");

	  //		r.BeforeRewrite(elrEp,np);

	  //		rewrite(elrG.near, np); // rewrite this, so we need to have acces to the rdfstatement

	  Console.Error.WriteLine("before rewrite");

	  rewrite(elrG.near, np);

	  Console.Error.WriteLine("after rewrite");

		
	  {
	    r.AfterRewrite(elrG,np);
	  }

	  Console.Error.WriteLine("after rewrite");
	  if (CheckLogForSome(elrG))
	    {
	      // Look at Proof/LOGForSome.cs
	      LOGForSomeProof();
	    }
	  else {
	    elrG.near.getX(false, vt);
	    elrG.near.forX(false, vt);
	    if (vt.Count > varmax) varmax = vt.Count;
	    r.Query(elrG.near);
	    query++;
		    
	    // get the next
	    elrG = elrG.near;
	  }
	}
      }

      Console.Error.WriteLine("end of proof");

    }

    public void EmitSemanticsOpen(StringBuilder proof)
    {
        proof.Append("{\n (\n");
    }
    public void EmitSemanticsClose(StringBuilder proof)
    {
        proof.Append(" ).").Append(LOGconjunction).Append(" =>\n");
        proof.Append(" <").Append(baseURI).Append(">.").Append(LOGsemantics).Append("\n}\n");
        pn = proof.Length;
        proof.Append(WHYbecause).Append("\n{\n");

    }
  public void EmitKeys(StringBuilder proof)
    {
      IEnumerator enu = (IEnumerator) loaded.Keys.GetEnumerator();
      while (enu.MoveNext()) 
	{
	    //	  proof.Append(enu.Current).Append(' ');
          proof.Append(' ').Append(enu.Current).Append('.').Append(LOGsemantics).Append("\n");

	}

    }


    void EmitHeader(StringBuilder proof) // line 407
    {
      proof.Append("# Generated with http://www.agfa.com/w3c/euler/#").Append(version);
      proof.Append(" on ").Append(DateTime.UtcNow.ToString()).Append('\n');
      proof.Append("# for query ").Append(baseURI).Append('\n');
      proof.Append("# given ");
    }

  public virtual void EmitNamespaces(Hashtable ns)
    {
      if (ns != null)
	{
	  IEnumerator en = (IEnumerator) ns.Keys.GetEnumerator();
	  while (en.MoveNext()) {
	    Object nsx = en.Current;
	    stbldNsps.Append("@prefix ");
	    stbldNsps.Append(nsx);
	    stbldNsps.Append(' ');
	    stbldNsps.Append(ns[nsx]);
	    stbldNsps.Append(" .\n");
	  }
	  stbldNsps.Append('\n');
	}

    }

  public virtual void CheckOWLsameAs(String verb, Euler other)
    {
      if (verb == OWLsameAs) synon(other);
    }

    public virtual void  EmitImplies(/*StringBuilder stbldPp, Euler elrGoal, StringBuilder stbldPc, ref int tab */)
    {

	if (elrGoal == null)
	{
	      Console.Error.WriteLine("goal is null, returning");
	      return;
	}
	if (stbldPp == null)	
	{
	      Console.Error.WriteLine("stbldPp is null");
	      stbldPp = new StringBuilder();
	}
//stbldPc
	if (stbldPc == null)	
	{
	      Console.Error.WriteLine("stbldPc is null");
	      stbldPc = new StringBuilder();
	}

      CheckOWLsameAs(elrGoal.obj.verb,elrGoal.obj);
    
      tab--;
    
      if (stbldPp[stbldPp.Length - 1] == '.') stbldPp[stbldPp.Length - 1] = '}';
      else stbldPp.Append('}');

      stbldPp.Append(' ');
      //LOGimplies is quoted here,
      stbldPp.Append(LOGimpliesQN);
      stbldPp.Append('\n');
    
      Indent(stbldPp,tab);
    
      stbldPp.Append('{');
      stbldPp.Append(elrGoal.obj);
    
      if (stbldPp[stbldPp.Length - 1] == '.') stbldPp[stbldPp.Length - 1] = '}';
      else stbldPp.Append('}');
    
      stbldPp.Append('.');
    
      if (tab == 0) stbldPc.Append(elrGoal.obj).Append('\n');

    }


    public virtual void EmitLiteral(/*StringBuilder stbldPp, Euler elrGoal, ref int tab*/)
    {
      stbldPp.Append('\n');
	
      Indent(stbldPp,tab);
	
      //TODO:
      //pp.Append(getLit(elrGoal.subj)).Append(" .");
    }
     
  public virtual void  StackPop(
				/*
				  Euler elrGoal, Euler elrTs,
				  Euler[] vars, EStack stack, StringBuilder stbldPp,
				  StringBuilder stbldPc ,
				  Euler elrLr,
				  ref int tab
				*/
				)
    {
      Console.Error.WriteLine("StackPop");

      if (not || think && elrGoal == null) {
	elrGoal = null;
	Euler elrB = null;

	// pop untill we find an unbound variable

	while ((elrB = stack.pop()) != null) {

	  if (elrB.bound) {

	    // this gets deleted

	    elrB.bound = false; // unbind
	    elrB.refr = null;   // unlink
	  }
	  else {
	    // not bound at all
	    tab = elrB.varid;
	    stbldPc.Length = stack.pop().varid;
	    stbldPp.Length = stack.pop().varid;
			
	    elrLr = stack.pop();
	    elrTs = stack.pop();
	    elrGoal = stack.pop();

	    if (trace) 
	      r.Redo(step,elrGoal); 


	    break;
	  }
	}
      }
    }
   
  public virtual void LOGForSomeProof()
    {
      // Look at Proof/LOGForSome.cs
    }

  public virtual Euler NewStep(long step, Euler elrGoal, int hc)
    {
      // create a new euler, with variable ts1
      Euler tsnear = new Euler();
      tsnear.cverb = "[" + step + "]";
      tsnear.obj = elrGoal;
      tsnear.bound = true; // it is bound
      tsnear.varid = hc;        // from line 1124
      tsnear.near = elrGoal.near;  // from line 1125
      tsnear.far = elrGoal.far;    // from line 1126
      return tsnear; 
    }

  public virtual void  EvalGoals(
				 /*
				   Euler elrGoal, Euler elrTs,
				   Euler[] vars, EStack stack, StringBuilder stbldPp,
				   StringBuilder stbldPc ,
				   Euler elrLr, Euler elrTsb
				 */
) 
    {
	Console.Error.WriteLine("EvalGoals");
	if (elrGoal == null)
	    {		 
		 Console.Error.WriteLine("Goal is null");
		 //elrGoal = Parent.elrGoal;
		 //if (elrGoal == null)
		 //   {
			 Console.Error.WriteLine("Parent Goal is null");
			 elrGoal =new Euler();
			 //   }
		 

	    }
	Euler elrTe = elrGoal;
	while (elrTe.near != null) {
	    
	    Console.Error.WriteLine("Going to Eval elrTe.near" + elrTe.near);

	    elrTe.near = elrTe.near.eval(vars, stack); // line 422

	    Console.Error.WriteLine("After Eval elrTe.near" + elrTe.near);

	    elrTe = elrTe.near;
	}

	elrGoal = elrGoal.near; // line 425
    }

    public virtual void Unify(/*Euler elrTs, StringBuilder stbldPc, StringBuilder stbldPp, Euler elrGoal,  EStack stack, Euler[] vars, ref int tab, Euler elrTsb*/)
    {
      int hc = elrTs.GetHashCode();

      Euler elrT1;
      Euler elrT2;

      // from Euler.cs 1036 -- removed!!!
      if (elrTs.eval(vars, stack).unify(elrGoal, this, stack)) {   
	Euler elrEp = elrGoal.near;
	while (elrEp != null) {
	  if (elrEp.verb == null 
	      && 
	      hc == elrEp.varid 
	      &&  // unify here
	      elrEp.obj.unify(elrGoal, this, null)
	      )
	    break;
	  elrEp = elrEp.near; // line 1047  was line 1103
	}
    
	if (elrEp != null) {
	  //Euler.cs:1106 if (trace) Console.Error.WriteLine("@@ cycle (2) " + elrEp);
	  if (trace) r.Cycle(elrEp,2);
	  not = true;
	}
	else {
	  elrTs = elrTs.premis; // line 1056 -- was 1110 : diff -54 lines
	
	  if (elrTs != null) {

	    // this seems to set elrT1 to the empty elrT2, but copy the data.
	    elrTs2 = new Euler();

	    // set the elrTs1 to be empy, now, loop over the elrT.near
	    // call eval for each value of elrT
	    // and store the value in elrTs1.near
	    // the head of the chain is elrTs2
	    // the list is walked, each eval adding on new node 
	    // to the end. The near poinelrT to the end.?
	    elrTs1 = elrTs2;
	    while (elrTs != null) {

	    Console.Error.WriteLine("Going to Eval elrTs" + elrTs);

		elrT1.near = elrTs.eval(vars, stack); // 1059
		elrT1 = elrT1.near; // 1060
		elrTs = elrTs.near; // 1061
	    }

	    // create a new euler, with variable elrT1
	    elrTs1.near = NewStep(step,
				 elrGoal,
				 hc);

	    // the current elrT1, which is at the end, geelrT a new node
	    // next in the list!
	    elrTs1 = elrTs1.near; // was line 1120!

	    elrGoal = elrTs2; // line 1071(1.39)  -- was line 1125 
	    tab = Indent(stbldPp,tab); // lines 1128-1131
	  }
	  else {
	    // TOCUT OWLsameAs
	    CheckOWLsameAs(elrGoal.verb,elrGoal);
	    //if (elrGoal.verb == OWLsameAs) synon(elrGoal);

	    Indent(stbldPp,tab);
	    stbldPp.Append(elrGoal);
	    if (tab == 0) 
	      {
		stbldPc.Append(elrGoal).Append('\n');
	      }

	    // ENDCUT OWLsameAs
	  }
	}
      }
      else not = true; // END OF UNIFY
    }



  
 
};