/****************************************************************** 

  * Copyright (c) 2003, Mario Hochreiter, Student of 

  * Software Engineering at FH-Hagenberg, Austria. 

  * Project member of the isac team at the Institute for 

  * Software-Technologie, Graz University of Technology, Austria. 

  * 

  * Use is subject to license terms.

  ******************************************************************/

 package isac.util;

 import isac.bridge.xml.DataTypes; // from libisabelle-full.jar

 import edu.tum.cs.isabelle.api.XML; // from libisabelle-full.jar

 import java.io.Serializable;

 import java.util.ArrayList;

 import java.util.Iterator;

 /**

  * Every calculation in the isac system starts with a formalization that

  * characterizes the calculation. A formalization object can contain multiple

  * <code>Variant</code> objects because a calculation can be calculated in

  * different ways (using different methods to solve the calculation).

  * 

  * @author Mario Hochreiter

  * @version 0.1

  *  

  */

 public class Formalization implements Serializable {

     static final long serialVersionUID = 4539906901989017369L;

 	protected ArrayList<Variant> variants_;

     public Formalization() {

         variants_ = new ArrayList<Variant>();

     }

     public void addNewVariant(Variant v) {

         variants_.add(v);

     }

     public ArrayList<Variant> getVariants() {

     	return variants_;

     }

     public Iterator<?> iterator() {

         return new FormalizationIterator(this);

     }

     public String toString() {

         String content = "<FORMALIZATION>\n";

         for (int index = 0; index < variants_.size(); index++)

             content += variants_.get(index) + "\n";

         content += "</FORMALIZATION>\n";

         return content;

     }

     /**

      * Format the object in a way that the bridge can handle it

      * 

      * @return SML representation of this Formalization

      */

     public String toSMLString() {

         // Use this String for empty Formalization:

         // Calculation from scratch

         if (variants_.isEmpty())

             return "[([], (\"e_domID\", [\"e_pblID\"], [\"e_metID\"]))]";

         //FIXME.WN04 e_domID, etc. will disappear soon: empty formalization

         // would be "[([], (\"\", [], []))]"

         StringBuffer sb = new StringBuffer();

         int size = variants_.size();

         int i = 0;

         Variant v;

         sb.append("[");

         Iterator<Variant> it = variants_.iterator();

         while (it.hasNext()) {

             v = (Variant) it.next();

             sb.append("(");

             sb.append(v.toSMLString());

             sb.append(")");

             if (i < size - 1) {

                 sb.append(",");

             }

             i++;

         }

         sb.append("]");

         return sb.toString();

     }

    /**

    * Format the object in a way that libisabelle/PIDE can handle it

    * @return XML representation of this Formalization

    */

    public XML.Tree toXML() {

     	DataTypes.xml_of_str("equality (x+1=(2::real))");

         return null; //XML.Tree

     }

 }

 class FormalizationIterator implements Iterator<Object> {

     Iterator<?> it_;

     FormalizationIterator(Formalization f) {

         it_ = f.variants_.iterator();

     }

     public void remove() {

         it_.remove();

     }

     public boolean hasNext() {

         return it_.hasNext();

     }

     public Object next() {

         return it_.next();

     }

 }