// FILE. . . . . /home/hak/hlt/src/hlt/osfv2/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 Feb 17 08:32:10 2014 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;

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

    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;
      }

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

    /**
     * This is the maximal subterm position of positional subterms (counting
     * from 1). Note that the actual number of positional subterms may be less
     * than this number due to possible gaps in positions (for which missing
     * subterms would be <tt>null</tt>).
     */
    public int positionArity ()
      {
	return _positions.size();
      }

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

    /**
     * This is the number of contiguous initial positional subterms (counting
     * from 1). Note that the total number of positional subterms may be more
     * than this number due to possible gaps in positions (for which missing
     * subterms would be <tt>null</tt>).
     */
    public int contiguousArity ()
      {
	int arity = positionArity();
	
	for (int position = 1; position <= arity; position++)
	  if (_positions.get(position-1) == null) // -1 since positions are counted from 1
	    return position;	    
	
	return arity;
      }

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

    /**
     * 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 > _positions.size())
	  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.secureSet(position-1,psiterm); // -1 since positions are counted from 1
      }

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

    /**
     * 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 this term's sort expression with the specified one by
     * conjoining them into an "and"sort expression.
     */
    public void mergeSortWith (SortExpression otherSort)
    {
      if (_sort.equals(otherSort))
	// no need to duplicate since "foo & foo = foo":
	return;

      // merge this term's sort expression with the specified one (ignoring top):
      if (_sort.isSymbol() && ((SymbolSortExpression)_sort).sort().isTop())
	_sort = otherSort;
      else
	if (!(otherSort.isSymbol() && ((SymbolSortExpression)otherSort).sort().isTop()))
	  _sort = new AndSortExpression(_sort,otherSort);
    }

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

    /**
     * This merges the uninterpreted structure of the specified &psi;-term
     * into this one's 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):
	mergeSortWith(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)
	    {
	      int arity = Math.max(positionArity(),other.positionArity());
	      
	      for (int i=1; i<=arity; 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()));
		    }
		}
	    }

	return this;
      }

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

    /**
     * Returns a pretty-printed string form for this dereferenced
     * &psi;-term, offset by the specified margin.
     */
    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 value of the sort expression evaluation flag.
     */
    public static boolean evalSorts ()
      {
	return _evalSorts;
      }

    /**
     * Sets sort expression evaluation to the specified flag.
     */
    public static void evaluateSorts (boolean flag)
      {
	_evalSorts = flag;
      }

    /**
     * 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))
	  // a psiterm with this tag was already processed - just print the
	  // tag alone:
	  {
	    buf.append(_tag.name());
	    return buf;
	  }

	// use the sort expression for the header:
	String header = _evalSorts
	  ? _sort.maxLowerBound()	// interpret the sort expression
	  : _sort.displayForm();	// do not interpret sort expression

	if (_tag.isShared())
	  // this tag is shared so it must be printed:
	  { 
	    if (header == "@" && _positions == null && _features == null)
	      {
		// this is just top with no subterms - just print the tag alone:
		buf.append(_tag.name());
		return buf;
	      }

	    // this is a shared tag with a non-top sort or with subterms, 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;
	  }

	// print the header:
	buf.append(header);

	// record the tag as already processed:
	tags.add(_tag);

	// process the subterms if any:	
	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;
      }

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

  }
