//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\
// PLEASE DO NOT EDIT WITHOUT THE EXPLICIT CONSENT OF THE AUTHOR! \\
//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\

package ilog.language.design.kernel;

/**
 * @version     Last modified on Wed Nov 27 10:55:44 2002 by hak
 * @author      <a href="mailto:hak@ilog.fr">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; 2000-2002 <a href="http://www.ilog.fr/">ILOG, S.A.</a>
 */

import ilog.language.design.types.*;
import ilog.language.design.base.*;

import ilog.language.tools.Debug;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;

/**
 * This class is a <a href="Let.html"><tt>Let</tt></a> set up to represent a monoid
 * comprehension constructed from the parts of the syntactic form of the comprehension.
 * The syntax of a monoid comprehension is given by an expression of the form:
 *
 * <font color="brown"><pre>
 * [op,id] { e | q<sub>1</sub>, ..., q<sub>n</sub> }
 * </pre></font>
 *
 * where <tt>[op,id]</tt> define a monoid, <tt>e</tt> is an expression, and the
 * <tt>q<sub>i</sub></tt>'s are <i>qualifiers</i>. A qualifier is either a <i>boolean</i>
 * expression or a pair <tt>p <- e</tt>, where <tt>p</tt> is a pattern (any expression)
 * and <tt>e</tt> is an expression. The sequence of qualifiers may also be empty. Such a
 * monoid comprehension is syntactic sugar that is in fact translated into a combination
 * of homomorphisms and filtering tests.
 */

public class Comprehension extends ProtoExpression
{
  public static boolean OPAQUE_PARAMETERS = true;
  public static boolean FULL_UNNESTING = false;

  private Tables _tables;
  private RawInfo _raw;
  private Expression _construct;
  private Expression _operation;
  private Expression _identity;

  private Expression _enclosingScope;

  public Comprehension (ArrayList parameters, ArrayList values, Expression body)
    {
      _construct = new Let(parameters,values,body);
    }

  public Comprehension (Tables tables, Expression operation, Expression identity,
                        Expression expression, ArrayList patterns, ArrayList expressions)
    {
      this(tables,operation,identity,expression,patterns,expressions,Homomorphism.DEFAULT_IN_PLACE);
    }

  public Comprehension (Tables tables, Expression operation, Expression identity,
                        Expression expression, ArrayList patterns, ArrayList expressions,
                        byte inPlace)
    {
      _tables = tables;

      _operation = operation;
      _identity = identity;

      if (patterns == null)
        patterns = expressions = new ArrayList(0);

      _raw = new RawInfo(new Dummy("$OP$").addTypes(operation),
                         new Dummy("$ID$").addTypes(identity),
                         expression,patterns,expressions,inPlace);
    }      

  private Comprehension (Expression construct)
    {
      _construct = construct;
    }

  public final Tables tables ()
    {
      return _tables;
    }

  public final Expression operation ()
    {
      return _operation;
    }

  public final Expression identity ()
    {
      return _identity;
    }

  public final Expression copy ()
    {
      if (_raw == null)
        return new Comprehension(_construct.copy());

      ArrayList patterns = new ArrayList(_raw.patterns.size());
      for (int i=0; i<patterns.size(); i++)
        patterns.add(((Expression)_raw.patterns.get(i)).copy());

      ArrayList expressions = new ArrayList(_raw.expressions.size());
      for (int i=0; i<expressions.size(); i++)
        expressions.add(((Expression)_raw.expressions.get(i)).copy());

      return new Comprehension(_tables,_operation.copy(),_identity.copy(),
                               _raw.expression.copy(),patterns,expressions,
                               _raw.inPlace);
    }

