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

 * 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();

    }

}