#include <stdio.h>
#include "Parser.h"
#include "Wff.h"


/* released under the GNU General Public License Version 2, June 1991
   L.Allison 19 February 2001, 18 January 2002
*/


void WriteWffSlave( Wff T, int indent )                        /*L.Allison*/
/* Write a Wff, with root at the LHS, by a right-to-left, infix traversal */
 { int i;  char str[]="----------|";

   if( T != NULL )
    { WriteWffSlave(T->right, indent+1);                  /* right at top */

      for(i=0; i < indent; i++) printf("          |");

      if(      T->nodeType == ident )   sprintf(str, "%s", T->id); /*infix*/
      else if( T->nodeType == trueSy )  sprintf(str, "%s", "true");
      else if( T->nodeType == falseSy ) sprintf(str, "%s", "false");
      else if( T->nodeType == andSy )   sprintf(str, "%s", "and");
      else if( T->nodeType == orSy )    sprintf(str, "%s", "or");
      else if( T->nodeType == implies ) sprintf(str, "%s", "->");
      else if( T->nodeType == notSy )   sprintf(str, "%s", "not");
      else  /* error */  sprintf(str, "? nodeType = %s ?", T->nodeType);

      i = 0;
      while( str[i] != 0 ) i++;             /* to get the tree  */
      while( i < 10 ) { str[i]='-'; i++; }  /* right we have to */
      str[i] = '|';                         /* pad out any      */
      str[i+1] = 0;                         /* strings          */
      printf("%s\n", str);

      WriteWffSlave(T->left, indent+1);                 /* left at bottom */
    }
 }/*WriteWffSlave*/


void WriteWff( Wff T ) { WriteWffSlave(T, 0); }


/* Write a Wff down the page. */

