+
+ ht.add(this);
+ for(Forest<NodeType> f : hp) f.gather(ht);
+ }
+
+ private void touched() {
+ if (touched) return;
+ touched = true;
+ /*
+ FastSet<Forest<NodeType>> f2 = new FastSet<Forest<NodeType>>();
+ for(Forest f : hp)
+ if (f instanceof Forest.One) f2.add(f);
+ else for(Forest ff : ((Forest.Many<NodeType>)f))
+ f2.add(ff);
+ hp = f2;
+ */
+ }
+ public boolean contains(Forest f) {
+ touched();
+ return hp.contains(f);
+ }
+ public void merge(Forest p) {
+ if (touched) throw new RuntimeException("attempt to merge() on a Forest.Many that has already been examined");
+ if (p==this) throw new RuntimeException("attempt to merge() a Forest.Many to itself!");
+ hp.add(p, true);
+ }
+ boolean ambiguous() {
+ touched();
+ if (hp.size()==0) return false;
+ if (hp.size()==1) return hp.iterator().next().ambiguous();
+ return true;
+ }
+
+ void expand(HashSet<Tree<NodeType>> ht, HashSet<Forest<NodeType>> ignore, Tree<NodeType> bogus) {
+ touched();
+ if (ignore.contains(this)) { ht.add(bogus); return; }
+ for (Forest<NodeType> f : hp) f.expand(ht, ignore, bogus);
+ }
+
+
+ // GraphViz, ToInt //////////////////////////////////////////////////////////////////////////////
+
+ public boolean isTransparent() { return hp.size()==1; }
+ public boolean isHidden() { return hp.size()==0; }
+ public void edges(GraphViz.Node n) {
+ if (hp.size()==1) { hp.iterator().next().edges(n); return; }
+ for(Forest f : hp) f.edges(n);
+ }
+ public GraphViz.Node toGraphViz(GraphViz gv) {
+ if (hp.size()==1) return hp.iterator().next().toGraphViz(gv);
+ if (gv.hasNode(this)) return gv.createNode(this);
+ GraphViz.Node n = gv.createNode(this);
+ n.label = "?";
+ n.color = "red";
+ for(Forest f : hp) n.edge(f, null);
+ return n;