/*
 * ExprChecker.java
 *
 * Created on 18 de Junho de 2005, 09:03
 *
 * 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.circustools.ast.ChanSetType;
import net.sourceforge.czt.circustools.ast.NameSetType;

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

import net.sourceforge.czt.base.ast.*;
import net.sourceforge.czt.base.visitor.*;
import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.z.visitor.*;
import net.sourceforge.czt.circus.ast.*;
import net.sourceforge.czt.circus.visitor.*;
import net.sourceforge.czt.typecheck.z.util.*;
import net.sourceforge.czt.typecheck.z.impl.*;
import net.sourceforge.czt.typecheck.circus.impl.*;
import net.sourceforge.czt.typecheck.z.*;

/**
 *
 * @author Manuela
 */
public class ExprChecker 
  extends Checker
  implements 
    ApplChannelSetVisitor,
    RefChannelSetVisitor,
    BasicChannelSetVisitor,
    ApplNameSetVisitor,
    RefNameSetVisitor,
    BasicNameSetVisitor
{
    
  //a Z expr checker
  protected net.sourceforge.czt.typecheck.z.ExprChecker zExprChecker_;

  public ExprChecker(TypeChecker typeChecker)
  {
    super(typeChecker);
    zExprChecker_ =
      new net.sourceforge.czt.typecheck.z.ExprChecker(typeChecker);
  }

  // Expression
  public Object visitTerm(Term term)
  {
    return term.accept(zExprChecker_);
  }

  // CSExpression ::= CSExpression \cup CSExpression
  // CSExpression ::= CSExpression \cap CSExpression
  // CSExpression ::= CSExpression \setminus CSExpression
  //ok - verificado em 15/09/2005 ās 13:12
  public Object visitApplChannelSet(ApplChannelSet term)
  {
    List<NameTypePair> allPairs = new ArrayList<NameTypePair>();
    
    TupleExpr tupleExpr = (TupleExpr)((ApplExpr)term.getExpr()).getRightExpr();
    
    List<Expr> exprs = tupleExpr.getExpr();
    ChannelSet exprChanSet = null;
    for (Expr expr : exprs) {
      if (expr instanceof RefExpr) {
        exprChanSet = factory().createRefChannelSet(((RefExpr)expr).getRefName());
      } else if (expr instanceof SetExpr) {
        List<RefExpr> refExprs = ((SetExpr)expr).getExpr();
        ListTerm newExprs = listTerm();
        for(RefExpr rexpr : refExprs) {
          if (!(rexpr instanceof RefExpr))
              throw new UnsupportedOperationException("Circus typechecker only supports simple set operators for application expressions of channel sets.");
          RefExpr refExpr = (RefExpr)rexpr;
          newExprs.add(refExpr.getRefName());
        }
        exprChanSet = factory().createBasicChannelSet(newExprs);
      } else {
        exprChanSet = factory().createApplChannelSet(expr);
      }
      Signature sig = ((ChanSetType)exprChanSet.accept(exprChecker())).getChannels();
      List<NameTypePair> pairs = sig.getNameTypePair();
      for(NameTypePair pair : pairs) {
        if(!allPairs.contains(pair)) {
          allPairs.add(pair);
        }
      }
    }
   
    Signature channelsSig = factory().createSignature(allPairs);
    ChanSetType type = factory().createChanSetType(channelsSig);
    
    addTypeAnn(term, type);

    return type;
  }

  // CSExpression ::= N
  //ok - verificado em 15/09/2005 ās 11:10
  public Object visitRefChannelSet(RefChannelSet term)
  {
    RefName chansetRef = term.getRefName();
    Signature channelsSig = factory().createSignature(new ArrayList<NameTypePair>());
    ChanSetType type = factory().createChanSetType(channelsSig);
    DeclName chansetDecl = factory().createDeclName(chansetRef.getWord(), null, null);
    
    if(!isChannelSet(chansetDecl)){
      Object [] params = {chansetRef.getWord()};
      error(term, ErrorMessage.IS_NOT_CHANSET_NAME, params);
    }
    else{
      type = (ChanSetType)sectTypeEnv().getType(chansetRef);
    }
    
    addTypeAnn(term, type);

    return type;
  }

  // CSExpression ::= {| |}
  // CSExpression ::= {| N+ |}
  //ok - verificado em 15/09/2005 ās 11:09
  public Object visitBasicChannelSet(BasicChannelSet term)
  {
    List<RefName> chanDecls = term.getRefName();
    List<NameTypePair> pairs = new ArrayList<NameTypePair>();
    
    for(RefName chanDecl : chanDecls) {
      DeclName decl = factory().createDeclName(chanDecl);
      if(!isChannel(decl)){ 
        Object [] params = {chanDecl.getDecl().getWord()};
        error(term, ErrorMessage.IS_NOT_CHANNEL_IN_CHANSET, params);
      } 
      else {
        Type typeChan = getChannelType(decl);
        NameTypePair pair = factory().createNameTypePair(decl, typeChan);
        pairs.add(pair);
      }
    }

    Signature channelsSig = factory().createSignature(pairs);
    Type type = factory().createChanSetType(channelsSig);
    
    addTypeAnn(term, type);

    return type;
  }

  // NSExpression ::= NSExpression \cup NSExpression
  // NSExpression ::= NSExpression \cap NSExpression
  // NSExpression ::= NSExpression \setminus NSExpression
  //ok - verificado em 15/09/2005 ās 13:14
  public Object visitApplNameSet(ApplNameSet term)
  {
    List<NameTypePair> allPairs = new ArrayList<NameTypePair>();    
    TupleExpr tupleExpr = (TupleExpr)((ApplExpr)term.getExpr()).getRightExpr();    
    List<Expr> exprs = tupleExpr.getExpr();
    
    NameSet exprNameSet = null;
    for (Expr expr : exprs) {
      if (expr instanceof RefExpr) {
        exprNameSet = factory().createRefNameSet(((RefExpr)expr).getRefName());
      } else if (expr instanceof SetExpr) {
        List<RefExpr> refExprs = ((SetExpr)expr).getExpr();
        ListTerm newNames = listTerm();
        for(Expr rexpr : refExprs) {
          if (!(rexpr instanceof RefExpr))
              throw new UnsupportedOperationException("Circus typechecker only supports simple set operators for application expressions of name sets.");
          RefExpr refExpr = (RefExpr)rexpr;
          newNames.add(refExpr.getRefName());
          // TODO: Opps... what about the generic types from refExpr.getExprList()?
        }
        exprNameSet = factory().createBasicNameSet(newNames);
      } else {
        exprNameSet = factory().createApplNameSet(expr);
      }
      Signature sig = ((NameSetType)exprNameSet.accept(exprChecker())).getNames();
      List<NameTypePair> pairs = sig.getNameTypePair();
      for(NameTypePair pair : pairs) {
        if(!allPairs.contains(pair)) {
          allPairs.add(pair);
        }
      }
    }
   
    Signature namesSig = factory().createSignature(allPairs);
    NameSetType type = factory().createNameSetType(namesSig);
    
    addTypeAnn(term, type);

    return type;
  }

  // NSExpression ::= N
  //ok - verificado em 15/09/2005 ās 13:15
  public Object visitRefNameSet(RefNameSet term)
  {
    RefName namesetRef = term.getRefName();
    Type type = factory().createNameSetType();
    DeclName name = factory().createDeclName(namesetRef);
    
    if(!localCircTypeEnv().isNameSet(name)){
      Object [] params = {name.getWord()};
      error(term, ErrorMessage.IS_NOT_NAMESET_NAME, params);
    }
    else{
      type = unwrapType(typeEnv().getType(namesetRef));
    }

    addTypeAnn(term, type);

    return type;
  }

  // NSExpression ::= {}
  // NSExpression ::= {N+}
  //ok - verificado em 15/09/2005 ās 13:16
  public Object visitBasicNameSet(BasicNameSet term)
  {
    List<RefName> nameDecls = term.getRefName();
    NameSetType result = factory().createNameSetType();
    List<NameTypePair> pairs = new ArrayList<NameTypePair>();
    
    for(RefName nameDecl : nameDecls) {
      DeclName name = nameDecl.getDecl();
      if(isLocalVar(nameDecl)) {
        Type type = typeEnv().getType(nameDecl);
        NameTypePair pair = factory().createNameTypePair(name, type);
        pairs.add(pair);
      } 
      else {
        Object [] params = {currentProcess().getWord(), name.getWord()};
        error(term, ErrorMessage.IS_NOT_LOCAL_VAR_NAME_IN_NAMESET, params);
        break;
      }
    }

    Signature namesSig = factory().createSignature(pairs);
    Type type = factory().createNameSetType(namesSig);
   
    addTypeAnn(term, type);

    return type;
  }
  
}
