/* CommandVisitor - Decompiled by JODE
 * Visit http://jode.sourceforge.net/
 */
package alloy.semantic;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Assertion;
import alloy.ast.CheckCommand;
import alloy.ast.Command;
import alloy.ast.EvalCommand;
import alloy.ast.Excluded;
import alloy.ast.Fact;
import alloy.ast.FormulaPara;
import alloy.ast.Function;
import alloy.ast.GeneralScope;
import alloy.ast.Id;
import alloy.ast.LeafId;
import alloy.ast.Module;
import alloy.ast.Paragraph;
import alloy.ast.QualifiedName;
import alloy.ast.QualifiedNames;
import alloy.ast.RunCommand;
import alloy.ast.SigExpr;
import alloy.ast.SigExprs;
import alloy.ast.Signature;
import alloy.ast.SpecificScope;
import alloy.ast.TypeScope;
import alloy.ast.TypeScopes;
import alloy.type.IntType;
import alloy.type.SigType;
import alloy.type.VarType;
import alloy.util.Dbg;
import alloy.util.Msg;

public class CommandVisitor extends ASTDepthFirstVisitor
{
    private ModuleScope _curModuleScope;
    private Map _varTypeMapping;
    private Map _paramExprMapping;
    private FormulaPara _curFormulaPara;
    public static Map curTypeToScope;
    public static Integer curScope;
    public static boolean settingScopes = false;
    
    public static void addMappingForNewType(String string) {
	Dbg.chk(settingScopes);
	if (curScope == null)
	    Dbg.user
		("no scope specified for polymorphic type in paragraph referenced by command");
	else
	    _addTypeScopeMapping(curTypeToScope, string, curScope);
    }
    
    public void visit(Module module) {
	_curModuleScope = ModuleScopeTable.getInstance()
			      .get(module.getName().nodeString());
	this.visit((alloy.ast.Node) module);
    }
    
    public void visit(RunCommand runcommand) {
	QualifiedName qualifiedname = runcommand.getFunction();
	Function function
	    = (Function) _getParagraph(qualifiedname, "alloy.ast.Function",
				       "run", "function");
	if (function != null) {
	    runcommand.functionPara = function;
	    _curFormulaPara = function;
	    _checkScope(runcommand);
	    runcommand.setExcluded(_checkExcluded(runcommand.getExcluded()));
	}
    }
    
    public void visit(CheckCommand checkcommand) {
	QualifiedNames qualifiednames = checkcommand.getAssertions();
	Object object = null;
	if (!qualifiednames.isLeaf()) {
	    QualifiedName qualifiedname
		= (QualifiedName) qualifiednames.getQualifiedNameIter().next();
	    Assertion assertion
		= ((Assertion)
		   _getParagraph(qualifiedname, "alloy.ast.Assertion", "check",
				 "assertion"));
	    if (assertion == null)
		return;
	    checkcommand.assertionPara = assertion;
	    _curFormulaPara = assertion;
	} else {
	    Dbg.user(new Msg("must specify assertion to check", checkcommand));
	    return;
	}
	_checkScope(checkcommand);
	checkcommand.setExcluded(_checkExcluded(checkcommand.getExcluded()));
    }
    
    public void visit(EvalCommand evalcommand) {
	evalcommand.evalPara
	    = (Function) _getParagraph(evalcommand.getEvalFunction(),
				       "alloy.ast.Function", "evaluate",
				       "function");
	if (evalcommand.evalPara != null) {
	    evalcommand.usingPara
		= (Function) _getParagraph(evalcommand.getUsingFunction(),
					   "alloy.ast.Function", "use",
					   "function");
	    if (evalcommand.usingPara != null) {
		_checkScope(evalcommand);
		evalcommand
		    .setExcluded(_checkExcluded(evalcommand.getExcluded()));
	    }
	}
    }
    
    private void _checkScope(Command command) {
	HashMap hashmap = new HashMap(SigType.getStringToType());
	command.stringToType = SigType.getStringToType();
	Object object = null;
	EvalCommand evalcommand = null;
	FormulaPara formulapara;
	if (command instanceof RunCommand)
	    formulapara = ((RunCommand) command).functionPara;
	else if (command instanceof CheckCommand)
	    formulapara = ((CheckCommand) command).assertionPara;
	else {
	    formulapara = ((EvalCommand) command).usingPara;
	    evalcommand = (EvalCommand) command;
	}
	if (_generateDummyTypes(formulapara, evalcommand)) {
	    command.varTypeMapping = _varTypeMapping;
	    command.paramExprMapping = _paramExprMapping;
	    ArrayList arraylist = new ArrayList(SigType.getSigTypeStrings());
	    arraylist.add("Int");
	    Iterator iterator = formulapara.getTypeParams().getIdIter();
	    while (iterator.hasNext())
		arraylist.add(((Id) iterator.next()).nodeString() + "@@");
	    Object object_0_ = null;
	    alloy.ast.Scope scope = command.getScope();
	    HashMap hashmap_1_;
	    if (scope instanceof GeneralScope) {
		hashmap_1_ = _handleScope((GeneralScope) scope, arraylist);
		command.intWidth
		    = _getIntWidth(((GeneralScope) scope).getButScopes());
	    } else {
		hashmap_1_ = _handleScope((SpecificScope) scope, arraylist);
		command.intWidth
		    = _getIntWidth(((SpecificScope) scope).getTypeScopes());
	    }
	    if (hashmap_1_ != null)
		command.typeToScope = hashmap_1_;
	    if (command instanceof EvalCommand)
		((EvalCommand) command).evalStringToType
		    = new HashMap(command.stringToType);
	    SigType.setStringToType(hashmap);
	}
    }
    