  public final Expression typedCopy ()
    {
      if (_raw == null)
        return new Comprehension(_construct.typedCopy());

      ArrayList patterns = new ArrayList(_raw.patterns.size());
      for (int i=0; i<patterns.size(); i++)
        patterns.add(((Expression)_raw.patterns.get(i)).typedCopy());

      ArrayList expressions = new ArrayList(_raw.expressions.size());
      for (int i=0; i<expressions.size(); i++)
        expressions.add(((Expression)_raw.expressions.get(i)).typedCopy());

      return new Comprehension(_tables,_operation.typedCopy(),_identity.typedCopy(),
                               _raw.expression.typedCopy(),patterns,expressions,
                               _raw.inPlace).addTypes(this);
    }

  public final int numberOfSubexpressions ()
    {
      if (_raw != null) _construct();
      return _construct.numberOfSubexpressions();
    }

  public final Expression subexpressions (int n)
    {
      if (_raw != null) _construct();
      return _construct.subexpression(n);
    }

  public final Expression setSubexpressions (int n, Expression expression)
    {
      if (_raw != null) _construct();
      return _construct.setSubexpression(n,expression);
    }

  public final Expression sanitizeNames (ParameterStack parameters, ClassTypeHandle handle)
    {
      if (_raw != null) _construct();
      _construct = _construct.sanitizeNames(parameters,handle);
      return this;
    }

  public final void sanitizeSorts (Enclosure enclosure)
    {
      _construct.sanitizeSorts(enclosure);
    }

  public final Expression substitute (HashMap substitution)
    {
      if (_raw == null)
        return _construct.substitute(substitution);

      if (!substitution.isEmpty())
        {
          _operation = _operation.substitute(substitution);
          _identity = _identity.substitute(substitution);

          _substituteRest(0,substitution);
        }

      return this;
    }

  private final void _substituteRest (int index, HashMap substitution)
    {
      if (index == _raw.patterns.size())
        _raw.expression = _raw.expression.substitute(substitution);
      else
        {
          Expression pattern = (Expression)_raw.patterns.get(index);
          Expression expression = (Expression)_raw.expressions.get(index);

          if (pattern == null)
            {
              _raw.expressions.set(index,expression.substitute(substitution));
              _substituteRest(index+1,substitution);
            }
          else
            if (pattern instanceof Parameter || (pattern instanceof Dummy && OPAQUE_PARAMETERS))
              {
                String name = pattern instanceof Dummy ? ((Dummy)pattern).name()
                                                       : ((Parameter)pattern).name();
                _raw.expressions.set(index,expression.substitute(substitution));
                Object value = substitution.remove(name);
                _substituteRest(index+1,substitution);
                if (value != null) substitution.put(name,value);
              }
            else
              {
                _raw.patterns.set(index,pattern.substitute(substitution));
                _raw.expressions.set(index,expression.substitute(substitution));
                _substituteRest(index+1,substitution);
              }
        }
    }

  /**
   * Constructs this monoid comprehension as a let expression wrapping a composition
   * of monoid homomorphisms. The let is needed in order to factor out the computation
   * of the operation and the identity.
   */
  private final void _construct () throws UndefinedEqualityException
    {
      if (FULL_UNNESTING)
        {
          desugarPatterns();
          linkScopeTree(null);
          unnestInnerFilters();
        }
      else
        {
          _desugarPatterns();
          _unnestFilters();
        }
    }

  /**
   * Sets this comprehension's enclosing scope link to the specified expression, then
   * visits all the qualifier expressions to link up their scope trees of nested
   * comprehensions to this, and returns the nummber of such nested comprehensions.
   */
  final int linkScopeTree (Expression ancestor)
    {
      _enclosingScope = ancestor;
      _nestedComprehensionCount = _raw.expression.linkScopeTree(this);
      
      for (int i=_raw.expressions.size(); i-->0;)
        _nestedComprehensionCount += ((Expression)_raw.expressions.get(i)).linkScopeTree(this);

      return 1 + _nestedComprehensionCount;
    }

