/* This code is written the functional "subset" of Java supported by DrJava.  It is identical to Java except
   that mutation is forbidden and constructors, getters, equals, hashcode, and toString are automatically 
   generated for each class.  You can load this file into DrJava and it will transparently execute it.  If you
   want to see the expanded code, you can open BoolSimpSolution.java after compiling this file in DrJava.
*/

/* The definitions of the basic formula interfaces, Form and IfForm, appear below. Interfaces are used rather 
 * than abstract classes so that the Constant and Variable classes can be subtypes in BOTH hierarchies. */

/** Form ::= Constant | Variable | Not(Form) | And(Form, Form) | Or(Form, Form) | Implies(Form, Form) | 
  *          If(Form, Form, Form) 
  */
interface Form {
  /* The visitor pattern hook for the Form type. */
  public Object accept(FormVisitor v);  // Form visitor pattern hook
}

/** IfForm ::= Constant | Variable | IfIf(IfForm, IfForm, IfForm) */
interface IfForm {
  /* The visitor pattern hook for the IfForm type. */
  public Object accept(IfFormVisitor v);
}

interface IfFormVisitor {
  
  Object forConstant(Constant host);
  Object forVariable(Variable host);
  Object forIfIf(IfIf host);  // an If with IfForm subForms 
}

interface FormVisitor {
  
  Object forConstant(Constant host);
  Object forVariable(Variable host);
  Object forNot(Not host);
  Object forAnd(And host);
  Object forOr(Or host);
  Object forImplies(Implies host);
  Object forIf(If host);
}

/* An Environment is a list of bindings of variables to constants (instances of Constant). */
abstract class Environment {

  Environment bind(Variable s, IfForm v) { return new AddBinding(s,v,this); }
  /** Returns the matching Constant bound to v.  If no such Constant is found, returns v. */
  abstract public IfForm lookup(Variable v);
}

/** The Empty Environment class, akin to Scheme empty */
class EmptyEnvironment extends Environment {
  /** Single empty environment. */
  static Environment ONLY = new EmptyEnvironment();
  private EmptyEnvironment() { }
  
  IfForm lookup(Variable v) { return v; }
}
  
/** The non-empty Environment class, akin to Scheme cons. */
class AddBinding extends Environment {
  Variable sym;
  IfForm value;
  Environment rest;
  
  IfForm lookup(Variable s) {
    if (s.equals(sym)) return value;
    else return rest.lookup(s);
  }
}

/* The concrete classes in the Form and IfForm composite hierarchies follow. */
class Variable implements Form, IfForm { 
 
  String name;
  
  public Object accept(FormVisitor v) { return v.forVariable(this); }
  public Object accept(IfFormVisitor v) { return v.forVariable(this); }
}

class Constant implements Form, IfForm {
  boolean value;
    
  /** Singleton definitions of true and false. */
  static Constant TRUE = new Constant(true);
  static Constant FALSE = new Constant(false);
  
  private Constant(boolean v) { value = v; }
  
  public Object accept(FormVisitor v) { return v.forConstant(this); }
  public Object accept(IfFormVisitor v) { return v.forConstant(this); }
}

class IfIf implements IfForm {
  
  IfForm test,conseq,alt;
  public Object accept(IfFormVisitor v) { return v.forIfIf(this); }
}

class If implements Form {
  
  Form test,conseq,alt;
  public Object accept(FormVisitor v) { return v.forIf(this); }
}

class Not implements Form {
  
  Form arg;
  public Object accept(FormVisitor v) { return v.forNot(this); }
}

class And implements Form {
  
  Form left,right;
  public Object accept(FormVisitor v) { return v.forAnd(this); }
}

class Or implements Form {
  
  Form left,right; 
  public Object accept(FormVisitor v) { return v.forOr(this); }
}

class Implies implements Form {
  
  Form left,right;  
  public Object accept(FormVisitor v) { return v.forImplies(this); }
}

/** Visigtor corresponding to convertToIf method. */
class ConvertToIf implements FormVisitor {
  
  static ConvertToIf ONLY = new ConvertToIf();
  
  public IfForm forVariable(Variable s) { return s; }
  public IfForm forConstant(Constant c) { return c; } 
  
  public IfForm forNot(Not n) {         
    IfForm arg = (IfForm) n.arg().accept(this);
    return new IfIf(arg,Constant.FALSE,Constant.TRUE);
  }
  
  public IfForm forAnd(And a) {         
    IfForm left = (IfForm) a.left().accept(this);
    IfForm right = (IfForm) a.right().accept(this);
    return new IfIf(left, right, Constant.FALSE);
  }
  
  public IfForm forOr(Or o) {         
    IfForm left = (IfForm) o.left().accept(this);
    IfForm right = (IfForm) o.right().accept(this);
    return new IfIf(left, Constant.TRUE, right);
  }
  
