/* TranslatableASTCheckVisitor - Decompiled by JODE
 * Visit http://jode.sourceforge.net/
 */
package alloy.transl;
import java.util.HashSet;
import java.util.Set;
import java.util.TreeSet;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.DeclIter;
import alloy.ast.Leaf;
import alloy.ast.Node;
import alloy.ast.VarCreator;
import alloy.ast.VariableExpr;
import alloy.util.Dbg;

class TranslatableASTCheckVisitor extends ASTDepthFirstVisitor
{
    private Set _nodesSeen = new TreeSet();
    private Set _definedLeafIds = new HashSet();
    
    public void visit(Node node) {
	Dbg.chk(_nodesSeen.add(node), ("duplicate node " + node.nodeString()
				       + " at " + node.getLocation().toString()
				       + ", " + node.getClass().toString()));
	if (node instanceof Leaf) {
	    Dbg.chk(((Leaf) node).getLeafId() != null,
		    ("no id for leaf " + node.nodeString() + " at "
		     + node.getLocation().toString() + ", "
		     + node.getClass().toString()));
	    if (node instanceof VariableExpr
		&& ((VariableExpr) node).isQuantified)
		Dbg.chk(_definedLeafIds
			    .contains(((VariableExpr) node).getLeafId()),
			"quantified variable " + node + " undefined");
	} else {
	    Set set = _definedLeafIds;
	    if (node instanceof VarCreator) {
		_definedLeafIds = new HashSet(_definedLeafIds);
		DeclIter decliter = new DeclIter((VarCreator) node);
		while (decliter.hasNext()) {
		    decliter.next();
		    Dbg.chk(decliter.getLeafId());
		    _definedLeafIds.add(decliter.getLeafId());
		}
	    }
	    super.visit(node);
	    _definedLeafIds = set;
	}
    }
}