  /**
   * Unnests the local filters after doing so for all nested comprehensions if any.
   */
  final void unnestInnerFilters ()
    {
      if (_nestedComprehensionCount > 0)
        {
          _raw.expression.unnestInnerFilters();
          for (int i=_raw.expressions.size(); i-->0;)
            ((Expression)_raw.expressions.get(i)).unnestInnerFilters();
          }

      _unnestFilters();
    }

  final void desugarPatterns () throws UndefinedEqualityException
    {
      if (_raw == null || _raw.isDesugared)
        return;

      _desugarPatterns();

      for (int i=0; i<_raw.patterns.size(); i++)
        {
          Expression pattern = (Expression)_raw.patterns.get(i);
          if (pattern != null) pattern.desugarPatterns();
          ((Expression)_raw.expressions.get(i)).desugarPatterns();
        }

      _raw.expression.desugarPatterns();
    }

  /**
   * Converts the patterns into simple parameters and substitutes free occurrences of
   * the formal names from the patterns by what's appropriate in terms of the new
   * parameters inside the raw expression (and any other pertinent expression in
   * raw expressions - <i>i.e.</i>, those to the right of a pattern's generator).
   * While desugaring, new filters may be generated along the way upon repeated
   * occurrences of formal names or the presence of interpretable expressions in the
   * patterns. These are simply appended to the raw list of expressions. Because of
   * this, we need to append as many <tt>null</tt>s to the list of patterns in order
   * to maintain the two lists at equal lengths.
   */
  private final void _desugarPatterns () throws UndefinedEqualityException
    {
      HashMap substitution = new HashMap();

      int size = _raw.patterns.size();
      for (int i=0; i<size; i++)
        _raw.patterns.set(i,_desugarPattern(i,(Expression)_raw.patterns.get(i),substitution));

      for (int i=_raw.expressions.size()-size; i-->0;) _raw.patterns.add(null);

      _substituteExpressions(substitution);

      _raw.isDesugared = true;
    }

  private final Parameter _desugarPattern (int index, Expression pattern, HashMap substitution)
    throws UndefinedEqualityException
    {
      if (pattern == null || pattern instanceof Parameter)
        return (Parameter)pattern;

      Parameter parameter = null;
      Dummy variable = null;

      if (pattern instanceof Dummy)
        {
          variable = (Dummy)pattern;
          parameter = new Parameter(variable);

          if (!OPAQUE_PARAMETERS)
            {
              IndexedExpression value = (IndexedExpression)substitution.get(variable.name());

              if (value == null)
                substitution.put(variable.name(),new IndexedExpression(index,variable));
              else
                {
                  variable = new Dummy(parameter = new Parameter(value.expression.typeRef()));
                  _raw.expressions.add(new Application(_tables.equality(),
                                                       variable,
                                                       value.expression.typedCopy()));
                }
            }

          return parameter;
        }

      parameter = new Parameter(pattern.typeRef());
      variable = new Dummy(parameter.name());

      if (pattern instanceof Tuple)
        _desugarTuplePattern(index,(Tuple)pattern,variable,substitution);
      else      
        _raw.expressions.add(new Application(_tables.equality(),variable,pattern));

      return parameter;
    }

  private final void _desugarTuplePattern (int index, Tuple tuple, Expression father,
                                           HashMap substitution)
    throws UndefinedEqualityException
    {
      if (tuple instanceof NamedTuple)
        {
          _desugarNamedTuplePattern(index,(NamedTuple)tuple,father,substitution);
          return;
        }
        
      int dimension = tuple.dimension();
      for (int i=0; i<dimension; i++)
        _desugarTupleComponent(index,
                               tuple.component(i),
                               new TupleProjection(father,new Int(i+1)),
                               substitution);
    }

