// file:    LogicTree.java
// author:  Robert Keller
// purpose: A class for representing syntax trees for logic expressions

/**
 * A LogicTree represents the syntax of a propositional logic expression.
 */

abstract class LogicTree
{
/**
 * C0 is a tree for the constant 0 (false).
 */

static LogicTree C0 = new False();


/**
 * C1 is a tree for the constant 1 (true).
 */

static LogicTree C1 = new True();


/**
 * additionalIndentation determines how much additional Indentation there
 * is at each level of the tree when it is converted to a String.
 */

static String additionalIndentation = " ";


/**
 * Convert the tree to a String representation.
 */

public String toString()
  {
  StringBuffer buffer = new StringBuffer();  
  toStringBuffer("", buffer);
  return buffer.toString();
  }


/**
 * Put the tree's representation into a StringBuffer.
 */

abstract public void toStringBuffer(String indentation, StringBuffer buffer);



/**
 * Tell whether this tree is a failure.
 */

public boolean isFailure()
  {
  return this instanceof Failure;
  }


/**
 * pseudo-constructor for an "iff" tree
 */

public static LogicTree iff(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new Iff(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for an "implies" tree
 */

public static LogicTree implies(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new Implies(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for an "or" tree
 */

public static LogicTree or(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new Or(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for an "and" tree
 */

public static LogicTree and(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new And(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for a "not" tree
 */

public static LogicTree not(LogicTree subtree)
  {
  return new Not(subtree);
  }


/**
 * pseudo-constructor for a logical variable
 */

public static LogicTree var(char name)
  {
  return new Var(name);
  }


/**
 * pseudo-constructor for a failure
 */

public static LogicTree failure(String cause)
  {
  return new Failure(cause);
  }


/**
 * test program that constructs several trees and displays them
 */

public static void main(String arg[])
  {
  System.out.println("Tree for: (a+b)' = a'*b'");
  System.out.println(
    iff(
        not(or(var('a'), var('b'))),
        and(not(var('a')), not(var('b')))
       ) );

  System.out.println("Tree for: c > 1");
  System.out.println(
    implies(var('c'), C1)
       );

  System.out.println("Tree for: 0 > d");
  System.out.println(
    implies(C0, var('d'))
       );

  System.out.println("Tree for: a + a'*b = a + b");
  System.out.println(
    iff(
        or(var('a'), and(not(var('a')), var('b'))), 
        or(var('a'), var('b')))
       );
  }
}


/**
 * a logic tree with a generic binary operator
 */

class BinaryTree extends LogicTree
{
/**
 * the operator
 */

String op;

/**
 * the left subtree of this tree
 */

LogicTree leftSubtree;


/**
 * the right subtree of this tree
 */

LogicTree rightSubtree;


/**
 * Construct a logic tree with a generic binary operator.
 */

BinaryTree(String op, LogicTree leftSubtree, LogicTree rightSubtree)
  {
  this.op           = op;
  this.leftSubtree  = leftSubtree;
  this.rightSubtree = rightSubtree;
  }

public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append(op);
  buffer.append("\n"); 
  leftSubtree.toStringBuffer(indentation + additionalIndentation, buffer);
  rightSubtree.toStringBuffer(indentation + additionalIndentation, buffer);
  }
}


/**
 * a logic tree with a generic unary operator
 */

class UnaryTree extends LogicTree
{
/**
 * the operator
 */

String op;


/**
 * the one subtree of this tree
 */

LogicTree subtree;


/**
 * Construct a logic tree with a generic unary operator.
 */

UnaryTree(String op, LogicTree subtree)
  {
  this.op       = op;
  this.subtree  = subtree;
  }

public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append(op);
  buffer.append("\n"); 
  subtree.toStringBuffer(indentation + additionalIndentation, buffer);
  }
}

/**
 * a LogicTree tree that is a leaf, either a constant or variable
 */

class Unit extends LogicTree
{
/**
 * the representation of this leaf as a string
 */

String value;


/**
 * construct a leaf
 */

Unit(String value)
  {
  this.value = value;
  }

public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append(value);
  buffer.append("\n"); 
  }
}



/**
 * a LogicTree tree representing the result of illegal input
 */

class Failure extends LogicTree
{
/**
 * description of the cause of failure
 */

String cause;

String residual;


/**
 * Construct a failure indicator from a cause.
 */

Failure(String cause)
  {
  this(cause, null);
  }


/**
 * Construct a failure indicator from a cause and a residual input.
 */

Failure(String cause, String residual)
  {
  this.cause    = cause;
  this.residual = residual;
  }

public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append("*** error: " + cause);
  buffer.append("\n"); 

  if( buffer != null )
    {
    buffer.append("*** starting at: "); 
    buffer.append(residual);
    buffer.append("\n"); 
    }
  }


public String getCause()
  {
  return cause;
  }


public String getResidual()
  {
  return residual;
  }
}


/**
 * a LogicTree tree with an "=" operator and two subtrees
 */

class Iff extends BinaryTree
{
Iff(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super("=", leftSubtree, rightSubtree);
  }
}


/**
 * a LogicTree tree with an ">" operator and two subtrees
 */

class Implies extends BinaryTree
{
Implies(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super(">", leftSubtree, rightSubtree);
  }
}


/**
 * a LogicTree tree with a "+" operator and two subtrees
 */

class Or extends BinaryTree
{
Or(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super("+", leftSubtree, rightSubtree);
  }
}


/**
 * a LogicTree tree with a "*" operator and two subtrees
 */

class And extends BinaryTree
{
And(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super("*", leftSubtree, rightSubtree);
  }
}


/**
 * a LogicTree tree with a "'" operator and one subtrees
 */

class Not extends UnaryTree
{
Not(LogicTree subtree)
  {
  super("'", subtree);
  }
}



/**
 * a LogicTree tree for the constant 0 (false)
 */

class False extends Unit
{
False()
  {
  super("0");
  }
}


/**
 * a LogicTree tree for the constant 1 (true)
 */

class True extends Unit
{
True()
  {
  super("1");
  }
}


/**
 * a LogicTree tree for a variable with a given name
 */

class Var extends Unit
{
Var(char name)
  {
  super("" + name);
  }
}