// add Intersection and Negation
Main { {{
  static void p(String s){ System.out.println(s); }
  public static void main(String args[]) throws Exception {

    // to say that Node is a builtIn class
    edu.neu.ccs.demeterf.util.Util.addBuiltIn(Node.class);

    // for debugging traversals
    // util.Util.setDebug(true);

    Main m = Main.parse(System.in);
    m.well_formed();
    System.out.println(" done ");
  }
}}
}
Main {
  void well_formed() to PathSpec (WellFormedVis);
}
WellFormedVis {
  {{ ClassGraph cg = new ClassGraph(true,false); }}

  before PathSpec {{ 
    PathSpec new_host = 
      new edu.neu.ccs.demeterf.Traversal(new ComplementMerge()).
        <PathSpec> traverse(host);
    boolean wff = new_host.well_formed();
    boolean wff2 = new_host.wf();
    Main.p(" input ================= ");
    Boolean wff3 = new 
      edu.neu.ccs.demeterf.Traversal(new WfCheck()).<Boolean> traverse(host);
    Boolean wff4 = host.DJwff(cg);
    Boolean wff5 = new edu.neu.ccs.demeterf.Traversal(new WfCheckExperiment()).<Boolean> traverse(host);

    Main.p(" BEFORE TRANSLATION ");
    host.print();
    Main.p(" AFTER TRANSLATION ");
    new_host.print();
    Main.p(" above path spec is well formed " + wff + " trav " + wff2 + 
    " bryan " + wff3 + " DJ " + wff4 + " Exp " + wff5);
    if ((wff != wff2) || (wff2 != wff3) || (wff3 != wff4)) Main.p( "DIFFERENT RESULTS ====================!!!!!!!!! ");
  }}
}

ComplementMerge { {{
  // PathSpec apply(Merge m, PathSpec first, PathSpec second) {
  // PathSpec apply(Merge m) {
  Complement apply(Merge m) {
    return new Complement(m);
  }
  // PathSpec apply(Join j, PathSpec first, PathSpec second) {
  PathSpec apply(Join j) {
    Main.p(" HELLO ");
    return new Complement(j);
  }
}} }

WfCheckExperiment { {{
  Boolean combine(Object j, Boolean fn, Boolean sn) {
    return fn && sn ;
    }
  Boolean combine(Object s, Boolean fn) {
    return fn; }
  Boolean combine(Simple s, Node source, Node target) {
    return false; }
}} }

WfCheck { {{
  Boolean combine(Join j, Boolean fn, Boolean sn) {
    boolean b =  j.get_first().target().equals(j.get_second().source());
    return fn && sn && b;
    }
  Boolean combine(Intersection m, Boolean fn, Boolean sn) {
    boolean source_equals =  
      m.get_first().source().equals(m.get_second().source());
    boolean target_equals =  
      m.get_first().target().equals(m.get_second().target());
    return fn & sn && source_equals && target_equals;
  }
  Boolean combine(Merge m, Boolean fn, Boolean sn) {
    boolean source_equals =  
      m.get_first().source().equals(m.get_second().source());
    boolean target_equals =  
      m.get_first().target().equals(m.get_second().target());
    return fn & sn && source_equals && target_equals;
  }


  Boolean combine(Simple s, Node source, Node target) {
    return true; }
// added
  Boolean combine(Complement s, Boolean fn) {
    return fn; }
}}
}


*{ void print() to * (PrintVisitor);}
// new
PathSpec {
  boolean wf() to Simple (WfVisitor);
}

// simulating an interposition variable with a stack
// NOT NEEDED
WfVisitor {
  {{ 
  Stack<Compound> enclosingC = new Stack<Compound>(); 
  public Compound currentEnclosingC()
     { return enclosingC.peek(); }
  }} 
  before Compound {{ enclosingC.push(host); }}
  after Compound {{ enclosingC.pop(); 
  }}
}

WfVisitor {
  Boolean get_return_val() {{ return new Boolean(wf); }}
  init {{ wf = true; }}

  after Join {{
    boolean b =  host.get_first().target().equals(host.get_second().source());
    wf = wf && b;
  }}

  after {Merge, Intersection} {{
    boolean source_equals =  
      host.get_first().source().equals(host.get_second().source());
    boolean target_equals =  
      host.get_first().target().equals(host.get_second().target());
    boolean b = source_equals && target_equals;
    wf = wf && b;
  }}
}
// end new
PathSpec { {{
  Boolean DJwff(ClassGraph cg){
    return (Boolean) cg.traverse(this,"from PathSpec to Simple", new Visitor(){
       Boolean wf;
       public Boolean getReturnValue() {return wf;}
       public void start() {wf = true;}
       public void after(Join j) {
         boolean b =  j.get_first().target().equals(j.get_second().source());
         wf = wf && b;
       }
       public void after(Merge m) {
         boolean source_equals =  
           m.get_first().source().equals(m.get_second().source());
         boolean target_equals =  
           m.get_first().target().equals(m.get_second().target());
           wf = wf && source_equals && target_equals;
       }

    });
  }
}} }


//well-formed
PathSpec { {{ abstract boolean well_formed(); }} }
{Simple} { {{ boolean well_formed(){return true;} }} } //7
{Complement} { {{ boolean well_formed(){return first.well_formed();} }} } //7
Binary { {{ // 8+9
  boolean well_formed_constituents(){
    return first.well_formed() && second.well_formed(); } }} }
Join { {{ //8
  boolean well_formed(){
    boolean b =  get_first().target().equals(get_second().source());
    Main.p(" check meeting point"); this.print(); Main.p(" result " + b);
    return b && well_formed_constituents();} }} }
{Merge, Intersection} { {{ //9
  boolean well_formed(){
    boolean source_equals =  
      get_first().source().equals(get_second().source());
    boolean target_equals =  
      get_first().target().equals(get_second().target());
    Main.p(" check merge conditions"); this.print(); 
    Main.p(" result " + source_equals + target_equals);
    boolean both = first.well_formed() && second.well_formed();
    return source_equals && target_equals && well_formed_constituents();}
}} }

//source
PathSpec { {{ abstract Node source(); }} }
Simple { {{ Node source(){ return get_source();} }} } //1
{Join, Merge, Intersection} { {{ Node source(){ return get_first().source();} }} } //2
Complement { {{ Node source(){ return get_first().source();} }} } //3

//target
PathSpec { {{ abstract Node target(); }} }
Simple { {{ Node target(){ return get_target();} }} } //4
{Join, Merge, Intersection} { {{ Node target(){ return get_second().target();} }} } //5
Complement { {{ Node target(){ return get_first().target();} }} } //3
// Merge { {{ Node target(){ return get_second().target();} }} } //6

// uses equals on Node
Node { {{
   boolean equals(Node s){ 
     return this.get_v().equals(s.get_v());}
}} }