  private final void _desugarNamedTuplePattern (int index, NamedTuple tuple, Expression father,
                                                HashMap substitution)
    throws UndefinedEqualityException
    {
      TupleFieldName[] fields = tuple.fields();
      int dimension = fields.length;
      for (int i=0; i<dimension; i++)
        _desugarTupleComponent(index,
                               tuple.component(i),
                               new TupleProjection(father,new StringConstant(fields[i].name())),
                               substitution);
    }

  private final void _desugarTupleComponent (int index, Expression component,
                                             TupleProjection projection, HashMap substitution)
    throws UndefinedEqualityException
    {
      if (component instanceof Dummy)
        {
          Dummy variable = (Dummy)component;
          IndexedExpression value = (IndexedExpression)substitution.get(variable.name());
          if (value == null)
            substitution.put(variable.name(),new IndexedExpression(index,projection));
          else
            _raw.expressions.add(new Application(_tables.equality(),
                                                 projection,
                                                 value.expression.typedCopy()));

          return;
        }

      if (component instanceof Tuple)
        _desugarTuplePattern(index,(Tuple)component,projection,substitution);
      else
        _raw.expressions.add(new Application(_tables.equality(),projection,component));
    }

  private final void _substituteExpressions (HashMap substitution)
    {
      if (substitution.isEmpty())
        return;

      int index = 0;
      int size = _raw.expressions.size();

      while (index < size) // skip to the first desugared pattern
        {
          Parameter parameter = (Parameter)_raw.patterns.get(index);
          if (parameter != null && parameter.isInternal())
            break;
          index++;
        }

      HashMap partialSubstitution = new HashMap(substitution.size());
      for (int i=index; i < size; i++)
        {
          _updateSubstitution(i,partialSubstitution,substitution);
          _raw.expressions.set(i,((Expression)_raw.expressions.get(i)).substitute(partialSubstitution));
        }

      _raw.expression = _raw.expression.substitute(partialSubstitution);
    }

  private final static void _updateSubstitution (int index, HashMap partial, HashMap substitution)
    {
      ArrayList keys = new ArrayList();

      for (Iterator i=substitution.entrySet().iterator(); i.hasNext();)
        {
          Map.Entry entry = (Map.Entry)i.next();
          String key = (String)entry.getKey();
          IndexedExpression value = (IndexedExpression)entry.getValue();
          if (index <= value.index)
            {
              partial.put(key,value.expression);
              keys.add(key);
            }
        }

      int size = keys.size();
      for (int i=size; i-->0;)
        substitution.remove(keys.get(i));
    }

  private final void _unnestFilters ()
    {
      Qualifier[] qualifiers = new Qualifier[_raw.patterns == null ? 0 : _raw.patterns.size()];
      for (int i=qualifiers.length; i-->0;)
        qualifiers[i] = new Qualifier((Parameter)_raw.patterns.get(i),
                                      (Expression)_raw.expressions.get(i));

      if (qualifiers.length > 0) _normalize(qualifiers);

      Parameter[] monoidParameters = { new Parameter("$OP$"), new Parameter("$ID$") };
      Expression[] monoidComponents = { _operation, _identity };

      _construct = new Let(monoidParameters,monoidComponents,_translate(qualifiers,0));
      _raw = null;
    }

  /**
   * Reshapes the specified array of qualifiers unnesting all boolean filters by moving
   * them to the left as far as they may go (<i>i.e.</i>, no further than a generator
   * whose parameter occurs free in the filter), and merging all filters related to the
   * same generator into an common <tt>and</tt>. A selector or slicing condition is
   * recognized and treated specially: it is passed to its generator qualifier where
   * it is then processed appropriately.
   */
  private final void _normalize (Qualifier[] qualifiers)
    {
      //System.out.print("Before normalization..."); Debug.step(qualifiers);
      _unnestFilters(qualifiers.length-1,qualifiers);
      //System.out.print("After normalization...");  Debug.step(qualifiers);
    }

