/*
 * ProcessChecker.java
 *
 * Created on 18 de Junho de 2005, 09:28
 *
 * 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.List;
import net.sourceforge.czt.typecheck.circus.impl.ProcessInfo;

import static net.sourceforge.czt.typecheck.circus.util.GlobalDefs.*;

import net.sourceforge.czt.base.ast.ListTerm;
import net.sourceforge.czt.base.impl.ListTermImpl;
import net.sourceforge.czt.typecheck.circus.util.GlobalDefs;
import net.sourceforge.czt.typecheck.z.impl.UnknownType;
import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.circus.ast.*;
import net.sourceforge.czt.circus.visitor.*;
import net.sourceforge.czt.circustools.ast.*;
import net.sourceforge.czt.circustools.visitor.*;
import net.sourceforge.czt.typecheck.circus.util.KindOfProcess;
import net.sourceforge.czt.z.util.ZString;

/**
 * Visitor que checa os tipos de processos. Retorna sempre um objeto do tipo
 * ProcessSignature.
 *
 * @author Manuela 
 */
public class ProcessChecker 
  extends Checker
  implements CircusProcessVisitor,
             Process1Visitor,
             Process2Visitor,
             IndexedProcessVisitor,
             CallProcessVisitor,
             BasicProcessVisitor,
             ProcessIteVisitor,
             ParamProcessVisitor,
             AlphabetisedParallelProcessIteVisitor,
             ParallelProcessIteVisitor,
             AlphabetisedParallelProcessIdxVisitor,
             ParallelProcessIdxVisitor,
             MuProcessVisitor,
             PrefixingProcessVisitor,
             GuardedProcessVisitor,
             HideProcessVisitor,
             RenameProcessVisitor,
             ParallelProcessVisitor,
             AlphabetisedParallelProcessVisitor
{
    
  //a Z decl checker
  protected net.sourceforge.czt.typecheck.z.DeclChecker zDeclChecker_;

  /** Creates a new instance of ProcessChecker */
  public ProcessChecker(TypeChecker typeChecker)
  {
    super(typeChecker);
    zDeclChecker_ =
      new net.sourceforge.czt.typecheck.z.DeclChecker(typeChecker);
  }
  
  public Object visitCircusProcess(CircusProcess term)
  {
    return factory().createProcessSignature();
  }
  
  //ok - verificado em 15/09/2005 às 19:03
  public Object visitProcess1(Process1 term)
  {
    ProcessSignature signature = (ProcessSignature)term.getCircusProcess().accept(processChecker());
    addProcessAnn(term, signature);
    return signature;
  }

  //ok - verificado em 15/09/2005 às 19:03
  public Object visitProcess2(Process2 term)
  {
    ProcessSignature procSigL = (ProcessSignature)term.getLeftProc().accept(processChecker());
    ProcessSignature procSigR = (ProcessSignature)term.getRightProc().accept(processChecker());
    ProcessSignature result = joinProcessSignature(procSigL, procSigR);
    addProcessAnn(term, result);
    return result;
  }

  // ParamProcess ::= Declaration \odot Process
  //ok - verificado em 15/09/2005 às 19:05
  public Object visitIndexedProcess(IndexedProcess term)
  {
    List<Decl> decls = term.getDecl();
    CircusProcess proc = term.getCircusProcess();
    
    List<NameTypePair> allPairs = new ArrayList<NameTypePair>();
    List paramsError = new ArrayList<Object>();
    paramsError.add(currentProcess().getWord());

    // novo escopo devido aos canais implicitos
    localCircTypeEnv().enterScope();
    
    for(Decl d : decls){
      if (!(d instanceof VarDecl))
          throw new UnsupportedOperationException("Indexed processes accept only VarDecl!");
      VarDecl decl = (VarDecl)d;
      List<NameTypePair> pairs = (List<NameTypePair>)decl.accept(declChecker());
      allPairs = checkDecls(allPairs, pairs, term, ErrorMessage.REDECLARED_INDEX_IN_PROCESS, paramsError);
    }

    // atualiza informações sobre o processo
    ProcessInfo procInfo = getProcessInfo(currentProcess());
    procInfo.setKindOfProcess(KindOfProcess.INDEX);
    procInfo.setParamsOrIndexes(allPairs);
    procInfo.getLocalVars().addAll(allPairs);
    
    ProcessSignature procSignature = (ProcessSignature)proc.accept(processChecker());
    ProcessSignature signature = cloneProcessSignature(procSignature);
    Signature sig = factory().createSignature(allPairs);
    signature.setParamsOrIndexes(sig);

    // extrai os canais implicitos a partir dos canais usados pelo processo
    List<NameTypePair> usedChans = localCircTypeEnv().getUsedChans();
    List<NameTypePair> implicitChans = extractImplicitChans(allPairs, usedChans);
    //
    
    localCircTypeEnv().exitScope();

    // adiciona os canais usados...
    localCircTypeEnv().addUsedChans(implicitChans);
    //
    
    addProcessAnn(term, signature);
        
    return signature;
  }
  
  // ParamProcess ::= Declaration @ Process
  //ok - verificado em 15/09/2005 às 19:08
  public Object visitParamProcess(ParamProcess term)
  {
    List<Decl> decls = term.getDecl();
    CircusProcess proc = term.getCircusProcess();

    List<NameTypePair> allPairs = new ArrayList<NameTypePair>();
    List paramsError = new ArrayList<Object>();
    paramsError.add(currentProcess().getWord());
    
    for(Decl d : decls){
      if (!(d instanceof VarDecl))
        throw new UnsupportedOperationException("Param processes accept only VarDecl!");
      VarDecl decl = (VarDecl)d;
      List<NameTypePair> pairs = (List<NameTypePair>)decl.accept(declChecker());
      allPairs = checkDecls(allPairs, pairs, term, ErrorMessage.REDECLARED_PARAM_IN_PROCESS, paramsError);
    }
    
    // atualiza informações sobre o processo
    ProcessInfo procInfo = getProcessInfo(currentProcess());
    procInfo.setKindOfProcess(KindOfProcess.PARAM);
    procInfo.setParamsOrIndexes(allPairs);
    procInfo.getLocalVars().addAll(allPairs);
    
    typeEnv().enterScope();

    typeEnv().add(allPairs);
    
    ProcessSignature procSig = (ProcessSignature)proc.accept(processChecker());
    ProcessSignature procSignature = cloneProcessSignature(procSig);
    Signature sig = factory().createSignature(allPairs);
    procSignature.setParamsOrIndexes(sig);
    
    typeEnv().exitScope();
    
    addProcessAnn(term, procSignature);
    
    return procSignature;
  }
  
  // Process ::= begin PParagraph* state StateParagraph PParagraph* @ Action end
  // Process ::= begin PParagraph* @ Action end
  //ok - verificado em 15/09/2005 às 19:11
  public Object visitBasicProcess(BasicProcess term)
  {
    BasicProcessSignature procSignature = factory().createBasicProcessSignature();
    
    RefName state = term.getStateSchema();
    
    // <04/11/2005>
    if(state != null) {
      DeclName declName = factory().createDeclName(state.getWord(), null, null);
      state.setDecl(declName);
      setStateName(state.getDecl());
    }
    //
    
    //
    //<<15/06/2006>>
    localCircTypeEnv().enterScopeLocalVars();
    //
    localCircTypeEnv().enterScope();
    typeEnv().enterScope();
    ProcessInfo procInfo = getProcessInfo(currentProcess());
    procInfo.getLocalVars().clear();
    if(procInfo.getParamsOrIndexes() != null) {
      procInfo.getLocalVars().addAll(procInfo.getParamsOrIndexes());
    }
    //
    
    localCircTypeEnv().getOnTheFlyActions().addAll(term.getOnTheFlyActionPara());
    
    List<Para> zParas = term.getZPara();
    List<NameTypePair> pairs = new ArrayList<NameTypePair>();
    
    for(Para zPara : zParas){

      Signature signature = (Signature)zPara.accept(paraChecker());

      if(state != null && isSchExprAction(zPara)) {
        NameTypePair pairSig = (NameTypePair)signature.getNameTypePair().get(0);
        DeclName actionName = pairSig.getName();
        SchemaType schType = (SchemaType)((PowerType)pairSig.getType()).getType();
        Signature vars = schType.getSignature();
        
        // cria um actionSignature aqui pois é um caso especial de zPara que
        // o parser não tem como identificar se é ou não uma ação.
        // Se o esquema referencia o estado, é ação!
        ActionSignature actSig = factory().createActionSignature();
        actSig.setActionName(actionName);
        actSig.setLocalVarsSignature(vars);
        // adiciona a ação na lista de ações do TypeChecker
        if(!localCircTypeEnv().addAction(actionName)) {
          Object [] params = {actionName.getWord(), currentProcess().getWord()};
          error(term, ErrorMessage.REDECLARED_ACTION_NAME, params);
        }

        // armazena o parágrafo como uma ação na assinatura do processo
        procSignature.getActionsSignature().add(actSig);

        typeEnv().add(pairSig);
        
      }
      else {
        boolean isState = false;
        procSignature.getLocalZDeclsSignature().add(signature);

        pairs = (List<NameTypePair>)signature.getNameTypePair();
        typeEnv().add(pairs);
        //<04/11/2005>
        addLocalVars(pairs, term);
        //
        if(state != null && procSignature.getStateSignature() == null) {
          for(NameTypePair pair : pairs){
            if(compareDeclName(pair.getName(), state.getDecl(), false)) {
              isState = true;
              List<NameTypePair> listPair = new ArrayList<NameTypePair>();
              listPair.add(pair);
              Signature stateSig = factory().createSignature(listPair);
              procSignature.setStateSignature(stateSig);
              addVarsState(pair, term);
              if(isSchExpr(zPara)) {
                extractStatesAux(zPara);
              }
              break;
            }
          }
        }
        // <04/11/2005>
        if(zPara instanceof AxPara) {
          if(((AxPara)zPara).getBox().equals(Box.SchBox) || isState) {
            for(NameTypePair pair : pairs) {
              DeclName delta = factory().createDeclName(ZString.DELTA + pair.getName().getWord(), null, null);
              typeEnv().add(delta, pair.getType());
              DeclName xi = factory().createDeclName(ZString.XI + pair.getName().getWord(), null, null);
              typeEnv().add(xi, pair.getType());
              DeclName prime = factory().createDeclName(pair.getName().getWord() + "'", null, null);
              typeEnv().add(prime, pair.getType());
            }
          }
        }
        //
      } 
    }

    List<ActionPara> actions = term.getCircusActionPara();
    
    for(ActionPara action : actions) {
      Signature signature = (Signature)action.accept(paraChecker());
      ActionType actionType = (ActionType)((NameTypePair)signature.getNameTypePair().get(0)).getType();
      ActionSignature actionSignature = actionType.getActionSignature();
      procSignature.getActionsSignature().add(actionSignature);
    }
    
    List<NameSetPara> namesets = term.getCircusNameSetPara();
    
    for(NameSetPara nameset : namesets) {
      Signature namesetSignature = (Signature)nameset.accept(paraChecker());
      DeclName name = ((NameTypePair)namesetSignature.getNameTypePair().get(0)).getName();
      procSignature.getDeclNameSets().add(name);
    }
    
    CircusAction mainAction = term.getMainAction();
    DeclName mainActionName = factory().createDeclName("$$mainAction", null, null);
    setCurrentAction(mainActionName);
    ActionSignature mainActionSig = (ActionSignature)mainAction.accept(actionChecker());
    ActionSignature mainSignature = cloneActionSignature(mainActionSig);
    mainSignature.setActionName(mainActionName);
    
    procSignature.getActionsSignature().add(mainSignature);
    
    addProcessAnn(term, procSignature);

    List<NameTypePair> usedChans = new ArrayList<NameTypePair>();
    usedChans.addAll(localCircTypeEnv().getUsedChans());
    
    // útil para chamadas cíclicas de ações: A \defs B e B \defs A ...
    // as regras de tipos de Circus não trata isto.
    postActionCallCheck();

    //
    //<<15/06/2006>>
    localCircTypeEnv().exitScopeLocalVars();
    //
    localCircTypeEnv().exitScope();
    typeEnv().exitScope();
    
    localCircTypeEnv().addUsedChans(usedChans);
    //
    
    setCurrentAction(null);

    return procSignature;
    
  }

  // Process ::= N
  // Process ::= N(Expression+)
  // Process ::= N[Expression+]
  // Process ::= N \lfloor Expression+ \rfloor
  // Process ::= (Declaration @ Process)(Expression+)
  // Process ::= (Declaration \odot Process) \lfloor Expression+ \rfloor
  // Process ::= (\mu N @ Declaration @ Process)(Expression+)
  // Process ::= (\mu N @ Declaration \odot Process) \lfloor Expression+ \rfloor
  //ok - verificado em 15/09/2005 às 19:18
  public Object visitCallProcess(CallProcess term)
  {

    ProcessSignature procSignature = factory().createProcessSignature();
    RefName procRef = term.getRefName();
    DeclName procDecl = factory().createDeclName(procRef);
    
    String nameRefProc = procDecl.getWord();
    if(nameRefProc.startsWith("$$implicitProcess_")) {
      // pegar da lista de processos implicitos, fazer a verificação e incluir no
      //SectTypeEnv!!
      List<ProcessPara> implicitProcs = (List<ProcessPara>)onTheFlyProcesses();
      for(ProcessPara implicitProc : implicitProcs) {
        if(compareDeclName(procDecl, implicitProc.getDeclName(), false)) {
          Signature implicitProcSig = (Signature)implicitProc.accept(paraChecker());
          // a assinatura de um processo sempre terá apenas um par
          NameTypePair pair = (NameTypePair)implicitProcSig.getNameTypePair().get(0);
          //if the name already exists globally, raise an error
          if (!sectTypeEnv().add(pair.getName(), pair.getType())) {
            Object [] params = {pair.getName()};
            error(pair.getName(), ErrorMessage.REDECLARED_GLOBAL_NAME, params);
          }
        }
      }
    }
    
    // verifica se é uma chamada a um processo mu
    if(isMuProcess(procDecl)) {
      if(!(term.getExpr().isEmpty())) {
        Object [] params = {currentProcess().getWord(), procDecl.getWord()};
        error(term, ErrorMessage.MU_PROC_CALL_ERROR, params);
      }
    }// caso não seja uma chamada ao processo mu
    else {
      Type typeRefName = (Type)sectTypeEnv().getType(procRef);

      if(!(typeRefName instanceof UnknownType)) {

        if(!isProcess(procDecl)) {
          Object [] params = {currentProcess().getWord(), procDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_PROCESS_NAME, params);
        } else {
          ProcessType procType = (ProcessType)typeRefName;
          procSignature = procType.getProcessSignature();
          // adiciona os canais usados...
          List<NameTypePair> usedChans = getUsedChannels(procDecl);
          localCircTypeEnv().addUsedChans(usedChans);
          //

          List<NameTypePair> paramsOrIndexes = null;
          if(procSignature.getParamsOrIndexes() != null) {
            paramsOrIndexes = procSignature.getParamsOrIndexes().getNameTypePair();
          }
          // chama um método auxiliar que irá verificar se a chamada está correta
          checkCallProcess(term, paramsOrIndexes);
        }
      } 
      else {
        if(!compareDeclName(procDecl, currentProcess(), false)) {
          if (!containsObject(paraErrors(), term)) {
            paraErrors().add(term);
            List<NameTypePair> pairs = typeEnv().getTypeEnvAnn().getNameTypePair();
            addProcesses4PostCheck(currentProcess(), pairs);
          }
        }
        else {
          // tratamento especial para o caso de chamada recursiva          
          List<NameTypePair> paramsOrIndexes = getProcessInfo(procDecl).getParamsOrIndexes();
          // chama um método auxiliar que irá verificar se a chamada está correta
          checkCallProcess(term, paramsOrIndexes);
        }
      }
    }
    
    addProcessAnn(term, procSignature);
    
    return procSignature;
  }
  
  //ok - verificado em 15/09/2005 às 19:21
  public Object visitProcessIte(ProcessIte term)
  {
    List<Decl> decs = term.getDecl();
    CircusProcess proc = term.getCircusProcess();

    List<NameTypePair> allPairs = new ArrayList<NameTypePair>();
    List paramsError = new ArrayList<Object>();
    paramsError.add(currentProcess().getWord());

    for(Decl d : decs) {
      if (!(d instanceof VarDecl))
        throw new UnsupportedOperationException("Iterated processes accept only VarDecl!");
      VarDecl dec = (VarDecl)d;
      boolean declOK = isFinity(dec.getExpr());
      List<NameTypePair> pairs = (List<NameTypePair>)dec.accept(declChecker());
      allPairs = checkDecls(allPairs, pairs, term, ErrorMessage.REDECLARED_VAR_IN_PROCESS_ITE, paramsError);
      if(!declOK) {
        Object [] params = {currentProcess().getWord()};
        error(term, ErrorMessage.INFINITY_VALUES_IN_PROCESS_ITE, params);
        break;
      }
    }

    typeEnv().enterScope();

    typeEnv().add(allPairs);
    ProcessSignature procSig = (ProcessSignature)proc.accept(processChecker());
    ProcessSignature procSignature = cloneProcessSignature(procSig);
    Signature sig = factory().createSignature(allPairs);
    procSignature.setParamsOrIndexes(sig);
    
    typeEnv().exitScope();

    addProcessAnn(term, procSignature);

    return procSignature;
  }
  
  // Process ::= \Parallel Declaration @ |[CSExpression]| Process
  //ok - verificado em 15/09/2005 às 19:27
  public Object visitAlphabetisedParallelProcessIte(AlphabetisedParallelProcessIte term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //
    ProcessSignature procSignature = (ProcessSignature)visitProcessIte(term);
    
    return procSignature;
  }

  // Process ::= |[CSExpression]| Declaration @ Process
  //ok - verificado em 15/09/2005 às 19:28
  public Object visitParallelProcessIte(ParallelProcessIte term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //
    ProcessSignature procSignature = (ProcessSignature)visitProcessIte(term);
    
    return procSignature;
  }
  
  //não existe mais
  public Object visitAlphabetisedParallelProcessIdx(AlphabetisedParallelProcessIdx term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //
    ProcessSignature procSignature = (ProcessSignature)visitProcessIte(term);
    
    return procSignature;
  }

  //não existe mais
  public Object visitParallelProcessIdx(ParallelProcessIdx term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //
    ProcessSignature procSignature = (ProcessSignature)visitProcessIte(term);
    
    return procSignature;
  }

  // Process ::= \mu N @ Process
  // Process ::= \mu N @ ParamProcess
  //ok - verificado em 15/09/2005 às 19:31
  public Object visitMuProcess(MuProcess term)
  {
    DeclName name = term.getDeclName();
    CircusProcess proc = term.getCircusProcess();

    addMuProcess(name);    
    ProcessSignature signature = (ProcessSignature)proc.accept(processChecker());
    removeMuProcess(name);
    
    addProcessAnn(term, signature);
    
    return signature;
  }
  
  // Process ::= Communication -> Process
  //ok - verificado em 15/09/2005 às 19:32
  public Object visitPrefixingProcess(PrefixingProcess term)
  {
    RefName chanName = term.getCommunication().getChanName();
    //<04/11/2005>
    DeclName declName = factory().createDeclName(chanName.getWord(), null, null);
    term.getCommunication().getChanName().setDecl(declName);
    //
    CircusProcess proc = term.getCircusProcess();
    
    List<NameTypePair> inputVars = (List<NameTypePair>)term.getCommunication().accept(communicChecker());
    typeEnv().enterScope();
    addVars(inputVars);

    ProcessSignature procSig = (ProcessSignature)proc.accept(processChecker());
    typeEnv().exitScope();
    addProcessAnn(term, procSig);    
    
    return procSig;
  }

  // Process ::= Predicate & Process
  //ok - verificado em 15/09/2005 às 19:36
  public Object visitGuardedProcess(GuardedProcess term)
  {
    term.getPred().accept(predChecker());
    ProcessSignature signature = (ProcessSignature)term.getCircusProcess().accept(processChecker());
    addProcessAnn(term, signature);
    
    return signature;
  }

  // Process ::= Process \ CSExpression
  //ok - verificado em 15/09/2005 às 19:36
  public Object visitHideProcess(HideProcess term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //

    ProcessSignature signature = (ProcessSignature)term.getCircusProcess().accept(processChecker());
    addProcessAnn(term,  signature);
    
    return signature;
  }
  
  // Process ::= Process[N+ := N+]
  //ok - verificado em 15/09/2005 às 19:38
  public Object visitRenameProcess(RenameProcess term)
  {
    ProcessSignature procSignature = (ProcessSignature)term.getCircusProcess().accept(processChecker());
    List<RefName> oldNames = (List<RefName>)term.getOldNames();
    List<RefName> newNames = (List<RefName>)term.getNewNames();
    
    if(oldNames.size() == newNames.size()) {
      int i = 0;
      for(RefName oldChan : (List<RefName>)oldNames) {
        DeclName oldName = factory().createDeclName(oldChan.getWord(), null, null);
        DeclName newName = factory().createDeclName(newNames.get(i).getWord(), null, null);
        if(!isChannel(oldName) || !isChannel(newName)) {
          Object [] params = {currentProcess().getWord(), procSignature.getProcessName().getWord()};
          error(term, ErrorMessage.NAMES_ARE_NOT_CHANNELS_IN_PROC_RENAME, params);
          break;
        } else {
          Type oldType = getChannelType(oldName);
          Type newType = getChannelType(newName);
          Type2 expectedU = unwrapType(oldType);
          Type2 foundU = unwrapType(newType);
          if (unify(foundU, expectedU) != SUCC) {
            Object [] params = {currentProcess().getWord(), expectedU, foundU, i+1, procSignature.getProcessName().getWord()};
            error(term, ErrorMessage.PROC_RENAME_NOT_UNIFY, params);
            break;
          }   
          // adiciona os canais usados...
          List<NameTypePair> usedChans = new ArrayList<NameTypePair>();
          NameTypePair oldC = factory().createNameTypePair(oldName, oldType);
          usedChans.add(oldC);
          NameTypePair newC = factory().createNameTypePair(newName, newType);
          usedChans.add(newC);
          localCircTypeEnv().addUsedChans(usedChans);
          //
          i++;
        }
      }
    } else {
      Object [] params = {currentProcess().getWord(), oldNames.size(), newNames.size(), procSignature.getProcessName().getWord()};
      error(term, ErrorMessage.PROC_RENAME_DIFF_NUMBER_CHANS, params);
    }
    
    addProcessAnn(term, procSignature);
    
    return procSignature;
  }
  
  // Process ::= Process |[CSExpression]| Process
  //ok - verificado em 15/09/2005 às 19:41
  public Object visitParallelProcess(ParallelProcess term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //
    ProcessSignature procSignature = (ProcessSignature)visitProcess2(term);
    
    return procSignature;
  }

  // Process ::= Process |[CSExpression | CSExpression]| Process
  //ok - verificado em 15/09/2005 às 19:42
  public Object visitAlphabetisedParallelProcess(AlphabetisedParallelProcess term)
  {
    List<NameTypePair> allPairs = new ArrayList<NameTypePair>();
    ChanSetType typeCSL = (ChanSetType)term.getLeftAlpha().accept(exprChecker());
    ChanSetType typeCSR = (ChanSetType)term.getRightAlpha().accept(exprChecker());
    allPairs.addAll(typeCSL.getChannels().getNameTypePair());
    allPairs.addAll(typeCSR.getChannels().getNameTypePair());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(allPairs);
    //
    ProcessSignature procSignature = (ProcessSignature)visitProcess2(term);
    
    return procSignature;
  }

  // MÉTODOS AUXILIARES
  
  private boolean checkCall(DeclName procName, List decs, List types){
    boolean result = true;
    int i = 0;
    if(decs.size() == types.size()) {
      for(NameTypePair pair : (List<NameTypePair>)decs) {
        Type2 expectedU = unwrapType(pair.getType());
        Type2 foundU = unwrapType((Type)types.get(i));
        if(foundU instanceof UnknownType) {
          Object [] params = {currentProcess().getWord(), procName.getWord(), i+1};
          error(procName, ErrorMessage.PARAM_PROC_CALL_UNDECLARED_VAR, params);
          result = false;
          break;
        }
        if (unify(foundU, expectedU) != SUCC) {
          Object [] params = {currentProcess().getWord(), expectedU, foundU, i, procName.getWord()};
          error(procName, ErrorMessage.PARAM_PROC_CALL_NOT_UNIFY, params);
          result = false;
          break;
        }   
        i++;
      }
    } else {
      Object [] params = {currentProcess().getWord(), decs.size(), types.size(), procName.getWord()};
      error(procName, ErrorMessage.PROC_CALL_DIFF_NUMBER_EXPRS, params);
      result = false;
    }
    
    return result;
  }

  private List<NameTypePair> extractImplicitChans(List<NameTypePair> decls, List<NameTypePair> usedChans) {
    List<NameTypePair> result = new ArrayList<NameTypePair>();
    
    for(NameTypePair chan : usedChans) {
      DeclName chanName = chan.getName();
      Type chanType = chan.getType();
      String newName = chanName.getWord();
      List<Type> newType = new ArrayList<Type>();
      for(NameTypePair decl : decls) {
        newName = newName + "\\_" + decl.getName().getWord();
        newType.add(decl.getType());
      }
      
      if(chanType instanceof GivenType) {
        DeclName name = ((GivenType)chanType).getName();
        if(!(name.getWord().equals("Synch"))) {
          newType.add(chanType);
        }
      } else {
        newType.add(chanType);
      }

      DeclName newChanName = factory().createDeclName(newName, null, null);
      ProdType newChanType = factory().createProdType(newType);
      NameTypePair pair = factory().createNameTypePair(newChanName, newChanType);

      if(!result.contains(pair)) {
        result.add(pair);
      }
      
      if(isGenericChannel(chanName)) {
        localCircTypeEnv().addGenericImplicitChan(newChanName);
      }
    }
    return result;
  }

  private void addVarsState(NameTypePair pair, BasicProcess term) {
    ProcessInfo procInfo = getProcessInfo(currentProcess());
    DeclName stateName = pair.getName();
    SchemaType schType = (SchemaType)((PowerType)pair.getType()).getType();
    List<NameTypePair> varsState = schType.getSignature().getNameTypePair();
    for(NameTypePair varState : varsState) {
      //<04/11/2005>
      if(!procInfo.addLocalVar(varState)) {
        Object [] params = {currentProcess().getWord(), varState.getName().getWord()};
        error(term, ErrorMessage.REDECLARED_LOCAL_NAME_IN_STATE_PROCESS, params);
      }
      else {
        if(!localCircTypeEnv().addStateVar(varState)){
          Object [] params = {currentProcess().getWord(), varState.getName().getWord(), stateName.getWord()};
          error(term, ErrorMessage.REDECLARED_LOCAL_NAME, params);
        } 
      }
    }
    //<<15/06/2006>>
    localCircTypeEnv().addLocalVars(varsState);
    //
  }  

  private void addLocalVars(List<NameTypePair> pairs, BasicProcess term) {
    ProcessInfo procInfo = getProcessInfo(currentProcess());
    for(NameTypePair pair : pairs) {
      if(!procInfo.addLocalVar(pair)){
        Object [] params = {currentProcess().getWord(), pair.getName().getWord()};
        error(term, ErrorMessage.REDECLARED_LOCAL_NAME_IN_PROCESS, params);
      } 
    }
  }
//
  
  // TALVEZ FOSSE MAIS INTERESSANTE AQUI UM VISITOR... TALVEZ EU ESTEJA AMARRANDO
  // O CÓDIGO E QUALQUER ALTERAÇÃO NA ESTRUTURA, QUEBRA ESTE MÉTODO...
  private boolean isSchExprAction(Para para) {
    boolean result = false;
    
    if(para instanceof AxPara) {
      Decl axDecl = (Decl)((AxPara)para).getSchText().getDecl().get(0);
      if(axDecl instanceof ConstDecl) {
        Expr exprAx = ((ConstDecl)axDecl).getExpr();
        if(exprAx instanceof SchExpr) {
          SchText schText = ((SchExpr)exprAx).getSchText();
          List<Decl> decls = schText.getDecl();
          for(Decl decl : decls) {
            if((decl instanceof InclDecl)) {
              Expr expr = ((InclDecl)decl).getExpr();
              if(expr instanceof RefExpr) {
                String refName = ((RefExpr)expr).getRefName().getWord();
                String stateName = stateName().getWord();
                if(refName.equals(stateName) 
                   || refName.equals(ZString.DELTA + stateName) 
                   || refName.equals(ZString.XI + stateName)
                   || refName.equals(stateName + "'")) 
                {
                  result = true;
                  break;
                }
                else {
                  List<RefName> statesAux = statesAux();
                  for(RefName name : statesAux) {
                    if(refName.equals(name) 
                       || refName.equals(ZString.DELTA + name) 
                       || refName.equals(ZString.XI + name)
                       || refName.equals(name + "'")) 
                    {
                      result = true;
                      break;
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
    
    return result;
  }
  
  private boolean isSchExpr(Para para) {
    boolean result = true;
    
    if(para instanceof AxPara) {
      Decl axDecl = (Decl)((AxPara)para).getSchText().getDecl().get(0);
      if(axDecl instanceof ConstDecl) {
        Expr exprAx = ((ConstDecl)axDecl).getExpr();
        if(exprAx instanceof SchExpr) {
          result = false;
        }
      }
    }
    
    return result;
  }  
  
  private void extractStatesAux(Para para) {
    if(para instanceof AxPara) {
      Decl axDecl = (Decl)((AxPara)para).getSchText().getDecl().get(0);
      if(axDecl instanceof ConstDecl) {
        Expr exprAx = ((ConstDecl)axDecl).getExpr();
        if(exprAx instanceof SchExpr2) {
          Expr exprL = ((SchExpr2)exprAx).getLeftExpr();
          Expr exprR = ((SchExpr2)exprAx).getRightExpr();
          if((exprL instanceof RefExpr) && (exprR instanceof RefExpr)) {
            List<RefName> namesStateAux = new ArrayList<RefName>();
            RefName nameL = ((RefExpr)exprL).getRefName();
            RefName nameR = ((RefExpr)exprR).getRefName();
            namesStateAux.add(nameL);
            namesStateAux.add(nameR);
            setStatesAux(namesStateAux);
          }
        }
      }
    }
  }

  private void checkCallProcess(CallProcess term, List<NameTypePair> paramsOrIndexes) {
    
    DeclName procDecl = factory().createDeclName(term.getRefName());
    String kindOfProcess = getKindOfProcess(procDecl);
    List<Type> typeExprs = new ArrayList<Type>();
    List<Expr> exprs = null;
    
    switch(term.getCallType()) {
      case Param :
        if(!kindOfProcess.equals("PARAM")){
          Object [] params = {currentProcess().getWord(), procDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_PARAM_PROCESS_IN_PROC_CALL, params);
        }
        else {
          exprs = (List<Expr>)term.getExpr();
          for(Expr expr : exprs) {
            Type type = (Type)expr.accept(exprChecker());
            typeExprs.add(type);
          }
          checkCall(procDecl, paramsOrIndexes, typeExprs);
        }
        break;
      case Index :
        if(!kindOfProcess.equals("INDEX")){
          Object [] params = {currentProcess().getWord(), procDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_INDEX_PROCESS_IN_PROC_CALL, params);
        }
        else {
          exprs = (List<Expr>)term.getExpr();
          for(Expr expr : exprs) {
            Type type = (Type)expr.accept(exprChecker());
            typeExprs.add(type);
          }
          checkCall(procDecl, paramsOrIndexes, typeExprs);
        }
        break;
      case Gen :
        if(!isGenericProcess(procDecl)){
          Object [] params = {currentProcess().getWord(), procDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_GEN_PROCESS_IN_PROC_CALL, params);
        }
        else {
          exprs = (List<Expr>)term.getGenExpr();
          for(Expr expr : exprs) {
            Type type = (Type)expr.accept(exprChecker());
            if(!(type instanceof PowerType)) {
              // ERRO. A EXPRESSÃO DEVE SER UM CONJUNTO
              Object [] params = {currentProcess().getWord(), procDecl.getWord()};
              error(term, ErrorMessage.IS_NOT_POWER_TYPE_IN_GEN_PROCESS, params);
              break;
            }
            else {
              typeExprs.add(type);
            }
          }
          List<DeclName> genParams = getGenParamsProcess(procDecl);
          if(genParams.size() != typeExprs.size()) {
            Object [] params = {currentProcess().getWord(), procDecl.getWord(),
                                genParams.size(), typeExprs.size()};
            error(term, ErrorMessage.GEN_PROCESS_INSTANTIATION_ERROR, params);
          }
        }
        break;
      case GenParam :
        if(!isGenericProcess(procDecl)){
          Object [] params = {currentProcess().getWord(), procDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_GEN_PROCESS_IN_PROC_CALL, params);
        }
        else {
          List<Expr> genExprs = (List<Expr>)term.getGenExpr();
          List<Type> typeGenExprs = new ArrayList<Type>();
          for(Expr genExpr : genExprs) {
            Type type = (Type)genExpr.accept(exprChecker());
            typeGenExprs.add(type);
          }
          List<DeclName> genParams = getGenParamsProcess(procDecl);
          if(genParams.size() != typeGenExprs.size()) {
            Object [] params = {currentProcess().getWord(), procDecl.getWord(),
                                genParams.size(), typeGenExprs.size()};
            error(term, ErrorMessage.GEN_PROCESS_INSTANTIATION_ERROR, params);
          }
          if(!kindOfProcess.equals("PARAM")){
            Object [] params = {currentProcess().getWord(), procDecl.getWord()};
            error(term, ErrorMessage.IS_NOT_PARAM_PROCESS_IN_PROC_CALL, params);
          }
          else {
            exprs = (List<Expr>)term.getExpr();
            for(Expr expr : exprs) {
              Type type = (Type)expr.accept(exprChecker());
              typeExprs.add(type);
            }
            checkCall(procDecl, paramsOrIndexes, typeExprs);
          }
        }
        break;
      case GenIndex :
        if(!isGenericProcess(procDecl)){
          Object [] params = {currentProcess().getWord(), procDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_GEN_PROCESS_IN_PROC_CALL, params);
        }
        else {
          List<Expr> genExprs = (List<Expr>)term.getGenExpr();
          List<Type> typeGenExprs = new ArrayList<Type>();
          for(Expr genExpr : genExprs) {
            Type type = (Type)genExpr.accept(exprChecker());
            typeGenExprs.add(type);
          }
          List<DeclName> genParams = getGenParamsProcess(procDecl);
          if(genParams.size() != typeGenExprs.size()) {
            Object [] params = {currentProcess().getWord(), procDecl.getWord(),
                                genParams.size(), typeGenExprs.size()};
            error(term, ErrorMessage.GEN_PROCESS_INSTANTIATION_ERROR, params);
          }
          if(!kindOfProcess.equals("INDEX")){
            Object [] params = {currentProcess().getWord(), procDecl.getWord()};
            error(term, ErrorMessage.IS_NOT_INDEX_PROCESS_IN_PROC_CALL, params);
          }
          else {
            exprs = (List<Expr>)term.getExpr();
            for(Expr expr : exprs) {
              Type type = (Type)expr.accept(exprChecker());
              typeExprs.add(type);
            }
            checkCall(procDecl, paramsOrIndexes, typeExprs);
          }
        }
        break;
      case Normal :
        if(!kindOfProcess.equals("NORMAL")){
          Object [] params = {currentProcess().getWord(), procDecl.getWord()};
          error(term, ErrorMessage.PROC_CALL_NEEDS_PARAMS, params);
        }
        break;
    }
    
  }

  private void postActionCallCheck()
  {
    //post-check any previously unresolved expressions
    List<Object> paraErrors = new ArrayList<Object>();
    List pErrors = new ArrayList<Object>();
    pErrors.addAll(paraErrors());
    for (Object next : pErrors) {
      if (next instanceof CircusAction) {
        CircusAction act = (CircusAction) next;
        ErrorAnn errorAnn = (ErrorAnn) act.accept(postChecker());
        if (errorAnn != null) {
          paraErrors.add(errorAnn);
        }
      } 
      else {
        paraErrors.add(next);
      }
    }
    paraErrors().clear();
    paraErrors().addAll(paraErrors);
//    errors().addAll(paraErrors);
  }

}
