/*
 * Checker.java
 *
 * Created on 15 de Junho de 2005, 21:23
 *
 * 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 java.util.Hashtable;
import java.util.Stack;
import net.sourceforge.czt.circustools.ast.ActionAnn;
import net.sourceforge.czt.circustools.ast.ActionSignature;
import net.sourceforge.czt.circustools.ast.BasicProcessSignature;
import net.sourceforge.czt.circustools.ast.ProcessAnn;
import net.sourceforge.czt.circustools.ast.ProcessSignature;
import static net.sourceforge.czt.typecheck.circus.util.GlobalDefs.*;

import java.util.List;

import net.sourceforge.czt.base.ast.*;
import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.circus.ast.*;
import net.sourceforge.czt.session.*;
import net.sourceforge.czt.typecheck.z.util.TypeEnv;
import net.sourceforge.czt.typecheck.z.util.SectTypeEnv;
import net.sourceforge.czt.typecheck.z.util.UResult;
import net.sourceforge.czt.typecheck.z.impl.UnknownType;
import net.sourceforge.czt.typecheck.circus.util.*;
import net.sourceforge.czt.typecheck.circus.impl.*;
import net.sourceforge.czt.z.util.ZString;


/**
 *
 * @author Manuela
 */
abstract public class Checker
  extends net.sourceforge.czt.typecheck.z.Checker
{
    
  //the information required for the typechecker classes.
  protected TypeChecker typeChecker_;

  public Checker(TypeChecker typeChecker)
  {
    super(typeChecker);
    typeChecker_ = typeChecker;
  }

  //a Factory for creating Circus terms
  protected net.sourceforge.czt.typecheck.circus.impl.Factory factory()
  {
    return typeChecker_.circusFactory_;
  }

  protected Checker actionChecker()
  {
    return typeChecker_.actionChecker_;
  }

  protected Checker commandChecker()
  {
    return typeChecker_.commandChecker_;
  }

  protected Checker communicChecker()
  {
    return typeChecker_.communicChecker_;
  }
  
  protected Checker processChecker()
  {
    return typeChecker_.processChecker_;
  }

  protected Checker channelDeclChecker()
  {
    return typeChecker_.channelDeclChecker_;
  }
/*  
  protected Checker channelsUsedChecker()
  {
    return typeChecker_.channelsUsedChecker_;
  }
*/
  protected DeclName currentProcess()
  {
    return typeChecker_.currentProcess_;
  }
  
  protected void setCurrentProcess(DeclName name)
  {
    typeChecker_.currentProcess_ = name;
  }

  protected DeclName currentAction()
  {
    return typeChecker_.currentAction_;
  }

  protected void setCurrentAction(DeclName name)
  {
    typeChecker_.currentAction_ = name;
  }

  protected DeclName stateName()
  {
    return typeChecker_.stateName_;
  }
  
  protected void setStateName(DeclName name)
  {
    typeChecker_.stateName_ = name;
  }

  protected List<RefName> statesAux() {
    return typeChecker_.statesAux_;
  }
  
  protected void setStatesAux(List<RefName> names) {
    typeChecker_.statesAux_ = names;
  }
  
  protected void setCurrentGenParams(List params)
  {
    typeChecker_.currentGenParams_ = params;
  }

  protected List currentGenParams()
  {
    return typeChecker_.currentGenParams_;
  }

  protected void setOnTheFlyProcesses(List<ProcessPara> procs)
  {
    typeChecker_.onTheFlyProcesses_= procs;
  }
  
  protected List onTheFlyProcesses() {
    return typeChecker_.onTheFlyProcesses_;
  }
  
  protected List<ChannelInfo> channels() {
    return typeChecker_.channels_;
  }

  protected List<DeclName> chansets() {
    return typeChecker_.chansets_;
  }

  protected List<ProcessInfo> processes() {
    return typeChecker_.processes_;
  }
  
  protected List<DeclName> muProcesses() {
    return typeChecker_.muProcesses_;
  }
  
  protected List<DeclName> muActions() {
    return typeChecker_.muActions_;
  }
  
  protected List<List<NameTypePair>> localVars4ActPostCheck() {
    return typeChecker_.localVars4ActPostCheck_;
  }

  protected List<List<NameTypePair>> localVars4ProcPostCheck() {
    return typeChecker_.localVars4ProcPostCheck_;
  }

  protected List<DeclName> actions4PostCheck() {
    return typeChecker_.actions4PostCheck_;
  }

  protected List<DeclName> processes4PostCheck() {
    return typeChecker_.processes4PostCheck_;
  }

  protected boolean isChannel(DeclName name){
    boolean result = false;
    for (ChannelInfo channel : channels()) {
      DeclName decl = channel.getChannelType().getName();
      if (compareDeclName(name, decl, false)) {
        result = true;
        break;
      }
    }
    return result;
  }

  protected boolean isGenericChannel(DeclName name){
    boolean result = false;
    for (ChannelInfo channel : channels()) {
      DeclName decl = channel.getChannelType().getName();
      if (compareDeclName(name, decl, false)) {
        if(channel.isGeneric()) {
          result = true;
          break;
        }
      }
    }
    return result;
  }
  
  protected List<DeclName> getGenParamsChannel(DeclName name) {
    List<DeclName> result = new ArrayList<DeclName>();
    for (ChannelInfo channel : channels()) {
      DeclName decl = channel.getChannelType().getName();
      if (compareDeclName(name, decl, false)) {
        result = channel.getParams();
        break;
      }
    }
    return result;
  }

  protected boolean isProcess(DeclName name){
    boolean result = false;
    for (ProcessInfo process : processes()) {
      DeclName decl = process.getProcessName();
      if (compareDeclName(name, decl, false)) {
        result = true;
        break;
      }
    }
    return result;
  }

  protected boolean isGenericProcess(DeclName name){
    boolean result = false;
    for (ProcessInfo process : processes()) {
      DeclName decl = process.getProcessName();
      if (compareDeclName(name, decl, false)) {
        if(process.isGeneric()) {
          result = true;
          break;
        }
      }
    }
    return result;
  }

  protected boolean isChannelSet(DeclName name){
    boolean result = false;
    for (DeclName chanset : chansets()) {
      if(compareDeclName(chanset, name, false)) {
        result = true;
        break;
      }
    }
    return result;
  }

  protected boolean addChannel(DeclName declName, Type type)
  {
    boolean result = true;
    for (ChannelInfo channel : channels()) {
      if(compareDeclName(channel.getChannelType().getName(), declName, false)){
        channel.getChannelType().setType(type);
        result = false;
      }
    }

    if(result){
      NameTypePair nameType = factory().createNameTypePair(declName, type);
      ChannelInfo insert = new ChannelInfo(nameType);
      channels().add(insert);
    }
    
    return result;
  }
  
  protected boolean addGenChannel(DeclName declName, Type type, List<DeclName> params)
  {
    boolean result = true;
    for (ChannelInfo channel : channels()) {
      if(compareDeclName(channel.getChannelType().getName(), declName, false)){
        channel.getChannelType().setType(type);
        result = false;
      }
    }

    if(result){
      NameTypePair nameType = factory().createNameTypePair(declName, type);
      ChannelInfo insert = new ChannelInfo(nameType, true, params);
      channels().add(insert);
    }
    
    return result;
  }
  
  protected boolean addChannelSet(DeclName declName)
  {
    boolean result = true;
    for (DeclName chanset : chansets()) {
      if(compareDeclName(chanset, declName, false)){
        result = false;
      }
    }

    if(result){
      chansets().add(declName);
    }
    
    return result;
  }
  
  protected boolean addProcess(DeclName declName)
  {
    boolean result = true;
    for (ProcessInfo process : processes()) {
      if(compareDeclName(process.getProcessName(), declName, false)){
        result = false;
      }
    }

    if(result){
      ProcessInfo insert = new ProcessInfo(declName, false, null);
      processes().add(insert);
    }
    return result;
  }

  protected boolean addGenProcess(DeclName declName, List<DeclName> params)
  {
    boolean result = true;
    for (ProcessInfo process : processes()) {
      if(compareDeclName(process.getProcessName(), declName, false)){
        result = false;
      }
    }

    if(result){
      ProcessInfo insert = new ProcessInfo(declName, true, params);
      processes().add(insert);
    }
    
    return result;
  }
  
  protected void addVars(List<NameTypePair> vars) {
    for(NameTypePair var : vars) {
      typeEnv().add(var);
      DeclName primedVar = factory().createDeclName(var.getName().getWord() + "'", null, null);
      typeEnv().add(primedVar, var.getType());
    }
  }

  protected ProcessInfo getProcessInfo(DeclName name) {
    ProcessInfo result = null;
    List<ProcessInfo> processes = processes();
    for(ProcessInfo proc : processes) {
      if(compareDeclName(proc.getProcessName(), name, false)){
        result = proc;
      }
    }    
    return result;
  }
  
  protected Type getChannelType(DeclName name) {
    Type result = null;
    for(ChannelInfo chan : channels()){
      if(compareDeclName(chan.getChannelType().getName(), name, false)) {
        result = chan.getChannelType().getType();
        break;
      }
    }
    return result;
  }
  
  protected String getKindOfProcess(DeclName name) {
    String result = "";
    for (ProcessInfo process : processes()) {
      DeclName decl = process.getProcessName();
      if(compareDeclName(decl, name, false)) {
        result = process.getKindOfProcess().name();
        break;
      }
    }
    return result;
  }
 
  /**
   * Método que verifica se o nome passado como parâmetro é
   * um nome local novo.
   * @param name  o nome a verificar
   * @return true caso o nome seja novo (localmente)
   *         false, caso contrário.
   */
  protected boolean isNewDef(DeclName name) {
    boolean result = true;
    RefName refName = factory().createRefName(name);    
    
    Type typeLocal = typeEnv().getType(refName);
    if(!(typeLocal instanceof UnknownType)) {
      result = false;
    }

    return result;
  }
  
  protected List<NameTypePair> getUsedChannels(DeclName procName) {
    List<NameTypePair> result = new ArrayList<NameTypePair>();
    for(ProcessInfo proc : processes()) {
      if(compareDeclName(proc.getProcessName(), procName, false)) {
        result.addAll(proc.getUsedChans());
        break;
      }
    }
    return result;
  }
  
  protected List<DeclName> getGenParamsProcess(DeclName procName) {
    List<DeclName> result = new ArrayList<DeclName>();
    for(ProcessInfo proc : processes()) {
      if(compareDeclName(proc.getProcessName(), procName, false)) {
        result = proc.getGenParams();
        break;
      }
    }
    return result;
  }
  
  public void addMuProcess(DeclName name) {
    muProcesses().add(name);
  }
  
  public void addMuAction(DeclName name) {
    muActions().add(name);
  }

  public void addProcesses4PostCheck(DeclName name, List<NameTypePair> pairs) {
    processes4PostCheck().add(name);
    localVars4ProcPostCheck().add(pairs);
  }

  public void addAction4PostCheck(DeclName name, List<NameTypePair> pairs) {
    actions4PostCheck().add(name);
    localVars4ActPostCheck().add(pairs);
  }

  public void removeMuProcess(DeclName name) {
    for(DeclName nameMuProc : muProcesses()) {
      if(compareDeclName(nameMuProc, name, false)) {
        muProcesses().remove(name);
        break;
      }
    }
  }

  public void removeMuAction(DeclName name) {
    for(DeclName nameMuAct : muActions()) {
      if(compareDeclName(nameMuAct, name, false)) {
        muActions().remove(name);
        break;
      }
    }
  }

  public void removeAction4PostCheck(DeclName name) {
    for(DeclName act : actions4PostCheck()) {
      if(compareDeclName(act, name, false)) {
        actions4PostCheck().remove(name);
        break;
      }
    }
  }

  public boolean isMuProcess(DeclName name) {
    boolean result = false;
    for(DeclName nameMuProc : muProcesses()) {
      if(compareDeclName(nameMuProc, name, false)) {
        result = true;
        break;
      }
    }
    return result;
  }
  
  public boolean isMuAction(DeclName name) {
    boolean result = false;
    for(DeclName nameMuAct : muActions()) {
      if(compareDeclName(nameMuAct, name, false)) {
        result = true;
        break;
      }
    }
    return result;
  }
  
  public boolean isLocalVar(RefName name) {
    //<<15/06/2006>>
    //boolean result = true;
    boolean result = false;
    DeclName declName = factory().createDeclName(name.getWord(), null, null);
    Type type = typeEnv().getType(name);
    if(!(type instanceof UnknownType)) {
      if(localCircTypeEnv().isLocalVar(declName)) {
        result = true;
      }
/*      if(localCircTypeEnv().isAction(declName) || localCircTypeEnv().isNameSet(declName)) {
        result = false;
      }
    } 
    else {
      result = false; */
    }
    return result;
  }
  
  public boolean isLocalVars(List<RefName> names) {
    boolean result = true;
    for(RefName name : names) {
      result = isLocalVar(name);
      if(!result) {
        break;
      }
    }
    return result;
  }
  
  
  //typecheck a file using an instance of this typechecker
  protected List typecheck(TermA termA, SectionInfo sectInfo)
  {
    return TypeCheckUtils.typecheck(termA, sectInfo, markup());
  }

  protected void error(TermA termA, ErrorMessage error, Object [] params)
  {
    ErrorAnn errorAnn = this.errorAnn(termA, error, params);
    error(termA, errorAnn);
  }

  protected void error(TermA termA,
                       net.sourceforge.czt.typecheck.z.ErrorMessage error,
                       Object [] params)
  {
    ErrorAnn errorAnn = this.errorAnn(termA, error.toString(), params);
    error(termA, errorAnn);
  }

  protected ErrorAnn errorAnn(TermA termA, ErrorMessage error, Object [] params)
  {
    ErrorAnn errorAnn = new ErrorAnn(error.toString(), params, sectInfo(),
                                     sectName(), nearestLocAnn(termA),
                                     markup());
    return errorAnn;
  }

  protected ErrorAnn errorAnn(TermA termA, String error, Object [] params)
  {
    ErrorAnn errorAnn = new ErrorAnn(error, params, sectInfo(),
                                     sectName(), nearestLocAnn(termA),
                                     markup());
    return errorAnn;
  }

  protected UResult unify(Type2 typeA, Type2 typeB)
  {
    UnificationEnv unificationEnv = (UnificationEnv) unificationEnv();
    return unificationEnv.unify(typeA, typeB);
  }

  //the local TypeEnv
  protected LocalTypeEnv localCircTypeEnv()
  {
    return typeChecker_.localCircTypeEnv_;
  }
  
  //add generic types from a list of DeclNames to the TypeEnv
  protected void addGlobalGenParamTypes(List<DeclName> declNames)
  {
    //add each DeclName and its type
    List<String> names = new ArrayList<String>();
    for (DeclName declName : declNames) {
      GenParamType genParamType = factory().createGenParamType(declName);
      PowerType powerType = factory().createPowerType(genParamType);

      //check if a generic parameter type is redeclared
      if (names.contains(declName.getWord())) {
        Object [] params = {declName};
        error(declName, ErrorMessage.REDECLARED_GEN, params);
      }
      else {
        names.add(declName.getWord());
      }

      //add the name and type to the TypeEnv
      sectTypeEnv().add(declName, powerType);
    }
  }
  
  protected void addProcessAnn(CircusProcess term, ProcessSignature psig) {
    ProcessAnn pAnn = (ProcessAnn) term.getAnn(ProcessAnn.class);
    if (pAnn == null) {
      pAnn = factory().createProcessAnn(psig);
      term.getAnns().add(pAnn);
    } else {
      pAnn.setProcessSignature(psig);
    }
  }

  protected void addActionAnn(CircusAction term, ActionSignature asig) {
    ActionAnn aAnn = (ActionAnn) term.getAnn(ActionAnn.class);
    if (aAnn == null) {
      aAnn = factory().createActionAnn(asig);
      term.getAnns().add(aAnn);
    } else {
      aAnn.setActionSignature(asig);
    }
  }

  protected ProcessSignature cloneProcessSignature(ProcessSignature procSig) {

    ProcessSignature result = factory().createProcessSignature();
    
    if(procSig instanceof BasicProcessSignature) {
      BasicProcessSignature resultTemp = factory().createBasicProcessSignature();
      BasicProcessSignature signature = (BasicProcessSignature)procSig;
      if(signature.getActionsSignature() != null) {
        resultTemp.getActionsSignature().addAll(signature.getActionsSignature());
      }
      if(signature.getDeclNameSets() != null){
        resultTemp.getDeclNameSets().addAll(signature.getDeclNameSets());
      }
      if(signature.getLocalZDeclsSignature() != null){
        resultTemp.getLocalZDeclsSignature().addAll(signature.getLocalZDeclsSignature());
      }
      if(signature.getStateSignature() != null){
        resultTemp.setStateSignature(signature.getStateSignature());
      }
      result = resultTemp;
    } 
   
    if(procSig.getParamsOrIndexes() != null){
      Signature sig = factory().createSignature(procSig.getParamsOrIndexes().getNameTypePair());
      result.setParamsOrIndexes(sig);
    }
   
    return result;
  }

  protected ActionSignature cloneActionSignature(ActionSignature actionSig) {
    ActionSignature result = factory().createActionSignature();
    
    if(actionSig.getLocalVarsSignature() != null) {
      result.setLocalVarsSignature(actionSig.getLocalVarsSignature());
    }
    if(actionSig.getParams() != null) {
      result.setParams(actionSig.getParams());
    }
    return result;
  }
  
  /*
   * Método auxiliar que verifica se existe redeclaração de variáveis
   */
  protected List<NameTypePair> checkDecls(List<NameTypePair> list, List<NameTypePair> news, 
                                       TermA term, ErrorMessage error, List paramsError) 
  {
    for(NameTypePair newDec : news) {
      boolean put = true;
      for(NameTypePair oldDec : list) {
        if(compareDeclName(newDec.getName(), oldDec.getName(), false)) {
          Type2 typeNewDec = unwrapType(newDec.getType());
          Type2 typeOldDec = unwrapType(oldDec.getType());
          if (unify(typeNewDec, typeOldDec) != SUCC) {
            paramsError.add(oldDec.getName().getWord());
            paramsError.add(typeOldDec);
            paramsError.add(typeNewDec);
            Object [] params = paramsError.toArray();
            error(term, error, params); 
          }
          put = false;
          break;
        }
      }
      if(put) {
        list.add(newDec);
      }
    } 
    return list;
  }

  protected ProcessSignature joinProcessSignature(ProcessSignature procSigL, ProcessSignature procSigR){

    ProcessSignature result = factory().createProcessSignature();
    BasicProcessSignature resultTemp = factory().createBasicProcessSignature();
    
    if(procSigL instanceof BasicProcessSignature) {
      BasicProcessSignature sigL = (BasicProcessSignature)procSigL;
      if(sigL.getActionsSignature() != null) {
        resultTemp.getActionsSignature().addAll(sigL.getActionsSignature());
      }
      if(sigL.getDeclNameSets() != null) {
        resultTemp.getDeclNameSets().addAll(sigL.getDeclNameSets());
      }
      if(sigL.getLocalZDeclsSignature() != null) {
        resultTemp.getLocalZDeclsSignature().addAll(sigL.getLocalZDeclsSignature());
      }
      if(sigL.getStateSignature() != null) {
        if(resultTemp.getStateSignature() != null) {
          List<NameTypePair> pairs = sigL.getStateSignature().getNameTypePair();
          List<NameTypePair> resultPairs = new ArrayList<NameTypePair>();
          resultPairs.addAll(resultTemp.getStateSignature().getNameTypePair());
          for(NameTypePair pair : pairs) {
            if(!resultPairs.contains(pair)) {
              resultPairs.add(pair);
            }
          }
          resultTemp.setStateSignature(factory().createSignature(resultPairs));
        } else {
          resultTemp.setStateSignature(sigL.getStateSignature());
        }
      }
      result = resultTemp;
    }

    if(procSigR instanceof BasicProcessSignature) {
      BasicProcessSignature sigR = (BasicProcessSignature)procSigR;
      if(sigR.getActionsSignature() != null) {
        resultTemp.getActionsSignature().addAll(sigR.getActionsSignature());
      }
      if(sigR.getDeclNameSets() != null) {
        resultTemp.getDeclNameSets().addAll(sigR.getDeclNameSets());
      }
      if(sigR.getLocalZDeclsSignature() != null) {
        resultTemp.getLocalZDeclsSignature().addAll(sigR.getLocalZDeclsSignature());
      }
      if(sigR.getStateSignature() != null) {
        if(resultTemp.getStateSignature() != null) {
          List<NameTypePair> pairs = sigR.getStateSignature().getNameTypePair();
          List<NameTypePair> resultPairs = new ArrayList<NameTypePair>();
          resultPairs.addAll(resultTemp.getStateSignature().getNameTypePair());
          for(NameTypePair pair : pairs) {
            if(!resultPairs.contains(pair)) {
              resultPairs.add(pair);
            }
          }
          resultTemp.setStateSignature(factory().createSignature(resultPairs));
        } else {
          resultTemp.setStateSignature(sigR.getStateSignature());
        }
      }
      result = resultTemp;
    }
    
    if(procSigL.getParamsOrIndexes() != null) {
      if(result.getParamsOrIndexes() != null) {
        List<NameTypePair> pairs = procSigL.getParamsOrIndexes().getNameTypePair();
        List<NameTypePair> resultPairs = new ArrayList<NameTypePair>();
        resultPairs.addAll(result.getParamsOrIndexes().getNameTypePair());
        for(NameTypePair pair : pairs) {
          if(!resultPairs.contains(pair)) {
            resultPairs.add(pair);
          }
        }
        result.setParamsOrIndexes(factory().createSignature(resultPairs));
      } else {
        result.setParamsOrIndexes(procSigL.getParamsOrIndexes());
      }
    }
    if(procSigR.getParamsOrIndexes() != null) {
      if(result.getParamsOrIndexes() != null) {
        List<NameTypePair> pairs = procSigR.getParamsOrIndexes().getNameTypePair();
        List<NameTypePair> resultPairs = new ArrayList<NameTypePair>();
        resultPairs.addAll(result.getParamsOrIndexes().getNameTypePair());
        for(NameTypePair pair : pairs) {
          if(!resultPairs.contains(pair)) {
            resultPairs.add(pair);
          }
        }
        result.setParamsOrIndexes(factory().createSignature(resultPairs));
      } else {
        result.setParamsOrIndexes(procSigR.getParamsOrIndexes());
      }
    }

    return result;
    
  }

  protected ActionSignature joinActionSignature(ActionSignature actionSigL, ActionSignature actionSigR){

    ActionSignature result = factory().createActionSignature();
    
    if(actionSigL.getLocalVarsSignature() != null) {
      result.setLocalVarsSignature(actionSigL.getLocalVarsSignature());
    }
    if(actionSigR.getLocalVarsSignature() != null) {
      if(result.getLocalVarsSignature() != null) {
        List<NameTypePair> pairs = actionSigR.getLocalVarsSignature().getNameTypePair();
        List<NameTypePair> resultPairs = new ArrayList<NameTypePair>();
        resultPairs.addAll(result.getLocalVarsSignature().getNameTypePair());
        for(NameTypePair pair : pairs) {
          if(!resultPairs.contains(pair)) {
            resultPairs.add(pair);
          }
        }
        result.setLocalVarsSignature(factory().createSignature(resultPairs));
      } else {
        result.setLocalVarsSignature(actionSigR.getLocalVarsSignature());
      }
    }
    if(actionSigL.getParams() != null) {
      result.setParams(actionSigL.getParams());
    }
    if(actionSigR.getParams() != null) {
      if(result.getParams() != null) {
        List<NameTypePair> pairs = actionSigR.getParams().getNameTypePair();
        List<NameTypePair> resultPairs = new ArrayList<NameTypePair>();
        resultPairs.addAll(result.getParams().getNameTypePair());
        for(NameTypePair pair : pairs) {
          if(!resultPairs.contains(pair)) {
            resultPairs.add(pair);
          }
        }
        result.setParams(factory().createSignature(resultPairs));
      } else {
        result.setParams(actionSigR.getParams());
      }
    }

    return result;
    
  }
  
}
