/* Copyright (C) 2008 Hugh McGuire http://www.cis.gvsu.edu/~mcguire/ * Grand Valley State University, MI 49401-9403 */ /* This program 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. This program 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. For a copy of the GNU General Public License, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth floor, Boston, MA 02110-1301, USA. Another option as of January 1, 2008 is to browse the following URL: http://www.gnu.org/copyleft/gpl.html */ import java.util.*; /** * Representation and fundamental actions for mathematical symbols. * @author Hugh McGuire */ class Symbol implements Grammar_Construct, java.io.Serializable { // "The Java Language Specification" specified: // "nested enum types are implicitly static." enum Specifier { // Precedence mostly follows the order of these items, // but is actually more complex than just the straightforward order. // See the dragon book ("Compilers" by Aho, Sethi, and Ullman) // re operator-precedence parsing. // One might expect some of the distinct items here // to have equal precedence, but for those that are nonassociative // anyway, it shouldn't matter if the precedences vary slightly. // Others (PLUS, MINUS) are handled as special cases. // Names here are derived from sources such as TeX, Unicode, and HTML. ENDMARKER, // '$' re compilation BREAK, // "NEWLINE" but newline characters aren't breaks if at infix ops. // special ~~delimiter // infix to avoid ... TIMES BREAK // See also |is_right_associative()| regarding this. // Delimiters actually handled intriguingly // (as indicated in book "Compilers"): // any opening delimiter always pushed on stack // as if strong precedence, // but needs to have weak precedence while in stack; // closing delimiter should never get in stack // so won't have to worry about precedence in there, // but otherwise weak precedence. // I've decided closing delimiters have weaker precedence than // opening ones. CLOSING_DELIMITER, // postfix so "(x+y)" won't have ... y TIMES ) OPENING_DELIMITER, // LET, SUM, PROD, // |is_binary_infix()|: |EQUIV| to |EXP|, plus |QUANT_SEP| and |SUBST| EQUIV, IMPLIES, OR, AND, /* ONLY, // rem. "if" handled as |OPENING_DELIMITER| */ FOR, TO, SUCH_THAT, // CONSIDER ARRANGING ~~SAME PRECEDENCE FOR RELATIONS // SO CAN HAVE FOR EXAMPLE "0 < k <= n" // BUT THEN TO HANDLE SUCH E.G. IN |simplify()|, // COULD ~~SIMPLY CHECK EACH SIDE OF RELATION EXPRESSION // FOR ANOTHER RELATION EXPRESSION ANYWAY IS, PMOD, // name derived from TeX; see also BMOD /* EQUALS_DEF, BECOMES, */ CONGRUENT, EQUALS, NEQ, LEQ, GEQ, LESS_THAN, GREATER_THAN, DIVIDES, IS_IN, NOT_IN, SUBSET, SUBSETEQ, // CONSIDER: Having a special 'comma' for quantifiers // might enable things such as lambda expressions. COMMA, // This is at this place (regarding precedence) because // this is a delimiter for terms BMOD, // name derived from TeX; see also PMOD // maybe debatable precedence position REMAINDER_CODE, // maybe debatable precedence position UNION, INTERSECT, TIMES_X, PLUS, MINUS, // PLUS and MINUS are supposed to have equal precedence /* I'm giving QUOTIENT weaker precedence * than TIMES considering expressions * such as a/bc , i.e. a/(b*c) . Remember: "Some of the operators have the wrong precedence." *The C Programming Language*, by Brian W. Kernighan and Dennis M. Ritchie, i.e. the source(s) of C/C++/Java. */ // See also |is_right_associative()| regarding TIMES. QUOTIENT, TIMES, GROUP_OP, EXP, // alternatively "EXPONENT" // right associativity handled below // |is_binary_infix()|: |PMOD| to |EXP|, plus |QUANT_SEP| and |SUBST| // postfix: // ? Needed to leave the identifier "prime" available. ? PRIME, FACTORIAL, COMPLEMENT_POST, // unary/prefix: NEGATIVE, POWERSET, LN, LOG10, LG, LOG, LOG_, // THETA_UPPERCASE, // OMEGA_UPPERCASE, OMEGA_LOWERCASE, NOT, TILDE, // McGuire: COMPLEMENT_PRE; Epp: NOT // NEED TO REDO CODE SO SIMPLY CHANGE // APPEARANCE OF |NOT| INSTEAD OF USING // DIFFERENT |Specifier| // Consider "QUANTIFICATION". // infix! QUANT_SEP, // This symbol's token is a THIN_SPACE or nothing(!) // (and for a while I tried ".") // between quantifier and what it quantifies. // Jape uses ".". (I thought of it independently.) SUBST, // infix! FORALL, // prefix EXISTS, // prefix // EXISTS_UNIQUE, // operands / ~~zeroary: IDENTIFIER, INT, INFINITY, C_NUMBERS, R_NUMBERS, Q_NUMBERS, Z_NUMBERS, N_NUMBERS, // NATURAL, REAL, RATIONAL, INT, // SET EMPTYSET, TRUE, FALSE, COMMENT, //USER_DEFINED } // Could this be inside the |Specifier| class? private final static EnumSet spec_usable_by_name // LET = EnumSet.range(Specifier.SUM, Specifier.INTERSECT); static { spec_usable_by_name.remove(Specifier.PMOD); spec_usable_by_name.remove(Specifier.COMMA); spec_usable_by_name.remove(Specifier.REMAINDER_CODE); //spec_usable_by_name.add(Specifier.EXP); spec_usable_by_name.add(Specifier.LN); spec_usable_by_name.add(Specifier.LOG10); spec_usable_by_name.add(Specifier.LG); spec_usable_by_name.add(Specifier.LOG); spec_usable_by_name.add(Specifier.LOG_); spec_usable_by_name.add(Specifier.NOT); spec_usable_by_name.add(Specifier.FORALL); spec_usable_by_name.add(Specifier.EXISTS); spec_usable_by_name.add(Specifier.INFINITY); spec_usable_by_name.add(Specifier.C_NUMBERS); spec_usable_by_name.add(Specifier.R_NUMBERS); spec_usable_by_name.add(Specifier.Q_NUMBERS); spec_usable_by_name.add(Specifier.Z_NUMBERS); spec_usable_by_name.add(Specifier.N_NUMBERS); spec_usable_by_name.add(Specifier.EMPTYSET); spec_usable_by_name.add(Specifier.TRUE); spec_usable_by_name.add(Specifier.FALSE); } static final String UNUSED_NOTE = "[unused]"; // parenthesized integers also taken as comments // considering when copy from HTML. static final String[] EOL_DELIMITED_COMMENT_STARTS = {"//", "#"}; static final String INLINE_COMMENT_START = "/*"; static final String INLINE_COMMENT_END = "*/"; static final char NAME_COMMENT_START = '"'; static final char NAME_COMMENT_END = '"'; static final String PMOD_ = "(mod "; static final char THREE_BAR_UNICODE = '\u2261'; static final String ARROW_LEFT_RIGHT_TWO_BARS_ASCII = "<==>"; static final char ARROW_LEFT_RIGHT_TWO_BARS_UNICODE = '\u21D4'; static final String ARROW_LEFT_RIGHT_ONE_BAR_ASCII = "<-->"; static final char ARROW_LEFT_RIGHT_ONE_BAR_UNICODE = '\u2194'; static final String ARROW_RIGHT_TWO_BARS_ASCII = "==>"; static final char ARROW_RIGHT_TWO_BARS_UNICODE = '\u21D2'; static final String ARROW_RIGHT_ONE_BAR_ASCII = "-->"; static final char ARROW_RIGHT_ONE_BAR_UNICODE = '\u2192'; static final char IMPLIES_U_COUNTERCLOCKWISE_UNICODE = '\u2283'; // consider '\u2283' Unicode specifies "SUPERSET OF" // but used for implication e.g. by Enderton, ETPS static final String ARROW_RIGHT_ONE_BAR_ASCII_ = "->"; // "->" was used at Michigan State University, January 2008. static final String ARROW_RIGHT_TWO_BARS_ASCII_ = "=>"; // "=>" was used in "Logical Foundations of Artificial Intelligence" // by Genesereth & Nilsson, and that book may once have been used for // Stanford's CS 157 (in 2008 ~~CS 103a) static final String OR_ASCII = "\\/"; static final String OR_ASCII_ = "V"; static final String OR_PROG2_ASCII = "||"; //static final char OR_PROG1_ASCII = '|'; // DIVIDES static final char OR_UNICODE = '\u2228'; static final char OR_NARY_UNICODE = '\u22C1'; static final String AND_ASCII = "/\\"; static final String AND_PROG2_ASCII = "&&"; static final char AND_PROG1_ASCII = '&'; static final char AND_UNICODE = '\u2227'; static final char AND_NARY_UNICODE = '\u22C0'; static final String ARROW_LEFT_ONE_BAR_ASCII = "<--"; static final char ARROW_LEFT_ONE_BAR_UNICODE = '\u2190'; static final char THIN_SPACE_UNICODE = '\u2009'; static final String COLON_EQUALS_ASCII = ":="; static final char COLON_EQUALS_UNICODE = '\u2254'; static final char EQUALS_DEF_UNICODE = '\u225D'; static final String EQUALS_PROG_ASCII = "=="; static final String NEQ_ASCII = "!="; static final char NEQ_UNICODE = '\u2260'; static final String LEQ_PROG_ASCII = "<="; static final char LEQ_UNICODE = '\u2264'; static final String GEQ_PROG_ASCII = ">="; static final char GEQ_UNICODE = '\u2265'; static final char CONGRUENT_UNICODE = '\u2245'; static final char VERTICAL_LINE_UNICODE = '\u2223'; // Unicode specifies the official name is "DIVIDES" but // then says "= such that" and "--> 007C vertical line" static final char IS_IN_UNICODE = '\u2208'; static final char NOT_IN_UNICODE = '\u2209'; static final char SUBSET_UNICODE = '\u2282'; static final char SUBSETEQ_UNICODE = '\u2286'; static final char SETMINUS_UNICODE = '\u2216'; static final char MINUS_UNICODE = '\u2212'; static final char INTERSECT_UNICODE = '\u2229'; static final char UNION_UNICODE = '\u222A'; static final char TIMES_X_UNICODE = '\u00D7'; // Cartesian product // for sets; // currently not // accepted for // multiplication // of numbers //static final char REMAINDER_CODE_ASCII = '%'; static final char TIMES_ASCII = '*'; static final char INVISIBLE_TIMES_UNICODE = '\u2062'; static final char TIMES_ASTERISK_UNICODE = '\u2217'; static final char MIDDLE_DOT_UNICODE = '\u00B7'; // The difference between DOT_OPERATOR_UNICODE // and MIDDLE_DOT_UNICODE is that // DOT_OPERATOR appears to include more blank space // surrounding the dot. Thus I conjecture that // DOT_OPERATOR would be better for major operations // such as dot products of things such as vectors // while MIDDLE_DOT is actually nice for // simple products such as '2*7'. static final char DOT_OPERATOR_UNICODE = '\u22C5'; static final char GROUP_OP_ASCII = 'o'; // static final char GROUP_OP_UNICODE = '\u2218'; // appears terrible static final char DIVISION_SIGN_UNICODE = '\u00F7'; static final char DIVIDE_SLASH_UNICODE = '\u2215'; static final char EXP_MCGUIRE_ASCII = '`'; // "M" for "McGuire" (;-) static final char EXP_ASCII = '^'; static final char SUPERSCRIPT_0_UNICODE = '\u2070'; static final char SUPERSCRIPT_1_UNICODE = '\u00B9'; static final char SUPERSCRIPT_2_UNICODE = '\u00B2'; static final char SUPERSCRIPT_3_UNICODE = '\u00B3'; static final char SUPERSCRIPT_4_UNICODE = '\u2074'; static final char SUPERSCRIPT_5_UNICODE = '\u2075'; static final char SUPERSCRIPT_6_UNICODE = '\u2076'; static final char SUPERSCRIPT_7_UNICODE = '\u2077'; static final char SUPERSCRIPT_8_UNICODE = '\u2078'; static final char SUPERSCRIPT_9_UNICODE = '\u2079'; static final char SUPERSCRIPT_MINUS_UNICODE = '\u207B'; static final char SUPERSCRIPT_OPENING_PAREN_UNICODE = '\u207D'; static final char SUPERSCRIPT_CLOSING_PAREN_UNICODE = '\u207E'; static final char SUBSCRIPT_1_UNICODE = '\u2081'; static final char SUBSCRIPT_2_UNICODE = '\u2082'; static final char SUBSCRIPT_3_UNICODE = '\u2083'; //static final char NOT_PROG_ASCII = '!'; // need '!' for factorial // consider lexing " ! " as NOT, "!something" as NOT, // "something!" as factorial, // and "something!something" as factorial as in "k!*(n-k)!" static final char TILDE_ASCII = '~'; static final char NOT_UNICODE = '\u00AC'; static final char PRIME_UNICODE = '\u2032'; static final char FORALL_UNICODE = '\u2200'; static final char EXISTS_UNICODE = '\u2203'; // The following appeared poorly; // see the bracket corners next static final char LCEIL_UNICODE = '\u2308'; static final char RCEIL_UNICODE = '\u2309'; static final char LFLOOR_UNICODE = '\u230A'; static final char RFLOOR_UNICODE = '\u230B'; /* static final char LEFT_SQUARE_BRACKET_UPPER_CORNER_UNICODE = '\u23A1'; static final char LEFT_SQUARE_BRACKET_LOWER_CORNER_UNICODE = '\u23A3'; static final char RIGHT_SQUARE_BRACKET_UPPER_CORNER_UNICODE = '\u23A4'; static final char RIGHT_SQUARE_BRACKET_LOWER_CORNER_UNICODE = '\u23A6'; */ static final char LEFT_UPPER_CORNER_UNICODE = '\u23A1'; static final char LEFT_LOWER_CORNER_UNICODE = '\u23A3'; static final char RIGHT_UPPER_CORNER_UNICODE = '\u23A4'; static final char RIGHT_LOWER_CORNER_UNICODE = '\u23A6'; static final char PROD_UNICODE = '\u220F'; static final char SUM_UNICODE = '\u2211'; static final char TRIANGLE_FILLED_LEFT_POINTING_UNICODE = '\u25C0'; static final char TRIANGLE_FILLED_LEFT_POINTING_SMALL_UNICODE = '\u25C2'; static final char TRIANGLE_FILLED_LEFT_POINTING_NARROW_UNICODE = '\u25C4'; static final char INFINITY_UNICODE = '\u221E'; static final char THETA_UPPERCASE_UNICODE = '\u0398'; static final char OMEGA_UPPERCASE_UNICODE = '\u03A9'; static final char OMEGA_LOWERCASE_UNICODE = '\u03C9'; static final char C_NUMBERS_UNICODE = '\u2102'; static final char R_NUMBERS_UNICODE = '\u211D'; static final char Q_NUMBERS_UNICODE = '\u211A'; static final char Z_NUMBERS_UNICODE = '\u2124'; static final char N_NUMBERS_UNICODE = '\u2115'; static final char SCRIPT_CAPITAL_P_UNICODE = '\u2118'; // for power set as indicated in HTML char. ents. documentation static final char EMPTYSET_UNICODE = '\u2205'; static final String EMPTYSET_BRACES = "{}"; static final char TOP_UNICODE = '\u22A4'; static final char BOTTOM_UNICODE = '\u22A5'; static final char FUNCTION_APPLICATION_UNICODE = '\u2062'; // CONSIDER // USE THIS static final String LETTERS_SPECIAL = "" + C_NUMBERS_UNICODE + R_NUMBERS_UNICODE + Q_NUMBERS_UNICODE + Z_NUMBERS_UNICODE + N_NUMBERS_UNICODE; // The following are glyphs/texts that may be used for narrative, // not necessarily as symbols in expressions: static final char ETA_LOWERCASE_UNICODE = '\u03B7'; static final char NU_LOWERCASE_UNICODE = '\u03BD'; static final char XI_LOWERCASE_UNICODE = '\u03BE'; static final char PI_LOWERCASE_UNICODE = '\u03C0'; static final char TAU_LOWERCASE_UNICODE = '\u03C4'; static final char PHI_LOWERCASE_UNICODE = '\u03C6'; static final char ARROW_DOWNWARD_ONE_BAR_UNICODE = '\u2193'; static final char CIRCLED_CAPITAL_R_UNICODE = '\u00AE'; // to stand for a relation as in FORALL VAR REL SOMETHING // alternatively maybe use just 'R' static boolean is_reserved(String s) { try { Specifier.valueOf(s.toUpperCase()); return true; } catch ( IllegalArgumentException e ) { return false; } } static boolean is_superscript(char ch) { return ch == SUPERSCRIPT_MINUS_UNICODE || ch == SUPERSCRIPT_0_UNICODE || ch == SUPERSCRIPT_1_UNICODE || ch == SUPERSCRIPT_2_UNICODE || ch == SUPERSCRIPT_3_UNICODE || ch == SUPERSCRIPT_4_UNICODE || ch == SUPERSCRIPT_5_UNICODE || ch == SUPERSCRIPT_6_UNICODE || ch == SUPERSCRIPT_7_UNICODE || ch == SUPERSCRIPT_8_UNICODE || ch == SUPERSCRIPT_9_UNICODE; } boolean text_is_superscript() { // currently returns |true| if |text| is empty for ( char ch : text.toCharArray() ) if ( !is_superscript(ch) ) return false; return true; } /* static int get_val(char ch) { if ( Character.isDigit(ch) ) return ch - '0'; // SUPERSCRIPT_2_UNICODE and SUPERSCRIPT_3_UNICODE were placed 'early' // also SUPERSCRIPT_1_UNICODE (though I didn't get a clue from HTML // documentation as I did with 2 and 3) if ( ch == SUPERSCRIPT_1_UNICODE ) return 1; if ( ch == SUPERSCRIPT_2_UNICODE ) return 2; if ( ch == SUPERSCRIPT_3_UNICODE ) return 3; if ( is_superscript(ch) ) return ch - SUPERSCRIPT_0_UNICODE; throw new IllegalArgumentException( "char ch='" + ch + "' ('\\u" + Integer.toHexString(ch) + "')" ); } int get_val() { assert specifier == Specifier.INT : "specifier == Specifier.INT"; int result = 0; for ( char ch : text.toCharArray() ) result += get_val(ch); return result; } */ String text_unsuperscript() { assert text_is_superscript() : "text_is_superscript()"; char[] result_chars = new char[text.length()]; for ( int i = 0; i < text.length(); i++ ) { assert is_superscript(text.charAt(i)) : "is_superscript(text.charAt(i))"; if ( text.charAt(i) == SUPERSCRIPT_MINUS_UNICODE ) result_chars[i] = '-'; // SUPERSCRIPT_2_UNICODE and SUPERSCRIPT_3_UNICODE were // placed 'early' // also SUPERSCRIPT_1_UNICODE (though I didn't get a clue // from HTML documentation as I did with 2 and 3) else if ( text.charAt(i) == SUPERSCRIPT_1_UNICODE ) result_chars[i] = '1'; else if ( text.charAt(i) == SUPERSCRIPT_2_UNICODE ) result_chars[i] = '2'; else if ( text.charAt(i) == SUPERSCRIPT_3_UNICODE ) result_chars[i] = '3'; else result_chars[i] = (char) ('0' + text.charAt(i) - SUPERSCRIPT_0_UNICODE); } return new String(result_chars); } /** * * throws NumberFormatException() if material isn't good */ int get_val() { //assert specifier == Specifier.INT : "specifier == Specifier.INT"; return Integer .parseInt(text_is_superscript() ? text_unsuperscript() : text); } static String superscript(int val) { // initially forgot about 0 if ( val == 0 ) return Character.toString(SUPERSCRIPT_0_UNICODE); StringBuilder result_sb = //new StringBuilder(1 + Math.log10(Integer.MAX_VALUE)); new StringBuilder(); // 2008 Java API documentation: init. cap.: 16 // which is generally fine boolean negative = val < 0; for ( val = Math.abs(val); val > 0; val /= 10 ) { byte digit = (byte) (val % 10); // Should the language // have suffix "B" as w/"10B" // to specify type "byte"? (;-) switch ( digit ) { // SUPERSCRIPT_2_UNICODE and SUPERSCRIPT_3_UNICODE were // placed 'early' // also SUPERSCRIPT_1_UNICODE (though I didn't get a clue // from HTML documentation as I did with 2 and 3) case 1: result_sb.append(SUPERSCRIPT_1_UNICODE); break; case 2: result_sb.append(SUPERSCRIPT_2_UNICODE); break; case 3: result_sb.append(SUPERSCRIPT_3_UNICODE); break; default: result_sb.append((char) (SUPERSCRIPT_0_UNICODE + digit)); } } if ( negative ) result_sb.append(SUPERSCRIPT_MINUS_UNICODE); return result_sb.reverse().toString(); } // somewhat kludge; I wonder whether |Character| should or shouldn't have // this boolean text_is_ASCII() { if ( text.equals("") ) return false; for ( char ch : text.toCharArray() ) if ( ch < 0 || Byte.MAX_VALUE < ch ) return false; return true; } boolean text_is_letters() { if ( text.equals("") ) return false; for ( char ch : text.toCharArray() ) if ( ch != ' ' && !is_nonspecial_letter(ch) ) return false; return true; } boolean text_is_uppercase_letters() { /* if ( !text_is_letters() ) return false; */ if ( text.equals("") ) return false; for ( char ch : text.toCharArray() ) if ( ch != ' ' && !(is_nonspecial_letter(ch) && Character.isUpperCase(ch)) ) return false; return true; } // I'm tempted to make this an old-fashioned public-data record class. // In that case, I'd probably dispense with |context_limit| and have // |get_limit()| return |context_begin + text.length()|. private final Specifier specifier; private final String text; private int context_begin, context_limit; void set_context(int begin_given) { context_begin = begin_given; context_limit = context_begin + text.length(); } Symbol(Specifier specifier_given, String text0, int begin_given) { specifier = specifier_given; /* if ( text0 == null ) throw new IllegalArgumentException("Symbol(null text)"); */ text = text0; set_context(begin_given); } Symbol(Specifier specifier_given, String text0) { this(specifier_given, text0, -1); } /* Symbol(Specifier specifier_given, int begin_given) { this( specifier_given, //spec_String_map.get(specifier_given), null, begin_given ); } Symbol(Specifier specifier_given) { this(specifier_given, -1); } */ Symbol(int val_given) { this(Specifier.INT, Integer.toString(val_given)); } public String get_text() { return text; } Specifier get_specifier() { return specifier; } public int get_begin() { return context_begin; } public int get_limit() { return context_limit; } //void replace_text(String text_given) { text = text_given; } public void context_shift(int increment) { context_begin += increment; context_limit += increment; } /* private static EnumSet text_form_specifiers = EnumSet.of(Specifier.IDENTIFIER, Specifier.INT); */ public boolean equivalent_form(Grammar_Construct other_gc) { // Consider checking class of |other_gc| // and if necessary throwing |IllegalArgumentException|. Symbol other = (Symbol) other_gc; return specifier.equals(other.specifier) /* && (!text_form_specifiers.contains(specifier) || text.equals(other.text) ) */ && (specifier != Specifier.IDENTIFIER && specifier != Specifier.INT || text.equals(other.text) ) ; } /* static final EnumSet quantifiers_set = EnumSet.of(Specifier.FORALL, Specifier.EXISTS); static final EnumSet relations_set = EnumSet.range(Specifier.EQUALS, Specifier.DIVIDES); static final EnumSet infix_set = EnumSet.range(Specifier.EQUIV, Specifier.EXP); // |Expression.simplify()| relies upon // right-associativity of |COMMA| static { infix_set.add(Specifier.QUANT_SEP); infix_set.add(Specifier.SUBST); } static final EnumSet postfix_set = EnumSet.range(Specifier.FACTORIAL, Specifier.APOSTROPHE); ?REVERSED? boolean is_quantifier() { return quantifiers_set.contains(specifier); } boolean is_relation() { return relations_set.contains(specifier); } boolean is_binary_infix() { return infix_set.contains(specifier); } boolean is_unary_postfix() { return postfix_set.contains(specifier); } */ private char closing_delimiter_for_one_char_opening_delim() { assert specifier.equals(Specifier.OPENING_DELIMITER); assert text.length() <= 1; if ( text.length() == 0 ) // PMOD trans/phantom opening delimiter return ')'; switch ( text.charAt(0) ) { case '(': return ')'; case '[': return ']'; case '{': return '}'; case '|': return '|'; case Symbol.LCEIL_UNICODE: return Symbol.RCEIL_UNICODE; case Symbol.LEFT_UPPER_CORNER_UNICODE: return Symbol.RIGHT_UPPER_CORNER_UNICODE; case Symbol.LFLOOR_UNICODE: return Symbol.RFLOOR_UNICODE; case Symbol.LEFT_LOWER_CORNER_UNICODE: return Symbol.RIGHT_LOWER_CORNER_UNICODE; } throw new IllegalStateException(text); } boolean matching_delimiter(Symbol proposed_closing_delim) { assert specifier.equals(Specifier.OPENING_DELIMITER) : "specifier.equals(Specifier.OPENING_DELIMITER)"; if ( proposed_closing_delim.specifier != Specifier.CLOSING_DELIMITER ) return false; if ( text.equalsIgnoreCase("IF") ) return proposed_closing_delim.text.equals("") || proposed_closing_delim.text.equals(","); return proposed_closing_delim.text.length() == 1 && proposed_closing_delim.text.charAt(0) == closing_delimiter_for_one_char_opening_delim(); } boolean is_quantifier() { return specifier.equals(Specifier.FORALL) || specifier.equals(Specifier.EXISTS) ; } boolean is_relation() { return Specifier.SUCH_THAT.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.COMMA) <= 0; } static boolean is_transitive_numeric_comparator(Specifier specifier) { return // EQUALS_DEF specifier != null && specifier != Specifier.NEQ && Specifier.EQUALS.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.GREATER_THAN) <= 0; // CONSIDER |DIVIDES| } boolean is_transitive_numeric_comparator() { return is_transitive_numeric_comparator(specifier); } boolean is_numeric_comparator() { return is_transitive_numeric_comparator(specifier) || specifier.equals(Specifier.NEQ) || specifier.equals(Specifier.DIVIDES); } static boolean is_basic_transitive_comparator(Specifier specifier) { return specifier == Specifier.EQUIV || is_transitive_numeric_comparator(specifier); } boolean is_basic_transitive_comparator() { return is_basic_transitive_comparator(specifier); } static Specifier reverse_numeric_comparator(Specifier specifier) { switch ( specifier ) { case LEQ: return Specifier.GEQ; case GEQ: return Specifier.LEQ; case LESS_THAN: return Specifier.GREATER_THAN; case GREATER_THAN: return Specifier.LESS_THAN; case EQUALS: /* case EQUALS_DEF: */ case EQUIV: case CONGRUENT: case NEQ: case DIVIDES: return specifier; /* case BECOMES: return Specifier.EQUALS; */ default: // throw new IllegalArgumentException(...); return null; } } Specifier reverse_numeric_comparator() { return reverse_numeric_comparator(specifier); } // The point here is to handle symbols used with and without // negating strikes through them. Specifier specifier_negate() { switch ( specifier ) { /* case LEQ: return Specifier.GREATER_THAN; case GEQ: return Specifier.LESS_THAN; case LESS_THAN: return Specifier.GEQ; case GREATER_THAN: return Specifier.LEQ; */ case EQUALS: return Specifier.NEQ; case IS_IN: return Specifier.NOT_IN; default: return null; // throw new IllegalArgumentException(...); } } Specifier specifier_unnegate() { switch ( specifier ) { /* case LEQ: return Specifier.GREATER_THAN; case GEQ: return Specifier.LESS_THAN; case LESS_THAN: return Specifier.GEQ; case GREATER_THAN: return Specifier.LEQ; */ case NEQ: return Specifier.EQUALS; case NOT_IN: return Specifier.IS_IN; default: return null; // throw new IllegalArgumentException(...); } } static int sign_of_basic_transitive_comparator( Specifier basic_transitive_comparator_spec ) { assert is_basic_transitive_comparator(basic_transitive_comparator_spec) : "is_basic_transitive_comparator(basic_transitive_comparator_spec)"; switch ( basic_transitive_comparator_spec ) { case EQUIV: case EQUALS: /* case EQUALS_DEF: case BECOMES: */ return 0; case LEQ: case LESS_THAN: return -1; case GEQ: case GREATER_THAN: return 1; /* default: return __?__; */ } throw new IllegalArgumentException( "argument " + basic_transitive_comparator_spec ); } static boolean basic_transitive_comparator_applicable_to( Specifier basic_transitive_comparator_spec, // The following old comment is wrong: // the code here does handle cases // when |other_spec| is a comparator. // But I don't remember what's up // regarding equiv. Specifier other_spec, // can be neither equiv. nor comparison // --- maybe even |null| int substrate_polarity ) { assert is_basic_transitive_comparator(basic_transitive_comparator_spec) : "is_basic_transitive_comparator(basic_transitive_comparator_spec)"; switch ( basic_transitive_comparator_spec ) { case EQUIV: case EQUALS: /* case EQUALS_DEF: case BECOMES: */ return true; case LEQ: case LESS_THAN: case GEQ: case GREATER_THAN: return sign_of_basic_transitive_comparator( basic_transitive_comparator_spec ) * sign_of_basic_transitive_comparator(other_spec) == substrate_polarity; default: // ? what else is there ? return false; } } static boolean comparator_is_strong(Specifier specifier) { return specifier == Specifier.LESS_THAN || specifier == Specifier.GREATER_THAN; } static Specifier comparator_strengthen(Specifier specifier) { switch ( specifier ) { case LEQ: return Specifier.LESS_THAN; case GEQ: return Specifier.GREATER_THAN; default: return specifier; } } static Specifier comparator_weaken(Specifier specifier) { switch ( specifier ) { case LESS_THAN: return Specifier.LEQ; case GREATER_THAN: return Specifier.GEQ; default: return specifier; } } boolean is_binary_infix() { return Specifier.EQUIV.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.EXP) <= 0 || specifier.equals(Specifier.QUANT_SEP) || specifier.equals(Specifier.SUBST) || specifier.equals(Specifier.BREAK); } boolean is_unary_postfix() { return specifier == Specifier.CLOSING_DELIMITER || Specifier.PRIME.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.COMPLEMENT_POST) <= 0; } /* static final EnumSet always_arguments_set = EnumSet.complementOf( EnumSet.of( Specifier.IDENTIFIER, Specifier.INT, Specifier.TRUE, Specifier.FALSE ) ); */ boolean taking_arguments() { return /* always_arguments_set.contains(specifier) */ specifier.compareTo(Specifier.IDENTIFIER) < 0; } // REALLY NEED TO CHANGE TO HAVE A GENERALLY INVISIBLE // OPERATOR |ID_APPLICATION| AS WITH UNICODE's |FUNCTION_APPLICATION| boolean taking_arguments(Symbol following) { return taking_arguments() || specifier.equals(Specifier.IDENTIFIER) && following != null // ~~kludge && following.specifier.equals(Specifier.OPENING_DELIMITER) && following.text.equals("(") ; } boolean is_unary_prefix() { return !is_binary_infix() && !is_unary_postfix(); // Not |&& taking_arguments()|: // see |Expression.Expression()| and |Expression.gen_text()| } /* private static EnumSet right_associative_specifiers = EnumSet.of(Specifier.EXP, Specifier.QUANT_SEP, Specifier.IMPLIES, Specifier.COMMA ); // this is somewhat arbitrary */ private boolean is_right_associative() { /* return right_associative_specifiers.contains(specifier); */ return specifier.equals(Specifier.EXP) || specifier.equals(Specifier.QUANT_SEP) || specifier.equals(Specifier.IMPLIES) || specifier.equals(Specifier.COMMA) || specifier.equals(Specifier.TIMES) // Right-associativity for TIMES seemed nice // for algebraic manipulations as in the // proof that a sum of squares yields n(n+1)(2n+1)/6. || specifier.equals(Specifier.BREAK) || is_unary_prefix() // ? ; } // NEED TO CHANGE TO USE AN |EnumSet| boolean spec_boolean() { return Specifier.EQUIV.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.AND) <= 0 || Specifier.IS.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.COMMA) < 0 || specifier.equals(Specifier.NOT) || specifier.equals(Specifier.QUANT_SEP) || specifier.equals(Specifier.TRUE) || specifier.equals(Specifier.FALSE); } // NEED TO CHANGE TO USE AN |EnumSet| // users of this method need to handle |PRIME| specially // when using apostrophe/prime for not public static boolean spec_domainval(Specifier specifier) { return Specifier.COMMA.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.LOG_) <= 0 //|| specifier.equals(Specifier.COMPLEMENT_PRE) || specifier.equals(Specifier.COMPLEMENT_POST) || specifier.equals(Specifier.INFINITY) || specifier.equals(Specifier.EMPTYSET) || specifier.equals(Specifier.INT); } boolean spec_domainval() { return spec_domainval(specifier); } /* // NEED TO CHANGE TO USE AN |EnumSet| boolean is_arithmetic() { return specifier.equals(Specifier.PLUS) || specifier.equals(Specifier.MINUS) || specifier.equals(Specifier.TIMES) || specifier.equals(Specifier.QUOTIENT) || specifier.equals(Specifier.NEGATIVE); } */ boolean spec_id_arg_boolean() { return Specifier.EQUIV.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.AND) <= 0 || specifier.equals(Specifier.NOT) || specifier.equals(Specifier.QUANT_SEP) /* || specifier.equals(Specifier.TRUE) || specifier.equals(Specifier.FALSE) */ ; } boolean spec_id_arg_domainval() { return specifier.equals(Specifier.COMMA) || Specifier.IS.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.LOG_) <= 0 /* || specifier.equals(Specifier.IDENTIFIER) || specifier.equals(Specifier.INT) */ ; } /* private static EnumSet precedence_PM_specifiers = EnumSet.of(Specifier.PLUS, Specifier.MINUS); private static EnumSet precedence_TD_specifiers = EnumSet.of(Specifier.TIMES, Specifier.QUOTIENT); */ // Rem. as indicated in dragon book ("Compilers" by Aho, Sethi, & Ullman) // re operator-precedence parsing, // 'gerrymandering' (OK, carefully arranging dual values for) // precedence values/checking also handles associativity. // Logically, the name "...precedence_weaker..." was fine // and avoided a "!" where this is used, // but thinking about it always gave me ~~headaches. boolean stack_precedence_stronger_than( Symbol other, HashSet binary_infix_ops_weakened ) { /* return !(precendence_PM_specifiers.contains(specifier) && precendence_PM_specifiers.contains(other.specifier) || precedence_TD_specifiers.contains(specifier) && precedence_TD_specifiers.contains(other.specifier) ) */ if ( other.specifier.equals(Specifier.OPENING_DELIMITER) || is_quantifier() && other.is_relation() ) return false; if ( specifier == Specifier.IDENTIFIER // Function application has strongest precedence // as in programming languages (C,Java,...). // But note need the clause for OPENING_DELIMITER // to precede this. || other.specifier == Specifier.CLOSING_DELIMITER ) return true; if ( other.is_unary_postfix() ) return false; if ( is_binary_infix() && other.is_binary_infix() && ((binary_infix_ops_weakened.contains(this) || specifier == Specifier.BREAK ) ^ (binary_infix_ops_weakened.contains(other) || other.specifier == Specifier.BREAK ) ) ) return binary_infix_ops_weakened.contains(other) || other.specifier == Specifier.BREAK; if ( specifier == Specifier.PLUS && other.specifier == Specifier.MINUS || specifier == Specifier.MINUS && other.specifier == Specifier.PLUS /* I'm choosing not to have equal precedences * for TIMES and QUOTIENT considering expressions * such as a/bc , i.e. a/b*c . Remember: "Some of the operators have the wrong precedence." *The C Programming Language*, by Brian W. Kernighan and Dennis M. Ritchie, i.e. the source(s) of C/C++/Java. || specifier == Specifier.TIMES && other.specifier == Specifier.QUOTIENT || specifier == Specifier.QUOTIENT && other.specifier == Specifier.TIMES */ ) return true; // equal precedences but left associativity return !(specifier.compareTo(other.specifier) < 0 || specifier.equals(other.specifier) // it happens to be the case that the // only symbols that are right associative // don't have precedences equal to // any other Symbols && is_right_associative() ); } /* static class user_defined extends Symbol { private final Specifier specifier; // EXPECT NEED TO OVERRIDE THE FOLLOWING, // PROBABLY INVOLVING FIELDS TO BE HERE boolean is_prefix() { ... } boolean is_right_associative() { ... } boolean precedence_weaker_than(Symbol other) { ... } } */ // Rem. need to check for long symbols before short ones // which may be prefixes. // FUTURE: // * set Symbols // * Greek letters (for sets) // * double-struck capitals for standard sets (N, Z, Q, R, C) // * HTML character entity references e.g. "∅", "∃", "⇒" // * summation, 'production' (;-) // * square root // * more negated Symbols such as does-not-divide, not-an-element-of // * bitwise Symbols static boolean is_nonspecial_letter(char ch) { return Character.isLetter(ch) && LETTERS_SPECIAL.indexOf(ch) == -1 // kludge until properly handle subscripts || ch == SUBSCRIPT_1_UNICODE || ch == SUBSCRIPT_2_UNICODE || ch == SUBSCRIPT_3_UNICODE; } static int get_limit_eol_delim_comment_mark( // Symbol prev_symbol, boolean preceding_whitespace_delim_newline_or_nothing, String text ) { if ( text.charAt(0) == '(' /* && (prev_symbol == null || prev_symbol.specifier == Specifier.BREAK ) */ && preceding_whitespace_delim_newline_or_nothing ) { int end_numref = text.indexOf(')', 2); // 2: not accepting // "()" here for ( int i = 1; i < end_numref; i++ ) if ( !Character.isDigit(text.charAt(i)) ) end_numref = -1; if ( end_numref != -1 ) return end_numref + 1; } for ( String eol_delim_comment_start : EOL_DELIMITED_COMMENT_STARTS ) if ( text.startsWith(eol_delim_comment_start) ) return eol_delim_comment_start.length(); return -1; } String get_comment_content() { /* Currently (like things in C) returning |null| in bad cases. * May throw |IndexOutOfBoundsException| for a left parenthesis. if ( specifier != Specifier.COMMENT ) throw new IllegalArgumentException(); // or something */ if ( text.charAt(0) == NAME_COMMENT_START ) return text; String result_ = null; if ( text.charAt(0) == '(' ) result_ = text.substring(text.indexOf(')', 2) + 1); else if ( text.charAt(0) == '#' ) result_ = text.substring(1); else if ( text.startsWith(INLINE_COMMENT_START) ) result_ = text.substring( INLINE_COMMENT_START.length(), text.indexOf( INLINE_COMMENT_END, INLINE_COMMENT_START.length() ) ); else if ( text.charAt(0) == '/' ) result_ = text.substring(2); else if ( text.startsWith(INLINE_COMMENT_START) ) result_ = text.substring( INLINE_COMMENT_START.length(), text.indexOf( INLINE_COMMENT_END, INLINE_COMMENT_START.length() ) ); return result_.trim(); } // try to construct a |Symbol| from a prefix(!) of the text // starting at |begin_given|: Symbol(String context, int begin_given, Symbol prev_symbol) { /* final char preceding_ch = input_position == 0 ? '\0' : text0.charAt(input_position - 1), assert text0 != null : "text0 != null"; */ String text0 = context.substring(begin_given); assert !text0.equals("") : "!text0.equals(\"\")"; /* assert !Character.isWhitespace(text0.charAt(0)) : "!Character.isWhitespace(text0.charAt(0))"; */ // DOCUMENTATION: // interpretation of '-' is as follows, depending on // what's around it: // * space following ==> binary minus // * otherwise, there should be material immed. following // - then material immediately preceding ==> binary minus // - otherwise, there should be space immed. preceding // @ then digits following ==> negative int // @ otherwise ==> unary negative int i; for ( i = begin_given - 1; i >= 0 && Character.isWhitespace(context.charAt(i)) && context.charAt(i) != '\n'; i-- ) ; boolean preceding_whitespace_delim_newline_or_nothing = i < 0 || context.charAt(i) == '\n'; // I'd like the capability as in C++ to declare a variable in the // head of an |if| int limit_eol_delim_comment_mark; if ( (limit_eol_delim_comment_mark = get_limit_eol_delim_comment_mark( preceding_whitespace_delim_newline_or_nothing, text0 ) ) != -1 ) { specifier = Specifier.COMMENT; int end = text0.indexOf('\n', limit_eol_delim_comment_mark); int unused_index = text0.indexOf(UNUSED_NOTE, limit_eol_delim_comment_mark); if ( unused_index != -1 && unused_index < end || end == -1 ) end = unused_index - 1; // actually maybe |end == -1| should raise a flag here // (or maybe raise an eyebrow? ;-) // since my intention is for a comment to precede // the expression that it describes /* |Expressions_Mgmt.parse()| expects |Symbol()| to return * text with length corresponding to amount of input consumed. * See |get_comment_content()|. text = text0.substring(limit_eol_delim_comment_mark, end).trim(); //+ (end == -1 ? "\n" : ""); */ text = end == -1 ? text0 : text0.substring(0, end + 1); } else if ( text0.startsWith(INLINE_COMMENT_START) ) { int start_of_end = text0.indexOf( INLINE_COMMENT_END, INLINE_COMMENT_START.length() ); if ( start_of_end == -1 ) throw new IllegalArgumentException( /* fmt_illargexc_msg( begin_given, begin_given + INLINE_COMMENT_START.length(), "following indicated name-comment start," + " didn't find end \"" + INLINE_COMMENT_END + "\"." ) */ "following the indicated comment start \"" + INLINE_COMMENT_START + "\", didn't find comment end \"" + INLINE_COMMENT_END + "\" in the line." ); specifier = Specifier.COMMENT; int end = start_of_end + INLINE_COMMENT_END.length(); /* while ( end < text0.length() && Character.isWhitespace(text0.charAt(end)) ) end++; */ text = text0.substring(0, end); } else if ( text0.startsWith(String.valueOf(NAME_COMMENT_START)) ) { int length_of_end = String.valueOf(NAME_COMMENT_END).length(); int start_of_end = text0.indexOf(NAME_COMMENT_END, length_of_end); if ( start_of_end == -1 ) throw new IllegalArgumentException( /* fmt_illargexc_msg( begin_given, begin_given + INLINE_COMMENT_START.length(), "following indicated name-comment start," + " didn't find end \"" + INLINE_COMMENT_END + "\"." ) */ "following the indicated comment start '" + NAME_COMMENT_START + "', didn't find comment end '" + NAME_COMMENT_END + "' in the line." ); specifier = Specifier.COMMENT; int end = start_of_end + length_of_end; /* while ( end < text0.length() && Character.isWhitespace(text0.charAt(end)) ) end++; */ text = text0.substring(0, end); } else if ( (text0.startsWith("IF AND ONLY IF") || text0.startsWith("if and only if") ) /* && */ ) { specifier = Specifier.EQUIV; text = text0.substring(0, "IF AND ONLY IF".length()); } // Character.isUnicodeIdentifierStart(text0.charAt(0) else if ( is_nonspecial_letter(text0.charAt(0)) || Character.isDigit(text0.charAt(0)) || text0.charAt(0) == '-' && text0.length() > 1 && Character.isDigit(text0.charAt(1)) /* && (begin_given == 0 || Character.isWhitespace( context.charAt(begin_given - 1) ) ) */ // SHOULD HANDLE THIS // IN |Expressions_Mgmt.parse()| // PROBABLY IN POST-LEXING PROCESSING // OF SYMBOLS && (prev_symbol == null || prev_symbol.taking_arguments() && !prev_symbol.is_unary_postfix() ) ) { int local_limit = 1; while ( local_limit < text0.length() && (is_nonspecial_letter(text0.charAt(0)) // Character.isUnicodeIdentifierPart( ? (Character.isJavaIdentifierPart( text0.charAt(local_limit) ) // kludge until properly handle subscripts || text0.charAt(local_limit) == SUBSCRIPT_1_UNICODE || text0.charAt(local_limit) == SUBSCRIPT_2_UNICODE || text0.charAt(local_limit) == SUBSCRIPT_3_UNICODE ) : Character.isDigit(text0.charAt(local_limit)) ) ) local_limit++; text = text0.substring(0, local_limit); // Character.isUnicodeIdentifierStart(text0.charAt(0)) if ( is_nonspecial_letter(text0.charAt(0)) ) { Specifier spec_buf = null; // needed to use |spec_buf| // to convince Java // that |specifier| was assigned to // only once, exclusively either in the // |try| block or exclusively // in the |catch| block try { spec_buf = Specifier.valueOf(text.toUpperCase()); /* // kludge: switch ( spec_buf ) { case C: case R: case Q: case Z: case N: throw new IllegalArgumentException(); } */ /* if ( text.equals(text.toUpperCase()) ) user_uppercase++; else user_lowercase++; */ if ( !spec_usable_by_name.contains(spec_buf) ) // Should I not use |IllegalArgumentException| // as part of the processing? throw new IllegalArgumentException(); } // Should I not use |IllegalArgumentException| // as part of the processing? catch ( IllegalArgumentException e ) { if ( spec_buf != null && text.equals(spec_buf.name()) && is_reserved(text) ) // Should I not use |IllegalArgumentException| // as part of the processing? throw new IllegalArgumentException( /* fmt_illargexc_msg( begin_given, begin_given + text.length(), "You need to use a different identifier." + "\nThis one is reserved for internal use here." ) */ "You need to use a different identifier." + "\n\"" + text + "\" is reserved for internal use here." ); // Next ~~identifiers that are special, |else IDENTIFIER|: if ( text.equals("mod") ) spec_buf = Specifier.BMOD; else if ( text.equalsIgnoreCase("IFF") ) { spec_buf = Specifier.EQUIV; /* if ( text.equals(text.toUpperCase()) ) user_uppercase++; else user_lowercase++; */ } else if ( text.equalsIgnoreCase("MEANS") ) { spec_buf = Specifier.EQUIV; /* if ( text.equals(text.toUpperCase()) ) user_uppercase++; else user_lowercase++; */ } else if ( text.equalsIgnoreCase("IF") ) { spec_buf = Specifier.OPENING_DELIMITER; /* if ( text.equals(text.toUpperCase()) ) user_uppercase++; else user_lowercase++; */ } else if ( text.equalsIgnoreCase("THEN") ) { spec_buf = Specifier.IMPLIES; /* if ( text.equals(text.toUpperCase()) ) user_uppercase++; else user_lowercase++; */ } else if ( text.equals("V") ) spec_buf = Specifier.OR; /* else if ( text.equals("A") ) // FUTURE // may need to allow // for constant // capital "A" // (for sets); // should // try to ascertain // which is intended // considering // context { spec_buf = Specifier.FORALL; user_spec_String(Specifier.EXISTS, "E"); } */ /* else if ( text.equalsIgnoreCase("FORSOME") // || text.equals("E") ) { user_spec_String(spec_buf = Specifier.EXISTS, text); // if ( text.equals("E") ) // user_spec_String(Specifier.FORALL, "A"); // else if ( text.equals("forsome") ) { user_spec_String(Specifier.FORALL, "forall"); user_uppercase++; } else { user_spec_String(Specifier.FORALL, "FORALL"); user_lowercase++; } } */ else spec_buf = Specifier.IDENTIFIER; // |Expressions_Mgmt.parse()| may split this // identifier into others it has recorded. // This class doesn't maintain such a record // because that would be beyond any one |Symbol|. // (An earlier version of this code had such a record // statically, but that wasn't good considering issues // such as saving proofs.) } //user_spec_String(specifier = spec_buf, text); specifier = spec_buf; } else { specifier = Specifier.INT; /* try { Integer.parseInt(text); } catch ( NumberFormatException e ) { // Should I not use |IllegalArgumentException| // as part of the processing? throw new IllegalArgumentException( fmt_illargexc_msg( begin_given, (begin_given + text.length()), "typed integer's magnitude exceeds this" + "\nsystem's capabilities for handling such" ) ); } */ //Integer.parseInt(text); } /* if ( specifier == null ) throw new IllegalStateException( begin_given + ERR_POSNS_SEP + (begin_given + 1) + ERR_POSNS_SEP + "failed to determine specifier for symbol" ); */ assert specifier != null : "specifier != null"; } else if ( text0.charAt(0) == SUPERSCRIPT_MINUS_UNICODE ? text0.length() > 1 && is_superscript(text0.charAt(1)) /* && (begin_given == 0 || Character.isWhitespace( context.charAt(begin_given - 1) ) ) */ // SHOULD HANDLE THIS // IN |Expressions_Mgmt.parse()| // PROBABLY IN POST-LEXING PROCESSING // OF SYMBOLS && (prev_symbol == null || prev_symbol.taking_arguments() && !prev_symbol.is_unary_postfix() ) : is_superscript(text0.charAt(0)) ) { int local_limit = 1; while ( local_limit < text0.length() && is_superscript(text0.charAt(local_limit)) ) local_limit++; text = text0.substring(0, local_limit); specifier = Specifier.INT; /* try { Integer.parseInt(text); } catch ( NumberFormatException e ) { throw new IllegalArgumentException( fmt_illargexc_msg( begin_given, (begin_given + text.length()), "typed integer's magnitude exceeds this" + "\nsystem's capabilities for handling such" ) ); } */ //Integer.parseInt(text); } else if ( text0.startsWith("(mod ") ) /* { user_spec_String( specifier = Specifier.PMOD, text = PMOD_ ); user_ascii++; } */ { specifier = Specifier.PMOD; text = PMOD_; } else if ( text0.startsWith(ARROW_LEFT_RIGHT_TWO_BARS_ASCII) ) /* { user_spec_String( specifier = Specifier.EQUIV, text = ARROW_LEFT_RIGHT_TWO_BARS_ASCII ); user_ascii++; } */ { specifier = Specifier.EQUIV; text = ARROW_LEFT_RIGHT_TWO_BARS_ASCII; } else if ( text0.startsWith(ARROW_LEFT_RIGHT_ONE_BAR_ASCII) ) { /* user_spec_String( specifier = Specifier.EQUIV, text = ARROW_LEFT_RIGHT_ONE_BAR_ASCII ); user_ascii++; */ specifier = Specifier.EQUIV; text = ARROW_LEFT_RIGHT_ONE_BAR_ASCII; } else if ( text0.startsWith(ARROW_RIGHT_TWO_BARS_ASCII) ) { /* user_spec_String( specifier = Specifier.IMPLIES, text = ARROW_RIGHT_TWO_BARS_ASCII ); user_ascii++; */ specifier = Specifier.IMPLIES; text = ARROW_RIGHT_TWO_BARS_ASCII; } else if ( text0.startsWith(ARROW_RIGHT_ONE_BAR_ASCII) ) { /* user_spec_String( specifier = Specifier.IMPLIES, text = ARROW_RIGHT_ONE_BAR_ASCII ); user_ascii++; */ specifier = Specifier.IMPLIES; text = ARROW_RIGHT_ONE_BAR_ASCII; } else if ( text0.startsWith(ARROW_RIGHT_ONE_BAR_ASCII_) ) { /* user_spec_String( specifier = Specifier.IMPLIES, text = ARROW_RIGHT_ONE_BAR_ASCII_ ); user_ascii++; */ specifier = Specifier.IMPLIES; text = ARROW_RIGHT_ONE_BAR_ASCII_; } else if ( text0.startsWith(ARROW_RIGHT_TWO_BARS_ASCII_) ) { /* user_spec_String( specifier = Specifier.IMPLIES, text = ARROW_RIGHT_TWO_BARS_ASCII_ ); user_ascii++; */ specifier = Specifier.IMPLIES; text = ARROW_RIGHT_TWO_BARS_ASCII_; } else if ( text0.startsWith(OR_ASCII) ) { /* user_spec_String(specifier = Specifier.OR, text = OR_ASCII); user_ascii++; */ specifier = Specifier.OR; text = OR_ASCII; } else if ( text0.startsWith(OR_PROG2_ASCII) ) { specifier = Specifier.OR; text = OR_PROG2_ASCII; //user_ascii++; } else if ( text0.startsWith(AND_ASCII) ) { /* user_spec_String(specifier = Specifier.AND, text = AND_ASCII); user_ascii++; */ specifier = Specifier.AND; text = AND_ASCII; } else if ( text0.startsWith(AND_PROG2_ASCII) ) { specifier = Specifier.AND; text = AND_PROG2_ASCII; /* user_ascii++; */ } else if ( text0.startsWith(EQUALS_PROG_ASCII) ) { specifier = Specifier.EQUALS; text = EQUALS_PROG_ASCII; //user_ascii++; } else if ( text0.startsWith(COLON_EQUALS_ASCII) ) { /* user_spec_String( specifier = Specifier.BECOMES, text = COLON_EQUALS_ASCII ); //user_ascii++; */ specifier = Specifier.EQUALS; text = COLON_EQUALS_ASCII; } else if ( text0.startsWith(ARROW_LEFT_ONE_BAR_ASCII) ) { /* user_spec_String( specifier = Specifier.BECOMES, text = ARROW_LEFT_ONE_BAR_ASCII ); //user_ascii++; */ specifier = Specifier.EQUALS; text = ARROW_LEFT_ONE_BAR_ASCII; } else if ( text0.startsWith(NEQ_ASCII) ) { /* user_spec_String(specifier = Specifier.NEQ, text = NEQ_ASCII); user_ascii++; */ specifier = Specifier.NEQ; text = NEQ_ASCII; } else if ( text0.startsWith(LEQ_PROG_ASCII) ) { /* user_spec_String(specifier = Specifier.LEQ, text = LEQ_PROG_ASCII); user_ascii++; */ specifier = Specifier.LEQ; text = LEQ_PROG_ASCII; } else if ( text0.startsWith(GEQ_PROG_ASCII) ) { /* user_spec_String(specifier = Specifier.GEQ, text = GEQ_PROG_ASCII); user_ascii++; */ specifier = Specifier.GEQ; text = GEQ_PROG_ASCII; } else if ( text0.startsWith(EMPTYSET_BRACES) ) { /* user_spec_String(specifier = Specifier.EMPTYSET, text = EMPTYSET_BRACES); */ specifier = Specifier.EMPTYSET; text = EMPTYSET_BRACES; } else { // check for single-character Symbols: switch ( text0.charAt(0) ) { case '\n': specifier = Specifier.BREAK; break; case ')': case ']': case '}': case RCEIL_UNICODE: case RIGHT_UPPER_CORNER_UNICODE: case RFLOOR_UNICODE: case RIGHT_LOWER_CORNER_UNICODE: specifier = Specifier.CLOSING_DELIMITER; break; case '(': case '[': case '{': case LCEIL_UNICODE: case LEFT_UPPER_CORNER_UNICODE: case LFLOOR_UNICODE: case LEFT_LOWER_CORNER_UNICODE: specifier = Specifier.OPENING_DELIMITER; break; case SUM_UNICODE: specifier = Specifier.SUM; //user_unicode++; break; case PROD_UNICODE: specifier = Specifier.PROD; //user_unicode++; break; case THREE_BAR_UNICODE: case ARROW_LEFT_RIGHT_TWO_BARS_UNICODE: case ARROW_LEFT_RIGHT_ONE_BAR_UNICODE: /* user_spec_String( specifier = Specifier.EQUIV, text0.substring(0,1) ); user_unicode++; */ specifier = Specifier.EQUIV; break; case ARROW_RIGHT_TWO_BARS_UNICODE: case ARROW_RIGHT_ONE_BAR_UNICODE: case IMPLIES_U_COUNTERCLOCKWISE_UNICODE: /* user_spec_String( specifier = Specifier.IMPLIES, text0.substring(0,1) ); user_unicode++; */ specifier = Specifier.IMPLIES; break; //case OR_PROG1_ASCII: // DIVIDES case OR_UNICODE: case OR_NARY_UNICODE: /* user_spec_String( specifier = Specifier.OR, text0.substring(0,1) ); user_unicode++; */ specifier = Specifier.OR; break; case AND_PROG1_ASCII: case AND_UNICODE: case AND_NARY_UNICODE: /* user_spec_String( specifier = Specifier.AND, text0.substring(0,1) ); if ( text0.charAt(0) != AND_PROG1_ASCII ) user_unicode++; */ specifier = Specifier.AND; break; case '.': // as in Jape. // (I thought of this independently. // Some logic book (for which I don't // remember the specifics of title, author) // used it as a general delimiter.) case THIN_SPACE_UNICODE: //user_spec_String(specifier = Specifier.QUANT_SEP, "."); specifier = Specifier.QUANT_SEP; break; case '@': case TRIANGLE_FILLED_LEFT_POINTING_UNICODE: case TRIANGLE_FILLED_LEFT_POINTING_SMALL_UNICODE: case TRIANGLE_FILLED_LEFT_POINTING_NARROW_UNICODE: //user_spec_String(specifier = Specifier.SUBST, "@"); specifier = Specifier.SUBST; break; case COLON_EQUALS_UNICODE: case ARROW_LEFT_ONE_BAR_UNICODE: /* user_spec_String( specifier = Specifier.BECOMES, text0.substring(0,1) ); //user_unicode++; */ specifier = Specifier.EQUALS; break; case '=': specifier = Specifier.EQUALS; break; case CONGRUENT_UNICODE: specifier = Specifier.CONGRUENT; //user_unicode++; break; case NEQ_UNICODE: specifier = Specifier.NEQ; //user_unicode++; break; case LEQ_UNICODE: specifier = Specifier.LEQ; //user_unicode++; break; case GEQ_UNICODE: specifier = Specifier.GEQ; //user_unicode++; break; case '<': specifier = Specifier.LESS_THAN; break; case '>': specifier = Specifier.GREATER_THAN; break; case '|': case VERTICAL_LINE_UNICODE: /* user_spec_String( specifier = Specifier.DIVIDES, text0.substring(0,1) ); */ specifier = text0.length() < 2 ? Specifier.CLOSING_DELIMITER : begin_given == 0 ? Specifier.OPENING_DELIMITER : Character.isWhitespace(text0.charAt(1)) ? (Character.isWhitespace( context.charAt(begin_given - 1) ) ? Specifier.SUCH_THAT : Specifier.CLOSING_DELIMITER ) : Character.isWhitespace( context.charAt(begin_given - 1) ) || prev_symbol.taking_arguments() && !prev_symbol.is_unary_postfix() ? Specifier.OPENING_DELIMITER : Specifier.DIVIDES; break; case ',': specifier = Specifier.COMMA; break; case ':': specifier = Specifier.SUCH_THAT; break; /* case OMEGA_LOWERCASE_UNICODE: / * user_spec_String( specifier = Specifier.OMEGA_LOWERCASE, text0.substring(0,1) ); * / specifier = Specifier.OMEGA_LOWERCASE; break; case OMEGA_UPPERCASE_UNICODE: / * user_spec_String( specifier = Specifier.OMEGA_UPPERCASE, text0.substring(0,1) ); * / specifier = Specifier.OMEGA_UPPERCASE; break; case THETA_UPPERCASE_UNICODE: / * user_spec_String( specifier = Specifier.THETA_UPPERCASE, text0.substring(0,1) ); * / specifier = Specifier.THETA_UPPERCASE; break; */ case INFINITY_UNICODE: specifier = Specifier.INFINITY; //user_unicode++; break; case C_NUMBERS_UNICODE: /* user_spec_String( specifier = Specifier.C_NUMBERS, text0.substring(0,1) ); */ specifier = Specifier.C_NUMBERS; break; case R_NUMBERS_UNICODE: /* user_spec_String( specifier = Specifier.R_NUMBERS, text0.substring(0,1) ); */ specifier = Specifier.R_NUMBERS; break; case Q_NUMBERS_UNICODE: /* user_spec_String( specifier = Specifier.Q_NUMBERS, text0.substring(0,1) ); */ specifier = Specifier.Q_NUMBERS; break; case Z_NUMBERS_UNICODE: /* user_spec_String( specifier = Specifier.Z_NUMBERS, text0.substring(0,1) ); */ specifier = Specifier.Z_NUMBERS; break; case N_NUMBERS_UNICODE: /* user_spec_String( specifier = Specifier.N_NUMBERS, text0.substring(0,1) ); */ specifier = Specifier.N_NUMBERS; break; case EMPTYSET_UNICODE: /* user_spec_String( specifier = Specifier.EMPTYSET, text0.substring(0,1) ); */ specifier = Specifier.EMPTYSET; break; case IS_IN_UNICODE: /* user_spec_String( specifier = Specifier.IS_IN, text0.substring(0,1) ); */ specifier = Specifier.IS_IN; break; case NOT_IN_UNICODE: /* user_spec_String( specifier = Specifier.NOT_IN, text0.substring(0,1) ); */ specifier = Specifier.NOT_IN; break; case SUBSET_UNICODE: /* user_spec_String( specifier = Specifier.SUBSET, text0.substring(0,1) ); */ specifier = Specifier.SUBSET; break; case SUBSETEQ_UNICODE: /* user_spec_String( specifier = Specifier.SUBSETEQ, text0.substring(0,1) ); */ specifier = Specifier.SUBSETEQ; break; case UNION_UNICODE: /* user_spec_String( specifier = Specifier.UNION, text0.substring(0,1) ); */ specifier = Specifier.UNION; break; case INTERSECT_UNICODE: /* user_spec_String( specifier = Specifier.INTERSECT, text0.substring(0,1) ); */ specifier = Specifier.INTERSECT; break; case TIMES_X_UNICODE: specifier = Specifier.TIMES_X; break; case '+': specifier = Specifier.PLUS; break; // DOCUMENTATION: // interpretation of '-' is as follows, depending on // what's around it: // * space following ==> binary minus // * otherwise, there should be material immed. following // - then material immediately preceding ==> binary minus // - otherwise, there should be space immed. preceding // @ then digits following ==> negative int // @ otherwise ==> unary negative case '-': case MINUS_UNICODE: specifier = text0.length() > 1 && Character.isWhitespace(text0.charAt(1)) /* || begin_given > 0 && !Character.isWhitespace( context.charAt(begin_given - 1) ) */ || prev_symbol != null && (!prev_symbol.taking_arguments() || prev_symbol.is_unary_postfix() ) ? Specifier.MINUS : Specifier.NEGATIVE; break; case '%': specifier = Specifier.REMAINDER_CODE; break; case TIMES_ASCII: case TIMES_ASTERISK_UNICODE: case MIDDLE_DOT_UNICODE: case DOT_OPERATOR_UNICODE: /* user_spec_String( specifier = Specifier.TIMES, text0.substring(0,1) ); */ specifier = Specifier.TIMES; break; case '/': case DIVISION_SIGN_UNICODE: case DIVIDE_SLASH_UNICODE: /* user_spec_String( specifier = Specifier.QUOTIENT, text0.substring(0,1) ); */ specifier = Specifier.QUOTIENT; break; /* Need to catch like "mod", "iff" case GROUP_OP_ASCII: / * user_spec_String( specifier = Specifier.GROUP_OP, text0.substring(0,1) ); * / specifier = Specifier.GROUP_OP; break; */ case EXP_MCGUIRE_ASCII: case EXP_ASCII: /* user_spec_String( specifier = Specifier.EXP, text0.substring(0,1) ); */ specifier = Specifier.EXP; break; case '\'': case PRIME_UNICODE: specifier = Specifier.PRIME; break; case SCRIPT_CAPITAL_P_UNICODE: specifier = Specifier.POWERSET; break; case TILDE_ASCII: specifier = Specifier.TILDE; break; case SUPERSCRIPT_MINUS_UNICODE: specifier = Specifier.COMPLEMENT_POST; break; case '!': specifier = Specifier.FACTORIAL; break; //case NOT_PROG_ASCII: //case NOT_ASCII: case NOT_UNICODE: specifier = Specifier.NOT; break; case FORALL_UNICODE: /* user_spec_String( specifier = Specifier.FORALL, text0.substring(0,1) ); user_unicode++; */ specifier = Specifier.FORALL; break; case EXISTS_UNICODE: /* user_spec_String( specifier = Specifier.EXISTS, text0.substring(0,1) ); user_unicode++; */ specifier = Specifier.EXISTS; break; case TOP_UNICODE: /* user_spec_String( specifier = Specifier.TRUE, text0.substring(0,1) ); user_unicode++; */ specifier = Specifier.TRUE; break; case BOTTOM_UNICODE: /* user_spec_String( specifier = Specifier.FALSE, text0.substring(0,1) ); user_unicode++; */ specifier = Specifier.FALSE; break; default: throw new IllegalArgumentException( /* fmt_illargexc_msg( begin_given, begin_given, "failed to recognize symbol following cursor." ) */ "failed to recognize symbol following cursor." ); } text = text0.substring(0, 1); } /* return new Symbol( begin_given, specifier, text, begin_given + text.length() ); */ context_begin = begin_given; context_limit = begin_given + text.length(); } public Object clone() { Symbol result; try { result = (Symbol) super.clone(); } catch ( CloneNotSupportedException exception ) { throw new InternalError(exception.toString()); } // Regarding the thought of doing |specifier.clone()|, // documentation specifies that |clone()| is not applicable to |Enum|s. return result; } /* static String extract_name_from_comment(String name_comment_text) { boolean newline_at_end = name_comment_text.charAt(name_comment_text.length() - 1) == '\n'; return name_comment_text .substring( newline_at_end ? 1 : 2, newline_at_end ? name_comment_text.length() - 1 : name_comment_text.indexOf(INLINE_COMMENT_END) ) .trim(); } */ boolean arg1_group_worthwhile() { return specifier == Specifier.IDENTIFIER || Specifier.LN.compareTo(specifier) <= 0 && specifier.compareTo(Specifier.LOG_) <= 0; } }