/*
 * CommunicationChecker.java
 *
 * Created on 18 de Junho de 2005, 14:55
 *
 * To change this template, choose Tools | Options and locate the template under
 * the Source Creation and Management node. Right-click the template and choose
 * Open. You can then make changes to the template in the Source Editor.
 */

package net.sourceforge.czt.typecheck.circus;

import java.util.ArrayList;
import net.sourceforge.czt.typecheck.circus.impl.ActionInfo;
import static net.sourceforge.czt.typecheck.circus.util.GlobalDefs.*;

import java.util.List;
import net.sourceforge.czt.circus.ast.*;
import net.sourceforge.czt.circus.visitor.*;
import net.sourceforge.czt.typecheck.circus.util.GlobalDefs;
import net.sourceforge.czt.typecheck.z.impl.UnknownType;
import net.sourceforge.czt.z.ast.*;

/**
 *
 * @author Manuela
 */
public class CommunicationChecker
  extends Checker
  implements CommunicationVisitor,
             DotFieldVisitor,
             InputFieldVisitor,
             OutputFieldVisitor
{
  
  //a Z decl checker
  protected net.sourceforge.czt.typecheck.z.DeclChecker zDeclChecker_;
  
  private int position_;
  private Type chanType_;
  private Type currentType_;
  private DeclName chanName_;

  /** Creates a new instance of CommunicationChecker */
  public CommunicationChecker(TypeChecker typeChecker)
  {
    super(typeChecker);
    zDeclChecker_ = new net.sourceforge.czt.typecheck.z.DeclChecker(typeChecker);
  }

  // Communication ::= N
  // Communication ::= N CParameter+
  // Communication ::= N[Expression+] CParameter+
  //ok - verificado em 15/09/2005 às 14:33
  public Object visitCommunication(Communication term)
  {
    List<NameTypePair> result = new ArrayList<NameTypePair>();

    this.chanName_ = factory().createDeclName(term.getChanName().getWord(), null, null);

    if(isChannel(this.chanName_)) {
      DeclName name = factory().createDeclName("Synch", null, null);
      Type typeSynch = factory().createGivenType(name);

      this.chanType_ = getChannelType(this.chanName_);
      this.position_ = 0;
      
      List<Field> cParams = term.getChanFields();
      Object [] params = {currentProcess().getWord(), this.chanName_.getWord()};
      
      // caso o canal seja de sincronização
      if(this.chanType_.equals(typeSynch)) {
        if(!cParams.isEmpty()) {
          // erro pois o canal é de sincronização e não deve ter parâmetros
          error(term, ErrorMessage.SYNCH_CHANNEL_WITH_CPARAMS_ERROR, params);
        }
      }
      else {
        if(!cParams.isEmpty()) {
          if(this.chanType_ instanceof ProdType) {
            // <<15/06/2006>> alteração para conformidade com as regras de tipos
            // substituição de != por <
            if(((ProdType)this.chanType_).getType().size() < cParams.size()) {
              // o número de parâmetros não atende ao tipo do canal
              error(term, ErrorMessage.NUMBER_CPARAMS_INCOMPATIBLE_CHANNEL_TYPE, params);
            }
          } 
          else {
            if(cParams.size() > 1) {
              // o número de parâmetros não atende ao tipo do canal
              error(term, ErrorMessage.NUMBER_CPARAMS_INCOMPATIBLE_CHANNEL_TYPE, params);
            } 
          }
          
          // tratamento de comunicação genérica
          if(!term.getGenActuals().isEmpty()) {
            if(!isGenericChannel(this.chanName_)) {
              error(term, ErrorMessage.IS_NOT_GENERIC_CHANNEL, params);
            }
            else {
              List<Expr> exprs = term.getGenActuals();
              List<DeclName> genParams = getGenParamsChannel(this.chanName_);
              if(exprs.size() != genParams.size()) {
                error(term, ErrorMessage.DIFF_NUMBER_IN_GENERIC_CHANNEL_INSTATIATION, params);
              }
              else {
                int i = 0;
                for(Expr expr : exprs) {
                  Type typeExpr = (Type)expr.accept(exprChecker());
                  DeclName genName = genParams.get(i);
                  if(typeExpr instanceof PowerType) {
                    Type type = ((PowerType)typeExpr).getType();
                    this.chanType_ = replaceChannelType(genName, type, this.chanType_);
                  } else {
                    error(term, ErrorMessage.EXPR_TYPE_IS_NOT_POWERSET, params);
                    break;
                  }
                  i++;
                }
              }
            }
          }

          //eh preciso um novo ambiente para tratar o seguite caso: c?x!x. O x
          //deve estar no escopo da expressão do outputField !Exp...
          typeEnv().enterScope();
          int numParams = cParams.size();
          int count = 0;
          Type tailType = this.chanType_;
          for(Field cParam : cParams) {
            // <<15/06/2006>> Inclusão de tratamento para ficar em conformidade
            // com as regras de tipo correspondentes.
            count = count + 1;
            if(count == numParams) {
              this.currentType_ = tailType;
            } else {
              this.currentType_ = getHeadType(tailType);
              tailType = getTailType(tailType);
            }
            //
            List<NameTypePair> pairs = (List<NameTypePair>)cParam.accept(communicChecker());
            List paramsError = new ArrayList<Object>();
            paramsError.add(currentProcess().getWord());            
            // chama uma função que verifica se existe redeclaração de variáveis de entrada
            // com tipos diferentes.
            result = checkDecls(result, pairs, term, ErrorMessage.REDECLARED_INPUT_VAR_IN_PROCESS, paramsError);
            this.position_++;
            typeEnv().add(pairs);
          }
          typeEnv().exitScope();
        }
        else {
          // erro pois o canal exige parâmetros
          error(term, ErrorMessage.CHANNEL_NEEDS_CPARAMS, params);
        }
      }
      // adicionando os canais usados...
      List<NameTypePair> usedChans = new ArrayList<NameTypePair>();
      NameTypePair usedChan = factory().createNameTypePair(this.chanName_, this.chanType_);
      usedChans.add(usedChan);
      localCircTypeEnv().addUsedChans(usedChans);
      //
    } else {
      Object [] params = {this.chanName_.getWord()};
      error(term, ErrorMessage.IS_NOT_CHANNEL_NAME, params); 
    }
    
    addTypeAnn(term.getChanName(), this.chanType_);
    
    return result;
  }
  
  // CParameter ::= .Expression
  //ok - verificado em 15/09/2005 às 14:35
  public Object visitDotField(DotField term)
  {
    Type exprType = (Type)term.getExpression().accept(exprChecker());
    // <<15/06/2006>>
/*
    Type type = this.chanType_;

    if(this.chanType_ instanceof ProdType) {
      List<Type2> types = ((ProdType)this.chanType_).getType();
      type = types.get(this.position_);
    } 
*/
    
    Type type = this.cloneType(this.currentType_);
    //
    if(!(exprType instanceof UnknownType)) {
      Type2 expectedU = unwrapType(type);
      Type2 foundU = unwrapType(exprType);
      if (unify(foundU, expectedU) != SUCC) {
        Object [] params = {currentProcess().getWord(), expectedU, this.chanName_.getWord(), foundU};
        error(term, ErrorMessage.CHANNEL_PARAM_NOT_UNIFY, params);
      }   
    }
    
    return new ArrayList<NameTypePair>();
  }
  
  // CParameter ::= ?N
  // CParameter ::= ?N : Predicate
  //ok - verificado em 15/09/2005 às 14:38
  public Object visitInputField(InputField term)
  {
    List<NameTypePair> result = new ArrayList<NameTypePair>();
    DeclName varName = factory().createDeclName(term.getVariable());
    // <<15/06/2006>>
    
    Type varType = this.cloneType(this.currentType_);
            
/*    Type varType = factory().createUnknownType();
      
    if(this.chanType_ instanceof ProdType) {
      List<Type2> types = ((ProdType)this.chanType_).getType();
      if(types.size() > this.position_) {
        varType = types.get(this.position_);
      } else {
        Object [] params = {varName.getWord(), this.chanName_.getWord()};
        error(term, ErrorMessage.IMPOSSIBLE_EXTRACT_INPUT_VAR, params);
      }
    } else {
      if(this.position_ == 0) {
        varType = this.chanType_;
      } else {
        Object [] params = {varName.getWord(), this.chanName_.getWord()};
        error(term, ErrorMessage.IMPOSSIBLE_EXTRACT_INPUT_VAR, params);
      }
    }
*/    
    //
    NameTypePair pair = factory().createNameTypePair(varName, varType);
    result.add(pair);
/*    
    if(currentAction() != null) {
      ActionInfo actionInfo = localCircTypeEnv().getActionInfo(currentAction());
      if(actionInfo != null) {
        actionInfo.getLocalVars().addAll(result);
      }
    }
    else {
      // COLOCAR LOCAL VARS NO PROCESSO
    }
*/    
    typeEnv().enterScope();
    typeEnv().add(pair);
    term.getRestriction().accept(predChecker());
    typeEnv().exitScope();
    
    addTypeAnn(term.getVariable(), varType);
    
    return result;
  }

  // CParameter ::= !Expression
  //ok - verificado em 15/09/2005 às 14:38
  public Object visitOutputField(OutputField term)
  {
    return visitDotField(term);
  }

  /*
   * Método auxiliar que instancia o tipo de um canal genérico
   */
  private Type replaceChannelType(DeclName genName, Type typeExpr, Type typeChan) {
    Type result = null;
    
    if(typeChan instanceof ProdType) {
      List<Type2> types = ((ProdType)typeChan).getType();
      List<Type2> typesResult = new ArrayList<Type2>();
      for(Type2 type : types) {
        Type res = replaceChannelType(genName, typeExpr,  type);
        typesResult.add(unwrapType(res));
      }
      result = factory().createProdType(typesResult);
    }
    else if(typeChan instanceof PowerType) {
      Type2 type = ((PowerType)typeChan).getType();
      Type res = replaceChannelType(genName, typeExpr, type);
      result = factory().createPowerType((Type2)res);
    }
    else if(typeChan instanceof GenParamType) {
      DeclName nameType = ((GenParamType)typeChan).getName();
      if(compareDeclName(nameType, genName, false)) {
        result = typeExpr;
      } else {
        result = typeChan;
      }
    }
    else {
      result = typeChan;
    }
    
    return result;
  }

  private Type getHeadType(Type type) {
    Type retorno = type;
    
    if (type instanceof ProdType) {
      List<Type2> types = ((ProdType)type).getType();
      retorno = types.get(0);
    }
    
    return retorno;
  } 
  
  private Type getTailType(Type type) {
    Type retorno = type;
    
    if (type instanceof ProdType) {
      List<Type2> types = ((ProdType)type).getType();
      if(types.size() > 2) {
        List<Type2> newTypes = new ArrayList<Type2>();
        for(int i = 1; i<types.size(); i++) {
          newTypes.add((Type2)types.get(i));
        }
        retorno = factory().createProdType(newTypes);
      } else {
        retorno = types.get(1);
      }
    }
    
    return retorno;
  }
  
  private Type cloneType(Type type) {
    Type retorno = factory().createUnknownType();
    
    if(type instanceof ProdType) {
      List<Type2> types = ((ProdType)type).getType();
      List<Type2> typesResult = new ArrayList<Type2>();
      for(Type2 t : types) {
        Type res = this.cloneType(t);
        typesResult.add(unwrapType(res));
      }
      retorno = factory().createProdType(typesResult);
    } 
    else if(type instanceof PowerType) {
      Type2 t = ((PowerType)type).getType();
      Type res = this.cloneType(t);
      retorno = factory().createPowerType((Type2)res);
    } 
    else if(type instanceof GivenType) {
      DeclName nameType = ((GivenType)type).getName();
      retorno = factory().createGivenType(nameType);
    }
    else if(type instanceof GenParamType) {
      DeclName nameType = ((GenParamType)type).getName();
      retorno = factory().createGenParamType(nameType); 
    }
    
    return retorno;
  }
  
}
