// 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 Thu Sep 12 10:59:13 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 implicitly 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>_positionArity</tt> must be kept consistent.
     */
    private int _nextContiguousPosition = 0;

    /**
     * This is the highest position that has an actual positional subterm for
     * this &psi;-term (counting positions starting at 1 instead of 0). Since
     * subterms may also be stored using explicit positions that may be out of
     * order or non-contiguous using the <tt>set</tt> method, this value must
     * be updated explicitly. In all cases, we must ensure that the capacity
     * of the array <tt>_positions</tt> is sufficient.
     */
    private int _positionArity = 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 positionArity ()
      {
	return _positionArity;
      }

    /**
     * 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++;
	_positionArity = Math.max(_positionArity,_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 > _positionArity)
	  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

	_positionArity = Math.max(_positionArity,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;

	System.out.println("----------------------------------------------");
	System.out.println(">>> Merging psiterm:");
	System.out.println("    "+displayForm(4));
	System.out.println(">>> with psiterm:");
	System.out.println("    "+other.displayForm(4));

	// 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();
	else
	  if (other.features() != null)
	    for (Iterator it=other.features().keySet().iterator(); it.hasNext();)
	      {
		Feature feature = (Feature)it.next();
		PsiTerm subterm = getSubterm(feature);
		PsiTerm otherSubterm = other.getSubterm(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();
	else
	  if (other.positions() != null)
	    for (int i=1; i<=Math.max(_positionArity,other.positionArity()); i++)
	      {
		System.out.println("\t>>> Merging position "+i);
		PsiTerm subterm = getSubterm(i);
		PsiTerm otherSubterm = other.getSubterm(i);
		if (subterm == null)
		  {
		    if (otherSubterm != null)
		      setSubterm(i,otherSubterm.deref());
		  }
		else
		  {
		    if (otherSubterm != null)
		      setSubterm(i,subterm.deref().merge(otherSubterm.deref()));
		  }
	      }
	
	System.out.println(">>> Results in psiterm:");
	System.out.println("    "+displayForm(4));
	System.out.println("----------------------------------------------");

	return this;
      }

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

    /**
     * Returns a pretty-printed form offset by the specified margin of this
     * dereferenced &psi;-term.
     */
    public String displayForm (int margin)
      {
	return deref().prettyPrint(margin,new HashSet()).toString();
      }

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

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

    /**
     * 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.displayForm();	// 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 position = 1;
		    // as long as there is no gap -> no feature needed
		    for (;position<=_positionArity; position++)
		      {
			PsiTerm subterm = getSubterm(position);
			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');

			// add a comma if there are more subterms after this one
			if (position<_positionArity || _features != null)
			  buf.append(offset + ", ");
		      }
		    
		    // above a gap up to _positionArity, print the position as a
		    // feature for non null subterms
		    for (;position<=_positionArity; position++)
		      {
			PsiTerm subterm = getSubterm(position);
			if (subterm != null)
			  {
			    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');

			    // add a comma if there are more subterms after this one
			    if (position<_positionArity || _features != null)
			      buf.append(offset + ", ");
			  }
		      }
		  }

		// do the features
		if (_features != null)
		  for (Iterator it=_features.keySet().iterator(); it.hasNext();)
		    {
		      Feature feature = (Feature)it.next();
		      PsiTerm subterm = getSubterm(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;
      }

  }