  /**
   * Normalizes the specified array of qualifiers up to the specified index minus
   * one, then proceeds to unnest leftward the qualifier at the specified index.
   */
  private final void _unnestFilters (int index, Qualifier[] qualifiers)
    {
      if (index == -1) return;

      int upperLimit = index;
      _unnestFilters(upperLimit-1,qualifiers);
      Qualifier qualifier = qualifiers[index];

      // push this qualifier to the left over null qualifiers if any
      int i = index-1;
      while (i >= 0 && qualifiers[i] == null) i--;
      if (i < index-1)
        {
          qualifiers[index] = null;
          qualifiers[index = i+1] = qualifier;
        }

      if (qualifier.isGenerator()) return;

      // this qualifier is then a filter - unnest it as far as it can go
      while (index > 0)
        if (qualifiers[index-1].isGenerator())
          if (qualifier.expression.containsFreeName(qualifiers[index-1].parameter.name()))
            {  // collect if selector, or slicing with no selectors; otherwise, leave the filter there
              if (qualifier.isSelector(qualifiers[index-1].parameter))
                {
                  qualifiers[index-1].addSelector(qualifier.expression);
                  _eraseQualifier(index,upperLimit,qualifiers);
                }
              else
                if (qualifiers[index-1].selectors == null
                    && qualifier.isSlicing(qualifiers[index-1].parameter))
                  {
                    qualifiers[index-1].addSlicing(qualifier.expression);
                    _eraseQualifier(index,upperLimit,qualifiers);
                  }
              return; // this is as far as it can go
            }
          else // move this filter over one step to the left
            {
              qualifiers[index] = qualifiers[index-1];
              qualifiers[index = index-1] = qualifier;
            }
        else // qualifiers[index-1] is a filter
          if (index > 1) // if qualifiers[index-2] exists, it must contain a generator
            if (!qualifier.expression.containsFreeName(qualifiers[index-2].parameter.name()))
              { // move this filter over two steps to the left
                qualifiers[index] = qualifiers[index-1];
                qualifiers[index-1] = qualifiers[index-2];
                qualifiers[index = index-2] = qualifier;
              }
            else // collect if selector, or slicing with no selectors; otherwise, merge into the filter
              {
                if (qualifier.isSelector(qualifiers[index-2].parameter))
                  qualifiers[index-2].addSelector(qualifier.expression);
                else
                  if (qualifiers[index-2].selectors == null
                      && qualifier.isSlicing(qualifiers[index-2].parameter))
                    qualifiers[index-2].addSlicing(qualifier.expression);
                  else // merge this filter with the previous one using an 'and'
                    qualifiers[index-1].expression = new And(qualifiers[index-1].expression,
                                                             qualifier.expression);
                _eraseQualifier(index,upperLimit,qualifiers);
                return; // this is as far as it can go
              }
          else // unnest further up, or merge this filter into the previous one using an 'and'
            {
              if (!_isFurtherUnnestable(qualifier.expression))
                qualifiers[index-1].expression = new And(qualifiers[index-1].expression,
                                                         qualifier.expression);
              _eraseQualifier(index,upperLimit,qualifiers);
              return; // this is as far as it can go
            }

      // index == 0
      if (_isFurtherUnnestable(qualifier.expression))
        _eraseQualifier(index,upperLimit,qualifiers);      
    }

  /**
   * Goes up the scope tree as far as it can without crossing a scope that either
   * contains more than one nested comprehension or captures a free variable in the
   * specified filter, until it reaches a comprehension. It it can do so, adds the filter
   * to that comprehension, and returns <tt>true</tt>; otherwise, returns <tt>false</tt>.
   */
  private final boolean _isFurtherUnnestable (Expression filter)
    {
      Expression enclosingScope = _enclosingScope;

      while (enclosingScope != null && enclosingScope.nestedComprehensionCount() == 1)
        {
          if (enclosingScope instanceof Comprehension)
            {
              Comprehension comp = (Comprehension)enclosingScope;

              if (operation().equals(comp.operation())
                  && identity().equals(comp.identity()))
                {
                  comp.addFilter(filter);
                  return true;
                }

              return false;
            }

          Scope scope = (Scope)enclosingScope;
          for (int i=scope.arity(); i-->0;)
            if (filter.containsFreeName(scope.parameter(i).name()))
              return false;

          enclosingScope = scope.enclosingScope();
        }

      return false;
    }

