// @copyright@
// This file is part of nzdis-kif package. See the file LICENSE for copyright information 
// and the terms and conditions for copying, distribution and modification of nzdis-kif package.

package nzdis.lang.kif.tool;

/**/
import nzdis.lang.kif.analysis.*;
import nzdis.lang.kif.node.*;
import java.util.*;
import java.io.*;

/**
 * Abstract Syntax Tree to ASCII converter. This class is
 * responsible for conversion the tree structure into ascii
 * well-formed KIF format.
 *
 *@author Mariusz Nowostawski
 *@version @version@ $Revision: 1.1 $
 */
class Kif2AsciiWalker extends DepthFirstAdapter {

  int indent = 0;
  StringBuffer result;

  // Geoff: this param says if a new line should be added preceding AKnowledgeBase. 
  boolean addNewLine = false;

  public void setPrefixNewLine(boolean newLine){
    this.addNewLine = newLine;
  }

  /**
   * Converts given Node and its tree structure into ascii. 
   *@param Node to be converted into ascii
   *@return ascii representation of the node and all its children
   */
  public StringBuffer toAscii(Node ast){
    result = new StringBuffer();
    ast.apply(this);
    return result;
  }

  /**
   * Produce empty string which length is len.
   */
  String giveIndent(int len){
    String s = new String ("");
    for(int i=0; i < len; i++) s += " "; 
    return s;
  }
    
  /** 
   * Top level kif tree node.
   */
  public void caseAKnowledgeBase(AKnowledgeBase node)
  {
    inAKnowledgeBase(node);
    {
      Object temp[] = node.getForm().toArray();
      for(int i = 0; i < temp.length; i++)
        {
          indent = 0;
          if(addNewLine)  // addNewLine stuff by GRB.
            result.append(" "); // changed from "\n" to  " " GRB
          addNewLine = true;
          ((PForm) temp[i]).apply(this);
        }
    }
    outAKnowledgeBase(node);
  }


  /****** Unrestricted definitions ***********/


  /**
   * Kif defobject unrestricted definition.
   */
  public void caseADefobjectUnrestricted(ADefobjectUnrestricted node)
  {
    inADefobjectUnrestricted(node);
    int begin_indent = indent;
    result.append("(defobject "); indent += 11;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    int local_indent = indent+1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString().trim();
      result.append(s);
      indent += s.length();
    }
    result.append(" "); indent += 1;