    private Excluded _checkExcluded(Excluded excluded) {
	Excluded excluded_2_ = new Excluded();
	excluded_2_.setExcludeFacts(excluded.excludeFacts());
	excluded_2_.setExcludeConstraints(excluded.excludeConstraints());
	Iterator iterator = excluded.getParaNameIter();
	while (iterator.hasNext()) {
	    QualifiedName qualifiedname = (QualifiedName) iterator.next();
	    Fact fact = (Fact) _getParagraph(qualifiedname, "alloy.ast.Fact",
					     "exclude", "fact");
	    if (fact == null)
		return null;
	    excluded_2_.addParaName(fact.getName());
	}
	return excluded_2_;
    }
    
    private boolean _generateDummyTypes(FormulaPara formulapara,
					EvalCommand evalcommand) {
	_varTypeMapping = new HashMap();
	_paramExprMapping = new HashMap();
	LocalScope localscope = formulapara.getLocalScope();
	Iterator iterator = formulapara.getTypeParams().getIdIter();
	Object object = null;
	LocalScope localscope_3_ = null;
	Iterator iterator_4_ = null;
	if (evalcommand != null) {
	    Function function = evalcommand.evalPara;
	    if (function.getTypeParams().numChildren()
		!= formulapara.getTypeParams().numChildren()) {
		Dbg.user
		    (new Msg
		     ("mismatch in type parameters for paragraphs of eval/using command",
		      evalcommand));
		return false;
	    }
	    evalcommand.evalVarTypeMapping = new HashMap();
	    evalcommand.evalParamExprMapping = new HashMap();
	    localscope_3_ = function.getLocalScope();
	    iterator_4_ = function.getTypeParams().getIdIter();
	}
	while (iterator.hasNext()) {
	    Id id = (Id) iterator.next();
	    String string = id.nodeString();
	    String string_5_ = (string.substring(string.lastIndexOf("/") + 1,
						 string.length())
				+ "@@");
	    Signature signature
		= new Signature(new QualifiedName(new Id(string_5_),
						  formulapara.getName()
						      .getPath()));
	    try {
		_curModuleScope.addOpenedParagraph(signature.getName(),
						   signature);
	    } catch (AlreadyMappedException alreadymappedexception) {
		Dbg.fatal("shouldn't happen");
	    }
	    signature.setLeafId(new LeafId());
	    SigType sigtype = new SigType(signature, null);
	    SigType sigtype_6_ = SigType.getGlobalSigType(sigtype);
	    Dbg.chk(sigtype == sigtype_6_);
	    signature.setSigType(sigtype);
	    VarType vartype
		= ((VarType)
		   localscope.lookupType(id.nodeString()).getBasicTypeAt(0));
	    Dbg.chk(vartype != null);
	    _varTypeMapping.put(vartype, sigtype);
	    _paramExprMapping.put(id.nodeString(), signature.toSigExpr());
	    if (evalcommand != null) {
		Id id_7_ = (Id) iterator_4_.next();
		VarType vartype_8_
		    = (VarType) localscope_3_.lookupType
				    (id_7_.nodeString()).getBasicTypeAt(0);
		Dbg.chk(vartype_8_);
		evalcommand.evalVarTypeMapping.put(vartype_8_, sigtype);
		evalcommand.evalParamExprMapping.put(id_7_.nodeString(),
						     signature.toSigExpr());
	    }
	}
	return true;
    }
    
    private HashMap _handleScope(GeneralScope generalscope,
				 ArrayList arraylist) {
	HashMap hashmap = new HashMap();
	curTypeToScope = hashmap;
	if (!_addTypeScopesToMapping(generalscope.getButScopes(), hashmap,
				     arraylist))
	    return null;
	Integer integer = new Integer(generalscope.getBound().getInt());
	Iterator iterator = arraylist.iterator();
	while (iterator.hasNext()) {
	    String string = (String) iterator.next();
	    if (!hashmap.containsKey(string))
		_addTypeScopeMapping(hashmap, string, integer);
	}
	return hashmap;
    }
    
    private HashMap _handleScope(SpecificScope specificscope,
				 ArrayList arraylist) {
	HashMap hashmap = new HashMap();
	curTypeToScope = hashmap;
	if (!_addTypeScopesToMapping(specificscope.getTypeScopes(), hashmap,
				     arraylist))
	    return null;
	Iterator iterator = arraylist.iterator();
	while (iterator.hasNext()) {
	    String string = (String) iterator.next();
	    if (!hashmap.containsKey(string)) {
		if (string.equals("Int"))
		    hashmap.put(string, new Integer(0));
		else if (_isStaticSig(string))
		    hashmap.put(string, new Integer(1));
		else {
		    Dbg.user(new Msg(("no scope specified for type " + string
				      + " in command"),
				     specificscope));
		    return null;
		}
	    }
	}
	return hashmap;
    }
    