  final void addFilter (Expression filter)
    {
      _raw.patterns.add(null);
      _raw.expressions.add(filter);
    }  

  /**
   * Sets the qualifier at the specified <tt>index</tt> to <tt>null</tt> and percolates this
   * <tt>null</tt> as far to the right as it may go.
   */
  private final static void _eraseQualifier (int index, int upperLimit, Qualifier[] qualifiers)
    {
      qualifiers[index] = null;
      for (int i=index; i < upperLimit && qualifiers[i+1] != null; i++)
        {
          qualifiers[i] = qualifiers[i+1];
          qualifiers[i+1] = null;
        }
    }    

  /**
   * This translates monoid comprehension syntax using (possibly filtered) homomorphisms. It assumes
   * that the array of qualifiers has been normalized. The translation scheme is as follows:
   * <p>
   * <font color="navy"><pre>
   * [op,id]{e | } = op(e,id);
   *
   * [op,id]{e | c} = <b>if</b> c <b>then</b> op(e,id) <b>else</b> id;
   *
   * [op,id]{e | x <- e', c, Q} = <b>f_hom</b>(e', &lambda;x.[op,id]{e | Q}, op, id, &lambda;x.c);
   *
   * [op,id]{e | x <- e', y <- e'', Q} = <b>hom</b>(e', &lambda;x.[op,id]{e | y <- e'', Q}, op, id);
   * </pre></font>
   */
  private final Expression _translate (Qualifier[] qualifiers, int index)
    {
      if (index == qualifiers.length || qualifiers[index] == null)
        return new Application(_raw.op(),_raw.expression,_raw.id());

      Expression body = null;
      Homomorphism hom = null;
      
      if (index < qualifiers.length-1 && qualifiers[index].parameter != null
          && qualifiers[index+1] != null && qualifiers[index+1].parameter == null)
        {
          body = _translate(qualifiers,index+2);

          if (qualifiers[index].selectors != null)
            return _selectorExpression(qualifiers[index],qualifiers[index+1].expression,body);

          hom = new FilterHomomorphism(qualifiers[index].expression,
                                       new Scope(qualifiers[index].parameter,body).setNonExitable(),
                                       _raw.op(),_raw.id(),
                                       new Scope((Parameter)qualifiers[index].parameter.typedCopy(),
                                                 qualifiers[index+1].expression).setNonExitable());
          ((FilterHomomorphism)hom).setTables(_tables);
        }
      else
        {
          body = _translate(qualifiers,index+1);

          if (qualifiers[index].parameter == null)
            return new IfThenElse(qualifiers[index].expression,body,_raw.id());

          if (qualifiers[index].selectors != null)
            return _selectorExpression(qualifiers[index],null,body);

          hom = new Homomorphism(qualifiers[index].expression,
                                 new Scope(qualifiers[index].parameter,body).setNonExitable(),
                                 _raw.op(),_raw.id());
        }

      if (qualifiers[index].slicings != null)
        hom.setSlicings(qualifiers[index].slicings);
      
      if (_raw.inPlace == Homomorphism.ENABLED_IN_PLACE)
        return hom.enableInPlace();
      if (_raw.inPlace == Homomorphism.DISABLED_IN_PLACE)
        return hom.disableInPlace();

      return hom;
    }  

