/*
 * TypeCheckUtils.java
 *
 * Created on 18 de Junho de 2005, 15: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 circparser.CircusParser;
import java.io.*;
import java.util.ArrayList;
import java.util.List;
import net.sourceforge.czt.circustools.ast.CircusToolsFactory;
import net.sourceforge.czt.circustools.impl.CircusToolsFactoryImpl;

import net.sourceforge.czt.util.*;
import net.sourceforge.czt.base.ast.Term;
import net.sourceforge.czt.session.*;
import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.z.impl.ZFactoryImpl;
import net.sourceforge.czt.circus.ast.CircusFactory;
import net.sourceforge.czt.circus.impl.CircusFactoryImpl;
import net.sourceforge.czt.parser.circus.*;
import net.sourceforge.czt.parser.util.*;
import net.sourceforge.czt.typecheck.z.util.*;

/**
 * Utilities for typechecking Object-Z specifications.
 *
 * @author Petra Malik, Tim Miller
 */
public class TypeCheckUtils
  extends net.sourceforge.czt.typecheck.z.TypeCheckUtils
{
  /**
   * Do not generate instances of this class.
   */
  protected TypeCheckUtils()
  {
  }

  /**
   * Typecheck and type annotate a file.
   * @param term the <code>Term</code> to typecheck.
   * @param sectInfo the <code>SectionInfo</code> object to use.
   * @param markup the <code>Markup</code> of the specification.
   * returns the list of ErrorAnns in the AST added by the typechecker.
   */
  public static List typecheck(Term term,
                               SectionInfo sectInfo,
                               Markup markup)
  {
    TypeCheckUtils utils = new TypeCheckUtils();
    return utils.lTypecheck(term, sectInfo, markup, false);
  }

  protected List lTypecheck(Term term,
                            SectionInfo sectInfo,
                            Markup markup,
                            boolean useBeforeDecl)
  {
    return lTypecheck(term, sectInfo, markup);
  }

  protected List lTypecheck(Term term,
                            SectionInfo sectInfo,
                            Markup markup)
  {
    ZFactory zFactory = new ZFactoryImpl();
    CircusToolsFactory circusFactory = new CircusToolsFactoryImpl();
    TypeChecker typeChecker =
      new TypeChecker(zFactory, circusFactory, sectInfo, markup);
    typeChecker.visitTerm(term);
    return typeChecker.errors();
  }

  protected Term parse(Source src, SectionInfo sectInfo)
    throws IOException, net.sourceforge.czt.parser.util.ParseException {
        //return ParseUtils.parse(src, sectInfo);
        throw new UnsupportedOperationException("Circus Parser does not support parsing through Source objects yet.");
  }

  protected Term parse(String file, SectionInfo sectInfo)
    throws IOException, net.sourceforge.czt.parser.util.ParseException
  {
    Spec spec = null;
    try {
        System.out.println("Parsing: " + file);
        spec = CircusParser.parse(file);
        System.out.println("Parser OK!");
    } catch (Exception e) {
        System.out.println(file + " - Exception: " + e.getMessage() + "\n");
        e.printStackTrace(System.err);
    }
    return spec;
  }

  protected String name()
  {
    return "circustypecheck";
  }

  public static void main(String[] args)
    throws IOException
  {
    TypeCheckUtils utils = new TypeCheckUtils();
    utils.run(args);
  }
}