    private boolean _isStaticSig(String string) {
	SigType sigtype = SigType.getSigTypeForString(string);
	if (sigtype != null) {
	    Signature signature = sigtype.getSignature();
	    return signature.isStatic();
	}
	return false;
    }
    
    private boolean _addTypeScopesToMapping
	(TypeScopes typescopes, HashMap hashmap, ArrayList arraylist) {
	Iterator iterator = typescopes.getTypeScopeIter();
	while (iterator.hasNext()) {
	    TypeScope typescope = (TypeScope) iterator.next();
	    SigExpr sigexpr = typescope.getSigExpr();
	    if (!sigexpr.nodeString().equals("int")) {
		String string
		    = _fullyQualifiedTypeString(sigexpr, arraylist, false);
		if (string == null)
		    return false;
		if (hashmap.containsKey(string)) {
		    Dbg.user
			(new Msg("duplicate specification of scope for type",
				 sigexpr));
		    return false;
		}
		if (!arraylist.contains(string)) {
		    Dbg.user(new Msg("scope specified for unknown type",
				     sigexpr));
		    return false;
		}
		curScope = new Integer(typescope.getBound());
		_addTypeScopeMapping(hashmap, string, curScope);
		if (_paramExprMapping.containsKey(sigexpr.nodeString()))
		    _addTypeScopeMapping(hashmap,
					 ((SigExpr)
					  _paramExprMapping
					      .get(sigexpr.nodeString()))
					     .nodeString(),
					 curScope);
	    }
	}
	return true;
    }
    
    private String _fullyQualifiedTypeString
	(SigExpr sigexpr, ArrayList arraylist, boolean bool) {
	if (arraylist.contains(sigexpr.nodeString()))
	    return sigexpr.nodeString();
	QualifiedName qualifiedname = sigexpr.getSig();
	if (qualifiedname.hasEmptyPath()) {
	    Paragraph paragraph
		= _getParagraph(qualifiedname, "alloy.ast.Signature",
				"set scope", "signature");
	    if (paragraph == null)
		return null;
	    qualifiedname = ((Signature) paragraph).getName();
	}
	StringBuffer stringbuffer
	    = new StringBuffer(qualifiedname.nodeString());
	SigExprs sigexprs = sigexpr.getSigExprs();
	if (!sigexprs.isLeaf()) {
	    stringbuffer.append("[");
	    Iterator iterator = sigexprs.getSigExprIter();
	    while (iterator.hasNext()) {
		SigExpr sigexpr_9_ = (SigExpr) iterator.next();
		stringbuffer.append(_fullyQualifiedTypeString(sigexpr_9_,
							      arraylist,
							      true));
		if (iterator.hasNext())
		    stringbuffer.append(",");
	    }
	    stringbuffer.append("]");
	}
	return stringbuffer.toString();
    }
    
    private int _getIntWidth(TypeScopes typescopes) {
	int i = -1;
	Iterator iterator = typescopes.getTypeScopeIter();
	while (iterator.hasNext()) {
	    TypeScope typescope = (TypeScope) iterator.next();
	    if (typescope.getSigExpr().nodeString().equals("int")) {
		if (i != -1) {
		    Dbg.user(new Msg("duplicate declaration of int width",
				     typescope));
		    return -1;
		}
		i = typescope.getBound();
	    }
	}
	return i;
    }
    
    private static void _addTypeScopeMapping(Map map, String string,
					     Integer integer) {
	if (string.equals("Int")) {
	    IntType inttype = IntType.getInstance();
	} else {
	    SigType sigtype = SigType.getSigTypeForString(string);
	    SigType sigtype_10_ = sigtype;
	    Dbg.chk(sigtype_10_);
	    if (sigtype_10_.getSignature().isStatic())
		integer = new Integer(1);
	}
	map.put(string, integer);
    }
    
    private Paragraph _getParagraph(QualifiedName qualifiedname, String string,
				    String string_11_, String string_12_) {
	Paragraph paragraph = null;
	try {
	    if (qualifiedname.hasEmptyPath())
		paragraph = _curModuleScope.getParagraphUnqual(qualifiedname);
	    else
		paragraph = _curModuleScope.getParagraph(qualifiedname);
	    if (!paragraph.getClass().getName().equals(string)) {
		Dbg.user(new Msg(("attempt to " + string_11_ + " a non-"
				  + string_12_),
				 qualifiedname));
		paragraph = null;
	    }
	} catch (ModuleScope.MultipleMappingsException multiplemappingsexception) {
	    Dbg.user(new Msg(multiplemappingsexception.mappingsString(),
			     qualifiedname));
	} catch (ModuleScope.NoParagraphException noparagraphexception) {
	    Dbg.user(new Msg(("attempt to " + string_11_ + " a non-existent "
			      + string_12_),
			     qualifiedname));
	}
	return paragraph;
    }
}