  /**
   * This returns a <tt>Let</tt> wrapping an <tt>IfThenElse</tt> as the transformed
   * expression resulting from a (possibly filtered) generator that contains at least
   * one selector expression.
   *
   * More precisely, if the generator is of the form:
   * <font color="navy"><pre>
   * x <- e <b>such that</b> f
   *        <b>sliced by</b> s1, ..., sm
   *        <b>selected by</b> v1, ..., vn
   * </pre></font>
   * and the body of translating the remaining qualifiers is <font color="navy">
   * <tt>body</tt></font>, then the resulting selector expression is:
   * <font color="navy"><pre>
   * <b>let</b> x = v1
   *  <b>in</b> <b>if</b> x <b>is_in</b> e
   *        <b>and</b> x == v2 <b>and</b> ... <b>and</b> x == vn
   *        <b>and</b> s1 <b>and</b> ... <b>and</b> sm <b>and</b> f
   *     <b>then</b> body
   *     <b>else</b> id
   * </pre></font>
   * where each slicing has its slicing variable unsanitized from a dummy local back to a dummy. 
   */
  private final Expression _selectorExpression (Qualifier generator, Expression filter,
                                                       Expression body)
    {
      Expression condition = new Application(_tables.in(),
                                             new Dummy(generator.parameter),
                                             generator.expression);

      for (int i=1; i<generator.selectors.size(); i++)
        condition = new And(condition,
                            (Expression)generator.selectors.get(i));

      if (generator.slicings != null)
        for (int i=0; i<generator.slicings.size(); i++)
          condition = new And(condition,
                              ((Application)generator.slicings.get(i)).undoDummyLocal());

      if (filter != null)
        condition = new And(condition,filter);

      return new Let(generator.parameter,
                     ((Application)generator.selectors.get(0)).argument(1),
                     new IfThenElse(condition,body,_raw.id()));
    }
                                            

  public final void setCheckedType ()
    {
      if (setCheckedTypeLocked()) return;
      _construct.setCheckedType();
      setCheckedType(_construct.checkedType());
    }

  public final void typeCheck (TypeChecker typeChecker) throws TypingErrorException
    {
      if (typeCheckLocked()) return;

      if (!(_construct instanceof Let))
        {
          _construct.typeCheck(_type,typeChecker);
          return;
        }

      Let let = (Let)_construct;
      let.setType(_type);

      Scope scope = (Scope)let.function();
      typeChecker.unify(scope.parameter(0).typeRef(),operation().typeRef(),this);
      typeChecker.unify(scope.parameter(1).typeRef(),identity().typeRef(),this);

      Expression operation = let.argument(0);
      Expression identity = let.argument(1);

      Type[] argumentTypes = { operation.typeRef(), identity.typeRef() };
      FunctionType functionType = new FunctionType(argumentTypes,let.typeRef()).setNoCurrying();

      identity.typeCheck(typeChecker);
      let.function().typeCheck(functionType,typeChecker);
      operation.typeCheck(functionType.domains()[0],typeChecker);
    }

  public final void compile (Compiler compiler)
    {
      _fixTypeBoxing();
      _construct.compile(compiler);
    }

