/*
 * TypeChecker.java
 *
 * Created on 15 de Junho de 2005, 21:20
 *
 * 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.List;
import net.sourceforge.czt.base.ast.Term;
import net.sourceforge.czt.circustools.ast.CircusToolsFactory;
import net.sourceforge.czt.circustools.impl.CircusToolsFactoryImpl;
import net.sourceforge.czt.typecheck.z.util.SectTypeEnv;
import net.sourceforge.czt.typecheck.z.util.TypeEnv;

import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.circus.ast.*;
import net.sourceforge.czt.session.*;
import net.sourceforge.czt.z.impl.ZFactoryImpl;
import net.sourceforge.czt.typecheck.circus.util.*;
import net.sourceforge.czt.typecheck.circus.impl.*;
import net.sourceforge.czt.typecheck.circus.util.ChannelDeclChecker;
/**
 *
 * @author Manuela 
 */
public class TypeChecker 
  extends net.sourceforge.czt.typecheck.z.TypeChecker
{
    
  //a factory for object types
  protected net.sourceforge.czt.typecheck.circus.impl.Factory circusFactory_;
  
  //the name of the current process being typechecked - null if we are
  //not typechecking a process paragraph
  protected DeclName currentProcess_;

  //the name of the current action being typechecked - null if we are
  //not typechecking a action paragraph
  protected DeclName currentAction_;

  //the name of the current state process
  protected DeclName stateName_;
  
  // lista dos nomes de esquemas que são referenciados pela expressão do esquema 
  // que compoe o estado de um processo.
  protected List<RefName> statesAux_;
  
  protected List<DeclName> currentGenParams_;

  /** A lista de processos implícitos*/
  protected List<ProcessPara> onTheFlyProcesses_;

  /** The channels. */
  protected List<ChannelInfo> channels_;
  /** The chansets. */
  protected List<DeclName> chansets_;
  /** The processes. */
  protected List<ProcessInfo> processes_;
  //the local TypeEnv for Circus
  protected LocalTypeEnv localCircTypeEnv_;
  // mu processes
  protected List<DeclName> muProcesses_;
  // mu actions 
  protected List<DeclName> muActions_;
  
  protected List<DeclName> actions4PostCheck_;
  protected List<DeclName> processes4PostCheck_;
  protected List<List<NameTypePair>> localVars4ActPostCheck_;
  protected List<List<NameTypePair>> localVars4ProcPostCheck_;
  
  //the visitors used to typechecker a Circus program
  protected Checker actionChecker_;
  protected Checker commandChecker_;
  protected Checker communicChecker_;
  protected Checker processChecker_;
  // auxiliar visitor to typechecker a channel declaration
  protected Checker channelDeclChecker_;
  // auxiliar visitor to find used channels into a process
//  protected Checker channelsUsedChecker_;

  public TypeChecker() 
  {
    this(new ZFactoryImpl(),
         new CircusToolsFactoryImpl(),
         new SectionManager(),
         Markup.LATEX);
  }
  
  public TypeChecker(TypeChecker info)
  {
    this(info.zFactory_.getZFactory(),
         info.circusFactory_.getCircusFactory(),
         info.sectInfo_,
         info.markup_);
  }

  public TypeChecker(SectionInfo sectInfo)
  {
    this(new ZFactoryImpl(),
         new CircusToolsFactoryImpl(),
         sectInfo,
         Markup.UNICODE);
  }

  public TypeChecker(SectionInfo sectInfo, Markup markup)
  {
    this(new ZFactoryImpl(),
         new CircusToolsFactoryImpl(),
         sectInfo,
         markup);
  }

  public TypeChecker(ZFactory zFactory,
                     CircusToolsFactory circusFactory,
                     SectionInfo sectInfo,
                     Markup markup)
  {
    super(zFactory, sectInfo, markup, false);
    circusFactory_ = new Factory(zFactory, circusFactory);
    localCircTypeEnv_ = new LocalTypeEnv(circusFactory, typeEnv_);
    channels_ = new ArrayList<ChannelInfo>();
    chansets_ = new ArrayList<DeclName>();
    processes_ = new ArrayList<ProcessInfo>();
    sectInfo_ = sectInfo;
    unificationEnv_ = new UnificationEnv(zFactory);
    carrierSet_ = new CarrierSet();
    currentProcess_ = null;
    currentAction_ = null;
    stateName_ = null;
    statesAux_ = new ArrayList<RefName>();
    currentGenParams_ = null;
    onTheFlyProcesses_ = null;
    muProcesses_ = new ArrayList<DeclName>();
    muActions_ = new ArrayList<DeclName>();
    actions4PostCheck_ = new ArrayList<DeclName>();
    processes4PostCheck_ = new ArrayList<DeclName>();
    localVars4ActPostCheck_ = new ArrayList<List<NameTypePair>>();
    localVars4ProcPostCheck_ = new ArrayList<List<NameTypePair>>();
    specChecker_ = new SpecChecker(this);
    paraChecker_ = new ParaChecker(this);
    declChecker_ = new DeclChecker(this);
    exprChecker_ = new ExprChecker(this);
    predChecker_ = new PredChecker(this);
    postChecker_ = new PostChecker(this);
    actionChecker_ = new ActionChecker(this);
    commandChecker_ = new CommandChecker(this);
    communicChecker_ = new CommunicationChecker(this);
    processChecker_ = new ProcessChecker(this);
    // auxiliar visitors
    channelDeclChecker_ = new ChannelDeclChecker(this);
  }
  
  // método necessário para que outros programas tenham acesso às informações
  // dos tipos...
  public SectTypeEnv getSectTypeEnv() {
    return sectTypeEnv_;
  }
  
  public TypeEnv getTypeEnv() {
    return typeEnv_;
  }
  
  public Object visitTerm(Term term) {
    Object result = null;
    
    if(term instanceof CircusAction) {
      result = term.accept(actionChecker_);
    }
    else if(term instanceof Pred) {
      result = term.accept(predChecker_);
    }
    else if(term instanceof Expr) {
      result = term.accept(exprChecker_);
    }
    else {
      result = (Boolean) term.accept(specChecker_);
    }
    
    return result;
  }
  
  
}
