gt:             ParseResult r0 = (ParseResult) rs.Parses.get(j);
context: /*
   * Copyright (C) 2007-2014 Dylan Bumford, Lucas Champollion, Maribel Romero
   * and Joshua Tauberer
   * 
   * This file is part of The Lambda Calculator.
   * 
   * The Lambda Calculator is free software: you can redistribute it and/or
   * modify it under the terms of the GNU General Public License as published by
   * the Free Software Foundation, either version 3 of the License, or (at your
   * option) any later version.
   * 
   * The Lambda Calculator is distributed in the hope that it will be useful,
   * but WITHOUT ANY WARRANTY; without even the implied warranty of
   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
   * Public License for more details.
   * 
   * You should have received a copy of the GNU General Public License along
   * with The Lambda Calculator.  If not, see <http://www.gnu.org/licenses/>.
   *
   */
  
  /*
   * ExpressionParser.java
   *
   * Created on May 29, 2006, 3:02 PM
   */
  package lambdacalc.logic;
  
  import java.util.*;
  
  /**
   * Parses a string into an Expr object.
   *
   * This is a simple recursive descent parser augmented with the possibility for
   * the detection of ambiguous strings. For each of the main functions,
   * parseFunctionApplication, parseInfixExpression, and parsePrefixExpression,
   * the caller is asking the callee to find every legitimate instance of function
   * application, an infix expression, or a prefix expression starting at the
   * indicated position, but ending anywhere. So, for infix expressions like A & B
   * & C, the callee returns A, A & B, and A & B & C. Likewise, for function
   * applications like P a b c, the callee returns P (the predicate alone), P a,
   * (P a) b, and ((P a) b) c. This allows for the scopes of infix operators to
   * pop up. For instance, Ax.P(x) & Q(x), two parsing paths are taken.
   * parseInfixExpression calls parseFunctionApplication which calls
   * parsePrefixExpression, which sees the binder and calls parseInfixExpression
   * to get its inner expression. parseInfixExpression returns a set comprising
   * the parses P(x) and P(x) & Q(x). parsePrefixExpression wraps each possibility
   * with the binder, so it returns the set: Ax.P(x) and Ax.P(x) & Q(x). Above
   * that, parseFunctionApplicationException scans to the right of each
   * possibility looking for an argument, but it finds none so it just passes up
   * those two possibilities. parseInfixExpression looks to the right of each
   * possibility for a connective. In the first case, it finds the ampersand, so
   * it creates a conjunction yielding [Ax.P(x)] & Q(x). In the second case, it
   * hits the end of the string and just returns Ax.P(x) & Q(x) unchanged.
   *
   * Each such call can return either 1) a set of one or more possible parses, or
   * 2) an error condition (SyntaxException) indicating why nothing could be
   * parsed. Further, each possible parse can be tagged with why the parse didn't
   * go any further than it did (HowToContinue, a SyntaxException). For instance,
   * in "[Lx.P(x)] ^", parseFunctionApplication will try to parse the caret as an
   * expression, but will fail, so it will return as much as it could parse, which
   * is "[Lx.P(x)]", but tagged with the SyntaxException that occurred parsing the
   * next bit. This is used as the message for the user when the remainder of the
   * string couldn't be parsed.
   */
  public class ExpressionParser {
  
    /**
     * Testing routine. It prints out the various potential parses and the at the
     * end the actually accepted parse, or the error message that would be thrown
     * on failure.
     */
    public static void main(String[] args) {
      ParseOptions opts = new ParseOptions();
      opts.ASCII = true;
  
      ParseResultSet rs = parseExpression(args[0], 0, opts, "an expression");
      if (rs.Exception != null) {
        rs.Exception.printStackTrace();
        return;
      }
      for (int i = 0; i < rs.Parses.size(); i++) {
        ParseResult r = (ParseResult) rs.Parses.get(i);
        System.out.print(r.Next + "   " + r.Expression.toString());
        String type = "(type mismatch)";
        try {
          type = r.Expression.getType().toString();
        } catch (TypeEvaluationException tee) {
        }
        System.out.print(" " + type);
        if (r.HowToContinue != null) {
          System.out.print("  " + r.HowToContinue.getMessage());
        }
        System.out.println();
      }
  
      System.out.println();
  
      try {
        System.out.println(parse(args[0], opts));
      } catch (SyntaxException se) {
        System.err.println(se.getMessage());
      }
    }
  
    /**
     * Options for parsing expressions.
     */
    public static class ParseOptions {
  
      /**
       * This turns on single-letter-identifier mode, so that Pa is interpreted as
       * P(a), rather than as a single identifier.
       */
      public boolean singleLetterIdentifiers = false;
  
      /**
       * This turns on ASCII mode.
       * These symbols become special: A, E, L, ~, &, |, ->, <->
       * forall, exists, lambda, not, and, or, if, iff
       */
      public boolean ASCII = false;
  
      /**
       * This provides the types for identifiers encountered in the expression.
       * Every identifier must be identifiable as a constant or variable and with
       * a type. By default, this field contains an IdentifierTyper with a default
       * setup.
       */
      public IdentifierTyper typer = IdentifierTyper.createDefault();
  
      /**
       * This map is populated during the course of parsing an expression and
       * lists some of the types assigned explicitly in the expression. One type
       * is remembered per name, so if a single name is used with different types
       * in different places, only the last one parsed will be listed in the Map.
       */
      public Map explicitTypes = new HashMap();
  
      public boolean hasExplicitTypes() {
        return !explicitTypes.isEmpty();
      }
  
      public ParseOptions() {
  
      }
  
      public ParseOptions(boolean singleLetterIdentifiers, boolean ASCII, IdentifierTyper typer) {
        this.singleLetterIdentifiers = singleLetterIdentifiers;
        this.ASCII = ASCII;
        this.typer = typer;
      }
  
      public ParseOptions(boolean singleLetterIdentifiers, boolean ASCII) {
        this.singleLetterIdentifiers = singleLetterIdentifiers;
        this.ASCII = ASCII;
      }
  
      ParseOptions cloneContext() {
        ParseOptions ret = new ParseOptions();
        ret.singleLetterIdentifiers = singleLetterIdentifiers;
        ret.ASCII = ASCII;
        ret.typer = typer.cloneTyper();
        ret.explicitTypes = explicitTypes;
        return ret;
      }
    }
  
    /**
     * This class represents the set of possible parses that could be read at a
     * given position in the string, taking into account that some strings are
     * legitimately ambiguous, to be resolved at the end. This class can also
     * represent a fatal error condition when no parses are possible. So, either
     * Exception is set at Parses is null, or else Parses is a vector of one or
     * more elements, and Exception is null.
     */
    private static class ParseResultSet {
  
      public final SyntaxException Exception; // if set, a fatal error, no parses available
      public final Vector Parses; // if set, one or more possible parses
  
      public ParseResultSet(SyntaxException ex) {
        Exception = ex;
        Parses = null;
      }
  
      public ParseResultSet(Vector parses) {
        Exception = null;
        Parses = parses;
      }
  
      public ParseResultSet(ParseResult singletonParse) {
        Exception = null;
        Parses = new Vector();
        Parses.add(singletonParse);
      }
    }
  
    /**
     * This class represents a single potential parse of a string at a given
     * location. Expression contains the parsed substring. Next is the next
     * character position after the substring read. HowToContinue is an
     * informative error message about why the parser stopped when it did. It is
     * normally used when we were able to parse a substring as something, but when
     * it is the best we can parse of the user input yet it is not the whole
     * expression given.
     */
    private static class ParseResult {
  
      public final Expr Expression; // parsed subexpression
      public final int Next; // next character position after subexpression
      public final SyntaxException HowToContinue; // if set, why we stopped here
  
      public ParseResult(Expr expr, int next) {
        this(expr, next, null);
      }
  
      public ParseResult(Expr expr, int next, SyntaxException continuation) {
        Expression = expr;
        Next = next;
        HowToContinue = continuation;
      }
    }
  
    /**
     * Private constructor. All the methods in this class are static.
     */
    private ExpressionParser() {
    }
  
    public static Expr parseAndSuppressExceptions(String expression, ParseOptions options) {
      Expr result = null;
      try {
        result = parse(expression, options);
      } catch (SyntaxException s) {
        //s.printStackTrace();
      }
      return result;
    }
  
    /**
     * Parses an expression with the given options. This is the entry point of
     * this class.
     *
     * @param expression the expression to be parsed
     * @param options global options for parsing, e.g. typing conventions
     * @return an Expr object representing the expression
     * @throws SyntaxException if a parse error occurs
     *
     */
    public static Expr parse(String expression, ParseOptions options) throws SyntaxException {
      options.explicitTypes.clear();
  
      if (expression.trim().length() == 0) {
        throw new SyntaxException("Enter a lambda expression.", 0);
      }
  
      ParseResult r = parse2(expression, 0, options, "an expression", true);
  
      return r.Expression;
    }
  
    /**
     * This method starts off the main work of the class. It tries to parse an
     * expression and then resolve the ambiguities, according to several
     * constraints. If the expression could not be parsed at all, a
     * SyntaxException is thrown. To resolve ambiguities, first only the parses
     * that read the longest amount of the expression are considered. Then, if any
     * parse is well-typed, discard the non-well-typed parses. Last, take only the
     * parses that have the least number of free variables. If more than one parse
     * still results, a SyntaxException is thrown altering the user to the
     * ambiguities remaining.
     *
     * @param expression the text string being parsed
     * @param start the position at which to start scanning for a prefix
     * expression
     * @param context global options for parsing
     * @param whatIsExpected a string describing what kind of expression is
     * expected to occur at this position, for error messages
     * @param readFully true iff a failure to read to the end of the string should
     * cause an exception to be thrown.
     * @return a single ParseResult for the best parse
     * @throws SyntaxException if no parse is possible
     */
    private static ParseResult parse2(
      String expression, int start, ParseOptions context, String whatIsExpected, boolean readFully
    ) throws SyntaxException {
      // Parse the string into a number of potential ambiguous parses.
      ParseResultSet rs = parseExpression(expression, start, context, whatIsExpected);
  
      // If a fatal parsing error ocurred such that no parses were available, just
      // throw the error.
      if (rs.Exception != null) {
        throw rs.Exception;
      }
  
      // Use ordered constraints to filter out parses.
      // The first constraint is to drop all parses that don't go as far into the
      // string as the most extensive parse.
      int maxParse = -1;
      for (int i = 0; i < rs.Parses.size(); i++) { // get maximum
        ParseResult r = (ParseResult) rs.Parses.get(i);
        if (r.Next > maxParse) {
          maxParse = r.Next;
        }
      }
      for (int i = 0; i < rs.Parses.size(); i++) { // filter out non-maximal parses
        ParseResult r = (ParseResult) rs.Parses.get(i);
        if (r.Next < maxParse) {
          rs.Parses.remove(i);
          i--;
        } // decrement i to repeat iteration at same index
      }
  
      // If readFully is true, we are wanting to read the entire string. In that case,
      // if we haven't gotten to the end of the string, raise an exception.
      // (When parsing arguments to predicates, this method is called but we don't
      // want to read to the end of the string.) We'll just take the first error message
      // we can find in a HowToContinue field, or throw a generic one if there aren't any
      // prepared messages.
      if (readFully && maxParse != expression.length() &&
          skipWhitespace(expression, maxParse) != -1) {
        for (int i = 0; i < rs.Parses.size(); i++) { // filter out non-maximal parses
          ParseResult r = (ParseResult) rs.Parses.get(i);
          if (r.HowToContinue != null) {
            throw r.HowToContinue;
          }
        }
        throw new SyntaxException("\"" + expression.substring(maxParse) +
                                  "\" doesn't look like a complete lambda expression.",
                                  maxParse);
      }
  
      // Next, if any parse is well typed, then drop the non-well-typed parses.
      boolean hasWellTyped = false;
      for (int i = 0; i < rs.Parses.size(); i++) {
        ParseResult r = (ParseResult) rs.Parses.get(i);
        try {
          Type t = r.Expression.getType(); // return value is not important
          hasWellTyped = true; // not executed if type evaluation fails
        } catch (TypeEvaluationException tee) {
        }
      }
      if (hasWellTyped) {
        for (int i = 0; i < rs.Parses.size(); i++) { // filter out non-maximal parses
          ParseResult r = (ParseResult) rs.Parses.get(i);
          try {
            r.Expression.getType(); // return value is not important
          } catch (TypeEvaluationException tee) {
            rs.Parses.remove(i);
            i--; // decrement i to repeat iteration at same index
          }
        }
      }
    
      // If more than one parse remains, the expression might be ambiguous.
      if (rs.Parses.size() > 1) {
        Vector alternatives = new Vector();
        parses:
        for (int i = 0; i < rs.Parses.size(); i++) {
          ParseResult r = (ParseResult) rs.Parses.get(i);
          // This shouldn't happen, but just in case two parsing paths produced the 
          // same expression, keep only one of them
          if (i != 0) {
            for (int j = 0; j < i; j++) {
  