  /**
   * This fixes the boxing of the monoid operator and identity by systematically unboxing
   * all occurrences of the collection element type. This is a necessary hack [:( sigh!]
   * because collection-building built-in dummy instructions like <tt>SET_ADD</tt> have a
   * needlessly polymorphic type that becomes instantiated only when it is applied. However,
   * a monoid comprehension construct is a <a href="Let.html"><tt>Let</tt></a> that
   * abstracts the monoid operation and identity. Now, when the operation is <tt>SET_ADD</tt>,
   * for example, as the compiler compiles the application corresponding to the "let", it sees
   * it as a non-applied function argument with a polymorphic type and will proceed to "pad" it
   * (see <a href="Expression.html"><tt>Expression</tt></a>). This "padding" must be avoided,
   * as well as all boxing of the types corresponding to the collection's elements.
   */
  private final void _fixTypeBoxing ()
    {
      Let let = (Let)_construct;
      
      FunctionType potype = (FunctionType)((FunctionType)let.function().checkedType()).domain(0);
      FunctionType otype = (FunctionType)let.argument(0).checkedType();
      Type itype = let.argument(1).checkedType();

      if (itype.kind() == Type.BOXABLE)
        ((BoxableTypeConstant)itype).setBoxed(false);

      if (otype.domain(0).kind() == Type.BOXABLE)
        {
          ((BoxableTypeConstant)otype.domain(0)).setBoxed(false);
          otype.unsetDomainBox(0);

          ((BoxableTypeConstant)potype.domain(0)).setBoxed(false);
          potype.unsetDomainBox(0);

          if (otype.domain(0).isEqualTo(otype.domain(1)))   // primitive comprehension
            {
              ((BoxableTypeConstant)otype.domain(1)).setBoxed(false);
              otype.unsetDomainBox(1);

              ((BoxableTypeConstant)potype.domain(1)).setBoxed(false);
              potype.unsetDomainBox(1);

              ((BoxableTypeConstant)otype.range()).setBoxed(false);
              otype.unsetRangeBox();

              ((BoxableTypeConstant)potype.range()).setBoxed(false);
              potype.unsetRangeBox();
            }
        }
    }

  public final String toString ()
    {
      return _raw == null ? "Comprehension_"+_construct.toString() : _raw.toString();
    }   

  private class RawInfo
    {
      Expression operation;
      Expression identity;
      Expression expression;
      ArrayList patterns;
      ArrayList expressions;
      byte inPlace;

      boolean isDesugared;

      RawInfo (Expression operation, Expression identity, Expression expression,
               ArrayList patterns, ArrayList expressions, byte inPlace)
        {
          this.expression = expression;
          this.operation = operation;
          this.identity = identity;
          this.patterns = patterns;
          this.expressions = expressions;
          this.inPlace = inPlace;
        }

      final Expression op ()
        {
          return operation.typedCopy();
        }

      final Expression id ()
        {
          return identity.typedCopy();
        }

      public final String toString ()
        {
          StringBuffer buf = new StringBuffer("[")
                                 .append(operation())
                                 .append(",")
                                 .append(identity())
                                 .append("] { ")
                                 .append(expression)
                                 .append(" | ");

          for (int i=0; i<patterns.size(); i++)
            {
              Object pattern = patterns.get(i);
              if (pattern != null)
                buf.append(pattern).append(" <- ");
              buf.append(expressions.get(i));
              if (i < patterns.size() - 1)
                buf.append(", ");
            }

          return buf.append(" }").toString();
        }
    }    

  private static class IndexedExpression
    {
      int index;
      Expression expression;

      IndexedExpression (int index, Expression expression)
        {
          this.index = index;
          this.expression = expression;
        }

      public final String toString ()
        {
          return expression + "/" + index;
        }
    }

  private class Qualifier
    {
      Parameter parameter;
      Expression expression;
      ArrayList slicings;
      ArrayList selectors;

      Qualifier (Parameter parameter, Expression expression)
        {
          this.parameter = parameter;
          this.expression = expression;
        }

      final boolean isGenerator ()
        {
          return parameter != null;
        }

      final boolean isSlicing (Parameter parameter)
        {
          return expression.isSlicing(tables(),parameter);
        }

      final void addSlicing (Expression slicing)
        {
          if (slicings == null)
            slicings = new ArrayList();
          slicings.add(slicing);
        }

      final boolean isSelector (Parameter parameter)
        {
          return expression.isSelector(tables(),parameter);
        }

      final void addSelector (Expression selector)
        {
          if (selectors == null)
            selectors = new ArrayList();
          selectors.add(selector);
        }

      public final String toString ()
        {
          if (parameter == null)
            return expression.toString();

          return parameter + " <- " + expression +
                 (selectors == null ? "" : " selected by " + selectors) +
                 (slicings == null ? "" : " sliced by " + slicings);
        }
    }
}