/*
 * ActionChecker.java
 *
 * Created on 18 de Junho de 2005, 13:07
 *
 * 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.circustools.ast.ActionType;
import net.sourceforge.czt.circustools.ast.ChanSetType;
import net.sourceforge.czt.circustools.ast.NameSetType;
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.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.ActionSignature;
import net.sourceforge.czt.z.util.ZString;

/**
 *
 * @author Manuela
 */
public class ActionChecker
  extends Checker
  implements CircusActionVisitor,
             Action1Visitor,
             Action2Visitor,
             SchExprActionVisitor,
             BasicActionVisitor,
             CallActionVisitor,
             MuActionVisitor,
             PrefixingActionVisitor,
             SubstitutionActionVisitor,
             GuardedActionVisitor,
             HideActionVisitor,
             ActionIteVisitor,
             ParamActionVisitor,
             AlphabetisedParallelActionIteVisitor,
             InterleaveActionIteVisitor,
             ParallelActionIteVisitor,
             InterleaveActionVisitor,
             ParallelActionVisitor,
             AlphabetisedParallelActionVisitor,
             CircusCommandVisitor
{
  
  //a Z decl checker
  protected net.sourceforge.czt.typecheck.z.DeclChecker zDeclChecker_;

  /** Creates a new instance of ActionChecker */
  public ActionChecker(TypeChecker typeChecker)
  {
    super(typeChecker);
    zDeclChecker_ =
      new net.sourceforge.czt.typecheck.z.DeclChecker(typeChecker);
  }
  
  public Object visitCircusAction(CircusAction term)
  {
    return factory().createActionSignature();
  }

  //ok - verificado em 15/09/2005 às 16:42
  public Object visitAction1(Action1 term)
  {
    ActionSignature actionSignature = (ActionSignature)term.getCircusAction().accept(actionChecker());
    addActionAnn(term, actionSignature);    
    return actionSignature;
  }
  
  //ok - verificado em 15/09/2005 às 16:42
  public Object visitAction2(Action2 term)
  {
    ActionSignature actionSigL = (ActionSignature)term.getLeftAction().accept(actionChecker());
    ActionSignature actionSigR = (ActionSignature)term.getRightAction().accept(actionChecker());
    ActionSignature result = joinActionSignature(actionSigL, actionSigR);

    addActionAnn(term, result);

    return result;
  }

  // Action ::= Schema-Exp
  //ok - verificado em 15/09/2005 às 16:50
  public Object visitSchExprAction(SchExprAction term)
  {
    ActionSignature actionSignature = factory().createActionSignature();

    Type typeExpr = (Type)term.getExpr().accept(exprChecker());

    SchemaType schType = (SchemaType)((PowerType)typeExpr).getType();
    Signature vars = schType.getSignature();
    actionSignature.setLocalVarsSignature(vars);

    addActionAnn(term, actionSignature);

    return actionSignature;
  }

  // Action ::= Chaos
  // Action ::= Skip
  // Action ::= Stop
  //ok - verificado em 15/09/2005 às 16:52
  public Object visitBasicAction(BasicAction term)
  {
    ActionSignature actionSignature = factory().createActionSignature();
    addActionAnn(term, actionSignature);
    return actionSignature;
  }

  // Action ::= N
  // Action ::= N(Expression+)
  // Action ::= (Declaration @ Action)(Expression+)
  // Action ::= (\mu N @ ParAction)(Expression+)
  //ok - verificado em 15/09/2005 às 17:02
  public Object visitCallAction(CallAction term)
  {
    ActionSignature actionSignature = factory().createActionSignature();
    RefName actionRef = term.getRefName();
    DeclName actionDecl = factory().createDeclName(actionRef);

    if(actionDecl.getWord().startsWith("$$implicitAction_")) {
      // pegar da lista de ações implícitos, fazer a verificação e incluir no
      // TypeEnv!!
      List<ActionPara> implicitActions = (List<ActionPara>)localCircTypeEnv().getOnTheFlyActions();
      for(ActionPara implicitAction : implicitActions) {
        if(compareDeclName(actionDecl, implicitAction.getDeclName(), false)) {
          Signature implicitActionSig = (Signature)implicitAction.accept(paraChecker());
        }
      }
    }
    
    // verifica se é uma chamada a uma ação mu
    if(isMuAction(actionDecl)) {
      if(!(term.getExpr().isEmpty())) {
        Object [] params = {currentAction().getWord(), currentProcess().getWord(), actionDecl.getWord()};
        error(term, ErrorMessage.MU_ACTION_CALL_ERROR, params);
      }
    }// caso não seja uma chamada a uma ação mu
    else {

      Type typeRefName = typeEnv().getType(actionRef);

      if(!(typeRefName instanceof UnknownType)) {
        if(!localCircTypeEnv().isAction(actionDecl)) {
          Object [] params = {currentAction().getWord(), currentProcess().getWord(), actionDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_ACTION_NAME, params);
        } 
        else {
          if(typeRefName instanceof ActionType) {
            ActionType actionType = (ActionType)typeRefName;
            actionSignature = actionType.getActionSignature();
          }
          // a ação é um schExpr
          else {
            SchemaType schType = (SchemaType)((PowerType)typeRefName).getType();
            Signature vars = schType.getSignature();
            actionSignature.setActionName(actionDecl);
            actionSignature.setLocalVarsSignature(vars);
          }
          
          List<NameTypePair> params = null;
          if(actionSignature.getParams() != null) {
            params = actionSignature.getParams().getNameTypePair();
          }          

          // chama um método auxiliar que irá verificar se a chamada está correta
          checkCallAction(term, params);
        }
      } 
      else {
        if(!compareDeclName(actionDecl, currentAction(), false)) {
          //add this reference for post checking
          if (!containsObject(paraErrors(), term)) {
            paraErrors().add(term);
/*            ActionInfo actionInfo = localCircTypeEnv().getActionInfo(currentAction());
            List<NameTypePair> pairs = new ArrayList<NameTypePair>();
            if(actionInfo != null) {
              pairs = actionInfo.getLocalVars();
            } */
            List<NameTypePair> pairs = typeEnv().getTypeEnvAnn().getNameTypePair();
            addAction4PostCheck(currentAction(), pairs);
          }
        }
        else {
          // tratamento especial para o caso de chamada recursiva
          List<NameTypePair> params = localCircTypeEnv().getActionInfo(actionDecl).getParams();
          // chama um método auxiliar que irá verificar se a chamada está correta
          checkCallAction(term, params);
        }
      }
    }
    
    addActionAnn(term, actionSignature);
    
    return actionSignature;
  }
  
  // Action ::= \mu N @ Action
  //ok - verificado em 15/09/2005 às 17:03
  public Object visitMuAction(MuAction term)
  {
    DeclName name = term.getDeclName();
    CircusAction action = term.getCircusAction();
    
    addMuAction(name);
    ActionSignature signature = (ActionSignature)action.accept(actionChecker());
    removeMuAction(name);
    
    addActionAnn(term, signature);
    
    return signature;
  }
  
  // Action ::= Communication -> Action
  //ok -  verificado em 15/09/2005 às 17:05
  public Object visitPrefixingAction(PrefixingAction term)
  {
    CircusAction action = term.getCircusAction();
    
    // <04/11/2005>
    RefName chanName = term.getCommunication().getChanName();
    DeclName declName = factory().createDeclName(chanName.getWord(), null, null);
    term.getCommunication().getChanName().setDecl(declName);
    //

    List<NameTypePair> inputVars = (List<NameTypePair>)term.getCommunication().accept(communicChecker());

    typeEnv().enterScope();
    //<<15/06/2006>>
    localCircTypeEnv().enterScopeLocalVars();
    //

    addVars(inputVars);
    //
    localCircTypeEnv().addLocalVars(inputVars);
    //
    

    ActionSignature actionSignature = (ActionSignature)action.accept(actionChecker());

    //<<15/06/2006>>
    localCircTypeEnv().exitScopeLocalVars();
    //
    typeEnv().exitScope();
 
    addActionAnn(term, actionSignature);    
    return actionSignature;
  }

  // Action ::= Action[N+ := N+]
  //ok - verificado em 15/09/2005 às 17:06
  public Object visitSubstitutionAction(SubstitutionAction term)
  {
    ActionSignature actionSignature = (ActionSignature)term.getCircusAction().accept(actionChecker());
    List<RefName> oldNames = (List<RefName>)term.getOldNames();
    List<RefName> newNames = (List<RefName>)term.getNewNames();
    
    if(oldNames.size() == newNames.size()) {
      int i = 0;
      for(RefName oldName : (List<RefName>)oldNames) {
        RefName newName = newNames.get(0);

        if(!isLocalVar(oldName)) {
          Object [] params = {currentAction().getWord(), currentProcess().getWord(), oldName.getWord()};
          error(term, ErrorMessage.IS_NOT_LOCAL_VAR_NAME_IN_SUBST_ACTION, params);
          break;
        } 
        else if (!isLocalVar(newName)) {
          Object [] params = {currentAction().getWord(), currentProcess().getWord(), newName.getWord()};
          error(term, ErrorMessage.IS_NOT_LOCAL_VAR_NAME_IN_SUBST_ACTION, params);
          break;
        }
        else {
          Type2 expectedU = unwrapType(typeEnv().getType(oldName));
          Type2 foundU = unwrapType(typeEnv().getType(newName));
          if(foundU instanceof UnknownType) {
            Object [] params = {currentAction().getWord(), currentProcess().getWord(), 
                                actionSignature.getActionName().getWord(), newName.getWord()};
            error(term, ErrorMessage.RENAME_ACTION_UNDECLARED_VAR, params);
          } 
          else if(expectedU instanceof UnknownType) {
            Object [] params = {currentAction().getWord(), currentProcess().getWord(), 
                                actionSignature.getActionName().getWord(), oldName.getWord()};
            error(term, ErrorMessage.RENAME_ACTION_UNDECLARED_VAR, params);
          }
          else if (unify(foundU, expectedU) != SUCC) {
            Object [] params = {currentAction().getWord(), currentProcess().getWord(), 
                                actionSignature.getActionName().getWord(), expectedU, foundU, i+1};
            error(term, ErrorMessage.ACTION_RENAME_NOT_UNIFY, params);
            break;
          }   
          i++;
        }
      }
    } else {
      Object [] params = {currentAction().getWord(), currentProcess().getWord(), 
                          actionSignature.getActionName().getWord(), oldNames.size(), newNames.size()};
      error(term, ErrorMessage.ACTION_RENAME_DIFF_NUMBER_VARS, params);
    }
    
    addActionAnn(term, actionSignature);
    return actionSignature;
  }
  
  // Action ::= Predicate & Action
  //ok - verificado em 15/09/2005 às 17:08
  public Object visitGuardedAction(GuardedAction term)
  {
    term.getPred().accept(predChecker());
    ActionSignature signature = (ActionSignature)term.getCircusAction().accept(actionChecker());
    addActionAnn(term, signature);
    
    return signature;
  }
  
  // Action ::= Action \ CSExpression
  //ok - verificado em 15/09/2005 às 17:09
  public Object visitHideAction(HideAction term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //
    
    ActionSignature signature = (ActionSignature)term.getCircusAction().accept(actionChecker());
    addActionAnn(term,  signature);
    
    return signature;
  }
  
  //ok - verificado em 15/09/2005 às 17:47
  public Object visitActionIte(ActionIte term)
  {
    List<Decl> decs = term.getDecl();
    CircusAction action = term.getCircusAction();

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

    for(Decl d : decs) {
      if (!(d instanceof VarDecl))
          throw new UnsupportedOperationException("Iterated actions 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_ACTION_ITE, paramsError);
      if(!declOK) {
        Object [] params = {currentAction().getWord(), currentProcess().getWord()};
        error(term, ErrorMessage.INFINITY_VALUES_IN_ACTION_ITE, params);
        break;
      }
    }
    typeEnv().enterScope();

    typeEnv().add(allPairs);
    ActionSignature actionSig = (ActionSignature)action.accept(actionChecker());
    ActionSignature actionSignature = cloneActionSignature(actionSig);
    Signature sig = factory().createSignature(allPairs);
    actionSignature.setLocalVarsSignature(sig);
    
    typeEnv().exitScope();

    return actionSignature;
  }

  // Action ::= Declaration @ Action
  //ok - verificado em 15/09/2005 às 18:12
  public Object visitParamAction(ParamAction term)
  {
    List<Decl> decls = (List<Decl>)term.getDecl();
    CircusAction action = term.getCircusAction();

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

    for(Decl d : decls) {
      if (!(d instanceof VarDecl))
        throw new UnsupportedOperationException("Parameterised actions accept only VarDecl!");
      VarDecl decl = (VarDecl)d;
      List<NameTypePair> pairs = (List<NameTypePair>)decl.accept(declChecker());
      allPairs = checkDecls(allPairs, pairs, term, ErrorMessage.REDECLARED_PARAM_IN_ACTION, paramsError);
    }
    
    // atualiza informações sobre a ação
    ActionInfo actionInfo = localCircTypeEnv().getActionInfo(currentAction());
    actionInfo.setIsParam(true);
    actionInfo.setParams(allPairs);
//    actionInfo.getLocalVars().addAll(allPairs);

    typeEnv().enterScope();
    
    typeEnv().add(allPairs);    
    ActionSignature actionSig = (ActionSignature)action.accept(actionChecker());
    ActionSignature actionSignature = cloneActionSignature(actionSig);
    Signature varsSig = factory().createSignature(allPairs);
    actionSignature.setParams(varsSig);
    typeEnv().exitScope();
    
    addActionAnn(term, actionSignature);
    
    return actionSignature;
  }
  
  // Action ::= \Parallel Declaration @ |[NSExpression | CSExpression]| Action
  // Action ::= \Parallel Declaration @ |[CSExpression]| Action
  //ok - verificado em 15/09/2005 às 17:52
  public Object visitAlphabetisedParallelActionIte(AlphabetisedParallelActionIte term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //

    NameSetType typeNS = (NameSetType)term.getNameSet().accept(exprChecker());

    ActionSignature actionSignature = (ActionSignature)visitActionIte(term);
    addActionAnn(term, actionSignature);
    
    return actionSignature;
  }

  // Action ::= \Interleave Declaration @ Action
  // Action ::= \Interleave Declaration @ ||[NSExpression]|| Action
  //ok - verificado em 15/09/2005 às 17:53
  public Object visitInterleaveActionIte(InterleaveActionIte term)
  {
    NameSetType typeNS = (NameSetType)term.getNameSet().accept(exprChecker());
    
    ActionSignature actionSignature = (ActionSignature)visitActionIte(term);
    addActionAnn(term, actionSignature);
    
    return actionSignature;
  }

  // Action ::= |[CSExpression]| Declaration @ |[NSExpression]| Action
  // Action ::= |[CSExpression]| Declaration @ Action
  //ok - verificado em 15/09/2005 às 17:52
  public Object visitParallelActionIte(ParallelActionIte term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //

    NameSetType typeNS = (NameSetType)term.getNameSet().accept(exprChecker());

    ActionSignature actionSignature = (ActionSignature)visitActionIte(term);
    addActionAnn(term, actionSignature);
    
    return actionSignature;
  }
  
  // Action ::= Action \interleave Action
  // Action ::= Action ||[NSExpression | NSExpressio]|| Action
  //ok - verificado em 15/09/2005 às 18:04
  public Object visitInterleaveAction(InterleaveAction term)
  {
    NameSetType typeNSL = (NameSetType)term.getLeftNameSet().accept(exprChecker());
    NameSetType typeNSR = (NameSetType)term.getRightNameSet().accept(exprChecker());

    ActionSignature actionSignature = (ActionSignature)visitAction2(term);
    
    return actionSignature;
  }

  // Action ::= Action |[CSExpression]| Action
  // Action ::= Action |[NSExpression | CSExpression | NSExpression]| Action
  //ok - verificado em 15/09/2005 às 18:07
  public Object visitParallelAction(ParallelAction term)
  {
    ChanSetType typeCS = (ChanSetType)term.getChannelSet().accept(exprChecker());
    // adicionando os canais usados...
    localCircTypeEnv().addUsedChans(typeCS.getChannels().getNameTypePair());
    //
    
    term.getLeftNameSet().accept(exprChecker());
    term.getRightNameSet().accept(exprChecker());
    ActionSignature actionSignature = (ActionSignature)visitAction2(term);
    
    return actionSignature;
  }

  // Action ::= Action |[CSExpression || CSExpression]| Action
  // Action ::= Action |[NSExpression | CSExpression || CSExpression | NSExpression]| Action
  //ok - verificado em 15/09/2005 às 18:
  public Object visitAlphabetisedParallelAction(AlphabetisedParallelAction 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);
    //
    
    term.getLeftNameSet().accept(exprChecker());
    term.getRightNameSet().accept(exprChecker());
    ActionSignature actionSignature = (ActionSignature)visitAction2(term);
    
    return actionSignature;
  }

  // Action ::= ParamCommand
  //ok - verificado em 15/09/2005 às 18:10
  public Object visitCircusCommand(CircusCommand term)
  {
    return term.accept(commandChecker());
  }

  // Funções auxiliares
  
  private boolean checkCall(DeclName actionName, 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 = {currentAction().getWord(), currentProcess().getWord(), actionName.getWord(), i+1};
          error(actionName, ErrorMessage.PARAM_ACTION_CALL_UNDECLARED_VAR, params);
          result = false;
          break;
        }
        if(unify(foundU, expectedU) != SUCC) {
          Object [] params = {currentAction().getWord(), currentProcess().getWord(), actionName.getWord(), expectedU, foundU, i+1};
          error(actionName, ErrorMessage.PARAM_ACTION_CALL_NOT_UNIFY, params);
          result = false;
          break;
        }   
        i++;
      }
    } else {
      Object [] params = {currentAction().getWord(), currentProcess().getWord(),decs.size(), types.size(), actionName.getWord()};
      error(actionName, ErrorMessage.ACTION_CALL_DIFF_NUMBER_EXPRS, params);
      result = false;
    }
    
    return result;
  }

  private void checkCallAction(CallAction term, List<NameTypePair> params) {
    
    DeclName actionDecl = factory().createDeclName(term.getRefName());
    
    switch(term.getCallType()) {
      case Param :
        if(!localCircTypeEnv().isParamAction(actionDecl)){
          Object [] paramsError = {currentAction().getWord(), currentProcess().getWord(), actionDecl.getWord()};
          error(term, ErrorMessage.IS_NOT_PARAM_ACTION_IN_ACTION_CALL, paramsError);
        }
        else {
          List<Type> typeExprs = new ArrayList<Type>();
          List<Expr> exprs = null;
          exprs = (List<Expr>)term.getExpr();
          for(Expr expr : exprs) {
            Type type = (Type)expr.accept(exprChecker());
            typeExprs.add(type);
          }
          checkCall(actionDecl, params, typeExprs);
        }
        break;
      case Normal :
        if(localCircTypeEnv().isParamAction(actionDecl)) {
          Object [] paramsError = {currentAction().getWord(), currentProcess().getWord(), actionDecl.getWord()};
          error(term, ErrorMessage.PARAM_ACTION_CALL_WITHOUT_EXPRS, paramsError);
        }
        break;
    }
  }
  
}
