// FILE. . . . . /home/hak/hlt/src/hlt/osfv1/base/PsiTerm.java
// EDIT BY . . . Hassan Ait-Kaci
// ON MACHINE. . Hak-Laptop
// STARTED ON. . Mon Sep 02 09:16:22 2013

/**
 * This is the class of &psi;-terms as explained in the <a
 * href="../specs/basic.html#psiterms">specification</a>.
 *
 * @version     Last modified on Mon Sep 02 09:16:22 2013 by hak
 * @author      <a href="mailto:hak@acm.org">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; <a href="http://www.hassan-ait-kaci.net/">by the author</a>
 */

package hlt.osf.base;

import java.util.HashSet;
import java.util.HashMap;
import java.util.Iterator;

import hlt.language.tools.Misc;
import hlt.language.util.ArrayList;

public class PsiTerm extends OsfExpression
  {
    /**
     * This &psi;-term's tag.
     */
    private Tag _tag;

    /**
     * This &psi;-term's sort expression.
     */
    private SortExpression _sort;

    /**
     * This &psi;-term's positional subterms if any.
     */
    private ArrayList _positions;

    /**
     * This &psi;-term's featured subterms, if any.
     */
    private HashMap _features;

    /**
     * This is the next position where to store a new implicitly contiguous
     * positional subterms (counting positions starting at 1 instead of 0). Since
     * we may not rely on <tt>add</tt> to add contiguous positional subterms
     * (they are set using the <tt>set</tt> method), we need to update this value
     * for adding a new inplicitly contiguous positional subterm and must always
     * ensure that the capacity is sufficient. This does not mean that it is a
     * free position since a subterm may have already been stored there using an
     * explicit feature position (in which case the new and old subterm must be
     * merged). This value and <tt>_maxPosition</tt> must be ketp consistent.
     */
    private int _nextContiguousPosition = 0;

    /**
     * This is the highest position that has an actual positional subterm for
     * this &psi;-term (counting postions starting at 1 instead of 0). Since
     * subterms may be also stored using explicit positions that may be out of
     * order and non-contiguous using the <tt>set</tt> method, this value must be
     * updated explicit. We must always ensure that the capasity is sufficient.
     */
    private int _maxPosition = 0;

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

    public PsiTerm ()
      {
	_sort = new SymbolSortExpression("@");
      }

    public PsiTerm (Tag tag)
      {
	setTag(tag);
      }

    public PsiTerm (String sortName)
      {
	_sort = new SymbolSortExpression(sortName);
      }

    public PsiTerm (SortExpression sort)
      {
	_sort = sort;
      }

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

    public Tag tag ()
      {
	return _tag;
      }

    public PsiTerm deref ()
      {
	return _tag.deref().term();
      }

    /**
     * Set this tag's &psi;-term to the specified tag, sets the
     * specified tag's term to this &psi;-term, and returns this tag.
     */
    public PsiTerm setTag (Tag tag)
      {
	_tag = tag;
	tag.setTerm(this);
	return this;
      }

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

    /**
     * Returns the sort expression of this &psi;-term, or <tt>null</tt>
     * if none has been set for it yet.
     */
    public SortExpression sort ()
      {
	return _sort;
      }

    /**
     * Sets this &psi;-term's sort expression to the provided one and
     * returns this &psi;-term.
     */
    public PsiTerm setSort (SortExpression sort)
      {
	_sort = sort;
	return this;
      }

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

    public ArrayList positions ()
      {
	return _positions;
      }

    public HashMap features ()
      {
	return _features;
      }

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

    public int maxPosition ()
      {
	return _maxPosition;
      }

    /**
     * Returns the subterm at the next contiguous position if any, or
     * <tt>null</tt> if there isn't any.
     */
    public PsiTerm getNextContiguousPositionSubterm ()
      {
	if (_positions == null || _nextContiguousPosition == 0)
	  return null;

	return (PsiTerm)_positions.get(_nextContiguousPosition);
      }

    /**
     * This stores the provided term at the next contiguous position,
     * whether or not a term is already stored there.
     */
    public void addContiguousPositionSubterm (PsiTerm psiterm)
      {
	if (_positions == null)
	  _positions = new ArrayList(3);

	_positions.ensureCapacity(_nextContiguousPosition+1);
	_positions.set(_nextContiguousPosition,psiterm);
	_nextContiguousPosition++;
	_maxPosition = Math.max(_maxPosition,_nextContiguousPosition);
      }

    /**
     * This returns the subterm at the given position if there is one stored
     * there, or <tt>null</tt> otherwise, where positions are counted sarting
     * from 1.
     */
    public PsiTerm getSubterm (int position)
      {
	if (_positions == null || position > _maxPosition)
	  return null;

	return (PsiTerm)_positions.get(position-1); // -1 since positions are counted from 1
      }

    /**
     * This stores the provided &psi;-term at the specified position
     * (counting positions from 1), whether or not a term is already
     * stored there.
     */
    public void setSubterm (int position, PsiTerm psiterm)
      {
	if (_positions == null)
	  _positions = new ArrayList(position);
		    
	_positions.ensureCapacity(position);
	_positions.set(position-1,psiterm); // -1 since positions are counted from 1

	_maxPosition = Math.max(_maxPosition,position);

      }

    /**
     * This returns the subterm for the specified feature (which may be <tt>null</tt>).
     */
    public PsiTerm getSubterm (Feature feature)
    {
      if (_features == null || _features.isEmpty())
	return null;

      return (PsiTerm)_features.get(feature);
    }

    /**
     * This stores the provided term for the specified feature, whether or
     * not a term is already stored there.
     */
    public void setSubterm (Feature feature, PsiTerm psiterm)
      {
	if (_features == null)
	  _features = new HashMap();

	_features.put(feature,psiterm);
      }

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

    /**
     * This merges the uninterpreted structure of the specified &psi;-term
     * into this one's as explained in the <a
     * href="../specs/basic.html#merge">specification</a>, and returns this
     * &psi;-term resulting after the merging. This assumes that the
     * specified &psi;-term has been dereferenced to its true
     * identity. <b>NB</b>: Merging subterms must ensure dereferencing them
     * first.
     */
    public PsiTerm merge (PsiTerm other)
      {
	// if these are the same psiterm, no need to do anything:
	if (this == other)
	  return this;

	// merge the tags, binding the other term's tag to this one's:
	other.tag().bind(_tag);

	// merge the sort expressions if needed (i.e., ignoring top):
	if (_sort.isSymbol() && ((SymbolSortExpression)_sort).sort().isTop())
	  _sort = other.sort();
	else
	  if (!(other.sort().isSymbol() && ((SymbolSortExpression)other.sort()).sort().isTop()))
	    _sort = new AndSortExpression(_sort, other.sort());
	
	// merge the features:
	if (_features == null)
	  _features = other.features();

	if (other.features() != null)
	  for (Iterator it=other.features().keySet().iterator(); it.hasNext();)
	    {
	      Feature feature = (Feature)it.next();
	      PsiTerm subterm = (PsiTerm)_features.get(feature);
	      PsiTerm otherSubterm = (PsiTerm)other.features().get(feature);
	      if (subterm == null)
		{
		  if (otherSubterm != null)
		    _features.put(feature,otherSubterm.deref());
		}
	      else
		{		  
		  if (otherSubterm != null)
		    _features.put(feature,subterm.deref().merge(otherSubterm.deref()));
		}
	    }
	    
	// merge the positions:
	if (_positions == null)
	  _positions = other.positions();

	if (other.positions() != null)
	  for (int i = other.maxPosition(); i-->0;)
	    {
	      PsiTerm subterm = (i < _maxPosition) ? (PsiTerm)_positions.get(i) : null;
	      PsiTerm otherSubterm = (PsiTerm)other.positions().get(i);
	      if (subterm == null)
		{
		  if (otherSubterm != null)
		    setSubterm(i,otherSubterm.deref());
		}
	      else
		{
		  if (otherSubterm != null)
		    _positions.set(i,subterm.deref().merge(otherSubterm.deref()));
		}
	    }

	return this;
      }

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

    /**
     * Returns a pretty-printed form of this &psi;-term.
     */
    public String displayForm ()
      {
	return deref().prettyPrint(0,new HashSet()).toString();
      }

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

    /**
     * Flag to determine whether or not to evaluate sort
     * expressions. This is <tt>false</tt> by default.
     */
    private static boolean _evalSorts = false;

    /**
     * Returns the current sort expression evaluation flag's value.
     */
    public static boolean evaluateSorts ()
      {
	return _evalSorts;
      }

    /**
     * Toggles sort expression evaluation.
     */
    public static void toggleSortEvaluation ()
      {
	_evalSorts = !_evalSorts;
      }

    /**
     * Returns a pretty printed form of this &psi;-term, starting at the
     * specified margin width and the array list of already processed tags.
     */
    public StringBuffer prettyPrint (int margin, HashSet tags)
      {
	StringBuffer buf = new StringBuffer();

	if (tags.contains(_tag))
	  buf.append(_tag.name());
	else
	  {
	    String header = _evalSorts
	      ? _sort.maxLowerBound()	// the header is the interpreted sort expression
	      : _sort.toString();	// the header is the uninterpreted sort expression
	    
	    if (_tag.isShared())
	      { // this is a shared tag, so the header must start with tagging:
		header = _tag.name() + " : " + header;
		// since in this case the sort expression is preceded by
		// tagging, the margin is augmented with the length of the tag
		// and the 3 characters " : " that follow it:
		margin += _tag.name().length() + 3;
	      }

	    tags.add(_tag);

	    buf.append(header);

	    if (_positions != null || _features != null)
	      { // When this psiterm has a body, the open and closed
		// parentheses, as well as the comma between subterms, are
		// always aligned vertically under the first character of the
		// sort expression whether tagged or not.  So we must compute
		// the marginal offset depending on whether or not the sort
		// expression is preceded by a tag
		
		String offset = Misc.repeat(margin,' ');
		buf.append('\n' + offset + "( ");

		// do the positions
		if (_positions != null)
		  {
		    int index = 0;
		    // as long as there is no gap -> no feature needed
		    for (index=0; index<_maxPosition; index++)
		      {
			PsiTerm subterm = (PsiTerm)_positions.get(index);
			if (subterm == null)
			  break;

			// pretty-print the subterm with a margin augmented with
			// the 2 characters of the initial "( " or ", "
			buf.append(subterm.deref().prettyPrint(margin+2,tags));
			buf.append('\n');

			if (index<_maxPosition-1)
			  buf.append(offset + ", ");
		      }
		    
		    // above a gap up to maxPosition, print the position as a
		    // feature for non null subterms
		    for (;index<_maxPosition; index++)
		      {
			PsiTerm subterm = (PsiTerm)_positions.get(index);
			if (subterm != null)
			  {
			    int position = index+1;
			    subterm = subterm.deref();
			    buf.append(position + " => ");
			    // pretty-print the subterm with a margin augmented
			    // with the width of the position + the 2 characters
			    // of the initial "( " or ", " + the 4 characters of
			    // " => "
			    buf.append(subterm.prettyPrint(margin+Misc.numWidth(position)+6,tags));
			    buf.append('\n');

			    if (index<_maxPosition-1)
			      buf.append(offset + ", ");
			  }
		      }
		  }

		// do the features
		if (_features != null)
		  for (Iterator it=_features.keySet().iterator(); it.hasNext();)
		    {
		      Feature feature = (Feature)it.next();
		      PsiTerm subterm = ((PsiTerm)_features.get(feature)).deref();
		      buf.append(feature.name() + " => ");
		      // pretty-print the subterm with a margin augmented with
		      // the length of the feature name + the 2 characters of the
		      // initial "( " or ", " + the 4 characters of " => "
		      buf.append(subterm.prettyPrint(margin+feature.name().length()+6,tags));
		      buf.append('\n');

		      if (it.hasNext())
			buf.append(offset + ", ");
		    }
		
		buf.append(offset + ')');
	      }
	  }

	return buf;
      }

  }