  public IfForm forImplies(Implies i) {
    IfForm left = (IfForm) i.left().accept(this);
    IfForm right = (IfForm) i.right().accept(this);
    return new IfIf(left,right, Constant.TRUE);
  }
  
  public IfForm forIf(If i) {
    IfForm test = (IfForm) i.test().accept(this);
    IfForm conseq = (IfForm) i.conseq().accept(this);
    IfForm alt = (IfForm) i.alt().accept(this);
    return new IfIf(test, conseq, alt);
  }
}

/* Visitor corresponding to the normalize method. */
class Normalize implements IfFormVisitor {
  
  static Normalize ONLY = new Normalize();
  
  public IfForm forVariable(Variable s) { return s; }     
  public IfForm forConstant(Constant c) { return c; } 
  
  public IfForm forIfIf(IfIf i) {
    IfForm test = (IfForm) i.test().accept(this);
    IfForm conseq = (IfForm) i.conseq().accept(this);
    IfForm alt = (IfForm) i.alt().accept(this);
    return (IfForm) test.accept(new HeadNormalize(conseq, alt));
  }
}  

/* Visitor corresponding to the headNormalize method. */
class HeadNormalize implements IfFormVisitor {
  
  // test, conseq, alt are already normalized 
  
  IfForm conseq, alt;
  
  public IfForm forVariable(Variable test) { return new IfIf(test, conseq, alt); }
  
  public IfForm forConstant(Constant test) { return new IfIf(test, conseq, alt); } 
  
  public IfForm forIfIf(IfIf test) {
    return new IfIf(test.test(), 
                    (IfForm) test.conseq().accept(this), 
                    (IfForm) test.alt().accept(this));
  } 
}

/** Visitor corresponding to the eval method. */
class Evaluate implements IfFormVisitor {
  
  static Evaluate BASE = new Evaluate(EmptyEnvironment.ONLY);
  
  Environment env;
  
  public IfForm forVariable(Variable s) { return env.lookup(s); }     
  public IfForm forConstant(Constant c) { return c; } 
  
  public IfForm forIfIf(IfIf i) {
    IfForm test = (IfForm) i.test().accept(this);
    if (test.equals(Constant.TRUE)) return (IfForm) i.conseq().accept(this);
    if (test.equals(Constant.FALSE)) return (IfForm) i.alt().accept(this);

    Variable symtest = (Variable) test;
    IfForm conseq = (IfForm) i.conseq().accept(new Evaluate(env.bind(symtest,Constant.TRUE)));
    IfForm alt = (IfForm) i.alt().accept(new Evaluate(env.bind(symtest,Constant.FALSE)));
    if (conseq.equals(alt)) return conseq;
    if ((conseq.equals(Constant.TRUE)) && (alt.equals(Constant.FALSE))) return symtest;
    
    return new IfIf(test,conseq,alt);
  }
}  

/** Visitor corresponding to the convertToBool method */
class ConvertToBool implements IfFormVisitor {
  static ConvertToBool ONLY = new ConvertToBool();
  
  public Form forVariable(Variable s) { return s; }
  public Form forConstant(Constant c) { return c; } 
  
  public Form forIfIf(IfIf i) {
    Form test = (Form) i.test().accept(this);
    Form conseq = (Form) i.conseq().accept(this);
    Form alt = (Form) i.alt().accept(this);
    if (Constant.FALSE.equals(conseq) && Constant.TRUE.equals(alt))
      return new Not(test);
    else if (Constant.FALSE.equals(alt)) return new And(test,conseq);
    else if (Constant.FALSE.equals(conseq)) return new And(new Not(test),alt);
    else if (Constant.TRUE.equals(conseq)) return new Or(test,alt);
    else if (Constant.TRUE.equals(alt)) return new Implies(test,conseq);
    else return new If(test,conseq,alt);
  }
}
  
class Print implements FormVisitor, IfFormVisitor {
  
  String print(Form f) { return (String) f.accept(this); }
  String print(IfForm f) { return (String) f.accept(this); }
  
  static Print ONLY = new Print();
  
  public String forVariable(Variable v) { return v.name(); }

  public String forConstant(Constant c) {
    if (c.value()) return "T" ;
    else return "F"; 
  }
  
  public String forIf(If i) {
    return  "(? " + print(i.test()) + " " + print(i.conseq()) + " " + print(i.alt()) + ")";
  }
  
  public String forIfIf(IfIf i) {
    return  "(? " + print(i.test()) + " " + print(i.conseq()) + " " + print(i.alt()) + ")";
  }
  
  public String forNot(Not n) { return "(! " + print(n.arg()) + ")"; }
  
  public String forAnd(And a) { return "(& " + print(a.left()) + " " + print(a.right()) + ")"; }       
    
  public String forOr(Or o) { return "(| " + print(o.left()) + " " + print(o.right()) + ")"; }
  
  public String forImplies(Implies i) { return "(> " + print(i.left()) + " " + print(i.right()) + ")"; }
}