/*
 * SpecChecker.java
 *
 * Created on 15 de Junho de 2005, 21:15
 *
 * 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.circus.ast.CircusAction;
import net.sourceforge.czt.circus.ast.CircusProcess;
import net.sourceforge.czt.circus.ast.ProcessPara;
import static net.sourceforge.czt.typecheck.z.util.GlobalDefs.*;

import java.util.List;

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.session.*;
import net.sourceforge.czt.typecheck.z.util.*;
import net.sourceforge.czt.typecheck.z.impl.*;
import net.sourceforge.czt.base.util.*;
import net.sourceforge.czt.base.visitor.*;

/**
 *
 * @author Manuela 
 */
public class SpecChecker   
  extends Checker
  implements ZSectVisitor
{
  //a Z spec checker
  protected net.sourceforge.czt.typecheck.z.SpecChecker zSpecChecker_;

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

  public Object visitTerm(Term term)
  {
    return term.accept(zSpecChecker_);
  }

  public Object visitZSect(ZSect zSect)
  {
    //set the section name
    sectName(zSect.getName());

    //if this section has already been declared, raise an error
    if (sectTypeEnv().isChecked(sectName())) {
      Object [] params = {zSect.getName()};
      error(zSect, ErrorMessage.REDECLARED_SECTION, params);
    }

    //set this as the new section in SectTypeEnv
    sectTypeEnv().setSection(sectName());

    //get and visit the parent sections of the current section
    List<Parent> parents = zSect.getParent();
    List<String> names = new ArrayList<String>();
    for (Parent parent : parents) {
      parent.accept(specChecker());

      if (names.contains(parent.getWord())) {
        Object [] params = {parent.getWord(), sectName()};
        error(parent, ErrorMessage.REDECLARED_PARENT, params);
      }
      else if (parent.getWord().equals(sectName())) {
        Object [] params = {parent.getWord()};
        error(parent, ErrorMessage.SELF_PARENT, params);
      }
      else {
        names.add(parent.getWord());
      }
    }

//    List<Para> paras = zSect.getPara();
    //get and visit the paragraphs of the current section
    List<Para> allParas = zSect.getPara();
    List<Para> paras = new ArrayList<Para>();
    
    //remove as definições de processos implicitos da lista de parágrafos
    //e os adicionam numa lista específica.
    if(zSect.getName().equals("CircusParserSection")) {
      List<ProcessPara> implicitProcesses = new ArrayList<ProcessPara>();
      for(Para p : allParas) {
        if(p instanceof ProcessPara) {
          String nameProc = ((ProcessPara)p).getDeclName().getWord();
          if(nameProc.startsWith("$$implicitProcess_")){
            implicitProcesses.add((ProcessPara)p);
          } else {
            paras.add(p);
          }
        } else {
          paras.add(p);
        }
      }
      setOnTheFlyProcesses(implicitProcesses);
    } else {
      paras = allParas;
    }
    
    for (Para para : paras) {
      //add the global definitions to the SectTypeEnv
      Signature signature = (Signature) para.accept(paraChecker());
      List<NameTypePair> pairs = signature.getNameTypePair();
      for (NameTypePair pair : pairs) {
        //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);
        }
      }
      postCheck();
    }

    // CHAMAR AQUI O postProcessCallCheck...
    // útil para chamadas cíclicas de Processos: A \defs B e B \defs A ...
    postProcessCallCheck();
    
    if (useBeforeDecl() && !sectTypeEnv().getSecondTime()) {
      errors().clear();
      removeErrorAndTypeAnns(zSect);
      sectTypeEnv().setSecondTime(true);
      zSect.accept(specChecker());
    }

    //annotate this section with the type info from this section
    //and its parents
    addAnn(zSect, sectTypeEnv().getSectTypeEnvAnn());

    //get the result and return it
    Boolean result = getResult();
    if (result == Boolean.FALSE) {
      removeTypeAnns(zSect);
    }
    return result;
  }

  /**
   * Return the result result of the typechecking process -- FALSE if
   * there are any error messages, TRUE otherwise.
   */
  protected Boolean getResult()
  {
    Boolean result = Boolean.TRUE;
    if (errors().size() > 0) {
      result = Boolean.FALSE;
    }
    return result;
  }

  protected void postCheck()
  {
    //post-check any previously unresolved expressions
    List<ErrorAnn> paraErrors = new ArrayList<ErrorAnn>();
    List<Object> pErrors = new ArrayList<Object>();
    for (Object next : paraErrors()) {
      if (next instanceof Expr) {
        Expr expr = (Expr) next;
        ErrorAnn errorAnn = (ErrorAnn) expr.accept(postChecker());
        if (errorAnn != null) {
          paraErrors.add(errorAnn);
        }
      } 
      else if (next instanceof ErrorAnn) {
        ErrorAnn errorAnn = (ErrorAnn) next;
        paraErrors.add(errorAnn);
      }
      else {
        pErrors.add(next);
      }
    }
    paraErrors().clear();
    paraErrors().addAll(pErrors);
    errors().addAll(paraErrors);
  }
  
  // chamar isto depois que todos os paragrafos forem checados
  protected void postProcessCallCheck()
  {
    //post-check any previously unresolved expressions
    List<ErrorAnn> paraErrors = new ArrayList<ErrorAnn>();
    List<Object> errors = new ArrayList<Object>();
    errors.addAll(paraErrors());
    for (Object next : errors) {
      if (next instanceof CircusProcess) {
        CircusProcess proc = (CircusProcess) next;
        ErrorAnn errorAnn = (ErrorAnn) proc.accept(postChecker());
        if (errorAnn != null) {
          paraErrors.add(errorAnn);
        }
      } 
//      else {
//        paraErrors.add(next);
//      }
    }
    paraErrors().clear();
//    paraErrors().addAll(paraErrors);
    errors().addAll(paraErrors);
  }

}