    Object temp[] = node.getSentence().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(temp.length > 1){
        result.append("\n").append(giveIndent(local_indent));
        indent = local_indent;
      }
      ((PSentence) temp[i]).apply(this);
    }
    if(temp.length > 1){
      result.append("\n").append(giveIndent(begin_indent)).append(")");
      indent = begin_indent+1;
    }
    else
      result.append(")"); indent += 1;
    outADefobjectUnrestricted(node);
  }

  /**
   * Kif deffunction unrestricted definition.
   */
  public void caseADeffunctionUnrestricted(ADeffunctionUnrestricted node)
  {
    inADeffunctionUnrestricted(node);
    int begin_indent = indent;
    result.append("(deffunction "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    int local_indent = indent+1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString().trim();
      result.append(s);
      indent += s.length();
    }
    result.append(" "); indent += 1;

    Object temp[] = node.getSentence().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(temp.length > 1){
        result.append("\n").append(giveIndent(local_indent));
        indent = local_indent;
      }
      ((PSentence) temp[i]).apply(this);
    }
    if(temp.length > 1){
      result.append("\n").append(giveIndent(begin_indent)).append(")");
      indent = begin_indent+1;
    }
    else
      result.append(")"); indent += 1;
    outADeffunctionUnrestricted(node);
  }

  /**
   * Kif defrelation unrestricted definition.
   */
  public void caseADefrelationUnrestricted(ADefrelationUnrestricted node)
  {
    inADefrelationUnrestricted(node);

    int begin_indent = indent;
    result.append("(defrelation "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    int local_indent = indent+1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString().trim();
      result.append(s);
      indent += s.length();
    }
    result.append(" "); indent += 1;

    Object temp[] = node.getSentence().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(temp.length > 1){
        result.append("\n").append(giveIndent(local_indent));
        indent = local_indent;
      }
      ((PSentence) temp[i]).apply(this);
    }
    if(temp.length > 1){
      result.append("\n");
      result.append(giveIndent(begin_indent)).append(")");
      indent = begin_indent+1;
    }
    else
      result.append(")"); indent += 1;
    outADefrelationUnrestricted(node);
  }

  /** 
   * Kif deflogical unrestricted definition.
   */
  public void caseADeflogicalUnrestricted(ADeflogicalUnrestricted node)
  {
    inADeflogicalUnrestricted(node);
    int begin_indent = indent;
    result.append("(deflogical "); indent += 12;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    int local_indent = indent+1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString().trim();
      result.append(s);
      indent += s.length();
    }
    result.append(" "); indent += 1;

    Object temp[] = node.getSentence().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(temp.length > 1){
        result.append("\n").append(giveIndent(local_indent));
        indent = local_indent;
      }
      ((PSentence) temp[i]).apply(this);
    }
    if(temp.length > 1){
      result.append("\n").append(giveIndent(begin_indent)).append(")\n");
      result.append(giveIndent(begin_indent));
      indent = begin_indent;
    }
    else
      result.append(")"); indent += 1;
    outADeflogicalUnrestricted(node);
  }



  /****** Complete definitions ***********/

  /**
   * Kif defobject complete definition
   */
  public void caseADefobjectComplete(ADefobjectComplete node)
  {
    inADefobjectComplete(node);

    int begin_indent = indent;
    result.append("(defobject "); indent += 11;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString();
      result.append(s);
      indent += s.length();
    }
    result.append(" := "); indent += 4;
    if(node.getTerm() != null) {
      node.getTerm().apply(this);
    }
    result.append(")"); indent += 1;

    outADefobjectComplete(node);
  }

  /**
   * Kif deffunction complete definition
   */
  public void caseADeffunctionComplete(ADeffunctionComplete node)
  {
    inADeffunctionComplete(node);
        
    int begin_indent = indent;
    result.append("(deffunction "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    result.append(" ("); indent += 2;
    Object temp[] = node.getIndvar().toArray();
    for(int i = 0; i < temp.length; i++) {
      ((PIndvar) temp[i]).apply(this);
    }
    result.append(")"); indent += 1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString();
      result.append(s);
      indent += s.length();
    }
    result.append(" := "); indent += 4;
    if(node.getTerm() != null) {
      node.getTerm().apply(this);
    }
    result.append(")"); indent += 1;

    outADeffunctionComplete(node);
  }

  /**
   * Kif defrelation complete definition
   */
  public void caseADefrelationComplete(ADefrelationComplete node)
  {
    inADefrelationComplete(node);
                
    int begin_indent = indent;
    result.append("(defrelation "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }
    result.append(" ("); indent += 2;
    Object temp[] = node.getIndvar().toArray();
    for(int i = 0; i < temp.length; i++) {
      ((PIndvar) temp[i]).apply(this);
    }
    result.append(")"); indent += 1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString();
      result.append(s);
      indent += s.length();
    }
    result.append(" := "); indent += 4;

    if(node.getSentence() != null) {
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;

    outADefrelationComplete(node);
  }

  /**
   * Kif deflogical complete definition
   */    
  public void caseADeflogicalComplete(ADeflogicalComplete node)
  {
    inADeflogicalComplete(node);
                
    int begin_indent = indent;
    result.append("(deflogical "); indent += 12;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString();
      result.append(s);
      indent += s.length();
    }
    result.append(" := "); indent += 4;

    if(node.getSentence() != null) {
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;

    outADeflogicalComplete(node);
  }


  /******* Partial definitions *************/

  /**
   *
   */
  public void caseADefobjectLPartial(ADefobjectLPartial node)
  {
    inADefobjectLPartial(node);

    result.append("(defobject "); indent += 11;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString();
      result.append(s);
      indent += s.length();
    }
    result.append(" :-> "); indent += 4;

    if(node.getIndvar() != null){
      node.getIndvar().apply(this);
    }
    if(node.getColDblLArrow() != null) {
      node.getColDblLArrow().apply(this);
    }
    if(node.getSentence() != null){
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;

    outADefobjectLPartial(node);
  }

  /**
   * Kif defobject partial definition with right arrow.
   */
  public void caseADefobjectRPartial(ADefobjectRPartial node)
  {
    inADefobjectRPartial(node);
    result.append("(defobject "); indent += 11;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString();
      result.append(s);
      indent += s.length();
    }
    result.append(" :-> "); indent += 4;

    if(node.getIndvar() != null){
      node.getIndvar().apply(this);
    }
    if(node.getColDblRArrow() != null) {
      node.getColDblRArrow().apply(this);
    }
    if(node.getSentence() != null){
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outADefobjectRPartial(node);
  }

  /**
   * Kif deflogical partial definition with left arrow.
   */
  public void caseADeflogicalLPartial(ADeflogicalLPartial node) {
    inADeflogicalLPartial(node);

    result.append("(deflogical "); indent += 12;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString().trim();
      result.append(s);
      indent += s.length();
    }

    if(node.getColDblLArrow() != null) {
      node.getColDblLArrow().apply(this);
    }
    if(node.getSentence() != null){
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outADeflogicalLPartial(node);
  }

  /**
   * Kif deflogical partial definition with right arrow.
   */
  public void caseADeflogicalRPartial(ADeflogicalRPartial node) {
    inADeflogicalRPartial(node);
    result.append("(deflogical "); indent += 12;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    if(node.getString() != null) {
      result.append(" "); indent += 1;
      String s = node.getString().toString().trim();
      result.append(s);
      indent += s.length();
    }

    if(node.getColDblRArrow() != null) {
      node.getColDblRArrow().apply(this);
    }
    if(node.getSentence() != null){
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outADeflogicalRPartial(node);
  }

  /**
   * Kif deffunction partial definition with left arrow.
   */
  public void caseADeffunctionLPartial(ADeffunctionLPartial node) {
    inADeffunctionLPartial(node);
    result.append("(deffunction "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }
    result.append("("); indent += 1;
    Object temp[] = node.getIndvar().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(i>0) result.append(" "); indent += 1;
      ((PIndvar) temp[i]).apply(this);
    }
    if(node.getSeqvar() != null) {
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")"); indent += 1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      node.getString().toString().trim();
    }
    if(node.getColRArrow() != null) {
      result.append(" "); indent += 1;
      node.getColRArrow().apply(this);
    }
    if(node.getA() != null) {
      result.append(" "); indent += 1;
      node.getA().apply(this);
    }
    if(node.getColDblLArrow() != null) {
      result.append(" "); indent += 1;
      node.getColDblLArrow().apply(this);
    }
    if(node.getSentence() != null) {
      result.append(" "); indent += 1;
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outADeffunctionLPartial(node);
  }

  /**
   * Kif deffunction partial definition with right arrow.
   */
  public void caseADeffunctionRPartial(ADeffunctionRPartial node)
  {
    inADeffunctionRPartial(node);
    result.append("(deffunction "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }
    result.append("("); indent += 1;
    Object temp[] = node.getIndvar().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(i>0) result.append(" "); indent += 1;
      ((PIndvar) temp[i]).apply(this);
    }
    if(node.getSeqvar() != null) {
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")"); indent += 1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      node.getString().toString().trim();
    }
    if(node.getColRArrow() != null) {
      result.append(" "); indent += 1;
      node.getColRArrow().apply(this);
    }
    if(node.getA() != null) {
      result.append(" "); indent += 1;
      node.getA().apply(this);
    }
    if(node.getColDblRArrow() != null) {
      result.append(" "); indent += 1;
      node.getColDblRArrow().apply(this);
    }
    if(node.getSentence() != null) {
      result.append(" "); indent += 1;
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outADeffunctionRPartial(node);
  }

  /**
   * Kif defrelation partial definition with left arrow.
   */
  public void caseADefrelationLPartial(ADefrelationLPartial node)
  {
    inADefrelationLPartial(node);
    result.append("(deffunction "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }
    result.append("("); indent += 1;
    Object temp[] = node.getIndvar().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(i>0) result.append(" "); indent += 1;
      ((PIndvar) temp[i]).apply(this);
    }
    if(node.getSeqvar() != null) {
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")"); indent += 1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      node.getString().toString().trim();
    }
    if(node.getColDblLArrow() != null) {
      result.append(" "); indent += 1;
      node.getColDblLArrow().apply(this);
    }
    if(node.getSentence() != null) {
      result.append(" "); indent += 1;
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outADefrelationLPartial(node);
  }

  /**
   * Kif defrelation partial definition with right arrow.
   */
  public void caseADefrelationRPartial(ADefrelationRPartial node)
  {
    inADefrelationRPartial(node);
    result.append("(defrelation "); indent += 13;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }
    result.append("("); indent += 1;
    Object temp[] = node.getIndvar().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(i>0) result.append(" "); indent += 1;
      ((PIndvar) temp[i]).apply(this);
    }
    if(node.getSeqvar() != null) {
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")"); indent += 1;
    if(node.getString() != null) {
      result.append(" "); indent += 1;
      node.getString().toString().trim();
    }
    if(node.getColDblRArrow() != null) {
      result.append(" "); indent += 1;
      node.getColDblRArrow().apply(this);
    }
    if(node.getSentence() != null) {
      result.append(" "); indent += 1;
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outADefrelationRPartial(node);
  }



  /******* Equation *******/

  /**
   * Kif equation node.
   */
  public void caseAEquation(AEquation node)
  {
    inAEquation(node);

    result.append("(= "); indent += 3;
    if(node.getLeft() != null) {
      node.getLeft().apply(this);
    }
    result.append(" "); indent += 1;
    if(node.getRight() != null) {
      node.getRight().apply(this);
    }
    result.append(")");
    indent += 1;

    outAEquation(node);
  }

  /**
   * Kif inequality node.
   */
  public void caseAInequality(AInequality node)
  {
    inAInequality(node);

    result.append("(/= "); indent += 4;
    if(node.getLeft() != null) {
      node.getLeft().apply(this);
    }
    result.append(" "); indent += 1;
    if(node.getRight() != null) {
      node.getRight().apply(this);
    }
    result.append(")"); 
    indent += 1;

    outAInequality(node);
  }

  /****** Relations *********/

  /**
   * Kif implicit relsent node.
   */
  public void caseAImplicitRelsent(AImplicitRelsent node)
  {
    inAImplicitRelsent(node);
                
    int begin_indent = indent;
    result.append("("); indent += 1;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    Object temp[] = node.getTerm().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PTerm) temp[i]).apply(this);
    }
	
    if(node.getSeqvar() != null){
      result.append(" seq "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")");
    indent += 1;

    outAImplicitRelsent(node);
  }

  /**
   * Kif implicit relsent node.
   */
  public void caseAExplicitRelsent(AExplicitRelsent node)
  {
    inAExplicitRelsent(node);

    result.append("(holds "); indent += 7;

    if(node.getFirst() != null) {
      node.getFirst().apply(this);
    }
    Object temp[] = node.getRest().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PTerm) temp[i]).apply(this);
    }
	
    if(node.getSeqvar() != null){
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")");
    indent += 1;        

    outAExplicitRelsent(node);
  }

  /******** Strings,  variables, constants  *********/

  /**
   * Kif string term.
   */
  public void caseAStringTerm(AStringTerm node) {
    inAStringTerm(node);
    if(node.getString() != null) {
      String s = node.getString().toString().trim();
      result.append(s);
      indent += s.length();
    }
    outAStringTerm(node);
  }

  /**
   * Kif indvar node.
   */    
  public void caseAIndvar(AIndvar node) {
    inAIndvar(node);
    if(node.getTIndvar() != null){
      String s = node.getTIndvar().toString().trim();
      result.append(s); indent += s.length();
    }
    outAIndvar(node);
  }

  /**
   * Kif seqvar node.
   */
  public void caseASeqvar(ASeqvar node) {
    inASeqvar(node);
    if(node.getTSeqvar() != null){
      String s = node.getTSeqvar().toString().trim();
      result.append(s); indent += s.length();
    }
    outASeqvar(node);
  }

  /**
   * Kif constant node.
   *
   public void caseAConstant(AConstant node){
   inAConstant(node);
   if(node.getConstantWord() != null) {
   String s = node.getConstantWord().toString().trim();
   result.append(s); indent += s.length();
   }
   outAConstant(node);
   }
  */

  /**
   * Kif word identifier.
   */
  public void caseAWordIdentifier(AWordIdentifier node) {
    inAWordIdentifier(node);
    if(node.getWord() != null) {
      String s = node.getWord().toString().trim();
      result.append(s); indent += s.length();
    }
    outAWordIdentifier(node);
  }



  /********* funterm listterm **********/

  /**
   * Kif implicit funterm node.
   */
  public void caseAImplicitFunterm(AImplicitFunterm node)
  {
    inAImplicitFunterm(node);
                
    result.append("("); indent += 1;
    if(node.getConstant() != null) {
      node.getConstant().apply(this);
    }

    Object temp[] = node.getTerm().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PTerm) temp[i]).apply(this);
    }

    if(node.getSeqvar() != null){
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")");
    indent += 1;        

    outAImplicitFunterm(node);
  }

  /**
   * Kif explicit funterm node.
   */
  public void caseAExplicitFunterm(AExplicitFunterm node)
  {
    inAExplicitFunterm(node);
                
    result.append("(value "); indent += 7;
    if(node.getFirst() != null){
      node.getFirst().apply(this);
    }

    Object temp[] = node.getRest().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PTerm) temp[i]).apply(this);
    }

    if(node.getSeqvar() != null){
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")");
    indent += 1;        

    outAExplicitFunterm(node);
  }


  /**
   * Kif listterm node.
   */
  public void caseAListterm(AListterm node)
  {
    inAListterm(node);

    result.append("(listof "); indent += 8;
    Object temp[] = node.getTerm().toArray();
    for(int i = 0; i < temp.length; i++) {
      ((PTerm) temp[i]).apply(this);
    }

    if(node.getSeqvar() != null) {
      result.append(" "); indent += 1;
      node.getSeqvar().apply(this);
    }
    result.append(")");

    outAListterm(node);
  }



  /**********  If and Cond  statements **********8/

               /**
                * Kif if statement node.
                */
  public void caseAIfLogterm(AIfLogterm node)
  {
    inAIfLogterm(node);

    result.append("(if "); indent += 4;
    if(node.getSentence() != null){
      node.getSentence().apply(this);
    }
    if(node.getTrue() != null) {
      result.append(" "); indent += 1;
      node.getTrue().apply(this);
    }
    if(node.getFalse() != null) {
      result.append(" "); indent += 1;
      node.getFalse().apply(this);
    }
    result.append(")"); indent += 1;
    outAIfLogterm(node);
  }

  /**
   * Kif cond conditional sentence node.
   */
  public void caseACondLogterm(ACondLogterm node)
  {
    inACondLogterm(node);
    result.append("(cond"); indent += 5;
    Object temp[] = node.getLogitem().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PLogitem) temp[i]).apply(this);
    }
    result.append(")"); indent += 1;
    outACondLogterm(node);
  }

  /**
   * Kif single element of conditional sentence.
   */
  public void caseALogitem(ALogitem node)
  {
    inALogitem(node);

    result.append("("); indent += 1;
    if(node.getSentence() != null) {
      node.getSentence().apply(this);
    }
    if(node.getTerm() != null) {
      result.append(" "); indent += 1;
      node.getTerm().apply(this);
    }
    result.append(")"); indent += 1;
    outALogitem(node);
  }



  /********** Logocal sentences: not and or <= => <=> **********/

  /**
   * Kif negation longsent note.
   */
  public void caseANegationLogsent(ANegationLogsent node)
  {
    inANegationLogsent(node);

    result.append("(not "); indent += 5;
    if(node.getSentence() != null) {
      node.getSentence().apply(this);
    }
    result.append(")"); indent += 1;
    outANegationLogsent(node);
  }

  /**
   * Kif conjunction longsent node.
   */
  public void caseAConjunctionLogsent(AConjunctionLogsent node)
  {
    inAConjunctionLogsent(node);
    result.append("(and "); indent += 5;
    Object temp[] = node.getSentence().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PSentence) temp[i]).apply(this);
    }
    result.append(")"); indent += 1;
    outAConjunctionLogsent(node);
  }

 
  /**
   * Kif disjunction longsent node.
   */
  public void caseADisjunctionLogsent(ADisjunctionLogsent node)
  {
    inADisjunctionLogsent(node);

    result.append("(or "); indent += 4;
    Object temp[] = node.getSentence().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PSentence) temp[i]).apply(this);
    }
    result.append(")"); indent += 1;

    outADisjunctionLogsent(node);
  }

  /**
   * Kif implication node.
   */
  public void caseAImplicationLogsent(AImplicationLogsent node)
  {
    inAImplicationLogsent(node);

    int begin_indent = indent;
    result.append("(=>"); indent += 3;
	
    Object temp[] = node.getRest().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PSentence) temp[i]).apply(this);
    }
    result.append("\n").append(giveIndent(begin_indent+4));
    if(node.getLast() != null) {
      node.getLast().apply(this);
    }
    result.append(")");
    indent = begin_indent;

    outAImplicationLogsent(node);
  }

  /**
   * Kif reverse implication node.
   */
  public void caseAReverseImplicationLogsent(AReverseImplicationLogsent node)
  {
    inAReverseImplicationLogsent(node);

    int begin_indent = indent;
    result.append("(<= "); indent += 4;

    if(node.getFirst() != null){
      node.getFirst().apply(this);
    }
    result.append("\n").append(giveIndent(begin_indent+3));
    Object temp[] = node.getRest().toArray();
    for(int i = 0; i < temp.length; i++) {
      result.append(" "); indent += 1;
      ((PSentence) temp[i]).apply(this);
    }
    result.append(")");
    indent = begin_indent;

    outAReverseImplicationLogsent(node);
  }

  /**
   * Kif equivalence sentence node.
   */
  public void caseAEquivalenceLogsent(AEquivalenceLogsent node)
  {
    inAEquivalenceLogsent(node);

    result.append("(<=> "); indent += 5;
    if(node.getFirst() != null) {
      node.getFirst().apply(this);
    }
    result.append(" "); indent += 1;
    if(node.getLast() != null) {
      node.getLast().apply(this);
    }
    result.append(")"); indent += 1;
    outAEquivalenceLogsent(node);
  }

  /**
   * Kif universal quantsent. This method is responsible for processing
   * '(forall ...)' sentences.
   */
  public void caseAUniversalQuantsent(AUniversalQuantsent node)
  {
    inAUniversalQuantsent(node);

    result.append("(forall ("); indent += 9;
    Object temp[] = node.getVarspec().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(i>0) result.append(" "); indent += 1;
      ((PVarspec) temp[i]).apply(this);
    }
    result.append(") "); indent += 2;

    if(node.getSentence() != null) {
      node.getSentence().apply(this);
    }
    result.append(")"); indent +=1;

    outAUniversalQuantsent(node);
  }

  /**
   * Kif existential quantsent. This method is responsible for processing
   * '(exists ...)' sentences
   */
  public void caseAExistentialQuantsent(AExistentialQuantsent node)
  {
    inAExistentialQuantsent(node);

    result.append("(exists ("); indent += 9;
    Object temp[] = node.getVarspec().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(i>0) result.append(" "); indent += 1;
      ((PVarspec) temp[i]).apply(this);
    }
    result.append(") "); indent += 2;

    if(node.getSentence() != null) {
      node.getSentence().apply(this);
    }
    result.append(")"); indent +=1;
    outAExistentialQuantsent(node);
  }


  /********** quotations ***********/

  /**
   * Kif parenthesized quotation.
   */
  public void caseAParQuoterm(AParQuoterm node)
  {
    inAParQuoterm(node);
    result.append("(quote "); indent += 7;

    if(node.getListexpr() != null) {
      node.getListexpr().apply(this);
    }

    result.append(")"); indent += 1;
    outAParQuoterm(node);
  }

  /**
   * Kif quotation mark: '
   */
  public void caseASimple1Quoterm(ASimple1Quoterm node) {
    inASimple1Quoterm(node);
    result.append("'"); indent += 1;
    if(node.getListexpr() != null){
      node.getListexpr().apply(this);
    }
    outASimple1Quoterm(node);
  }
  /**
   * Kif quotation mark: ^
   */
  public void caseASimple2Quoterm(ASimple2Quoterm node) {
    inASimple2Quoterm(node);
    result.append("^"); indent += 1;
    if(node.getListexpr() != null){
      node.getListexpr().apply(this);
    }
    outASimple2Quoterm(node);
  }

  /**
   * Kif quoted indvar term.
   */
  public void caseAIndvarListexpr(AIndvarListexpr node) {
    inAIndvarListexpr(node);
    if(node.getIndvar() != null) {
      String s = node.getIndvar().toString().trim();
      result.append(s); indent += s.length();
    }
    outAIndvarListexpr(node);
  }

  /**
   * Kif quoted seqvar term.
   */
  public void caseASeqvarListexpr(ASeqvarListexpr node) {
    inASeqvarListexpr(node);
    if(node.getSeqvar() != null) {
      String s = node.getSeqvar().toString().trim();
      result.append(s); indent += s.length();
    }
    outASeqvarListexpr(node);
  }

  /**
   * Kif quoted word node.
   */
  public void caseAWordListexpr(AWordListexpr node) {
    inAWordListexpr(node);
    if(node.getWord() != null) {
      String s = node.getWord().toString().trim();
      result.append(s); indent += s.length();
    }
    outAWordListexpr(node);
  }

  /**
   * Kif quoted string node.
   */
  public void caseAStringListexpr(AStringListexpr node) {
    inAStringListexpr(node);
    if(node.getString() != null){
      String s = node.getString().toString().trim();
      result.append(s); indent += s.length();
    }
    outAStringListexpr(node);
  }

  /**
   * Kif quoted charref node.
   */
  public void caseACharrefListexpr(ACharrefListexpr node) {
    inACharrefListexpr(node);
    if(node.getCharref() != null) {
      String s = node.getCharref().toString().trim();
      result.append(s); indent += s.length();
    }
    outACharrefListexpr(node);
  }

  /**
   * Kif quoted reference to seqvar, e.g. <term> ,@var</term>
   */
  public void caseASeqvarRefListexpr(ASeqvarRefListexpr node)
  {
    inASeqvarRefListexpr(node);
    if(node.getRefSeqvar() != null){
      String s = node.getRefSeqvar().toString().trim();
      result.append(s); indent += s.length();
    }
    outASeqvarRefListexpr(node);
  }

  /**
   * Kif quoted reference to indvar, e.g. <term> ,?var</term>
   */
  public void caseAIndvarRefListexpr(AIndvarRefListexpr node)
  {
    inAIndvarRefListexpr(node);
    if(node.getRefIndvar() != null) {
      String s = node.getRefIndvar().toString().trim();
      result.append(s); indent += s.length();
    }
    outAIndvarRefListexpr(node);
  }

  /**
   * Kif quoted subexpression list.
   */
  public void caseAMultiListexpr(AMultiListexpr node) {
    inAMultiListexpr(node);

    result.append("("); indent += 1;
    Object temp[] = node.getListexpr().toArray();
    for(int i = 0; i < temp.length; i++) {
      if(i>0) result.append(" ");
      ((PListexpr) temp[i]).apply(this);
    }
    result.append(")"); indent += 1;

    outAMultiListexpr(node);
  }

  /**
   * Defined symbol '='. This node is used in quoted expressions.
   */
  public void caseAEqDefined(AEqDefined node) {
    inAEqDefined(node);
    if(node.getEq() != null) {
      String s = node.getEq().toString().trim();
      result.append(s); indent += s.length();
    }
    outAEqDefined(node);
  }

  /**
   * Defined symbol '/='. This node is used in quoted expressions.
   */
  public void caseAIneqDefined(AIneqDefined node)
  {
    inAIneqDefined(node);
    if(node.getIneq() != null) {
      String s = node.getIneq().toString().trim();
      result.append(s); indent += s.length();
    }
    outAIneqDefined(node);
  }

  /**
   * Defined symbol '@'. This node is used in quoted expressions.
   */
  public void caseAAtDefined(AAtDefined node) {
    inAAtDefined(node);
    if(node.getAt() != null) {
      String s = node.getAt().toString().trim();
      result.append(s); indent += s.length();
    }
    outAAtDefined(node);
  }

  /**
   * Defined symbol '?'. This node is used in quoted expressions.
   */
  public void caseAQMarkDefined(AQMarkDefined node) {
    inAQMarkDefined(node);
    if(node.getQMark() != null) {
      String s = node.getQMark().toString().trim();
      result.append(s); indent += s.length();
    }
    outAQMarkDefined(node);
  }
  /**
   * Defined symbol ':='. This node is used in quoted expressions.
   */
  public void caseAColEqDefined(AColEqDefined node) {
    inAColEqDefined(node);
    if(node.getColEq() != null) {
      String s = node.getColEq().toString().trim();
      result.append(s); indent += s.length();
    }
    outAColEqDefined(node);
  }
  /**
   * Defined symbol 'quote'. This node is used in quoted expressions.
   */
  public void caseAQuoteDefined(AQuoteDefined node) {
    inAQuoteDefined(node);
    if(node.getQuote() != null) {
      String s = node.getQuote().toString().trim();
      result.append(s); indent += s.length();
    }
    outAQuoteDefined(node);
  }
  /**
   * Defined symbol 'defobject'. This node is used in quoted expressions.
   */
  public void caseADefobjectDefined(ADefobjectDefined node){
    inADefobjectDefined(node);
    if(node.getDefobject() != null) {
      String s = node.getDefobject().toString().trim();
      result.append(s); indent += s.length();
    }
    outADefobjectDefined(node);
  }
  /**
   * Defined symbol 'deffunction'. This node is used in quoted expressions.
   */
  public void caseADeffunctionDefined(ADeffunctionDefined node) {
    inADeffunctionDefined(node);
    if(node.getDeffunction() != null) {
      String s = node.getDeffunction().toString().trim();
      result.append(s); indent += s.length();
    }
    outADeffunctionDefined(node);
  }
  /**
   * Defined symbol 'defrelation'. This node is used in quoted expressions.
   */
  public void caseADefrelationDefined(ADefrelationDefined node) {
    inADefrelationDefined(node);
    if(node.getDefrelation() != null) {
      String s = node.getDefrelation().toString().trim();
      result.append(s); indent += s.length();
    }
    outADefrelationDefined(node);
  }
  /**
   * Defined symbol 'deflogical'. This node is used in quoted expressions.
   */
  public void caseADeflogicalDefined(ADeflogicalDefined node){
    inADeflogicalDefined(node);
    if(node.getDeflogical() != null) {
      String s = node.getDeflogical().toString().trim();
      result.append(s); indent += s.length();
    }
    outADeflogicalDefined(node);
  }
  /**
   * Defined symbol 'not'. This node is used in quoted expressions.
   */
  public void caseANotDefined(ANotDefined node) {
    inANotDefined(node);
    if(node.getNot() != null) {
      String s = node.getNot().toString().trim();
      result.append(s); indent += s.length();
    }
    outANotDefined(node);
  }
  /**
   * Defined symbol 'and'. This node is used in quoted expressions.
   */
  public void caseAAndDefined(AAndDefined node){
    inAAndDefined(node);
    if(node.getAnd() != null) {
      String s = node.getAnd().toString().trim();
      result.append(s); indent += s.length();
    }
    outAAndDefined(node);
  }
  /**
   * Defined symbol 'or'. This node is used in quoted expressions.
   */
  public void caseAOrDefined(AOrDefined node){
    inAOrDefined(node);
    if(node.getOr() != null) {
      String s = node.getOr().toString().trim();
      result.append(s); indent += s.length();
    }
    outAOrDefined(node);
  }
  /**
   * Defined symbol '=>'. This node is used in quoted expressions.
   */
  public void caseADblRArrowDefined(ADblRArrowDefined node) {
    inADblRArrowDefined(node);
    if(node.getDblRArrow() != null) {
      String s = node.getDblRArrow().toString().trim();
      result.append(s); indent += s.length();
    }
    outADblRArrowDefined(node);
  }
  /**
   * Defined symbol '<='. This node is used in quoted expressions.
   */
  public void caseADblLArrowDefined(ADblLArrowDefined node) {
    inADblLArrowDefined(node);
    if(node.getDblLArrow() != null){
      String s = node.getDblLArrow().toString().trim();
      result.append(s); indent += s.length();
    }
    outADblLArrowDefined(node);
  }
  /**
   * Defined symbol '<=>'. This node is used in quoted expressions.
   */
  public void caseAArrowDblArrowDefined(AArrowDblArrowDefined node) {
    inAArrowDblArrowDefined(node);
    if(node.getArrowDblArrow() != null) {
      String s = node.getArrowDblArrow().toString().trim();
      result.append(s); indent += s.length();
    }
    outAArrowDblArrowDefined(node);
  }

  /**
   * Defined symbol ':=>'. This node is used in quoted expressions.
   */
  public void caseAColDblRArrowDefined(AColDblRArrowDefined node)
  {
    inAColDblRArrowDefined(node);
    if(node.getColDblRArrow() != null) {
      String s = node.getColDblRArrow().toString().trim();
      result.append(s); indent += s.length();
    }
    outAColDblRArrowDefined(node);
  }
  /**
   * Defined symbol ':<='. This node is used in quoted expressions.
   */
  public void caseAColDblLArrowDefined(AColDblLArrowDefined node){
    inAColDblLArrowDefined(node);
    if(node.getColDblLArrow() != null) {
      String s = node.getColDblLArrow().toString().trim();
      result.append(s); indent += s.length();
    }
    outAColDblLArrowDefined(node);
  }
  /**
   * Defined symbol ':->'. This node is used in quoted expressions.
   */
  public void caseAColRArrowDefined(AColRArrowDefined node) {
    inAColRArrowDefined(node);
    if(node.getColRArrow() != null) {
      String s = node.getColRArrow().toString().trim();
      result.append(s); indent += s.length();
    }
    outAColRArrowDefined(node);
  }

  /** 
   * Defined symbol 'if'. This node is used in quoted expressions.
   */
  public void caseAIfDefined(AIfDefined node) {
    inAIfDefined(node);
    if(node.getIf() != null) {
      String s = node.getIf().toString().trim();
      result.append(s); indent += s.length();
    }
    outAIfDefined(node);
  }
  /** 
   * Defined symbol 'cond'. This node is used in quoted expressions.
   */
  public void caseACondDefined(ACondDefined node) {
    inACondDefined(node);
    if(node.getCond() != null) {
      String s = node.getCond().toString().trim();
      result.append(s); indent += s.length();
    }
    outACondDefined(node);
  }
  /** 
   * Defined symbol 'value'. This node is used in quoted expressions.
   */
  public void caseAValueDefined(AValueDefined node) {
    inAValueDefined(node);
    if(node.getValue() != null) {
      String s = node.getValue().toString().trim();
      result.append(s); indent += s.length();
    }
    outAValueDefined(node);
  }
  /** 
   * Defined symbol 'listof'. This node is used in quoted expressions.
   */
  public void caseAListofDefined(AListofDefined node) {
    inAListofDefined(node);
    if(node.getListof() != null) {
      String s = node.getListof().toString().trim();
      result.append(s); indent += s.length();
    }
    outAListofDefined(node);
  }
  /** 
   * Defined symbol 'holds'. This node is used in quoted expressions.
   */
  public void caseAHoldsDefined(AHoldsDefined node) {
    inAHoldsDefined(node);
    if(node.getHolds() != null) {
      String s = node.getHolds().toString().trim();
      result.append(s); indent += s.length();
    }
    outAHoldsDefined(node);
  }
  /** 
   * Defined symbol 'forall'. This node is used in quoted expressions.
   */
  public void caseAForallDefined(AForallDefined node) {
    inAForallDefined(node);
    if(node.getForall() != null) {
      String s = node.getForall().toString().trim();
      result.append(s); indent += s.length();
    }
    outAForallDefined(node);
  }
  /** 
   * Defined symbol 'exists'. This node is used in quoted expressions.
   */
  public void caseAExistsDefined(AExistsDefined node) {
    inAExistsDefined(node);
    if(node.getExists() != null) {
      String s = node.getExists().toString().trim();
      result.append(s); indent += s.length();
    }
    outAExistsDefined(node);
  }

}