diff --git a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key index 8a037c8ce28..318720c42ee 100644 --- a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key +++ b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed by the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0 */ \profile "Java Profile"; \settings { diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index f1a67a2afd5..c1e4ef7285c 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -1,4 +1,6 @@ - +/* This file is part of KeY - https://key-project.org + * KeY is licensed by the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0 */ lexer grammar JmlLexer; @header {} diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index a66965df0fd..fabf12a7870 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed by the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0 */ parser grammar JmlParser; options { tokenVocab=JmlLexer; } diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 1ef3866446a..3d8ee883535 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -72,6 +72,18 @@ lexer grammar KeYLexer; tokens {MODALITY} +// Comments have precedence over operators // and /*. +SL_COMMENT +: + '//' + (~('\n' | '\uFFFF'))* ('\n' | '\uFFFF' | EOF) -> channel(HIDDEN) +; +DOC_COMMENT: '/*!' -> more, pushMode(docComment); +ML_COMMENT: '/*' -> more, pushMode(COMMENT); + + + +DATATYPES:'\\datatypes'; SORTS:'\\sorts'; GENERIC : '\\generic'; PROXY : '\\proxy'; @@ -208,10 +220,13 @@ AVOID : '\\avoid'; PREDICATES : '\\predicates'; FUNCTIONS : '\\functions'; -DATATYPES : '\\datatypes'; +FREE : '\\free'; TRANSFORMERS : '\\transformers'; UNIQUE : '\\unique'; -FREE : '\\free'; +INFIX: '\\infix'; +PREFIX: '\\prefix'; +SHORTCUT:'\\shortcut'; +POSTFIX: '\\postfix'; RULES : '\\rules'; AXIOMS : '\\axioms'; @@ -236,181 +251,830 @@ CONTAINERTYPE : '\\containerType'; //SEQ : '\\seq'; //BIGINT : '\\bigint'; -// Unicode symbols for special functions/predicates -UTF_PRECEDES : '\u227A' /*≺*/ | '\\precedes'; -UTF_IN : '\u220A' /*∊*/ | '\\in'; -UTF_EMPTY : '\u2205' /*∅*/ | '\\emptyset'; -UTF_UNION : '\u222A' /*∪*/ | '\\cup'; -UTF_INTERSECT : '\u2229' /*∩*/ | '\\cap'; -UTF_SUBSET_EQ : '\u2286' /*⊆*/ | '\\subseteq'; -UTF_SUBSEQ : '\u2282' /*⊂*/ | '\\subset'; -UTF_SETMINUS : '\u2216' /*∖*/ | '\\setminus'; - fragment VOCAB : '\u0003'..'\u0377' ; -SEMI -: ';' - ; - -SLASH -: '/' - ; - -COLON: ':'; - -DOUBLECOLON -: '::' - ; - -ASSIGN -: ':=' - ; - -DOT -: '.' - ; - -DOTRANGE -: '.' '.' - ; - -COMMA -: ',' - ; - -LPAREN -: - '(' - ; - -RPAREN -: ')' - ; - -LBRACE -: '{' - ; - -RBRACE -: '}' - ; - -LBRACKET -: '[' - ; - -RBRACKET -: ']' - ; - -EMPTYBRACKETS -: '[' ']' - ; - -AT -: '@' - ; - -PARALLEL -: '|' '|' - ; - - -OR -: '|' | '\u2228' - ; - -AND -: '&' | '\u2227' - ; - -NOT -: '!' | '\u00AC' - ; +fragment OP_SFX: ('-'|'='|'+'|'*'|'/'|'&'|'.'|'|'|'^'|'!'|':'|'>'|'<'); + +RPAREN : ')'; +LPAREN : '('; +RBRACE : '}'; +LBRACE : '{'; +LBRACKET : '['; +RBRACKET : ']'; +PARALLEL : '||'; + +SEMI: ';'; +COLON: ':'; +DOUBLECOLON: '::'; +ASSIGN: ':=' | '\u2254' ;// (8788) ≔ COLON EQUALS +DOT: '.'; +DOTRANGE: '.' '.'; +DOT_WITH_MORE:'.' OP_SFX*; +COMMA: ','; + +SET_IN : '\u220A' /*∊*/ | '\\in'; +EMPTY : '\u2205' /*∅*/ | '\\emptyset'; +UNION : '\u222A' /*∪*/ | '\\cup'; //(8746) ∪ UNION Vereinigungsmengenzeichen +INTERSECT : '\u2229' /*∩*/ | '\\cap'; //(8745) ∩ INTERSECTION Schnittmengenzeichen +SUBSET : '\u2282' /*⊂*/ | '\\subset'; +SETMINUS : '\u2216' /*∖*/ | '\\setminus'; + +DOT_PLUS : '\u2214'; // ∔ +MINUS_OR_PLUS: '\u2213'; //∓ +ASTERISK: '\u2217';// ∗ +RING: '\u2218'; //∘ +CDOT: '\u2219';// ∙ +DIVIDES: '\u2223';// (8739) ∣ DIVIDES teilt +NOT_DIVIDES: '\u2224';// (8740) ∤ DOES NOT DIVIDE teilt nicht +PARALLEL_TO: '\u2225';//(8741) ∥ PARALLEL TO parallel zu +NOT_PARALLEL_TO: '\u2226' ;//(8742) ∦ NOT PARALLEL TO nicht parallel zu +THEREFORE: '\u2234' ;//(8756) ∴ THEREFORE folglich +BECAUSE: '\u2235' ;//(8757) ∵ BECAUSE weil +RATION: '\u2236' ;//(8758) ∶ RATIO Verhältniszeichen +PROPORTION: '\u2237' ;//(8759) ∷ PROPORTION Proportionszeichen +DOT_MINUS: '\u2238' ;//(8760) ∸ DOT MINUS Minuszeichen mit Punkt +EXCESS: '\u2239' ;//(8761) ∹ EXCESS Exzess +GEOMETRIC_PROPORTION: '\u223A' ;//(8762) ∺ GEOMETRIC PROPORTION geometrische Proportion +HOMOTHETIC: '\u223B' ;//(8763) ∻ HOMOTHETIC Homothetiezeichen +REVERSE_TILDE: '\u223D' ;//(8765) ∽ REVERSED TILDE umgekehrte Tilde +INVERTED_LAZY_S: '\u223E' ;//(8766) ∾ INVERTED LAZY S invertiertes stummes S +SINE_WAVE: '\u223F' ;//(8767) ∿ SINE WAVE Sinuswelle +WREATH_PRODUCT: '\u2240' ;//(8768) ≀ WREATH PRODUCT Kranzprodukt +NOT_TILDE:'\u2241' ;//(8769) ≁ NOT TILDE durchgestrichene Tilde +MINUS_TILDE: '\u2242' ;//(8770) ≂ MINUS TILDE Minus über Tilde +ASYMPTOTICALLY_EQUAL_TO: '\u2243' ;// (8771) ≃ ASYMPTOTICALLY EQUAL TO asymptotisch gleich +NOT_ASYMPTOTICALLY_EQUAL_TO: '\u2244' ;// (8772) ≄ NOT ASYMPTOTICALLY EQUAL TO nicht asymptotisch gleich + +/* MATH PLAN UNICODE +'\u2245' ;// (8773) ≅ APPROXIMATELY EQUAL TO ungefähr gleich +'\u2246' ;// (8774) ≆ APPROXIMATELY BUT NOT ACTUALLY EQUAL TO ungefähr, aber nicht genau gleich +'\u2247' ;// (8775) ≇ NEITHER APPROXIMATELY NOR ACTUALLY EQUAL TO weder ungefähr noch genau gleich +'\u2248' ;// (8776) ≈ ALMOST EQUAL TO fast gleich +'\u2249' ;// (8777) ≉ NOT ALMOST EQUAL TO nicht fast gleich +'\u224A' ;// (8778) ≊ ALMOST EQUAL OR EQUAL TO fast gleich oder gleich +'\u224B' ;// (8779) ≋ TRIPLE TILDE dreifache Tilde +'\u224C' ;// (8780) ≌ ALL EQUAL TO alles Gleich +'\u224D' ;// (8781) ≍ EQUIVALENT TO äquivalent +'\u224E' ;// (8782) ≎ GEOMETRICALLY EQUIVALENT TO geometrisch äquivalent +'\u224F' ;// (8783) ≏ DIFFERENCE BETWEEN Differenz zwischen +'\u2250' ;// (8784) ≐ APPROACHES THE LIMIT Grenzwertannäherung +'\u2251' ;// (8785) ≑ GEOMETRICALLY EQUAL TO geometrisch gleich +'\u2252' ;// (8786) ≒ APPROXIMATELY EQUAL TO OR THE IMAGE OF ungefähr gleich oder Bild von +'\u2253' ;// (8787) ≓ IMAGE OF OR APPROXIMATELY EQUAL TO Bild oder ungefähr gleich +'\u2254' ;// (8788) ≔ COLON EQUALS Gleichheitszeichen mit vorangestelltem Doppelpunkt' ;// (Definitionszeichen) +'\u2255' ;// (8789) ≕ EQUALS COLON Gleichheitszeichen mit nachfolgendem Doppelpunkt +'\u2256' ;// (8790) ≖ RING IN EQUAL TO Kreis im Gleichheitszeichen +'\u2257' ;// (8791) ≗ RING EQUAL TO Kreis über Gleichheitszeichen' ;// (ungefähr gleich) +'\u2258' ;// (8792) ≘ CORRESPONDS TO Entspricht-Zeichen' ;// (unüblich) +'\u2259' ;// (8793) ≙ ESTIMATES entspricht +'\u225A' ;// (8794) ≚ EQUIANGULAR TO gleichwinklig +'\u225B' ;// (8795) ≛ STAR EQUALS Gleichheitszeichen mit Stern +'\u225C' ;// (8796) ≜ DELTA EQUAL TO Gleichheitszeichen mit Delta +'\u225D' ;// (8797) ≝ EQUAL TO BY DEFINITION gleich nach Definition +'\u225E' ;// (8798) ≞ MEASURED BY gemessen nach +'\u225F' ;// (8799) ≟ QUESTIONED EQUAL TO vielleicht gleich +'\u2260' ;// (8800) ≠ NOT EQUAL TO Ungleichheitszeichen +'\u2261' ;// (8801) ≡ IDENTICAL TO ist kongruent zu +'\u2262' ;// (8802) ≢ NOT IDENTICAL TO ist nicht kongruent zu +'\u2263' ;// (8803) ≣ STRICTLY EQUIVALENT TO genau äquivalent +'\u2264' ;// (8804) ≤ LESS-THAN OR EQUAL TO kleiner/gleich +'\u2265' ;// (8805) ≥ GREATER-THAN OR EQUAL TO größer/gleich +'\u2266' ;// (8806) ≦ LESS-THAN OVER EQUAL TO kleiner als über gleich +'\u2267' ;// (8807) ≧ GREATER-THAN OVER EQUAL TO größer als über gleich +'\u2268' ;// (8808) ≨ LESS-THAN BUT NOT EQUAL TO kleiner als, aber nicht gleich +'\u2269' ;// (8809) ≩ GREATER-THAN BUT NOT EQUAL TO größer als, aber nicht gleich +'\u226A' ;// (8810) ≪ MUCH LESS-THAN viel kleiner als +'\u226B' ;// (8811) ≫ MUCH GREATER-THAN viel größer als +'\u226C' ;// (8812) ≬ BETWEEN zwischen +'\u226D' ;// (8813) ≭ NOT EQUIVALENT TO nicht äquivalent +'\u226E' ;// (8814) ≮ NOT LESS-THAN ist nicht kleiner als +'\u226F' ;// (8815) ≯ NOT GREATER-THAN ist nicht größer als +'\u2270' ;// (8816) ≰ NEITHER LESS-THAN NOR EQUAL TO weder kleiner als noch gleich +'\u2271' ;// (8817) ≱ NEITHER GREATER-THAN NOR EQUAL TO weder größer als noch gleich +'\u2272' ;// (8818) ≲ LESS-THAN OR EQUIVALENT TO kleiner als oder äquivalent +'\u2273' ;// (8819) ≳ GREATER-THAN OR EQUIVALENT TO größer als oder äquivalent +'\u2274' ;// (8820) ≴ NEITHER LESS-THAN NOR EQUIVALENT TO weder kleiner als noch äquivalent +'\u2275' ;// (8821) ≵ NEITHER GREATER-THAN NOR EQUIVALENT TO weder größer als noch äquivalent +'\u2276' ;// (8822) ≶ LESS-THAN OR GREATER-THAN kleiner/größer als +'\u2277' ;// (8823) ≷ GREATER-THAN OR LESS-THAN größer/kleiner als +'\u2278' ;// (8824) ≸ NEITHER LESS-THAN NOR GREATER-THAN weder kleiner noch größer als +'\u2279' ;// (8825) ≹ NEITHER GREATER-THAN NOR LESS-THAN weder größer noch kleiner als +'\u227A' ;// (8826) ≺ PRECEDES vorangehend +'\u227B' ;// (8827) ≻ SUCCEEDS nachfolgend +'\u227C' ;// (8828) ≼ PRECEDES OR EQUAL TO vorangehend oder gleich +'\u227D' ;// (8829) ≽ SUCCEEDS OR EQUAL TO nachfolgend oder gleich +'\u227E' ;// (8830) ≾ PRECEDES OR EQUIVALENT TO vorangehend oder äquivalent +'\u227F' ;// (8831) ≿ SUCCEEDS OR EQUIVALENT TO nachfolgend oder äquivalent +'\u2280' ;// (8832) ⊀ DOES NOT PRECEDE nicht vorangehend +'\u2281' ;// (8833) ⊁ DOES NOT SUCCEED nicht nachfolgend +'\u2282' ;// (8834) ⊂ SUBSET OF ist ;// (echte) Teilmenge von +'\u2283' ;// (8835) ⊃ SUPERSET OF ist ;// (echte) Obermenge von +'\u2284' ;// (8836) ⊄ NOT A SUBSET OF ist keine ;// (echte) Teilmenge von +'\u2285' ;// (8837) ⊅ NOT A SUPERSET OF ist keine ;// (echte) Obermenge von +'\u2286' ;// (8838) ⊆ SUBSET OF OR EQUAL TO Teilmenge oder gleich +'\u2287' ;// (8839) ⊇ SUPERSET OF OR EQUAL TO Obermenge oder gleich +'\u2288' ;// (8840) ⊈ NEITHER A SUBSET OF NOR EQUAL TO weder Teilmenge noch gleich +'\u2289' ;// (8841) ⊉ NEITHER A SUPERSET OF NOR EQUAL TO weder Obermenge noch gleich +'\u228A' ;// (8842) ⊊ SUBSET OF WITH NOT EQUAL TO Teilmenge mit ungleich +'\u228B' ;// (8843) ⊋ SUPERSET OF WITH NOT EQUAL TO Obermenge mit ungleich +'\u228C' ;// (8844) ⊌ MULTISET Multimenge +'\u228D' ;// (8845) ⊍ MULTISET MULTIPLICATION Multimengenmultiplikation +'\u228E' ;// (8846) ⊎ MULTISET UNION Multimengenvereinigung +'\u228F' ;// (8847) ⊏ SQUARE IMAGE OF viereckiges Bild +'\u2290' ;// (8848) ⊐ SQUARE ORIGINAL OF viereckiges Original +'\u2291' ;// (8849) ⊑ SQUARE IMAGE OF OR EQUAL TO viereckiges Bild oder gleich +'\u2292' ;// (8850) ⊒ SQUARE ORIGINAL OF OR EQUAL TO viereckiges Original oder gleich +'\u2293' ;// (8851) ⊓ SQUARE CAP nach unten geöffnetes Viereck +'\u2294' ;// (8852) ⊔ SQUARE CUP nach oben geöffnetes Viereck +'\u2295' ;// (8853) ⊕ CIRCLED PLUS eingekreistes Pluszeichen +'\u2296' ;// (8854) ⊖ CIRCLED MINUS eingekreistes Minuszeichen +'\u2297' ;// (8855) ⊗ CIRCLED TIMES eingekreistes Multiplikationszeichen +'\u2298' ;// (8856) ⊘ CIRCLED DIVISION SLASH eingekreister Divisionsstrich +'\u2299' ;// (8857) ⊙ CIRCLED DOT OPERATOR eingekreister Punktoperator +'\u229A' ;// (8858) ⊚ CIRCLED RING OPERATOR eingekreister Ringoperator +'\u229B' ;// (8859) ⊛ CIRCLED ASTERISK OPERATOR eingekreister Sternoperator +'\u229C' ;// (8860) ⊜ CIRCLED EQUALS eingekreistes Gleichheitszeichen +'\u229D' ;// (8861) ⊝ CIRCLED DASH eingekreister Gedankenstrich +'\u229E' ;// (8862) ⊞ SQUARED PLUS eingerahmtes Pluszeichen +'\u229F' ;// (8863) ⊟ SQUARED MINUS eingerahmtes Minuszeichen +'\u22A0' ;// (8864) ⊠ SQUARED TIMES eingerahmtes Multiplikationszeichen +'\u22A1' ;// (8865) ⊡ SQUARED DOT OPERATOR eingerahmter Punktoperator +'\u22A2' ;// (8866) ⊢ RIGHT TACK ergibt +'\u22A3' ;// (8867) ⊣ LEFT TACK ergibt nicht +'\u22A4' ;// (8868) ⊤ DOWN TACK senkrecht von +'\u22A5' ;// (8869) ⊥ UP TACK senkrecht auf +'\u22A6' ;// (8870) ⊦ ASSERTION Assertion +'\u22A7' ;// (8871) ⊧ MODELS Modelle +'\u22A8' ;// (8872) ⊨ TRUE wahr +'\u22A9' ;// (8873) ⊩ FORCES erzwingen +'\u22AA' ;// (8874) ⊪ TRIPLE VERTICAL BAR RIGHT TURNSTILE dreifache vertikale Leiste mit rechtem Drehkreuz +'\u22AB' ;// (8875) ⊫ DOUBLE VERTICAL BAR DOUBLE RIGHT TURNSTILE doppelte vertikale Leiste mit doppeltem rechtem Drehkreuz +'\u22AC' ;// (8876) ⊬ DOES NOT PROVE beweist nicht +'\u22AD' ;// (8877) ⊭ NOT TRUE nicht wahr +'\u22AE' ;// (8878) ⊮ DOES NOT FORCE nicht erzwingen +'\u22AF' ;// (8879) ⊯ NEGATED DOUBLE VERTICAL BAR DOUBLE RIGHT TURNSTILE negierte doppelte vertikale Leiste mit doppeltem rechten Drehkreuz +'\u22B0' ;// (8880) ⊰ PRECEDES UNDER RELATION vorangehend in Relation +'\u22B1' ;// (8881) ⊱ SUCCEEDS UNDER RELATION nachfolgend in Relation +'\u22B2' ;// (8882) ⊲ NORMAL SUBGROUP OF normale Untergruppe +'\u22B3' ;// (8883) ⊳ CONTAINS AS NORMAL SUBGROUP als normale Untergruppe enthalten +'\u22B4' ;// (8884) ⊴ NORMAL SUBGROUP OF OR EQUAL TO normale Untergruppe oder gleich +'\u22B5' ;// (8885) ⊵ CONTAINS AS NORMAL SUBGROUP OR EQUAL TO als normale Untergruppe enthalten oder gleich +'\u22B6' ;// (8886) ⊶ ORIGINAL OF Original +'\u22B7' ;// (8887) ⊷ IMAGE OF Bild +'\u22B8' ;// (8888) ⊸ MULTIMAP Mehrfachzuordnung +'\u22B9' ;// (8889) ⊹ HERMITIAN CONJUGATE MATRIX hermitesch konjugierte Matrix +'\u22BA' ;// (8890) ⊺ INTERCALATE einschalten +'\u22BB' ;// (8891) ⊻ XOR Ausschließendes Oder +'\u22BC' ;// (8892) ⊼ NAND Nand-verknüpft mit +'\u22BD' ;// (8893) ⊽ NOR Nor +'\u22BE' ;// (8894) ⊾ RIGHT ANGLE WITH ARC rechter Winkel mit Bogen +'\u22BF' ;// (8895) ⊿ RIGHT TRIANGLE rechtes Dreieck +'\u22C0' ;// (8896) ⋀ N-ARY LOGICAL AND N-stufiges logisches Und +'\u22C1' ;// (8897) ⋁ N-ARY LOGICAL OR N-stufiges logisches Oder +'\u22C2' ;// (8898) ⋂ N-ARY INTERSECTION N-stufiger Durchschnitt +'\u22C3' ;// (8899) ⋃ N-ARY UNION N-stufige Vereinigung +'\u22C4' ;// (8900) ⋄ DIAMOND OPERATOR Rautenoperator +'\u22C5' ;// (8901) ⋅ DOT OPERATOR Multiplikationspunkt +'\u22C6' ;// (8902) ⋆ STAR OPERATOR Sternoperator +'\u22C7' ;// (8903) ⋇ DIVISION TIMES Divisionsanzahl +'\u22C8' ;// (8904) ⋈ BOWTIE Schleife +'\u22C9' ;// (8905) ⋉ LEFT NORMAL FACTOR SEMIDIRECT PRODUCT linkes halbdirektes Produkt' ;// (Normalfaktor) +'\u22CA' ;// (8906) ⋊ RIGHT NORMAL FACTOR SEMIDIRECT PRODUCT rechtes halbdirektes Produkt' ;// (Normalfaktor) +'\u22CB' ;// (8907) ⋋ LEFT SEMIDIRECT PRODUCT linkes halbdirektes Produkt +'\u22CC' ;// (8908) ⋌ RIGHT SEMIDIRECT PRODUCT rechtes halbdirektes Produkt +'\u22CD' ;// (8909) ⋍ REVERSED TILDE EQUALS umgekehrte Tilde gleich +'\u22CE' ;// (8910) ⋎ CURLY LOGICAL OR geschweiftes logisches Oder +'\u22CF' ;// (8911) ⋏ CURLY LOGICAL AND geschweiftes logisches Und +'\u22D0' ;// (8912) ⋐ DOUBLE SUBSET doppelte Teilmenge +'\u22D1' ;// (8913) ⋑ DOUBLE SUPERSET doppelte Obermenge +'\u22D2' ;// (8914) ⋒ DOUBLE INTERSECTION doppelter Durchschnitt +'\u22D3' ;// (8915) ⋓ DOUBLE UNION doppelte Vereinigung +'\u22D4' ;// (8916) ⋔ PITCHFORK echter Durchschnitt +'\u22D5' ;// (8917) ⋕ EQUAL AND PARALLEL TO gleich und parallel ;// (ähnlich dem Doppelkreuz) +'\u22D6' ;// (8918) ⋖ LESS-THAN WITH DOT kleiner als mit Punkt +'\u22D7' ;// (8919) ⋗ GREATER-THAN WITH DOT größer als mit Punkt +'\u22D8' ;// (8920) ⋘ VERY MUCH LESS-THAN Sehr viel kleiner als +'\u22D9' ;// (8921) ⋙ VERY MUCH GREATER-THAN sehr viel größer als +'\u22DA' ;// (8922) ⋚ LESS-THAN EQUAL TO OR GREATER-THAN kleiner als, gleich oder größer als +'\u22DB' ;// (8923) ⋛ GREATER-THAN EQUAL TO OR LESS-THAN größer als, gleich oder kleiner als +'\u22DC' ;// (8924) ⋜ EQUAL TO OR LESS-THAN gleich oder kleiner als +'\u22DD' ;// (8925) ⋝ EQUAL TO OR GREATER-THAN gleich oder größer als +'\u22DE' ;// (8926) ⋞ EQUAL TO OR PRECEDES gleich oder vorangehend +'\u22DF' ;// (8927) ⋟ EQUAL TO OR SUCCEEDS gleich oder nachfolgend +'\u22E0' ;// (8928) ⋠ DOES NOT PRECEDE OR EQUAL weder vorangehend oder gleich +'\u22E1' ;// (8929) ⋡ DOES NOT SUCCEED OR EQUAL weder nachfolgend oder gleich +'\u22E2' ;// (8930) ⋢ NOT SQUARE IMAGE OF OR EQUAL TO kein viereckiges Bild oder gleich +'\u22E3' ;// (8931) ⋣ NOT SQUARE ORIGINAL OF OR EQUAL TO kein viereckiges Original oder gleich +'\u22E4' ;// (8932) ⋤ SQUARE IMAGE OF OR NOT EQUAL TO viereckiges Bild oder ungleich +'\u22E5' ;// (8933) ⋥ SQUARE ORIGINAL OF OR NOT EQUAL TO viereckiges Original oder ungleich +'\u22E6' ;// (8934) ⋦ LESS-THAN BUT NOT EQUIVALENT TO kleiner als, aber nicht äquivalent +'\u22E7' ;// (8935) ⋧ GREATER-THAN BUT NOT EQUIVALENT TO größer als, aber nicht äquivalent +'\u22E8' ;// (8936) ⋨ PRECEDES BUT NOT EQUIVALENT TO vorangehend, aber nicht äquivalent +'\u22E9' ;// (8937) ⋩ SUCCEEDS BUT NOT EQUIVALENT TO nachfolgend, aber nicht äquivalent +'\u22EA' ;// (8938) ⋪ NOT NORMAL SUBGROUP OF keine normale Untergruppe +'\u22EB' ;// (8939) ⋫ DOES NOT CONTAIN AS NORMAL SUBGROUP nicht als normale Untergruppe enthalten +'\u22EC' ;// (8940) ⋬ NOT NORMAL SUBGROUP OF OR EQUAL TO keine normale Untergruppe oder gleich +'\u22ED' ;// (8941) ⋭ DOES NOT CONTAIN AS NORMAL SUBGROUP OR EQUAL nicht als normale Untergruppe enthalten oder gleich +'\u22EE' ;// (8942) ⋮ VERTICAL ELLIPSIS Vertikale Ellipse +'\u22EF' ;// (8943) ⋯ MIDLINE HORIZONTAL ELLIPSIS Zentrierte horizontale Ellipse +'\u22F0' ;// (8944) ⋰ UP RIGHT DIAGONAL ELLIPSIS Diagonale Ellipse, unten links nach oben rechts +'\u22F1' ;// (8945) ⋱ DOWN RIGHT DIAGONAL ELLIPSIS Diagonale Ellipse, oben links nach unten rechts +'\u22F2' ;// (8946) ⋲ ELEMENT OF WITH LONG HORIZONTAL STROKE Element mit langem horizontalen Strich +'\u22F3' ;// (8947) ⋳ ELEMENT OF WITH VERTICAL BAR AT END OF HORIZONTAL STROKE Element mit vertikalem Strich am Ende des horizontalen Strichs +'\u22F4' ;// (8948) ⋴ SMALL ELEMENT OF WITH VERTICAL BAR AT END OF HORIZONTAL STROKE kleines Element mit vertikalem Strich am Ende des horizontalen Strichs +'\u22F5' ;// (8949) ⋵ ELEMENT OF WITH DOT ABOVE Element mit Punkt ;// (oben) +'\u22F6' ;// (8950) ⋶ ELEMENT OF WITH OVERBAR Element mit Überstrich +'\u22F7' ;// (8951) ⋷ SMALL ELEMENT OF WITH OVERBAR kleines Element mit Überstrich +'\u22F8' ;// (8952) ⋸ ELEMENT OF WITH UNDERBAR Element mit Unterstrich +'\u22F9' ;// (8953) ⋹ ELEMENT OF WITH TWO HORIZONTAL STROKES Element mit 2 horizontalen Strichen +'\u22FA' ;// (8954) ⋺ CONTAINS WITH LONG HORIZONTAL STROKE umgekehrtes Elementzeichen mit langem horizontalen Strich +'\u22FB' ;// (8955) ⋻ CONTAINS WITH VERTICAL BAR AT END OF HORIZONTAL STROKE umgekehrtes Elementzeichen mit vertikalem Strich am Ende des horizontalen Strichs +'\u22FC' ;// (8956) ⋼ SMALL CONTAINS WITH VERTICAL BAR AT END OF HORIZONTAL STROKE kleines umgekehrtes Elementzeichen mit vertikalem Strich am Ende des horizontalen Strichs +'\u22FD' ;// (8957) ⋽ CONTAINS WITH OVERBAR umgekehrtes Elementzeichen mit Überstrich +'\u22FE' ;// (8958) ⋾ SMALL CONTAINS WITH OVERBAR kleines umgekehrtes Elementzeichen mit Überstrich +'\u22FF' ;// (8959) ⋿ Z NOTATION BAG MEMBERSHIP +*/ +/* +U+2980 (10624) ⦀ mathematisches Symbol TRIPLE VERTICAL BAR DELIMITER Trennzeichen in Form dreier senkrechter Striche +U+2981 (10625) ⦁ mathematisches Symbol Z NOTATION SPOT Punkt der Z-Notation +U+2982 (10626) ⦂ mathematisches Symbol Z NOTATION TYPE COLON Doppelpunkt in der Art der Z-Notation +U+2983 (10627) ⦃ öffnende Punktierung +(eines Paars) LEFT WHITE CURLY BRACKET Öffnende weiße geschweifte Klammer +U+2984 (10628) ⦄ schließende Punktierung +(eines Paars) RIGHT WHITE CURLY BRACKET Schließende weiße geschweifte Klammer +U+2985 (10629) ⦅ öffnende Punktierung +(eines Paars) LEFT WHITE PARENTHESIS Öffnende weiße runde Klammer +U+2986 (10630) ⦆ schließende Punktierung +(eines Paars) RIGHT WHITE PARENTHESIS Schließende weiße runde Klammer +U+2987 (10631) ⦇ öffnende Punktierung +(eines Paars) Z NOTATION LEFT IMAGE BRACKET +U+2988 (10632) ⦈ schließende Punktierung +(eines Paars) Z NOTATION RIGHT IMAGE BRACKET +U+2989 (10633) ⦉ öffnende Punktierung +(eines Paars) Z NOTATION LEFT BINDING BRACKET +U+298A (10634) ⦊ schließende Punktierung +(eines Paars) Z NOTATION RIGHT BINDING BRACKET +U+298B (10635) ⦋ öffnende Punktierung +(eines Paars) LEFT SQUARE BRACKET WITH UNDERBAR Öffnende eckige Klammer mit Unterstrich +U+298C (10636) ⦌ schließende Punktierung +(eines Paars) RIGHT SQUARE BRACKET WITH UNDERBAR Schließende eckige Klammer mit Unterstrich +U+298D (10637) ⦍ öffnende Punktierung +(eines Paars) LEFT SQUARE BRACKET WITH TICK IN TOP CORNER Öffnende eckige Klammer mit Strichlein in der oberen Ecke +U+298E (10638) ⦎ schließende Punktierung +(eines Paars) RIGHT SQUARE BRACKET WITH TICK IN BOTTOM CORNER Schließende eckige Klammer mit Strichlein in der unteren Ecke +U+298F (10639) ⦏ öffnende Punktierung +(eines Paars) LEFT SQUARE BRACKET WITH TICK IN BOTTOM CORNER Öffnende eckige Klammer mit Strichlein in der unteren Ecke +U+2990 (10640) ⦐ schließende Punktierung +(eines Paars) RIGHT SQUARE BRACKET WITH TICK IN TOP CORNER Schließende eckige Klammer mit Strichlein in der oberen Ecke +U+2991 (10641) ⦑ öffnende Punktierung +(eines Paars) LEFT ANGLE BRACKET WITH DOT Öffnende spitze Klammer mit Punkt +U+2992 (10642) ⦒ schließende Punktierung +(eines Paars) RIGHT ANGLE BRACKET WITH DOT Schließende spitze Klammer mit Punkt +U+2993 (10643) ⦓ öffnende Punktierung +(eines Paars) LEFT ARC LESS-THAN BRACKET +U+2994 (10644) ⦔ schließende Punktierung +(eines Paars) RIGHT ARC GREATER-THAN BRACKET +U+2995 (10645) ⦕ öffnende Punktierung +(eines Paars) DOUBLE LEFT ARC GREATER-THAN BRACKET +U+2996 (10646) ⦖ schließende Punktierung +(eines Paars) DOUBLE RIGHT ARC LESS-THAN BRACKET +U+2997 (10647) ⦗ öffnende Punktierung +(eines Paars) LEFT BLACK TORTOISE SHELL BRACKET Öffnende schwarze „Schildkrötenpanzer-Klammer“ +U+2998 (10648) ⦘ schließende Punktierung +(eines Paars) RIGHT BLACK TORTOISE SHELL BRACKET Schließende schwarze „Schildkrötenpanzer-Klammer“ +U+2999 (10649) ⦙ mathematisches Symbol DOTTED FENCE Gepunkteter Zaun +U+299A (10650) ⦚ mathematisches Symbol VERTICAL ZIGZAG LINE Senkrechte Zickzacklinie +U+299B (10651) ⦛ mathematisches Symbol MEASURED ANGLE OPENING LEFT Gerichteter Winkel nach links geöffnet +U+299C (10652) ⦜ mathematisches Symbol RIGHT ANGLE VARIANT WITH SQUARE Variante eines rechten Winkels mit Quadrat +U+299D (10653) ⦝ mathematisches Symbol MEASURED RIGHT ANGLE WITH DOT Gerichteter rechter Winkel mit Punkt +U+299E (10654) ⦞ mathematisches Symbol ANGLE WITH S INSIDE Winkel mit einem S darin +U+299F (10655) ⦟ mathematisches Symbol ACUTE ANGLE Spitzer Winkel +U+29A0 (10656) ⦠ mathematisches Symbol SPHERICAL ANGLE OPENING LEFT Raumwinkel nach links geöffnet +U+29A1 (10657) ⦡ mathematisches Symbol SPHERICAL ANGLE OPENING UP Raumwinkel nach oben geöffnet +U+29A2 (10658) ⦢ mathematisches Symbol TURNED ANGLE Gedrehtes Winkelzeichen +U+29A3 (10659) ⦣ mathematisches Symbol REVERSED ANGLE Gewendetes Winkelzeichen +U+29A4 (10660) ⦤ mathematisches Symbol ANGLE WITH UNDERBAR Winkelzeichen mit Unterstrich +U+29A5 (10661) ⦥ mathematisches Symbol REVERSED ANGLE WITH UNDERBAR Gewendetes Winkelzeichen mit Unterstrich +U+29A6 (10662) ⦦ mathematisches Symbol OBLIQUE ANGLE OPENING UP Stumpfer Winkel mit Öffnung nach oben +U+29A7 (10663) ⦧ mathematisches Symbol OBLIQUE ANGLE OPENING DOWN Stumpfer Winkel mit Öffnung nach unten +U+29A8 (10664) ⦨ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING UP AND RIGHT Gerichteter Winkel nach rechts geöffnet mit Pfeil nach rechts oben +U+29A9 (10665) ⦩ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING UP AND LEFT Gerichteter Winkel nach links geöffnet mit Pfeil nach links oben +U+29AA (10666) ⦪ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING DOWN AND RIGHT Gerichteter Winkel nach rechts geöffnet mit Pfeil nach rechts unten +U+29AB (10667) ⦫ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING DOWN AND LEFT Gerichteter Winkel nach links geöffnet mit Pfeil nach links unten +U+29AC (10668) ⦬ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING RIGHT AND UP Gerichteter Winkel nach oben geöffnet mit Pfeil nach rechts oben +U+29AD (10669) ⦭ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING LEFT AND UP Gerichteter Winkel nach oben geöffnet mit Pfeil nach links oben +U+29AE (10670) ⦮ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING RIGHT AND DOWN Gerichteter Winkel nach unten geöffnet mit Pfeil nach rechts unten +U+29AF (10671) ⦯ mathematisches Symbol MEASURED ANGLE WITH OPEN ARM ENDING IN ARROW POINTING LEFT AND DOWN Gerichteter Winkel nach unten geöffnet mit Pfeil nach links unten +U+29B0 (10672) ⦰ mathematisches Symbol REVERSED EMPTY SET Gewendetes Leere-Menge-Zeichen +U+29B1 (10673) ⦱ mathematisches Symbol EMPTY SET WITH OVERBAR Leere-Menge-Zeichen mit Überstrich +U+29B2 (10674) ⦲ mathematisches Symbol EMPTY SET WITH SMALL CIRCLE ABOVE Leere-Menge-Zeichen mit übergesetztem Kreis +U+29B3 (10675) ⦳ mathematisches Symbol EMPTY SET WITH RIGHT ARROW ABOVE Leere-Menge-Zeichen mit übergesetztem Pfeil nach rechts +U+29B4 (10676) ⦴ mathematisches Symbol EMPTY SET WITH LEFT ARROW ABOVE Leere-Menge-Zeichen mit übergesetztem Pfeil nach links +U+29B5 (10677) ⦵ mathematisches Symbol CIRCLE WITH HORIZONTAL BAR Kreis mit Querstrich +U+29B6 (10678) ⦶ mathematisches Symbol CIRCLED VERTICAL BAR Eingekreister senkrechter Strich +U+29B7 (10679) ⦷ mathematisches Symbol CIRCLED PARALLEL Eingekreistes Parallel-zu-Zeichen +U+29B8 (10680) ⦸ mathematisches Symbol CIRCLED REVERSE SOLIDUS Eingekreister umgekehrter Schrägstrich +U+29B9 (10681) ⦹ mathematisches Symbol CIRCLED PERPENDICULAR +U+29BA (10682) ⦺ mathematisches Symbol CIRCLE DIVIDED BY HORIZONTAL BAR AND TOP HALF DIVIDED BY VERTICAL BAR Kreis geteilt durch einen Querstrich und die obere Hälfte geteilt durch einen senkrechten Strich +U+29BB (10683) ⦻ mathematisches Symbol CIRCLE WITH SUPERIMPOSED X Kreis mit darübergelegtem X +U+29BC (10684) ⦼ mathematisches Symbol CIRCLED ANTICLOCKWISE-ROTATED DIVISION SIGN Eingekreistes gegen den Uhrzeigersinn gedrehtes Divisionszeichen +U+29BD (10685) ⦽ mathematisches Symbol UP ARROW THROUGH CIRCLE Pfeil nach oben durch Kreis hindurch +U+29BE (10686) ⦾ mathematisches Symbol CIRCLED WHITE BULLET Eingekreistes weißes Aufzählungszeichen +U+29BF (10687) ⦿ mathematisches Symbol CIRCLED BULLET Eingekreistes Aufzählungszeichen +U+29C0 (10688) ⧀ mathematisches Symbol CIRCLED LESS-THAN Eingekreistes Kleiner-als-Zeichen +U+29C1 (10689) ⧁ mathematisches Symbol CIRCLED GREATER-THAN Eingekreistes Größer-als-Zeichen +U+29C2 (10690) ⧂ mathematisches Symbol CIRCLE WITH SMALL CIRCLE TO THE RIGHT Kreis mit kleinem Kreis an der rechten Seite +U+29C3 (10691) ⧃ mathematisches Symbol CIRCLE WITH TWO HORIZONTAL STROKES TO THE RIGHT Kreis mit zwei waagerechten Strichen an der rechten Seite +U+29C4 (10692) ⧄ mathematisches Symbol SQUARED RISING DIAGONAL SLASH Von einem Quadrat umschlossene steigende Diagonale +U+29C5 (10693) ⧅ mathematisches Symbol SQUARED FALLING DIAGONAL SLASH Von einem Quadrat umschlossene fallende Diagonale +U+29C6 (10694) ⧆ mathematisches Symbol SQUARED ASTERISK Von einem Quadrat umschlossenes Sternchen +U+29C7 (10695) ⧇ mathematisches Symbol SQUARED SMALL CIRCLE Von einem Quadrat umschlossener kleiner Kreis +U+29C8 (10696) ⧈ mathematisches Symbol SQUARED SQUARE Von einem Quadrat umschlossenes Quadrat +U+29C9 (10697) ⧉ mathematisches Symbol TWO JOINED SQUARES Zwei verbundene Quadrate +U+29CA (10698) ⧊ mathematisches Symbol TRIANGLE WITH DOT ABOVE Dreieck mit übergesetztem Punkt +U+29CB (10699) ⧋ mathematisches Symbol TRIANGLE WITH UNDERBAR Dreieck mit Unterstrich +U+29CC (10700) ⧌ mathematisches Symbol S IN TRIANGLE S in einem Dreieck +U+29CD (10701) ⧍ mathematisches Symbol TRIANGLE WITH SERIFS AT BOTTOM Dreieck mit Serifen an der Unterseite +U+29CE (10702) ⧎ mathematisches Symbol RIGHT TRIANGLE ABOVE LEFT TRIANGLE Nach rechts zeigendes Dreieck über nach links zeigendem Dreieck +U+29CF (10703) ⧏ mathematisches Symbol LEFT TRIANGLE BESIDE VERTICAL BAR Nach links zeigendes Dreieck neben senkrechtem Strich +U+29D0 (10704) ⧐ mathematisches Symbol VERTICAL BAR BESIDE RIGHT TRIANGLE Senkrechter Strich neben einem nach rechts zeigenden Dreieck +U+29D1 (10705) ⧑ mathematisches Symbol BOWTIE WITH LEFT HALF BLACK Fliege mit schwarzer linker Hälfte +U+29D2 (10706) ⧒ mathematisches Symbol BOWTIE WITH RIGHT HALF BLACK Fliege mit schwarzer rechter Hälfte +U+29D3 (10707) ⧓ mathematisches Symbol BLACK BOWTIE Schwarze Fliege +U+29D4 (10708) ⧔ mathematisches Symbol TIMES WITH LEFT HALF BLACK Malzeichen mit schwarz aufgefüllter linker Hälfte +U+29D5 (10709) ⧕ mathematisches Symbol TIMES WITH RIGHT HALF BLACK Malzeichen mit schwarz aufgefüllter rechter Hälfte +U+29D6 (10710) ⧖ mathematisches Symbol WHITE HOURGLASS Weiße Sanduhr +U+29D7 (10711) ⧗ mathematisches Symbol BLACK HOURGLASS Schwarze Sanduhr +U+29D8 (10712) ⧘ öffnende Punktierung +(eines Paars) LEFT WIGGLY FENCE Linker welliger Strich +U+29D9 (10713) ⧙ schließende Punktierung +(eines Paars) RIGHT WIGGLY FENCE Rechter welliger Strich +U+29DA (10714) ⧚ öffnende Punktierung +(eines Paars) LEFT DOUBLE WIGGLY FENCE Linker doppelter welliger Strich +U+29DB (10715) ⧛ schließende Punktierung +(eines Paars) RIGHT DOUBLE WIGGLY FENCE Rechter doppelter welliger Strich +U+29DC (10716) ⧜ mathematisches Symbol INCOMPLETE INFINITY Unvollständiges Unendlichkeitszeichen +U+29DD (10717) ⧝ mathematisches Symbol TIE OVER INFINITY Bindebogen über Unendlichkeitszeichen +U+29DE (10718) ⧞ mathematisches Symbol INFINITY NEGATED WITH VERTICAL BAR +U+29DF (10719) ⧟ mathematisches Symbol DOUBLE-ENDED MULTIMAP Multimengenzeichen mit zwei Enden +U+29E0 (10720) ⧠ mathematisches Symbol SQUARE WITH CONTOURED OUTLINE D’Alembert-Operator +U+29E1 (10721) ⧡ mathematisches Symbol INCREASES AS +U+29E2 (10722) ⧢ mathematisches Symbol SHUFFLE PRODUCT Shuffle-Produkt +U+29E3 (10723) ⧣ mathematisches Symbol EQUALS SIGN AND SLANTED PARALLEL +U+29E4 (10724) ⧤ mathematisches Symbol EQUALS SIGN AND SLANTED PARALLEL WITH TILDE ABOVE +U+29E5 (10725) ⧥ mathematisches Symbol IDENTICAL TO AND SLANTED PARALLEL +U+29E6 (10726) ⧦ mathematisches Symbol GLEICH STARK tautologisch äquivalent +U+29E7 (10727) ⧧ mathematisches Symbol THERMODYNAMIC Thermodynamisch +U+29E8 (10728) ⧨ mathematisches Symbol DOWN-POINTING TRIANGLE WITH LEFT HALF BLACK Nach unten zeigendes Dreieck mit linker schwarzer Hälfte +U+29E9 (10729) ⧩ mathematisches Symbol DOWN-POINTING TRIANGLE WITH RIGHT HALF BLACK Nach unten zeigendes Dreieck mit rechter schwarzer Hälfte +U+29EA (10730) ⧪ mathematisches Symbol BLACK DIAMOND WITH DOWN ARROW Schwarzes Karo mit Pfeil nach unten +U+29EB (10731) ⧫ mathematisches Symbol BLACK LOZENGE Schwarzer Rhombus +U+29EC (10732) ⧬ mathematisches Symbol WHITE CIRCLE WITH DOWN ARROW Weißer Kreis mit Pfeil nach unten +U+29ED (10733) ⧭ mathematisches Symbol BLACK CIRCLE WITH DOWN ARROW Schwarzer Kreis mit Pfeil nach unten +U+29EE (10734) ⧮ mathematisches Symbol ERROR-BARRED WHITE SQUARE Weißes Quadrat mit Fehlerbalken +U+29EF (10735) ⧯ mathematisches Symbol ERROR-BARRED BLACK SQUARE Schwarzes Quadrat mit Fehlerbalken +U+29F0 (10736) ⧰ mathematisches Symbol ERROR-BARRED WHITE DIAMOND Weißer Rhombus mit Fehlerbalken +U+29F1 (10737) ⧱ mathematisches Symbol ERROR-BARRED BLACK DIAMOND Schwarzer Rhombus mit Fehlerbalken +U+29F2 (10738) ⧲ mathematisches Symbol ERROR-BARRED WHITE CIRCLE Weißer Kreis mit Fehlerbalken +U+29F3 (10739) ⧳ mathematisches Symbol ERROR-BARRED BLACK CIRCLE Schwarzer Kreis mit Fehlerbalken +U+29F4 (10740) ⧴ mathematisches Symbol RULE-DELAYED +U+29F5 (10741) ⧵ mathematisches Symbol REVERSE SOLIDUS OPERATOR Operator umgekehrter Schrägstrich +U+29F6 (10742) ⧶ mathematisches Symbol SOLIDUS WITH OVERBAR Schrägstrich mit Überstrich +U+29F7 (10743) ⧷ mathematisches Symbol REVERSE SOLIDUS WITH HORIZONTAL STROKE Umgekehrter Schrägstrich mit Querstrich +U+29F8 (10744) ⧸ mathematisches Symbol BIG SOLIDUS Großer Schrägstrich +U+29F9 (10745) ⧹ mathematisches Symbol BIG REVERSE SOLIDUS Großer umgekehrter Schrägstrich +U+29FA (10746) ⧺ mathematisches Symbol DOUBLE PLUS Doppeltes Pluszeichen +U+29FB (10747) ⧻ mathematisches Symbol TRIPLE PLUS Dreifaches Pluszeichen +U+29FC (10748) ⧼ öffnende Punktierung +(eines Paars) LEFT-POINTING CURVED ANGLE BRACKET Nach links zeigende gekrümmte spitze Klammer +U+29FD (10749) ⧽ schließende Punktierung +(eines Paars) RIGHT-POINTING CURVED ANGLE BRACKET Nach rechts zeigende gekrümmte spitze Klammer +U+29FE (10750) ⧾ mathematisches Symbol TINY Tiny (Kombinatorische Spieltheorie) +U+29FF (10751) ⧿ mathematisches Symbol MINY Miny (Kombinatorische Spieltheorie) +*/ +/* +PLAN B +U+2A00 (10752) ⨀ N-ARY CIRCLED DOT OPERATOR N-stelliger eingekreister Punktoperator +U+2A01 (10753) ⨁ N-ARY CIRCLED PLUS OPERATOR N-stelliges eingekreistes Pluszeichen +U+2A02 (10754) ⨂ N-ARY CIRCLED TIMES OPERATOR N-stelliges eingekreistes Multiplikationszeichen +U+2A03 (10755) ⨃ N-ARY UNION OPERATOR WITH DOT N-stelliges Vereinigungszeichen mit Punkt +U+2A04 (10756) ⨄ N-ARY UNION OPERATOR WITH PLUS N-stelliges Vereinigungszeichen mit Pluszeichen +U+2A05 (10757) ⨅ N-ARY SQUARE INTERSECTION OPERATOR N-stelliger viereckiger Schnittmengenoperator +U+2A06 (10758) ⨆ N-ARY SQUARE UNION OPERATOR N-stelliger viereckiger Vereinigungsmengenoperator +U+2A07 (10759) ⨇ TWO LOGICAL AND OPERATOR Doppelter logischer UND-Operator +U+2A08 (10760) ⨈ TWO LOGICAL OR OPERATOR Doppelter logischer ODER-Operator +U+2A09 (10761) ⨉ N-ARY TIMES OPERATOR N-stelliger Kreuzproduktoperator +U+2A0A (10762) ⨊ MODULO TWO SUM Summe modulo 2 +U+2A0B (10763) ⨋ SUMMATION WITH INTEGRAL Summenzeichen mit Integral +U+2A0C (10764) ⨌ QUADRUPLE INTEGRAL OPERATOR Vierfaches Integralzeichen +U+2A0D (10765) ⨍ FINITE PART INTEGRAL +U+2A0E (10766) ⨎ INTEGRAL WITH DOUBLE STROKE +U+2A0F (10767) ⨏ INTEGRAL AVERAGE WITH SLASH +U+2A10 (10768) ⨐ CIRCULATION FUNCTION +U+2A11 (10769) ⨑ ANTICLOCKWISE INTEGRATION +U+2A12 (10770) ⨒ LINE INTEGRATION WITH RECTANGULAR PATH AROUND POLE +U+2A13 (10771) ⨓ LINE INTEGRATION WITH SEMICIRCULAR PATH AROUND POLE +U+2A14 (10772) ⨔ LINE INTEGRATION NOT INCLUDING THE POLE +U+2A15 (10773) ⨕ INTEGRAL AROUND A POINT OPERATOR +U+2A16 (10774) ⨖ QUATERNION INTEGRAL OPERATOR +U+2A17 (10775) ⨗ INTEGRAL WITH LEFTWARDS ARROW WITH HOOK +U+2A18 (10776) ⨘ INTEGRAL WITH TIMES SIGN +U+2A19 (10777) ⨙ INTEGRAL WITH INTERSECTION Integralzeichen mit Schnittmenge +U+2A1A (10778) ⨚ INTEGRAL WITH UNION Integralzeichen mit Vereinigungsmenge +U+2A1B (10779) ⨛ INTEGRAL WITH OVERBAR Integral mit Oberstrich +U+2A1C (10780) ⨜ INTEGRAL WITH UNDERBAR Integral mit Unterstrich +U+2A1D (10781) ⨝ JOIN Join-Operator +U+2A1E (10782) ⨞ LARGE LEFT TRIANGLE OPERATOR +U+2A1F (10783) ⨟ Z NOTATION SCHEMA COMPOSITION +U+2A20 (10784) ⨠ Z NOTATION SCHEMA PIPING +U+2A21 (10785) ⨡ Z NOTATION SCHEMA PROJECTION +U+2A22 (10786) ⨢ PLUS SIGN WITH SMALL CIRCLE ABOVE Pluszeichen mit übergesetztem Ring +U+2A23 (10787) ⨣ PLUS SIGN WITH CIRCUMFLEX ACCENT ABOVE Pluszeichen mit übergesetztem Zirkumflex +U+2A24 (10788) ⨤ PLUS SIGN WITH TILDE ABOVE Pluszeichen mit übergesetzter Tilde +U+2A25 (10789) ⨥ PLUS SIGN WITH DOT BELOW Pluszeichen mit untergesetztem Punkt +U+2A26 (10790) ⨦ PLUS SIGN WITH TILDE BELOW Pluszeichen mit untergesetzter Tilde +U+2A27 (10791) ⨧ PLUS SIGN WITH SUBSCRIPT TWO Pluszeichen mit tiefgestellter Ziffer Zwei +U+2A28 (10792) ⨨ PLUS SIGN WITH BLACK TRIANGLE Pluszeichen mit schwarzem Dreieck +U+2A29 (10793) ⨩ MINUS SIGN WITH COMMA ABOVE Minuszeichen mit übergesetztem Komma +U+2A2A (10794) ⨪ MINUS SIGN WITH DOT BELOW Minuszeichen mit untergesetztem Punkt +U+2A2B (10795) ⨫ MINUS SIGN WITH FALLING DOTS Minuszeichen mit Punkt links oben und rechts unten +U+2A2C (10796) ⨬ MINUS SIGN WITH RISING DOTS Minuszeichen mit Punkt rechts oben und links unten +U+2A2D (10797) ⨭ PLUS SIGN IN LEFT HALF CIRCLE Pluszeichen in linksseitigem Halbkreis +U+2A2E (10798) ⨮ PLUS SIGN IN RIGHT HALF CIRCLE Pluszeichen in rechtsseitigem Halbkreis +U+2A2F (10799) ⨯ VECTOR OR CROSS PRODUCT Kreuzprodukt +U+2A30 (10800) ⨰ MULTIPLICATION SIGN WITH DOT ABOVE Multiplikationszeichen (Kreuzprodukt) mit übergesetztem Punkt +U+2A31 (10801) ⨱ MULTIPLICATION SIGN WITH UNDERBAR Multiplikationszeichen (Kreuzprodukt) mit Unterstrich +U+2A32 (10802) ⨲ SEMIDIRECT PRODUCT WITH BOTTOM CLOSED +U+2A33 (10803) ⨳ SMASH PRODUCT Smash-Produkt +U+2A34 (10804) ⨴ MULTIPLICATION SIGN IN LEFT HALF CIRCLE Multiplikationszeichen (Kreuzprodukt) in linksseitigem Halbkreis +U+2A35 (10805) ⨵ MULTIPLICATION SIGN IN RIGHT HALF CIRCLE Multiplikationszeichen (Kreuzprodukt) in rechtsseitigem Halbkreis +U+2A36 (10806) ⨶ CIRCLED MULTIPLICATION SIGN WITH CIRCUMFLEX ACCENT Eingekreistes Multiplikationszeichen mit Zirkumflex +U+2A37 (10807) ⨷ MULTIPLICATION SIGN IN DOUBLE CIRCLE Doppelt eingekreistes Multiplikationszeichen +U+2A38 (10808) ⨸ CIRCLED DIVISION SIGN Eingekreistes Divisionszeichen +U+2A39 (10809) ⨹ PLUS SIGN IN TRIANGLE Pluszeichen im Dreieck +U+2A3A (10810) ⨺ MINUS SIGN IN TRIANGLE Minuszeichen im Dreieck +U+2A3B (10811) ⨻ MULTIPLICATION SIGN IN TRIANGLE Multiplikationszeichen im Dreieck +U+2A3C (10812) ⨼ INTERIOR PRODUCT Inneres Produkt +U+2A3D (10813) ⨽ RIGHTHAND INTERIOR PRODUCT Rechtsseitiges inneres Produkt +U+2A3E (10814) ⨾ Z NOTATION RELATIONAL COMPOSITION +U+2A3F (10815) ⨿ AMALGAMATION OR COPRODUCT Koprodukt +U+2A40 (10816) ⩀ INTERSECTION WITH DOT Schnittmengenzeichen mit Punkt +U+2A41 (10817) ⩁ UNION WITH MINUS SIGN Vereinigungsmengenzeichen mit Minuszeichen +U+2A42 (10818) ⩂ UNION WITH OVERBAR Vereinigungsmengenzeichen mit übergesetztem Makron +U+2A43 (10819) ⩃ INTERSECTION WITH OVERBAR Schnittmengenzeichen mit übergesetztem Makron +U+2A44 (10820) ⩄ INTERSECTION WITH LOGICAL AND Schnittmengenzeichen mit logischem UND +U+2A45 (10821) ⩅ UNION WITH LOGICAL OR Vereinigungsmengenzeichen mit logischem ODER +U+2A46 (10822) ⩆ UNION ABOVE INTERSECTION Vereinigungsmengenzeichen über Schnittmengenzeichen +U+2A47 (10823) ⩇ INTERSECTION ABOVE UNION Schnittmengenzeichen über Vereinigungsmengenzeichen +U+2A48 (10824) ⩈ UNION ABOVE BAR ABOVE INTERSECTION Vereinigungsmengenzeichen über horizontalem Strich und Schnittmengenzeichen +U+2A49 (10825) ⩉ INTERSECTION ABOVE BAR ABOVE UNION Schnittmengenzeichen über horizontalem Strich und Vereinigungsmengenzeichen +U+2A4A (10826) ⩊ UNION BESIDE AND JOINED WITH UNION +U+2A4B (10827) ⩋ INTERSECTION BESIDE AND JOINED WITH INTERSECTION +U+2A4C (10828) ⩌ CLOSED UNION WITH SERIFS Geschlossenes Vereinigungsmengenzeichen mit Serifen +U+2A4D (10829) ⩍ CLOSED INTERSECTION WITH SERIFS Geschlossenes Schnittmengenzeichen mit Serifen +U+2A4E (10830) ⩎ DOUBLE SQUARE INTERSECTION Doppeltes eckiges Schnittmengenzeichen +U+2A4F (10831) ⩏ DOUBLE SQUARE UNION Doppeltes eckiges Vereinigungsmengenzeichen +U+2A50 (10832) ⩐ CLOSED UNION WITH SERIFS AND SMASH PRODUCT Geschlossenes Vereinigungsmengenzeichen mit Serifen und Smash-Produkt +U+2A51 (10833) ⩑ LOGICAL AND WITH DOT ABOVE Logisches UND mit übergesetztem Punkt +U+2A52 (10834) ⩒ LOGICAL OR WITH DOT ABOVE Logisches ODER mit übergesetztem Punkt +U+2A53 (10835) ⩓ DOUBLE LOGICAL AND Doppeltes logisches UND +U+2A54 (10836) ⩔ DOUBLE LOGICAL OR Doppeltes logisches ODER +U+2A55 (10837) ⩕ TWO INTERSECTING LOGICAL AND Zwei sich überschneidende logische UND-Operatoren +U+2A56 (10838) ⩖ TWO INTERSECTING LOGICAL OR Zwei sich überschneidende logische ODER-Operatoren +U+2A57 (10839) ⩗ SLOPING LARGE OR Schräges logisches Oder +U+2A58 (10840) ⩘ SLOPING LARGE AND Schräges logisches Und +U+2A59 (10841) ⩙ LOGICAL OR OVERLAPPING LOGICAL AND Sich mit logischem Und überschneidendes logisches Oder +U+2A5A (10842) ⩚ LOGICAL AND WITH MIDDLE STEM Logisches UND mit Mittelstrich +U+2A5B (10843) ⩛ LOGICAL OR WITH MIDDLE STEM Logisches ODER mit Mittelstrich +U+2A5C (10844) ⩜ LOGICAL AND WITH HORIZONTAL DASH Durchgestrichenes logisches Und +U+2A5D (10845) ⩝ LOGICAL OR WITH HORIZONTAL DASH Durchgestrichenes logisches Oder +U+2A5E (10846) ⩞ LOGICAL AND WITH DOUBLE OVERBAR Logisches Und mit übergesetztem doppeltem Makron +U+2A5F (10847) ⩟ LOGICAL AND WITH UNDERBAR Logisches Und mit Unterstrich +U+2A60 (10848) ⩠ LOGICAL AND WITH DOUBLE UNDERBAR Logisches Und mit doppeltem Unterstrich +U+2A61 (10849) ⩡ SMALL VEE WITH UNDERBAR Lateinischer Kleinbuchstabe V mit Unterstrich +U+2A62 (10850) ⩢ LOGICAL OR WITH DOUBLE OVERBAR Logisches Oder mit übergesetztem doppeltem Makron +U+2A63 (10851) ⩣ LOGICAL OR WITH DOUBLE UNDERBAR Logisches Oder mit doppeltem Unterstrich +U+2A64 (10852) ⩤ Z NOTATION DOMAIN ANTIRESTRICTION +U+2A65 (10853) ⩥ Z NOTATION RANGE ANTIRESTRICTION +U+2A66 (10854) ⩦ EQUALS SIGN WITH DOT BELOW Gleichheitszeichen mit untergesetztem Punkt +U+2A67 (10855) ⩧ IDENTICAL WITH DOT ABOVE Kongruenzzeichen mit übergesetztem Punkt +U+2A68 (10856) ⩨ TRIPLE HORIZONTAL BAR WITH DOUBLE VERTICAL STROKE Doppelt durchgestrichenes Kongruenzzeichen +U+2A69 (10857) ⩩ TRIPLE HORIZONTAL BAR WITH TRIPLE VERTICAL STROKE Dreifach durchgestrichenes Kongruenzzeichen +U+2A6A (10858) ⩪ TILDE OPERATOR WITH DOT ABOVE Tildeoperator mit übergesetztem Punkt +U+2A6B (10859) ⩫ TILDE OPERATOR WITH RISING DOTS Tildeoperator mit Punkt rechts oben und links unten +U+2A6C (10860) ⩬ SIMILAR MINUS SIMILAR Tilde über Minuszeichen und Tilde +U+2A6D (10861) ⩭ CONGRUENT WITH DOT ABOVE Ungefähr-gleich-Zeichen mit übergesetztem Punkt +U+2A6E (10862) ⩮ EQUALS WITH ASTERISK Gleichheitszeichen mit übergesetztem Stern +U+2A6F (10863) ⩯ ALMOST EQUAL TO WITH CIRCUMFLEX ACCENT Fast-gleich-Zeichen mit übergesetztem Zirkumflex +U+2A70 (10864) ⩰ APPROXIMATELY EQUAL OR EQUAL TO fast gleich oder gleich +U+2A71 (10865) ⩱ EQUALS SIGN ABOVE PLUS SIGN Gleichheitszeichen über Pluszeichen +U+2A72 (10866) ⩲ PLUS SIGN ABOVE EQUALS SIGN Pluszeichen über Gleichheitszeichen +U+2A73 (10867) ⩳ EQUALS SIGN ABOVE TILDE OPERATOR Gleichheitszeichen über Tildeoperator +U+2A74 (10868) ⩴ DOUBLE COLON EQUAL Zwei Doppelpunkte und Gleichheitszeichen +U+2A75 (10869) ⩵ TWO CONSECUTIVE EQUALS SIGNS Zwei Gleichheitszeichen +U+2A76 (10870) ⩶ THREE CONSECUTIVE EQUALS SIGNS Drei Gleichheitszeichen +U+2A77 (10871) ⩷ EQUALS SIGN WITH TWO DOTS ABOVE AND TWO DOTS BELOW Gleichheitszeichen mit übergesetztem und untergesetztem Trema +U+2A78 (10872) ⩸ EQUIVALENT WITH FOUR DOTS ABOVE Äquivalenzzeichen mit vier übergesetzten Punkten +U+2A79 (10873) ⩹ LESS-THAN WITH CIRCLE INSIDE Kleiner-als-Zeichen mit Ring +U+2A7A (10874) ⩺ GREATER-THAN WITH CIRCLE INSIDE Größer-als-Zeichen mit Ring +U+2A7B (10875) ⩻ LESS-THAN WITH QUESTION MARK ABOVE Kleiner-als-Zeichen mit übergesetztem Fragezeichen +U+2A7C (10876) ⩼ GREATER-THAN WITH QUESTION MARK ABOVE Größer-als-Zeichen mit übergesetztem Fragezeichen +U+2A7D (10877) ⩽ LESS-THAN OR SLANTED EQUAL TO Schräges Kleiner-als oder gleich +U+2A7E (10878) ⩾ GREATER-THAN OR SLANTED EQUAL TO Schräges Größer-als oder gleich +U+2A7F (10879) ⩿ LESS-THAN OR SLANTED EQUAL TO WITH DOT INSIDE Schräges Kleiner-als oder gleich mit Punkt +U+2A80 (10880) ⪀ GREATER-THAN OR SLANTED EQUAL TO WITH DOT INSIDE Schräges Größer-als oder gleich mit Punkt +U+2A81 (10881) ⪁ LESS-THAN OR SLANTED EQUAL TO WITH DOT ABOVE Schräges Kleiner-als oder gleich mit übergesetztem Punkt +U+2A82 (10882) ⪂ GREATER-THAN OR SLANTED EQUAL TO WITH DOT ABOVE Schräges Größer-als oder gleich mit übergesetztem Punkt +U+2A83 (10883) ⪃ LESS-THAN OR SLANTED EQUAL TO WITH DOT ABOVE RIGHT Schräges Kleiner-als oder gleich mit Punkt rechts oben +U+2A84 (10884) ⪄ GREATER-THAN OR SLANTED EQUAL TO WITH DOT ABOVE LEFT Schräges Größer-als oder gleich mit Punkt links oben +U+2A85 (10885) ⪅ LESS-THAN OR APPROXIMATE Kleiner oder ungefähr gleich +U+2A86 (10886) ⪆ GREATER-THAN OR APPROXIMATE Größer oder ungefähr gleich +U+2A87 (10887) ⪇ LESS-THAN AND SINGLE-LINE NOT EQUAL TO Kleiner und nicht gleich +U+2A88 (10888) ⪈ GREATER-THAN AND SINGLE-LINE NOT EQUAL TO Größer und nicht gleich +U+2A89 (10889) ⪉ LESS-THAN AND NOT APPROXIMATE Echt kleiner und nicht ungefähr gleich +U+2A8A (10890) ⪊ GREATER-THAN AND NOT APPROXIMATE Echt größer und nicht ungefähr gleich +U+2A8B (10891) ⪋ LESS-THAN ABOVE DOUBLE-LINE EQUAL ABOVE GREATER-THAN Kleiner-als über Gleichheitszeichen über Größer-als +U+2A8C (10892) ⪌ GREATER-THAN ABOVE DOUBLE-LINE EQUAL ABOVE LESS-THAN Größer-als über Gleichheitszeichen über Kleiner-als +U+2A8D (10893) ⪍ LESS-THAN ABOVE SIMILAR OR EQUAL Kleiner als oder gleich oder ungefähr +U+2A8E (10894) ⪎ GREATER-THAN ABOVE SIMILAR OR EQUAL Größer als oder gleich oder ungefähr +U+2A8F (10895) ⪏ LESS-THAN ABOVE SIMILAR ABOVE GREATER-THAN Kleiner-als über ungefähr über Größer-als +U+2A90 (10896) ⪐ GREATER-THAN ABOVE SIMILAR ABOVE LESS-THAN Größer-als über ungefähr über Kleiner-als +U+2A91 (10897) ⪑ LESS-THAN ABOVE GREATER-THAN ABOVE DOUBLE-LINE EQUAL Kleiner-als über Größer-als über Gleichheitszeichen +U+2A92 (10898) ⪒ GREATER-THAN ABOVE LESS-THAN ABOVE DOUBLE-LINE EQUAL Größer-als über Kleiner-als über Gleichheitszeichen +U+2A93 (10899) ⪓ LESS-THAN ABOVE SLANTED EQUAL ABOVE GREATER-THAN ABOVE SLANTED EQUAL +U+2A94 (10900) ⪔ GREATER-THAN ABOVE SLANTED EQUAL ABOVE LESS-THAN ABOVE SLANTED EQUAL +U+2A95 (10901) ⪕ SLANTED EQUAL TO OR LESS-THAN +U+2A96 (10902) ⪖ SLANTED EQUAL TO OR GREATER-THAN +U+2A97 (10903) ⪗ SLANTED EQUAL TO OR LESS-THAN WITH DOT INSIDE +U+2A98 (10904) ⪘ SLANTED EQUAL TO OR GREATER-THAN WITH DOT INSIDE +U+2A99 (10905) ⪙ DOUBLE-LINE EQUAL TO OR LESS-THAN +U+2A9A (10906) ⪚ DOUBLE-LINE EQUAL TO OR GREATER-THAN +U+2A9B (10907) ⪛ DOUBLE-LINE SLANTED EQUAL TO OR LESS-THAN +U+2A9C (10908) ⪜ DOUBLE-LINE SLANTED EQUAL TO OR GREATER-THAN +U+2A9D (10909) ⪝ SIMILAR OR LESS-THAN Ungefähr oder kleiner als +U+2A9E (10910) ⪞ SIMILAR OR GREATER-THAN Ungefähr oder größer als +U+2A9F (10911) ⪟ SIMILAR ABOVE LESS-THAN ABOVE EQUALS SIGN +U+2AA0 (10912) ⪠ SIMILAR ABOVE GREATER-THAN ABOVE EQUALS SIGN +U+2AA1 (10913) ⪡ DOUBLE NESTED LESS-THAN Doppeltes geschachteltes Kleiner-als +U+2AA2 (10914) ⪢ DOUBLE NESTED GREATER-THAN Doppeltes geschachteltes Größer-als +U+2AA3 (10915) ⪣ DOUBLE NESTED LESS-THAN WITH UNDERBAR Doppeltes geschachteltes Kleiner-als mit Unterstrich +U+2AA4 (10916) ⪤ GREATER-THAN OVERLAPPING LESS-THAN Größer-als und Kleiner-als überlappend +U+2AA5 (10917) ⪥ GREATER-THAN BESIDE LESS-THAN Größer-als und Kleiner-als nebeneinander +U+2AA6 (10918) ⪦ LESS-THAN CLOSED BY CURVE +U+2AA7 (10919) ⪧ GREATER-THAN CLOSED BY CURVE +U+2AA8 (10920) ⪨ LESS-THAN CLOSED BY CURVE ABOVE SLANTED EQUAL +U+2AA9 (10921) ⪩ GREATER-THAN CLOSED BY CURVE ABOVE SLANTED EQUAL +U+2AAA (10922) ⪪ SMALLER THAN +U+2AAB (10923) ⪫ LARGER THAN +U+2AAC (10924) ⪬ SMALLER THAN OR EQUAL TO +U+2AAD (10925) ⪭ LARGER THAN OR EQUAL TO +U+2AAE (10926) ⪮ EQUALS SIGN WITH BUMPY ABOVE +U+2AAF (10927) ⪯ PRECEDES ABOVE SINGLE-LINE EQUALS SIGN Vorgänger oder gleich +U+2AB0 (10928) ⪰ SUCCEEDS ABOVE SINGLE-LINE EQUALS SIGN Nachfolger oder gleich +U+2AB1 (10929) ⪱ PRECEDES ABOVE SINGLE-LINE NOT EQUAL TO Vorgänger und nicht gleich +U+2AB2 (10930) ⪲ SUCCEEDS ABOVE SINGLE-LINE NOT EQUAL TO Nachfolger und nicht gleich +U+2AB3 (10931) ⪳ PRECEDES ABOVE EQUALS SIGN +U+2AB4 (10932) ⪴ SUCCEEDS ABOVE EQUALS SIGN +U+2AB5 (10933) ⪵ PRECEDES ABOVE NOT EQUAL TO +U+2AB6 (10934) ⪶ SUCCEEDS ABOVE NOT EQUAL TO +U+2AB7 (10935) ⪷ PRECEDES ABOVE ALMOST EQUAL TO Vorgänger oder ungefähr +U+2AB8 (10936) ⪸ SUCCEEDS ABOVE ALMOST EQUAL TO Nachfolger oder ungefähr +U+2AB9 (10937) ⪹ PRECEDES ABOVE NOT ALMOST EQUAL TO Vorgänger und nicht ungefähr +U+2ABA (10938) ⪺ SUCCEEDS ABOVE NOT ALMOST EQUAL TO Nachfolger und nicht ungefähr +U+2ABB (10939) ⪻ DOUBLE PRECEDES Doppeltes Vorgänger-Zeichen +U+2ABC (10940) ⪼ DOUBLE SUCCEEDS Doppeltes Nachfolger-Zeichen +U+2ABD (10941) ⪽ SUBSET WITH DOT Teilmenge mit innenliegendem Punkt +U+2ABE (10942) ⪾ SUPERSET WITH DOT Obermenge mit innenliegendem Punkt +U+2ABF (10943) ⪿ SUBSET WITH PLUS SIGN BELOW Teilmenge mit darunterliegendem Pluszeichen +U+2AC0 (10944) ⫀ SUPERSET WITH PLUS SIGN BELOW Obermenge mit darunterliegendem Pluszeichen +U+2AC1 (10945) ⫁ SUBSET WITH MULTIPLICATION SIGN BELOW Teilmenge mit darunterliegendem Multiplikationszeichen (Kreuzprodukt) +U+2AC2 (10946) ⫂ SUPERSET WITH MULTIPLICATION SIGN BELOW Obermenge mit darunterliegendem Multiplikationszeichen (Kreuzprodukt) +U+2AC3 (10947) ⫃ SUBSET OF OR EQUAL TO WITH DOT ABOVE Teilmenge oder gleich mit darüberliegendem Punkt +U+2AC4 (10948) ⫄ SUPERSET OF OR EQUAL TO WITH DOT ABOVE Obermenge oder gleich mit darüberliegendem Punkt +U+2AC5 (10949) ⫅ SUBSET OF ABOVE EQUALS SIGN Teilmenge mit darunterliegendem Gleichheitszeichen +U+2AC6 (10950) ⫆ SUPERSET OF ABOVE EQUALS SIGN Obermenge mit darunterliegendem Gleichheitszeichen +U+2AC7 (10951) ⫇ SUBSET OF ABOVE TILDE OPERATOR Teilmenge mit darunterliegender Tilde +U+2AC8 (10952) ⫈ SUPERSET OF ABOVE TILDE OPERATOR Obermenge mit darunterliegender Tilde +U+2AC9 (10953) ⫉ SUBSET OF ABOVE ALMOST EQUAL TO Teilmenge mit darunterliegendem Ungefähr-gleich-Zeichen +U+2ACA (10954) ⫊ SUPERSET OF ABOVE ALMOST EQUAL TO Obermenge mit darunterliegendem Ungefähr-gleich-Zeichen +U+2ACB (10955) ⫋ SUBSET OF ABOVE NOT EQUAL TO Echte Teilmenge +U+2ACC (10956) ⫌ SUPERSET OF ABOVE NOT EQUAL TO Echte Obermenge +U+2ACD (10957) ⫍ SQUARE LEFT OPEN BOX OPERATOR +U+2ACE (10958) ⫎ SQUARE RIGHT OPEN BOX OPERATOR +U+2ACF (10959) ⫏ CLOSED SUBSET Geschlossenes Teilmengenzeichen +U+2AD0 (10960) ⫐ CLOSED SUPERSET Geschlossenes Obermengenzeichen +U+2AD1 (10961) ⫑ CLOSED SUBSET OR EQUAL TO Geschlossenes echtes Teilmengenzeichen +U+2AD2 (10962) ⫒ CLOSED SUPERSET OR EQUAL TO Geschlossenes echtes Obermengenzeichen +U+2AD3 (10963) ⫓ SUBSET ABOVE SUPERSET Teilmengenzeichen über Obermengenzeichen +U+2AD4 (10964) ⫔ SUPERSET ABOVE SUBSET Obermengenzeichen über Teilmengenzeichen +U+2AD5 (10965) ⫕ SUBSET ABOVE SUBSET Zwei Teilmengenzeichen übereinander +U+2AD6 (10966) ⫖ SUPERSET ABOVE SUPERSET Zwei Obermengenzeichen übereinander +U+2AD7 (10967) ⫗ SUPERSET BESIDE SUBSET Obermengenzeichen und Teilmengenzeichen nebeneinander +U+2AD8 (10968) ⫘ SUPERSET BESIDE AND JOINED BY DASH WITH SUBSET +U+2AD9 (10969) ⫙ ELEMENT OF OPENING DOWNWARDS Ist-Element-von mit Öffnung nach unten +U+2ADA (10970) ⫚ PITCHFORK WITH TEE TOP +U+2ADB (10971) ⫛ TRANSVERSAL INTERSECTION +U+2ADC (10972) ⫝̸ FORKING +U+2ADD (10973) ⫝ NONFORKING +U+2ADE (10974) ⫞ SHORT LEFT TACK +U+2ADF (10975) ⫟ SHORT DOWN TACK +U+2AE0 (10976) ⫠ SHORT UP TACK +U+2AE1 (10977) ⫡ PERPENDICULAR WITH S +U+2AE2 (10978) ⫢ VERTICAL BAR TRIPLE RIGHT TURNSTILE +U+2AE3 (10979) ⫣ DOUBLE VERTICAL BAR LEFT TURNSTILE +U+2AE4 (10980) ⫤ VERTICAL BAR DOUBLE LEFT TURNSTILE +U+2AE5 (10981) ⫥ DOUBLE VERTICAL BAR DOUBLE LEFT TURNSTILE +U+2AE6 (10982) ⫦ LONG DASH FROM LEFT MEMBER OF DOUBLE VERTICAL +U+2AE7 (10983) ⫧ SHORT DOWN TACK WITH OVERBAR +U+2AE8 (10984) ⫨ SHORT UP TACK WITH UNDERBAR +U+2AE9 (10985) ⫩ SHORT UP TACK ABOVE SHORT DOWN TACK +U+2AEA (10986) ⫪ DOUBLE DOWN TACK +U+2AEB (10987) ⫫ DOUBLE UP TACK Stochastische Unabhängigkeit +U+2AEC (10988) ⫬ DOUBLE STROKE NOT SIGN +U+2AED (10989) ⫭ REVERSED DOUBLE STROKE NOT SIGN +U+2AEE (10990) ⫮ DOES NOT DIVIDE WITH REVERSED NEGATION SLASH Ist-nicht-Teiler-von mit umgedrehtem Negationsschrägstrich +U+2AEF (10991) ⫯ VERTICAL LINE WITH CIRCLE ABOVE +U+2AF0 (10992) ⫰ VERTICAL LINE WITH CIRCLE BELOW +U+2AF1 (10993) ⫱ DOWN TACK WITH CIRCLE BELOW +U+2AF2 (10994) ⫲ PARALLEL WITH HORIZONTAL STROKE +U+2AF3 (10995) ⫳ PARALLEL WITH TILDE OPERATOR +U+2AF4 (10996) ⫴ TRIPLE VERTICAL BAR BINARY RELATION +U+2AF5 (10997) ⫵ TRIPLE VERTICAL BAR WITH HORIZONTAL STROKE +U+2AF6 (10998) ⫶ TRIPLE COLON OPERATOR +U+2AF7 (10999) ⫷ TRIPLE NESTED LESS-THAN Dreifaches geschachteltes kleiner-als +U+2AF8 (11000) ⫸ TRIPLE NESTED GREATER-THAN Dreifaches geschachteltes größer-als +U+2AF9 (11001) ⫹ DOUBLE-LINE SLANTED LESS-THAN OR EQUAL TO +U+2AFA (11002) ⫺ DOUBLE-LINE SLANTED GREATER-THAN OR EQUAL TO +U+2AFB (11003) ⫻ TRIPLE SOLIDUS BINARY RELATION Dreifacher Schrägstrich +U+2AFC (11004) ⫼ LARGE TRIPLE VERTICAL BAR OPERATOR +U+2AFD (11005) ⫽ DOUBLE SOLIDUS OPERATOR Doppelter Schrägstrich +U+2AFE (11006) ⫾ WHITE VERTICAL BAR Hohler vertikaler Balken (Dijkstra-Notation) +U+2AFF (11007) ⫿ N-ARY WHITE VERTICAL BAR N-stufiger hohler vertikaler Balken (Dijkstra-Notation) +*/ +/* PLAN A +U+27C0 (10176) ⟀ mathematisches Symbol THREE DIMENSIONAL ANGLE Dreidimensionaler Winkel +U+27C1 (10177) ⟁ mathematisches Symbol WHITE TRIANGLE CONTAINING SMALL WHITE TRIANGLE Weißes Dreieck in einem weißen Dreieck +U+27C2 (10178) ⟂ mathematisches Symbol PERPENDICULAR ist orthogonal zu +U+27C3 (10179) ⟃ mathematisches Symbol OPEN SUBSET Offene Teilmenge +U+27C4 (10180) ⟄ mathematisches Symbol OPEN SUPERSET Offene Obermenge +U+27C5 (10181) ⟅ öffnende Punktierung (eines Paars) LEFT S-SHAPED BAG DELIMITER Linkes s-förmiges Trennzeichen für Multimengen +U+27C6 (10182) ⟆ schließende Punktierung (eines Paars) RIGHT S-SHAPED BAG DELIMITER Rechtes s-förmiges Trennzeichen für Multimengen +U+27C7 (10183) ⟇ mathematisches Symbol OR WITH DOT INSIDE Logisches Oder mit Punkt +U+27C8 (10184) ⟈ mathematisches Symbol REVERSE SOLIDUS PRECEDING SUBSET Umgekehrter Schrägstrich gefolgt von Teilmenge +U+27C9 (10185) ⟉ mathematisches Symbol SUPERSET PRECEDING SOLIDUS Obermenge gefolgt von einem Schrägstrich +U+27CA (10186) ⟊ mathematisches Symbol VERTICAL BAR WITH HORIZONTAL STROKE Senkrechter Strich mit Querstrich +U+27CB (10187) ⟋ mathematisches Symbol MATHEMATICAL RISING DIAGONAL Mathematische steigende Diagonale +U+27CC (10188) ⟌ mathematisches Symbol LONG DIVISION Langes Divisionszeichen +U+27CD (10189) ⟍ mathematisches Symbol MATHEMATICAL FALLING DIAGONAL Mathematische fallende Diagonale +U+27CE (10190) ⟎ mathematisches Symbol SQUARED LOGICAL AND Logisches Und im Quadrat +U+27CF (10191) ⟏ mathematisches Symbol SQUARED LOGICAL OR Logisches Oder im Quadrat +U+27D0 (10192) ⟐ mathematisches Symbol WHITE DIAMOND WITH CENTRED DOT Weißes Karo mit Punkt in der Mitte +U+27D1 (10193) ⟑ mathematisches Symbol AND WITH DOT Logisches Und mit Punkt +U+27D2 (10194) ⟒ mathematisches Symbol ELEMENT OF OPENING UPWARDS Nach oben zeigendes Elementzeichen +U+27D3 (10195) ⟓ mathematisches Symbol LOWER RIGHT CORNER WITH DOT Untere rechte Ecke mit Punkt +U+27D4 (10196) ⟔ mathematisches Symbol UPPER LEFT CORNER WITH DOT Obere rechte Ecke mit Punkt +U+27D5 (10197) ⟕ mathematisches Symbol LEFT OUTER JOIN Linker äußerer Verbund +U+27D6 (10198) ⟖ mathematisches Symbol RIGHT OUTER JOIN Rechter äußerer Verbund +U+27D7 (10199) ⟗ mathematisches Symbol FULL OUTER JOIN Voller äußerer Verbund +U+27D8 (10200) ⟘ mathematisches Symbol LARGE UP TACK Große nach oben zeigende Reißzwecke +U+27D9 (10201) ⟙ mathematisches Symbol LARGE DOWN TACK Große nach unten zeigende Reißzwecke +U+27DA (10202) ⟚ mathematisches Symbol LEFT AND RIGHT DOUBLE TURNSTILE Linkes und rechtes doppeltes Drehkreuz +U+27DB (10203) ⟛ mathematisches Symbol LEFT AND RIGHT TACK Nach links und nach rechts zeigende Reißzwecke +U+27DC (10204) ⟜ mathematisches Symbol LEFT MULTIMAP Linke Mehrfachzuordnung +U+27DD (10205) ⟝ mathematisches Symbol LONG RIGHT TACK Lange nach rechts zeigende Reißzwecke +U+27DE (10206) ⟞ mathematisches Symbol LONG LEFT TACK Lange nach links zeigende Reißzwecke +U+27DF (10207) ⟟ mathematisches Symbol UP TACK WITH CIRCLE ABOVE Nach oben zeigende Reißzwecke mit übergesetztem Kreis +U+27E0 (10208) ⟠ mathematisches Symbol LOZENGE DIVIDED BY HORIZONTAL RULE Durch horizontale Linie geteilter Rhombus +U+27E1 (10209) ⟡ mathematisches Symbol WHITE CONCAVE-SIDED DIAMOND Weißes Karo mit konkaven Seiten +U+27E2 (10210) ⟢ mathematisches Symbol WHITE CONCAVE-SIDED DIAMOND WITH LEFTWARDS TICK Weißes Karo mit konkaven Seiten mit nach links zeigendem Strichlein +U+27E3 (10211) ⟣ mathematisches Symbol WHITE CONCAVE-SIDED DIAMOND WITH RIGHTWARDS TICK Weißes Karo mit konkaven Seiten mit nach rechts zeigendem Strichlein +U+27E4 (10212) ⟤ mathematisches Symbol WHITE SQUARE WITH LEFTWARDS TICK Weißes Quadrat mit nach links zeigendem Strichlein +U+27E5 (10213) ⟥ mathematisches Symbol WHITE SQUARE WITH RIGHTWARDS TICK Weißes Quadrat mit nach rechts zeigendem Strichlein +U+27E6 (10214) ⟦ öffnende Punktierung (eines Paars) MATHEMATICAL LEFT WHITE SQUARE BRACKET Mathematische öffnende weiße eckige Klammer +U+27E7 (10215) ⟧ schließende Punktierung (eines Paars) MATHEMATICAL RIGHT WHITE SQUARE BRACKET Mathematische schließende weiße eckige Klammer +U+27E8 (10216) ⟨ öffnende Punktierung (eines Paars) MATHEMATICAL LEFT ANGLE BRACKET Mathematische öffnende spitze Klammer +U+27E9 (10217) ⟩ schließende Punktierung (eines Paars) MATHEMATICAL RIGHT ANGLE BRACKET Mathematische schließende spitze Klammer +U+27EA (10218) ⟪ öffnende Punktierung (eines Paars) MATHEMATICAL LEFT DOUBLE ANGLE BRACKET Mathematische öffnende doppelte spitze Klammer +U+27EB (10219) ⟫ schließende Punktierung (eines Paars) MATHEMATICAL RIGHT DOUBLE ANGLE BRACKET Mathematische schließende doppelte spitze Klammer +U+27EC (10220) ⟬ öffnende Punktierung (eines Paars) MATHEMATICAL LEFT WHITE TORTOISE SHELL BRACKET Mathematische öffnende hohle stumpfe Klammer +U+27ED (10221) ⟭ schließende Punktierung (eines Paars) MATHEMATICAL RIGHT WHITE TORTOISE SHELL BRACKET Mathematische schließende hohle stumpfe Klammer +U+27EE (10222) ⟮ öffnende Punktierung (eines Paars) MATHEMATICAL LEFT FLATTENED PARENTHESIS Mathematische öffnende abgeflachte runde Klammer +U+27EF (10223) ⟯ schließende Punktierung (eines Paars) MATHEMATICAL RIGHT FLATTENED PARENTHESIS Mathematische schließende abgeflachte runde Klammer +*/ -IMP -: '->' | '\u2192' - ; +SEQARROW : '==>' | '\u27F9'; +NOT_EQUALS : '!=' OP_SFX* | '\u2260'; +APPROXIMATELY_BUT_NOT_ACTUALLY_EQUAL_TO : '\u2246'; // (8774) ≆ APPROXIMATELY BUT NOT ACTUALLY EQUAL TO ungefähr, aber nicht genau gleich +NEITHER_APPROXIMATELY_NOR_ACTUALLY_EQUAL_TO : '\u2247'; // (8775) ≇ NEITHER APPROXIMATELY NOR ACTUALLY EQUAL TO weder ungefähr noch genau gleich +NOT_IDENTICAL_TO : '\u2262'; // (8802) ≢ NOT IDENTICAL TO ist nicht kongruent zu -EQUALS -: '=' - ; +IMP : '->' | '\u2192'; +AT : '@' OP_SFX*; +OR : '|' OP_SFX? | '\u2228'; +SQUARE_CUP : '\u2294' | '\\sqcup'; // (8852) ⊔ SQUARE CUP nach oben geöffnetes Viereck -NOT_EQUALS -: '!=' | '\u2260' - ; +AND : '&' OP_SFX? | '\u2227'; +SQUARE_CAP : '\u2293' | '\\sqcap'; // (8851) ⊓ SQUARE CAP nach unten geöffnetes Viereck -SEQARROW -: '==>' | '\u27F9' - ; -EXP -: '^' - ; +NOT : '!' (OP_SFX|'!')? | '\u00AC'; +EQUALS : '=' OP_SFX?; +IDENTICAL_TO : '\u2261' | '\\equiv'; // (8801) ≡ IDENTICAL TO ist kongruent zu +CIRCLED_EQUALS : '\u229C'; // (8860) ⊜ CIRCLED EQUALS eingekreistes Gleichheitszeichen -TILDE -: '~' - ; +EXP : '^' OP_SFX?; +TILDE : ('~'|'\u223C') OP_SFX?; -PERCENT -: '%' - ; -STAR -: '*' - ; +SLASH : '/' OP_SFX*; +CIRCLED_DIVISION_SLASH : '\u2298'; // (8856) ⊘ CIRCLED DIVISION SLASH eingekreister Divisionsstrich -MINUS -: '-' - ; -PLUS -: '+' - ; +PERCENT : '%' OP_SFX?; +CIRCLED_RING_OPERATOR : '\u229A'; // (8858) ⊚ CIRCLED RING OPERATOR eingekreister Ringoperator -GREATER -: '>' - ; +STAR : '*' OP_SFX?; +CIRCLED_TIMES : '\u2297'; // (8855) ⊗ CIRCLED TIMES eingekreistes Multiplikationszeichen +CIRCLED_DOT_OPERATOR : '\u2299'; // (8857) ⊙ CIRCLED DOT OPERATOR eingekreister Punktoperator +CIRCLED_ASTERISK_OPERATOR : '\u229B'; // (8859) ⊛ CIRCLED ASTERISK OPERATOR eingekreister Sternoperator +SQUARED_TIMES :' \u22A0'; // (8864) ⊠ SQUARED TIMES eingerahmtes Multiplikationszeichen +SQUARED_DOT_OPERATOR : '\u22A1'; // (8865) ⊡ SQUARED DOT OPERATOR eingerahmter Punktoperator -GREATEREQUAL -: '>' '=' | '\u2265' - ; +MINUS : '-' OP_SFX?; +CIRCLED_DASH : '\u229D'; // (8861) ⊝ CIRCLED DASH eingekreister Gedankenstrich +SQUARED_MINUS : '\u229F'; // (8863) ⊟ SQUARED MINUS eingerahmtes Minuszeichen +CIRCLED_MINUS : '\u2296'; // (8854) ⊖ CIRCLED MINUS eingekreistes Minuszeichen +PLUS : '+' OP_SFX?; +CIRCLED_PLUS : '\u2295'; // (8853) ⊕ CIRCLED PLUS eingekreistes Pluszeichen +SQUARED_PLUS : '\u229E'; // (8862) ⊞ SQUARED PLUS eingerahmtes Pluszeichen -WS: [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace -STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ; -LESS: '<'; -LESSEQUAL: '<' '=' | '\u2264'; LGUILLEMETS: '<' '<' | '«' | '‹'; RGUILLEMETS: '>''>' | '»' | '›'; +GREATEREQUAL: '>' '=' | '\u2265'; +EQV : '<->' | '\u2194'; +LESSEQUAL : '<' '=' | '\u2264'; + + +LESS : '<' OP_SFX?; +LESS_THAN_WITH_DOT : '\u22D6'; // (8918) ⋖ LESS-THAN WITH DOT kleiner als mit Punkt +VERY_MUCH_LESS_THAN : '\u22D8'; // (8920) ⋘ VERY MUCH LESS-THAN Sehr viel kleiner als +LESS_THAN_EQUAL_TO_OR_GREATER_THAN: '\u22DA'; // (8922) ⋚ LESS-THAN EQUAL TO OR GREATER-THAN kleiner als, gleich oder größer als +EQUAL_TO_OR_LESS_THAN : '\u22DC'; // (8924) ⋜ EQUAL TO OR LESS-THAN gleich oder kleiner als +EQUAL_TO_OR_PRECEDES : '\u22DE'; // (8926) ⋞ EQUAL TO OR PRECEDES gleich oder vorangehend +DOES_NOT_PRECEDE_OR_EQUAL : '\u22E0'; // (8928) ⋠ DOES NOT PRECEDE OR EQUAL weder vorangehend oder gleich +NOT_SQUARE_IMAGE_OF_OR_EQUAL_TO : '\u22E2'; // (8930) ⋢ NOT SQUARE IMAGE OF OR EQUAL TO kein viereckiges Bild oder gleich +SQUARE_IMAGE_OF_OR_NOT_EQUAL_TO : '\u22E4'; // (8932) ⋤ SQUARE IMAGE OF OR NOT EQUAL TO viereckiges Bild oder ungleich +PRECEDES : '\u227A'; // (8826) ≺ PRECEDES vorangehend +PRECEDES_OR_EQUAL_TO : '\u227C'; // (8828) ≼ PRECEDES OR EQUAL TO vorangehend oder gleich +PRECEDES_OR_EQUIVALENT_TO : '\u227E'; // (8830) ≾ PRECEDES OR EQUIVALENT TO vorangehend oder äquivalent +NOT_A_SUBSET_OF : '\u2284'; // (8836) ⊄ NOT A SUBSET OF ist keine ;// (echte) Teilmenge von +SUBSET_OF_OR_EQUAL_TO : '\u2286' | '\\subseteq'; // (8838) ⊆ SUBSET OF OR EQUAL TO Teilmenge oder gleich + + +GREATER : '>' OP_SFX?; +SQUARE_ORIGINAL : '\u2290'; // (8848) ⊐ SQUARE ORIGINAL OF viereckiges Original +SQUARE_ORIGINAL_OF_OR_EQUAL_TO : '\u2292'; // (8850) ⊒ SQUARE ORIGINAL OF OR EQUAL TO viereckiges Original oder gleich +GREATER_THAN_WITH_DOT : '\u22D7' | '\\gedot'; // (8919) ⋗ GREATER-THAN WITH DOT größer als mit Punkt +VERY_MUCH_GREATER_THAN : '\u22D9' | '\\gg' ; // (8921) ⋙ VERY MUCH GREATER-THAN sehr viel größer als +GREATER_THAN_EQUAL_TO_OR_LESS_THAN : '\u22DB'; // (8923) ⋛ GREATER-THAN EQUAL TO OR LESS-THAN größer als, gleich oder kleiner als +EQUAL_TO_OR_GREATER_THAN : '\u22DD'; // (8925) ⋝ EQUAL TO OR GREATER-THAN gleich oder größer als +EQUAL_TO_OR_SUCCEEDS : '\u22DF'; // (8927) ⋟ EQUAL TO OR SUCCEEDS gleich oder nachfolgend +DOES_NOT_SUCCEED_OR_EQUAL : '\u22E1'; // (8929) ⋡ DOES NOT SUCCEED OR EQUAL weder nachfolgend oder gleich +NOT_SQUARE_ORIGINAL_OF_OR_EQUAL_TO : '\u22E3'; // (8931) ⋣ NOT SQUARE ORIGINAL OF OR EQUAL TO kein viereckiges Original oder gleich +SQUARE_ORIGINAL_OF_OR_NOT_EQUAL_TO : '\u22E5'; // (8933) ⋥ SQUARE ORIGINAL OF OR NOT EQUAL TO viereckiges Original oder ungleich +SUCCEEDS : '\u227B'; // (8827) ≻ SUCCEEDS nachfolgend +SUCCEEDS_OR_EQUAL_TO : '\u227D'; // (8829) ≽ SUCCEEDS OR EQUAL TO nachfolgend oder gleich +SUCCEEDS_OR_EQUIVALENT_TO : '\u227F'; // (8831) ≿ SUCCEEDS OR EQUIVALENT TO nachfolgend oder äquivalent +DOES_NOT_PRECEDE : '\u2280'; // (8832) ⊀ DOES NOT PRECEDE nicht vorangehend +DOES_NOT_SUCCEED : '\u2281'; // (8833) ⊁ DOES NOT SUCCEED nicht nachfolgend +SUPERSET_OF : '\u2283'; // (8835) ⊃ SUPERSET OF ist ;// (echte) Obermenge von +NOT_A_SUPERSET_OF : '\u2285'; // (8837) ⊅ NOT A SUPERSET OF ist keine ;// (echte) Obermenge von +SUPERSET_OF_OR_EQUAL_TO : '\u2287'; // (8839) ⊇ SUPERSET OF OR EQUAL TO Obermenge oder gleich +SQUARE_IMAGE_OF : '\u228F'; // (8847) ⊏ SQUARE IMAGE OF viereckiges Bild +SQUARE_IMAGE_OF_OR_EQUAL_TO : '\u2291'; // (8849) ⊑ SQUARE IMAGE OF OR EQUAL TO viereckiges Bild oder gleich + + IMPLICIT_IDENT: '<' (LETTER)+ '>' ('$lmtd')? -> type(IDENT); +PRIMES : ('\'')+; +CHAR_LITERAL: '\'' + ((' '..'&') | + ('('..'[') | + (']'..'~') | + ('\\' ('\'' | '\\' | 'n' | 'r' | 't' | 'b' | 'f' | '"' | 'u' HEX )) + ) + '\'' +; -EQV: '<->' | '\u2194'; -PRIMES: ('\'')+; -CHAR_LITERAL -: '\'' - ((' '..'&') | - ('('..'[') | - (']'..'~') | - ('\\' ('\'' | '\\' | 'n' | 'r' | 't' | 'b' | 'f' | '"' | 'u' HEX )) - ) - '\'' - ; +WS: [ \t\n\r\u00a0]+ -> channel(HIDDEN); //'\u00A0 = non breakable whitespace +STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ; QUOTED_STRING_LITERAL : '"' ('\\' . | '\n' | ~('\n' | '"' | '\\') )* '"' ; -SL_COMMENT -: - '//' - (~('\n' | '\uFFFF'))* ('\n' | '\uFFFF' | EOF) -> channel(HIDDEN) -; - -DOC_COMMENT: '/*!' -> more, pushMode(docComment); -ML_COMMENT: '/*' -> more, pushMode(COMMENT); BIN_LITERAL: '0' 'b' ('0' | '1' | '_')+ ('l'|'L')?; HEX_LITERAL: '0' 'x' (DIGIT | 'a'..'f' | 'A'..'F' | '_')+ ('l'|'L')?; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 2a2926ea015..b66d3329601 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -123,7 +123,7 @@ oneof_sorts keyjavatype : - type = simple_ident_dots (EMPTYBRACKETS)* + type = simple_ident_dots (LBRACKET RBRACKET)* ; prog_var_decls @@ -211,6 +211,7 @@ pred_decl pred_name = funcpred_name (whereToBind=where_to_bind)? argSorts=arg_sorts + functionMetaData? SEMI ; @@ -227,6 +228,7 @@ func_decl func_name = funcpred_name whereToBind=where_to_bind? argSorts = arg_sorts + functionMetaData? SEMI ; @@ -260,15 +262,20 @@ datatype_constructor: )? ; + +infixOperator: (opComparison|opWeak|opEqualities|opStrong1|opStrong2|opConjunction|opDisjunction); +functionMetaData +: + INFIX LPAREN infixOperator+ RPAREN #infixMetaData + | PREFIX LPAREN (opUnaryTerm)* RPAREN #prefixMetaData + | POSTFIX LPAREN (AT) RPAREN #postfixMetaData + | SHORTCUT LPAREN IDENT RPAREN #shortcutMetaData +; + func_decls - : - FUNCTIONS - LBRACE - ( - func_decl - ) * - RBRACE - ; +: + FUNCTIONS LBRACE (func_decl)* RBRACE +; // like arg_sorts but admits also the keyword "\formula" @@ -298,13 +305,12 @@ transform_decl SEMI ; - transform_decls: TRANSFORMERS LBRACE (transform_decl)* RBRACE ; arrayopid: - EMPTYBRACKETS LPAREN componentType=keyjavatype RPAREN + LBRACKET RBRACKET LPAREN componentType=keyjavatype RPAREN ; arg_sorts: @@ -326,7 +332,7 @@ ruleset_decls sortId : - id=simple_ident_dots (EMPTYBRACKETS)* + id=simple_ident_dots (LBRACKET RBRACKET)* ; id_declaration @@ -362,26 +368,61 @@ literals: | emptyset ; -emptyset: UTF_EMPTY; +opEqualities : NOT_EQUALS | EQUALS | APPROXIMATELY_BUT_NOT_ACTUALLY_EQUAL_TO + | NEITHER_APPROXIMATELY_NOR_ACTUALLY_EQUAL_TO + | NOT_IDENTICAL_TO | IDENTICAL_TO | CIRCLED_EQUALS + | NOT_PARALLEL_TO | PARALLEL_TO | NOT_DIVIDES | DIVIDES + | NOT_ASYMPTOTICALLY_EQUAL_TO | ASYMPTOTICALLY_EQUAL_TO + ; +opComparison: LESS | LESSEQUAL | GREATER | GREATEREQUAL | PRECEDES | SUBSET | SET_IN + | LESS_THAN_WITH_DOT | VERY_MUCH_LESS_THAN | LESS_THAN_EQUAL_TO_OR_GREATER_THAN | EQUAL_TO_OR_LESS_THAN + | EQUAL_TO_OR_PRECEDES |DOES_NOT_PRECEDE_OR_EQUAL | NOT_SQUARE_IMAGE_OF_OR_EQUAL_TO + | SQUARE_IMAGE_OF_OR_NOT_EQUAL_TO | PRECEDES| PRECEDES_OR_EQUAL_TO | PRECEDES_OR_EQUIVALENT_TO + | NOT_A_SUBSET_OF | SUBSET_OF_OR_EQUAL_TO | SQUARE_ORIGINAL | SQUARE_ORIGINAL_OF_OR_EQUAL_TO + | GREATER_THAN_WITH_DOT | VERY_MUCH_GREATER_THAN | GREATER_THAN_EQUAL_TO_OR_LESS_THAN + | EQUAL_TO_OR_GREATER_THAN | EQUAL_TO_OR_SUCCEEDS| DOES_NOT_SUCCEED_OR_EQUAL + | NOT_SQUARE_ORIGINAL_OF_OR_EQUAL_TO | SQUARE_ORIGINAL_OF_OR_NOT_EQUAL_TO | SUCCEEDS + | SUCCEEDS_OR_EQUAL_TO | SUCCEEDS_OR_EQUIVALENT_TO | DOES_NOT_PRECEDE | DOES_NOT_SUCCEED | SUPERSET_OF + | NOT_A_SUPERSET_OF | SUPERSET_OF_OR_EQUAL_TO | SQUARE_IMAGE_OF| SQUARE_IMAGE_OF_OR_EQUAL_TO + ; + +opWeak : PLUS|MINUS|UNION|INTERSECT|SETMINUS + | CIRCLED_DASH | SQUARED_MINUS | CIRCLED_MINUS + | CIRCLED_PLUS | SQUARED_PLUS | MINUS_TILDE | NOT_TILDE + | MINUS_OR_PLUS | DOT_PLUS + ; + + +opStrong1 : STAR | CIRCLED_TIMES | CIRCLED_DOT_OPERATOR | CIRCLED_ASTERISK_OPERATOR | SQUARED_TIMES | SQUARED_DOT_OPERATOR + | WREATH_PRODUCT | SINE_WAVE | INVERTED_LAZY_S | REVERSE_TILDE | HOMOTHETIC | GEOMETRIC_PROPORTION | EXCESS + | DOT_MINUS | PROPORTION | RATION | BECAUSE | THEREFORE | ASTERISK + ; + +opStrong2 : PERCENT | SLASH | CIRCLED_DIVISION_SLASH | CIRCLED_RING_OPERATOR | CDOT | RING; +opConjunction: AND; +opDisjunction: OR; +opUnaryTerm: MINUS | TILDE ; + +emptyset: EMPTY; term: parallel_term; // weigl: should normally be equivalence_term //labeled_term: a=parallel_term (LGUILLEMETS labels=label RGUILLEMETS)?; parallel_term: a=elementary_update_term (PARALLEL b=elementary_update_term)*; elementary_update_term: a=equivalence_term (ASSIGN b=equivalence_term)?; equivalence_term: a=implication_term (EQV b+=implication_term)*; implication_term: a=disjunction_term (IMP b=implication_term)?; -disjunction_term: a=conjunction_term (OR b+=conjunction_term)*; -conjunction_term: a=term60 (AND b+=term60)*; +disjunction_term: a=conjunction_term (op+=opDisjunction b+=conjunction_term)*; +conjunction_term: a=term60 (op+=opConjunction b+=term60)*; term60: unary_formula | equality_term; unary_formula: NOT sub=term60 #negation_term | (FORALL | EXISTS) bound_variables sub=term60 #quantifierterm | MODALITY sub=term60 #modality_term ; -equality_term: a=comparison_term ((NOT_EQUALS|EQUALS) b=comparison_term)?; -comparison_term: a=weak_arith_term ((LESS|LESSEQUAL|GREATER|GREATEREQUAL|UTF_PRECEDES|UTF_SUBSET_EQ|UTF_SUBSEQ|UTF_IN) b=weak_arith_term)?; -weak_arith_term: a=strong_arith_term_1 (op+=(PLUS|MINUS|UTF_UNION|UTF_INTERSECT|UTF_SETMINUS) b+=strong_arith_term_1)*; -strong_arith_term_1: a=strong_arith_term_2 (STAR b+=strong_arith_term_2)*; -strong_arith_term_2: a=atom_prefix (op+=(PERCENT|SLASH) b+=atom_prefix)*; +equality_term: left=comparison_term (op=opEqualities right=comparison_term)?; +comparison_term: left=weak_arith_term (op=opComparison right=weak_arith_term)?; +weak_arith_term: left=strong_arith_term_1 (op+=opWeak others+=strong_arith_term_1)*; +strong_arith_term_1: left=strong_arith_term_2 (op+=opStrong1 others+=strong_arith_term_2)*; +strong_arith_term_2: left=atom_prefix (op+=opStrong2 others+=atom_prefix)*; update_term: (LBRACE u=parallel_term RBRACE) (atom_prefix | unary_formula); substitution_term: @@ -390,7 +431,7 @@ substitution_term: (atom_prefix|unary_formula) ; cast_term: (LPAREN sort=sortId RPAREN) sub=atom_prefix; -unary_minus_term: MINUS sub=atom_prefix; +unary_minus_term: op=opUnaryTerm sub=atom_prefix; atom_prefix: update_term | substitution_term diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/AbstractSortedOperator.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/AbstractSortedOperator.java index 4877cf36daa..00ddedb320b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/AbstractSortedOperator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/AbstractSortedOperator.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic.op; +import java.util.stream.Collectors; + import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Sorted; import de.uka.ilkd.key.logic.Term; @@ -19,7 +21,7 @@ public abstract class AbstractSortedOperator extends AbstractOperator implements SortedOperator, Sorted { - private static final ImmutableArray EMPTY_SORT_LIST = new ImmutableArray<>(); + private static final ImmutableArray EMPTY_SORT_LIST = new ImmutableArray(); private final Sort sort; private final ImmutableArray argSorts; @@ -28,9 +30,8 @@ public abstract class AbstractSortedOperator extends AbstractOperator protected AbstractSortedOperator(Name name, ImmutableArray argSorts, Sort sort, ImmutableArray whereToBind, boolean isRigid) { super(name, argSorts == null ? 0 : argSorts.size(), whereToBind, isRigid); - if (sort == null) { + if (sort == null) throw new NullPointerException("Given sort is null"); - } this.argSorts = argSorts == null ? EMPTY_SORT_LIST : argSorts; this.sort = sort; } @@ -38,8 +39,8 @@ protected AbstractSortedOperator(Name name, ImmutableArray argSorts, Sort protected AbstractSortedOperator(Name name, Sort[] argSorts, Sort sort, Boolean[] whereToBind, boolean isRigid) { - this(name, new ImmutableArray<>(argSorts), sort, - new ImmutableArray<>(whereToBind), isRigid); + this(name, new ImmutableArray(argSorts), sort, + new ImmutableArray(whereToBind), isRigid); } @@ -50,7 +51,7 @@ protected AbstractSortedOperator(Name name, ImmutableArray argSorts, Sort protected AbstractSortedOperator(Name name, Sort[] argSorts, Sort sort, boolean isRigid) { - this(name, new ImmutableArray<>(argSorts), sort, null, isRigid); + this(name, new ImmutableArray(argSorts), sort, null, isRigid); } @@ -117,4 +118,9 @@ public final ImmutableArray argSorts() { public final Sort sort() { return sort; } + + public String toSignatureString() { + return argSorts.stream().map(it -> it.name().toString()) + .collect(Collectors.joining(",", name() + "(", ")")); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java index 95bf6cd2d63..9ba9ba8e700 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java @@ -4,21 +4,28 @@ package de.uka.ilkd.key.logic.op; import de.uka.ilkd.key.logic.Name; +import de.uka.ilkd.key.logic.overop.FunctionMetaData; import de.uka.ilkd.key.logic.sort.NullSort; import de.uka.ilkd.key.logic.sort.Sort; import org.key_project.util.Strings; import org.key_project.util.collection.ImmutableArray; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + /** * Objects of this class represent function and predicate symbols. Note that program variables are a * separate syntactic category, and not a type of function. */ +@NullMarked public class Function extends AbstractSortedOperator { private final boolean unique; private final boolean skolemConstant; + @Nullable + private final ImmutableArray metaData; // ------------------------------------------------------------------------- @@ -27,25 +34,26 @@ public class Function extends AbstractSortedOperator { Function(Name name, Sort sort, ImmutableArray argSorts, ImmutableArray whereToBind, boolean unique, boolean isRigid, - boolean isSkolemConstant) { + boolean isSkolemConstant, @Nullable ImmutableArray metaData) { super(name, argSorts, sort, whereToBind, isRigid); - this.unique = unique; - skolemConstant = isSkolemConstant; + this.skolemConstant = isSkolemConstant; + this.metaData = metaData; assert sort != Sort.UPDATE; assert !(unique && sort == Sort.FORMULA); assert !(sort instanceof NullSort) || name.toString().equals("null") : "Functions with sort \"null\" are not allowed: " + this; + } public Function(Name name, Sort sort, ImmutableArray argSorts, ImmutableArray whereToBind, boolean unique) { - this(name, sort, argSorts, whereToBind, unique, true, false); + this(name, sort, argSorts, whereToBind, unique, true, false, null); } public Function(Name name, Sort sort, ImmutableArray argSorts, ImmutableArray whereToBind, boolean unique, boolean isSkolemConstant) { - this(name, sort, argSorts, whereToBind, unique, true, isSkolemConstant); + this(name, sort, argSorts, whereToBind, unique, true, isSkolemConstant, null); } public Function(Name name, Sort sort, Sort[] argSorts, Boolean[] whereToBind, boolean unique) { @@ -61,7 +69,7 @@ public Function(Name name, Sort sort, Sort[] argSorts, Boolean[] whereToBind, bo } Function(Name name, Sort sort, ImmutableArray argSorts, boolean isRigid) { - this(name, sort, argSorts, null, false, isRigid, false); + this(name, sort, argSorts, null, false, isRigid, false, null); } public Function(Name name, Sort sort, ImmutableArray argSorts) { @@ -81,7 +89,15 @@ public Function(Name name, Sort sort) { } public Function(Name name, Sort sort, boolean isSkolemConstant) { - this(name, sort, new ImmutableArray<>(), null, false, true, isSkolemConstant); + this(name, sort, new ImmutableArray<>(), null, false, true, isSkolemConstant, null); + } + + public Function(Name name, Sort retSort, Sort[] argSort, + @Nullable Boolean[] whereToBind, boolean unique, + @Nullable ImmutableArray metaData) { + this(name, retSort, new ImmutableArray<>(argSort), + whereToBind == null ? null : new ImmutableArray<>(whereToBind), + unique, false, false, metaData); } @@ -125,4 +141,9 @@ public final String proofToString() { public Function rename(Name newName) { return new Function(newName, sort(), argSorts(), whereToBind(), unique, skolemConstant); } + + @Nullable + public ImmutableArray getMetaData() { + return metaData; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java index a99e71690d1..b6e998b420a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.logic.Namespace; import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.logic.overop.FunctionMetaData; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.logic.sort.ProgramSVSort; import de.uka.ilkd.key.logic.sort.Sort; @@ -80,7 +81,7 @@ public int hashCode() { } public static SortDependingFunction createFirstInstance(GenericSort sortDependingOn, Name kind, - Sort sort, Sort[] argSorts, boolean unique) { + Sort sort, Sort[] argSorts, boolean unique, ImmutableArray metaData) { SortDependingFunctionTemplate template = new SortDependingFunctionTemplate(sortDependingOn, kind, sort, new ImmutableArray<>(argSorts), unique); return new SortDependingFunction(template, Sort.ANY); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/overop/FunctionMetaData.java b/key.core/src/main/java/de/uka/ilkd/key/logic/overop/FunctionMetaData.java new file mode 100644 index 00000000000..9d641dfa503 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/overop/FunctionMetaData.java @@ -0,0 +1,28 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.logic.overop; + +import de.uka.ilkd.key.logic.op.Function; + +public interface FunctionMetaData { + int getPrecedence(); + + default boolean isInfix() { + return false; + } + + default boolean isPrefix() { + return false; + } + + default boolean isSuffix() { + return false; + } + + default boolean isShortcut() { + return false; + } + + Iterable getAlternativeSignatures(Function fun); +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/overop/InfixMetaData.java b/key.core/src/main/java/de/uka/ilkd/key/logic/overop/InfixMetaData.java new file mode 100644 index 00000000000..e05ab254aae --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/overop/InfixMetaData.java @@ -0,0 +1,33 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.logic.overop; + +import de.uka.ilkd.key.logic.op.Function; +import org.key_project.util.collection.ImmutableArray; + +import java.util.stream.Collectors; + +public record InfixMetaData(ImmutableArray infixOperator, int prec) implements FunctionMetaData { + public InfixMetaData(String text, int prec) { + this(new ImmutableArray<>(text), prec); + } + + @Override + public int getPrecedence() { + return prec; + } + + @Override + public boolean isInfix() { + return true; + } + + @Override + public Iterable getAlternativeSignatures(Function fun) { + var sig = fun.argSorts().stream().map(it -> it.name().toString()) + .collect(Collectors.joining(",", "(", ")")); + return infixOperator.stream().map(it -> it + sig) + .collect(Collectors.toList()); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/overop/OperatorInfo.java b/key.core/src/main/java/de/uka/ilkd/key/logic/overop/OperatorInfo.java new file mode 100644 index 00000000000..5e86c61f885 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/overop/OperatorInfo.java @@ -0,0 +1,277 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.logic.overop; + +import de.uka.ilkd.key.nparser.KeYLexer; + +import org.key_project.util.collection.ImmutableArray; + +import org.antlr.v4.runtime.Token; +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.pp.NotationInfo.*; + + +/** + * Information Table about all operators in KeY. + */ +public enum OperatorInfo { + /** + * // (8918) ⋖ LESS-THAN WITH DOT kleiner als mit Punkt + */ + LESS_THAN_WITH_DOT(KeYLexer.LESS_THAN_WITH_DOT, PRIORITY_COMPARISON, '⋖'), + /** + * (8922) ⋚ LESS-THAN EQUAL TO OR GREATER-THAN kleiner als, gleich oder größer als + */ + LESS_THAN_EQUAL_TO_OR_GREATER_THAN(KeYLexer.LESS_THAN_EQUAL_TO_OR_GREATER_THAN, + PRIORITY_COMPARISON, '⋚'), + /** + * (8920) ⋘ VERY MUCH LESS-THAN Sehr viel kleiner als + */ + VERY_MUCH_LESS_THAN(KeYLexer.VERY_MUCH_LESS_THAN, PRIORITY_COMPARISON, '⋘'), + /** + * (8924) ⋜ EQUAL TO OR LESS-THAN gleich oder kleiner als + */ + EQUAL_TO_OR_LESS_THAN(KeYLexer.EQUAL_TO_OR_LESS_THAN, PRIORITY_COMPARISON, '⋜'), + /** + * (8926) ⋞ EQUAL TO OR PRECEDES gleich oder vorangehend + */ + EQUAL_TO_OR_PRECEDES(KeYLexer.EQUAL_TO_OR_PRECEDES, PRIORITY_COMPARISON, '⋞'), + /** + * (8828) ≼ PRECEDES OR EQUAL TO vorangehend oder gleich + */ + PRECEDES_OR_EQUAL_TO(KeYLexer.PRECEDES_OR_EQUAL_TO, PRIORITY_COMPARISON, '≼'), + /** + * (8928) ⋠ DOES NOT PRECEDE OR EQUAL weder vorangehend oder gleich + */ + DOES_NOT_PRECEDE_OR_EQUAL("⋠", KeYLexer.DOES_NOT_PRECEDE_OR_EQUAL, PRIORITY_COMPARISON, + OperatorInfo.PRECEDES_OR_EQUAL_TO), + /** + * (8849) ⊑ SQUARE IMAGE OF OR EQUAL TO viereckiges Bild oder gleich + */ + SQUARE_IMAGE_OF_OR_EQUAL_TO(KeYLexer.SQUARE_IMAGE_OF_OR_EQUAL_TO, PRIORITY_COMPARISON, '⊑'), + + /** + * (8930) ⋢ NOT SQUARE IMAGE OF OR EQUAL TO kein viereckiges Bild oder gleich + */ + NOT_SQUARE_IMAGE_OF_OR_EQUAL_TO("⋢", KeYLexer.NOT_SQUARE_IMAGE_OF_OR_EQUAL_TO, + PRIORITY_COMPARISON, + SQUARE_IMAGE_OF_OR_EQUAL_TO), + /** + * (8932) ⋤ SQUARE IMAGE OF OR NOT EQUAL TO viereckiges Bild oder ungleich + */ + SQUARE_IMAGE_OF_OR_NOT_EQUAL_TO(KeYLexer.SQUARE_IMAGE_OF_OR_NOT_EQUAL_TO, PRIORITY_COMPARISON, + '⋤'), + /** + * (8826) ≺ PRECEDES vorangehend + */ + PRECEDES(KeYLexer.PRECEDES, PRIORITY_COMPARISON, '≺'), + /** + * (8830) ≾ PRECEDES OR EQUIVALENT TO vorangehend oder äquivalent + */ + PRECEDES_OR_EQUIVALENT_TO(KeYLexer.PRECEDES_OR_EQUIVALENT_TO, PRIORITY_COMPARISON, '≾'), + /** + * (8836) ⊄ NOT A SUBSET OF ist keine ;// (echte) Teilmenge von + */ + NOT_A_SUBSET_OF(KeYLexer.NOT_A_SUBSET_OF, PRIORITY_COMPARISON, '⊄'), + /** + * (8838) ⊆ SUBSET OF OR EQUAL TO Teilmenge oder gleich + */ + SUBSET_OF_OR_EQUAL_TO(KeYLexer.SUBSET_OF_OR_EQUAL_TO, PRIORITY_COMPARISON, '⊆', "\\subseteq"), + + /** + * ∖ SET MINUS + */ + SET_MINUS(KeYLexer.SETMINUS, PRIORITY_ARITH_WEAK, '∖', "\\setminus"), + + // (8848) ⊐ SQUARE ORIGINAL OF viereckiges Original + SQUARE_ORIGINAL_OF(KeYLexer.SQUARE_ORIGINAL, PRIORITY_COMPARISON, '⊐'), + // (8850) ⊒ SQUARE ORIGINAL OF OR EQUAL TO viereckiges Original oder gleich + SQUARE_ORIGINAL_OF_OR_EQUAL_TO(KeYLexer.SQUARE_ORIGINAL_OF_OR_EQUAL_TO, PRIORITY_COMPARISON, + '⊒'), + // (8919) ⋗ GREATER-THAN WITH DOT größer als mit Punkt + GREATER_THAN_WITH_DOT(KeYLexer.GREATER_THAN_WITH_DOT, PRIORITY_COMPARISON, '⋗', "\\gedot"), + // (8921) ⋙ VERY MUCH GREATER-THAN sehr viel größer als + VERY_MUCH_GREATER_THAN(KeYLexer.VERY_MUCH_GREATER_THAN, PRIORITY_COMPARISON, '⋙', "\\gg"), + // (8923) ⋛ GREATER-THAN EQUAL TO OR LESS-THAN größer als, gleich oder kleiner als + GREATER_THAN_EQUAL_TO_OR_LESS_THAN(KeYLexer.GREATER_THAN_EQUAL_TO_OR_LESS_THAN, + PRIORITY_COMPARISON, '⋛'), + // (8925) ⋝ EQUAL TO OR GREATER-THAN gleich oder größer als + EQUAL_TO_OR_GREATER_THAN(KeYLexer.EQUAL_TO_OR_GREATER_THAN, PRIORITY_COMPARISON, '⋝'), + // (8927) ⋟ EQUAL TO OR SUCCEEDS gleich oder nachfolgend + EQUAL_TO_OR_SUCCEEDS(KeYLexer.EQUAL_TO_OR_SUCCEEDS, PRIORITY_COMPARISON, '⋟'), + // (8929) ⋡ DOES NOT SUCCEED OR EQUAL weder nachfolgend oder gleich + DOES_NOT_SUCCEED_OR_EQUAL(KeYLexer.DOES_NOT_SUCCEED_OR_EQUAL, PRIORITY_COMPARISON, '⋡'), + // (8931) ⋣ NOT SQUARE ORIGINAL OF OR EQUAL TO kein viereckiges Original oder gleich + NOT_SQUARE_ORIGINAL_OF_OR_EQUAL_TO(KeYLexer.NOT_SQUARE_ORIGINAL_OF_OR_EQUAL_TO, + PRIORITY_COMPARISON, '⋣'), + // (8933) ⋥ SQUARE ORIGINAL OF OR NOT EQUAL TO viereckiges Original oder ungleich + SQUARE_ORIGINAL_OF_OR_NOT_EQUAL_TO(KeYLexer.SQUARE_ORIGINAL_OF_OR_NOT_EQUAL_TO, + PRIORITY_COMPARISON, '⋥'), + // (8827) ≻ SUCCEEDS nachfolgend + SUCCEEDS(KeYLexer.SUCCEEDS, PRIORITY_COMPARISON, '≻'), + // (8829) ≽ SUCCEEDS OR EQUAL TO nachfolgend oder gleich + SUCCEEDS_OR_EQUAL_TO(KeYLexer.SUCCEEDS_OR_EQUAL_TO, PRIORITY_COMPARISON, '≽'), + // (8831) ≿ SUCCEEDS OR EQUIVALENT TO nachfolgend oder äquivalent + SUCCEEDS_OR_EQUIVALENT_TO(KeYLexer.SUCCEEDS_OR_EQUIVALENT_TO, PRIORITY_COMPARISON, '≿'), + // (8832) ⊀ DOES NOT PRECEDE nicht vorangehend + DOES_NOT_PRECEDE(KeYLexer.DOES_NOT_PRECEDE, PRIORITY_COMPARISON, '⊀'), + // (8833) ⊁ DOES NOT SUCCEED nicht nachfolgend + DOES_NOT_SUCCEED(KeYLexer.DOES_NOT_SUCCEED, PRIORITY_COMPARISON, '⊁'), + // (8835) ⊃ SUPERSET OF ist ;// (echte) Obermenge von + SUPERSET_OF(KeYLexer.SUPERSET_OF, PRIORITY_COMPARISON, '⊃'), + // (8837) ⊅ NOT A SUPERSET OF ist keine ;// (echte) Obermenge von + NOT_A_SUPERSET_OF(KeYLexer.NOT_A_SUPERSET_OF, PRIORITY_COMPARISON, '⊅'), + + // (8839) ⊇ SUPERSET OF OR EQUAL TO Obermenge oder gleich + SUPERSET_OF_OR_EQUAL_TO(KeYLexer.SUPERSET_OF_OR_EQUAL_TO, PRIORITY_COMPARISON, '⊇'), + + // (8847) ⊏ SQUARE IMAGE OF viereckiges Bild + SQUARE_IMAGE_OF(KeYLexer.SQUARE_IMAGE_OF, PRIORITY_COMPARISON, '⊏'), + + + GREATER(KeYLexer.GREATER, PRIORITY_COMPARISON, '>'), + GREATER_EQUAL(KeYLexer.GREATEREQUAL, PRIORITY_COMPARISON, '≥', ">="), + + EQUALITY(KeYLexer.EQUALS, PRIORITY_COMPARISON, '↔', "<->"), + + LESS(KeYLexer.LESS, PRIORITY_COMPARISON, '<'), + LESS_EQUAL(KeYLexer.LESSEQUAL, PRIORITY_COMPARISON, '≤', "<="), + + // (8853) ⊕ CIRCLED PLUS eingekreistes Pluszeichen + CIRCLED_PLUS(KeYLexer.CIRCLED_PLUS, PRIORITY_ARITH_WEAK, '⊕'), + + // (8854) ⊖ CIRCLED MINUS eingekreistes Minuszeichen + CIRCLED_MINUS(KeYLexer.CIRCLED_MINUS, PRIORITY_ARITH_WEAK, '⊖'), + + // (8862) ⊞ SQUARED PLUS eingerahmtes Pluszeichen + SQUARED_PLUS(KeYLexer.SQUARED_PLUS, PRIORITY_ARITH_WEAK, '⊞'), + + // (8861) ⊝ CIRCLED DASH eingekreister Gedankenstrich + CIRCLED_DASH(KeYLexer.CIRCLED_DASH, PRIORITY_ARITH_WEAK, '⊝'), + + // (8863) ⊟ SQUARED MINUS eingerahmtes Minuszeichen + SQUARED_MINUS(KeYLexer.SQUARED_MINUS, PRIORITY_ARITH_WEAK, '⊟'), + + + // STAR + // (8855) ⊗ CIRCLED TIMES eingekreistes Multiplikationszeichen + CIRCLED_TIMES(KeYLexer.CIRCLED_TIMES, PRIORITY_ARITH_STRONG, '⊗'), + + // (8857) ⊙ CIRCLED DOT OPERATOR eingekreister Punktoperator + CIRCLED_DOT_OPERATOR(KeYLexer.CIRCLED_DOT_OPERATOR, PRIORITY_ARITH_STRONG, '⊙'), + + // (8859) ⊛ CIRCLED ASTERISK OPERATOR eingekreister Sternoperator + CIRCLED_ASTERISK_OPERATOR(KeYLexer.CIRCLED_ASTERISK_OPERATOR, PRIORITY_ARITH_STRONG, '⊛'), + + // (8864) ⊠ SQUARED TIMES eingerahmtes Multiplikationszeichen + SQUARED_TIMES(KeYLexer.SQUARED_TIMES, PRIORITY_ARITH_STRONG, '⊠'), + + // (8865) ⊡ SQUARED DOT OPERATOR eingerahmter Punktoperator + SQUARED_DOT_OPERATOR(KeYLexer.SQUARED_DOT_OPERATOR, PRIORITY_ARITH_STRONG, '⊡'), + + // SLASH + // (8858) ⊚ CIRCLED RING OPERATOR eingekreister Ringoperator + CIRCLED_RING_OPERATOR(KeYLexer.CIRCLED_RING_OPERATOR, PRIORITY_ARITH_STRONG, '⊚'), + + // (8856) ⊘ CIRCLED DIVISION SLASH eingekreister Divisionsstrich + CIRCLED_DIVISION_SLASH(KeYLexer.CIRCLED_DIVISION_SLASH, PRIORITY_ARITH_STRONG, '⊘'), + + + EQUALS(KeYLexer.EQUALS, PRIORITY_EQUAL, '=', "="), + + NOT_EQUALS("≠", KeYLexer.NOT_EQUALS, "!=", KeYLexer.NOT_EQUALS, PRIORITY_EQUAL, null), + + // (8774) ≆ APPROXIMATELY BUT NOT ACTUALLY EQUAL TO ungefähr, aber nicht genau gleich + APPROXIMATELY_BUT_NOT_ACTUALLY_EQUAL_TO(KeYLexer.APPROXIMATELY_BUT_NOT_ACTUALLY_EQUAL_TO, + PRIORITY_EQUAL, '≆'), + // (8775) ≇ NEITHER APPROXIMATELY NOR ACTUALLY EQUAL TO weder ungefähr noch genau gleich + NEITHER_APPROXIMATELY_NOR_ACTUALLY_EQUAL_TO( + KeYLexer.NEITHER_APPROXIMATELY_NOR_ACTUALLY_EQUAL_TO, PRIORITY_EQUAL, '≇'), + // (8801) ≡ IDENTICAL TO ist kongruent zu + IDENTICAL_TO(KeYLexer.IDENTICAL_TO, PRIORITY_EQUAL, '≡'), + // (8802) ≢ NOT IDENTICAL TO ist nicht kongruent zu + NOT_IDENTICAL_TO("≢", KeYLexer.NOT_IDENTICAL_TO, PRIORITY_EQUAL, IDENTICAL_TO), + IMPLICATION(KeYLexer.IMP, PRIORITY_IMP, '→', "->"), + OR(KeYLexer.OR, PRIORITY_OR, '∨'), + // (8852) ⊔ SQUARE CUP nach oben geöffnetes Viereck + SQUARE_CUP(KeYLexer.SQUARE_CUP, PRIORITY_OR, '⊔', "\\sqcup"), + + AND(KeYLexer.AND, PRIORITY_AND, '∧', "&"), + + // (8851) ⊓ SQUARE CAP nach unten geöffnetes Viereck + SQUARE_CAP(KeYLexer.SQUARE_CAP, PRIORITY_AND, '⊓', "\\sqcap"), + + NEGATION(KeYLexer.NOT, PRIORITY_NEGATION, '¬', "!"), + + // (8860) ⊜ CIRCLED EQUALS eingekreistes Gleichheitszeichen + CIRCLED_EQUALS(KeYLexer.CIRCLED_EQUALS, PRIORITY_EQUAL, '⊜'), + + UNION(KeYLexer.UNION, PRIORITY_OR, '∪', "\\cup"), + INTERSECT(KeYLexer.INTERSECT, PRIORITY_AND, '∩', "\\cap"), + ; + + + private final int precedence; + private final OperatorInfo positiveOperator; + private final int tokenTypeAlt; + private final int tokenTypeUtf8; + private final String utf8; + private final String alternative; + + OperatorInfo(int tokenType, int precedence, char operator) { + this(String.valueOf(operator), tokenType, null, -1, precedence, null); + } + + OperatorInfo(int tokenType, int precedence, char utf8, String longForm, int tokenTypeAlt) { + this(String.valueOf(utf8), tokenType, longForm, tokenTypeAlt, precedence, null); + } + + OperatorInfo(String utf8, int tokenTypeUtf8, @Nullable String alt, int tokenTypeAlt, + int precedence, + OperatorInfo positiveOperator) { + this.tokenTypeUtf8 = tokenTypeUtf8; + this.precedence = precedence; + this.positiveOperator = positiveOperator; + this.tokenTypeAlt = tokenTypeAlt; + this.utf8 = utf8; + this.alternative = alt; + } + + OperatorInfo(String utf8, int tokenType, int precedence, OperatorInfo positiveOperator) { + this(utf8, tokenType, null, -1, precedence, positiveOperator); + } + + OperatorInfo(int tokenType, int precedence, char utf8, String longForm) { + this(String.valueOf(utf8), tokenType, longForm, tokenType, precedence, null); + } + + + @Nullable + public static OperatorInfo find(Token opToken) { + for (OperatorInfo value : values()) { + if (value.tokenTypeUtf8 == opToken.getType() + || value.tokenTypeAlt == opToken.getType()) { + return value; + } + } + return null; + } + + public int getPrecedence() { + return precedence; + } + + + public OperatorInfo getPositiveForm() { + return positiveOperator; + } + + public ImmutableArray getNames() { + if (alternative == null) { + return new ImmutableArray<>(utf8); + } + return new ImmutableArray<>(utf8, alternative); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java index 70bece72ac1..4d11e1dd1f9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java @@ -344,8 +344,8 @@ public Sort visitSortId(KeYParser.SortIdContext ctx) { semanticError(ctx, "Could not find sort: %s", ctx.getText()); } - if (!ctx.EMPTYBRACKETS().isEmpty()) { - return toArraySort(new Pair<>(s, t), ctx.EMPTYBRACKETS().size()); + if (!ctx.LBRACKET().isEmpty()) { + return toArraySort(new Pair<>(s, t), ctx.LBRACKET().size()); } return s; } @@ -354,7 +354,7 @@ public Sort visitSortId(KeYParser.SortIdContext ctx) { public KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) { boolean array = false; StringBuilder type = new StringBuilder(visitSimple_ident_dots(ctx.simple_ident_dots())); - for (int i = 0; i < ctx.EMPTYBRACKETS().size(); i++) { + for (int i = 0; i < ctx.LBRACKET().size(); i++) { array = true; type.append("[]"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index 1cc53a2eda6..5baeb221b9a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java @@ -4,10 +4,7 @@ package de.uka.ilkd.key.nparser.builder; import java.math.BigInteger; -import java.util.Iterator; -import java.util.LinkedList; -import java.util.List; -import java.util.Objects; +import java.util.*; import java.util.function.Supplier; import java.util.stream.Collectors; @@ -20,9 +17,9 @@ import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.logic.overop.OperatorInfo; import de.uka.ilkd.key.logic.sort.ProgramSVSort; import de.uka.ilkd.key.logic.sort.Sort; -import de.uka.ilkd.key.nparser.KeYLexer; import de.uka.ilkd.key.nparser.KeYParser; import de.uka.ilkd.key.nparser.KeYParser.DoubleLiteralContext; import de.uka.ilkd.key.nparser.KeYParser.FloatLiteralContext; @@ -217,6 +214,95 @@ private Term binaryTerm(ParserRuleContext ctx, Operator operator, Term left, Ter () -> updateOrigin(getTermFactory().createTerm(operator, left, right), ctx, services)); } + private Term binaryTerm(ParserRuleContext ctx, Token opToken, Term left, Term right) { + var op = lookupOperator(ctx, left.sort(), right.sort(), opToken.getText()); + if (op == null) { + semanticError(ctx, "Could not find an operator with name '%s' and sorts [%s,%s]", + opToken.getText(), left.sort(), right.sort()); + } + return binaryTerm(ctx, op, left, right); + } + + private Term binaryTermWithNegationFallback(ParserRuleContext ctx, Token opToken, Term left, + Term right) { + var op = lookupOperator(ctx, left.sort(), right.sort(), opToken.getText()); + if (op == null) { + // we look up on UTFOperator if we find information about the operator, e.g., if there + // is a know + // positive entry for example NOT_EQUALS is modelted by NEGATION of EQUALS + var opTableEntry = OperatorInfo.find(opToken); + if (opTableEntry != null && opTableEntry.getPositiveForm() != null) { + var opInfo = opTableEntry.getPositiveForm(); + op = lookupOperator(ctx, left.sort(), right.sort(), opInfo.getNames()); + var eq = binaryTerm(ctx, op, left, right); + return capsulateTf(ctx, () -> getTermFactory().createTerm(Junctor.NOT, eq)); + } + } + return binaryTerm(ctx, op, left, right); + } + + private Operator lookupOperator(ParserRuleContext ctx, Sort left, Sort right, + String... opTexts) { + return lookupOperator(ctx, left, right, new ImmutableArray<>(opTexts)); + } + + private Operator lookupOperator(ParserRuleContext ctx, Sort left, Sort right, + ImmutableArray opTexts) { + if (left == null || right == null) { + semanticError(ctx, "Expected sort available on both sides"); + } + + if (isMetaSort(left)) { + left = right; + } + + if (isMetaSort(right)) { + right = left; + } + + var cache = getFunctionCache(); + var args = "(" + left.name() + "," + right.name() + ")"; + for (String opText : opTexts) { + var signature = opText + args; + var op = cache.get(signature); + if (op != null) { + return op; + } + } + return null; + } + + private boolean isMetaSort(Sort sort) { + return "Meta".equals(sort.name().toString()); + } + + private final Map functionLookupCache = new TreeMap<>(); + + private Map getFunctionCache() { + if (functionLookupCache.isEmpty()) { + for (Function fun : functions().allElements()) { + var oldOp = functionLookupCache.put(fun.toSignatureString(), fun); + if (oldOp != null) { + throw new IllegalStateException("Operator collision detected!"); + } + + if (fun.getMetaData() != null) { + var mds = fun.getMetaData(); + for (var md : mds) { + for (var alt : md.getAlternativeSignatures(fun)) { + oldOp = functionLookupCache.put(alt, fun); + if (oldOp != null) { + throw new IllegalStateException("Operator collision detected!"); + } + } + } + } + } + } + return functionLookupCache; + } + + @Override public Term visitImplication_term(KeYParser.Implication_termContext ctx) { Term termL = accept(ctx.a); @@ -248,7 +334,7 @@ public Term visitConjunction_term(KeYParser.Conjunction_termContext ctx) { public Object visitUnary_minus_term(KeYParser.Unary_minus_termContext ctx) { Term result = accept(ctx.sub); assert result != null; - if (ctx.MINUS() != null) { + if (ctx.opUnaryTerm().MINUS() != null) { Operator Z = functions().lookup("Z"); if (result.op() == Z) { // weigl: rewrite neg(Z(1(#)) to Z(neglit(1(#)) @@ -291,64 +377,43 @@ public Term visitNegation_term(KeYParser.Negation_termContext ctx) { @Override public Term visitEquality_term(KeYParser.Equality_termContext ctx) { - Term termL = accept(ctx.a); - Term termR = accept(ctx.b); - Term eq = binaryTerm(ctx, Equality.EQUALS, termL, termR); - if (ctx.NOT_EQUALS() != null) { - return capsulateTf(ctx, () -> getTermFactory().createTerm(Junctor.NOT, eq)); + Term termL = accept(ctx.left); + if (ctx.op == null) { + return termL; + } + + if (ctx.op.EQUALS() != null || ctx.op.NOT_EQUALS() != null) { // overloaded and built-in + Term eq = binaryTerm(ctx, Equality.EQUALS, termL, accept(ctx.right)); + if (ctx.op.NOT_EQUALS() != null) { + return capsulateTf(ctx, () -> getTermFactory().createTerm(Junctor.NOT, eq)); + } + return eq; } - return eq; + + Term termR = accept(ctx.right); + return binaryTermWithNegationFallback(ctx, ctx.op.start, termL, termR); } + @Override public Object visitComparison_term(KeYParser.Comparison_termContext ctx) { - Term termL = accept(ctx.a); - Term termR = accept(ctx.b); - - if (termR == null) { - return updateOrigin(termL, ctx, services); - } - - String op_name = ""; - if (ctx.LESS() != null) { - op_name = "lt"; - } - if (ctx.LESSEQUAL() != null) { - op_name = "leq"; - } - if (ctx.GREATER() != null) { - op_name = "gt"; - } - if (ctx.GREATEREQUAL() != null) { - op_name = "geq"; + Term termL = accept(ctx.left); + if (ctx.op == null) { + return termL; } - return binaryLDTSpecificTerm(ctx, op_name, termL, termR); + Term termR = accept(ctx.right); + return binaryTerm(ctx, ctx.op.start, termL, termR); } + @Override public Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx) { - Term termL = Objects.requireNonNull(accept(ctx.a)); + Term termL = Objects.requireNonNull(accept(ctx.left)); if (ctx.op.isEmpty()) { return updateOrigin(termL, ctx, services); } - - List terms = mapOf(ctx.b); - Term last = termL; - for (int i = 0; i < terms.size(); i++) { - String opname = ""; - switch (ctx.op.get(i).getType()) { - case KeYLexer.UTF_INTERSECT -> opname = "intersect"; - case KeYLexer.UTF_SETMINUS -> opname = "setMinus"; - case KeYLexer.UTF_UNION -> opname = "union"; - case KeYLexer.PLUS -> opname = "add"; - case KeYLexer.MINUS -> opname = "sub"; - default -> semanticError(ctx, "Unexpected token: %s", ctx.op.get(i)); - } - Term cur = terms.get(i); - last = binaryLDTSpecificTerm(ctx, opname, last, cur); - } - return last; + return getBinaryOperatorChain(ctx, termL, ctx.op, mapOf(ctx.others)); } private Term binaryLDTSpecificTerm(ParserRuleContext ctx, String opname, Term last, Term cur) { @@ -371,16 +436,32 @@ private Term binaryLDTSpecificTerm(ParserRuleContext ctx, String opname, Term la @Override public Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx) { - Term termL = accept(ctx.a); - if (ctx.b.isEmpty()) { + Term termL = accept(ctx.left); + if (ctx.others.isEmpty()) { return updateOrigin(termL, ctx, services); } - List terms = mapOf(ctx.b); - Term last = termL; - for (Term cur : terms) { - last = binaryLDTSpecificTerm(ctx, "mul", last, cur); + return getBinaryOperatorChain(ctx, termL, ctx.op, mapOf(ctx.others)); + } + + private Term getBinaryOperatorChain(ParserRuleContext ctx, Term left, + List operators, List right) { + if (operators.size() != right.size()) { + throw new IllegalArgumentException(); + } + + for (int i = 0; i < right.size(); i++) { + var cur = right.get(i); + var opText = operators.get(i).getText(); + var op = lookupOperator(operators.get(i), left.sort(), cur.sort(), opText); + if (op == null) { + var help = ""; + semanticError(ctx, "Unknown operator %s for sorts [%s,%s]\n%s", + operators.get(i).getText(), + left.sort(), cur.sort(), help); + } + left = binaryTerm(ctx, op, left, cur); } - return last; + return left; } @Override @@ -391,39 +472,11 @@ public Object visitEmptyset(KeYParser.EmptysetContext ctx) { @Override public Object visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx) { - if (ctx.b.isEmpty()) { // fast path - return accept(ctx.a); - } - - List termL = mapOf(ctx.b); - // List opName = ctx.op.stream().map(it -> it.getType()== KeYLexer.PERCENT ? "mod" : - // "div").collect(Collectors.toList()); - - Term term = accept(ctx.a); - var sort = term.sort(); - if (sort == null) { - semanticError(ctx, "No sort for term '%s'", term); - } - - var ldt = services.getTypeConverter().getLDTFor(sort); - - if (ldt == null) { - // falling back to integer ldt (for instance for untyped schema variables) - ldt = services.getTypeConverter().getIntegerLDT(); - } - - assert ctx.op.size() == ctx.b.size(); - - for (int i = 0; i < termL.size(); i++) { - var opName = ctx.op.get(i).getType() == KeYLexer.PERCENT ? "mod" : "div"; - Function op = ldt.getFunctionFor(opName, services); - if (op == null) { - semanticError(ctx, "Could not find function symbol '%s' for sort '%s'.", opName, - sort); - } - term = binaryTerm(ctx, op, term, termL.get(i)); + Term term = accept(ctx.left); + if (ctx.others.isEmpty()) { // fast path + return term; } - return term; + return getBinaryOperatorChain(ctx, term, ctx.op, mapOf(ctx.others)); } protected Term capsulateTf(ParserRuleContext ctx, Supplier termSupplier) { @@ -749,15 +802,15 @@ private String unescapeString(String string) { for (int i = 0; i < chars.length; i++) { if (chars[i] == '\\' && i < chars.length - 1) { switch (chars[++i]) { - case 'n' -> sb.append("\n"); - case 'f' -> sb.append("\f"); - case 'r' -> sb.append("\r"); - case 't' -> sb.append("\t"); - case 'b' -> sb.append("\b"); - case ':' -> sb.append("\\:"); - // this is so in KeY ... - default -> sb.append(chars[i]); - // this more relaxed than before, \a becomes a ... + case 'n' -> sb.append("\n"); + case 'f' -> sb.append("\f"); + case 'r' -> sb.append("\r"); + case 't' -> sb.append("\t"); + case 'b' -> sb.append("\b"); + case ':' -> sb.append("\\:"); + // this is so in KeY ... + default -> sb.append(chars[i]); + // this more relaxed than before, \a becomes a ... } } else { sb.append(chars[i]); @@ -870,8 +923,8 @@ public Object visitBracket_access_indexrange(KeYParser.Bracket_access_indexrange assert indexTerm != null; if (!isIntTerm(indexTerm)) { semanticError(ctx, - "Expecting term of sort %s as index of sequence %s, but found: %s", - IntegerLDT.NAME, term, indexTerm); + "Expecting term of sort %s as index of sequence %s, but found: %s", + IntegerLDT.NAME, term, indexTerm); } return getServices().getTermBuilder().seqGet(Sort.ANY, term, indexTerm); } @@ -882,19 +935,19 @@ public Object visitBracket_access_indexrange(KeYParser.Bracket_access_indexrange if (rangeTo != null) { if (quantifiedArrayGuard == null) { semanticError(ctx, - "Quantified array expressions are only allowed in locations."); + "Quantified array expressions are only allowed in locations."); } LogicVariable indexVar = - new LogicVariable(new Name("i"), sorts().lookup(new Name("int"))); + new LogicVariable(new Name("i"), sorts().lookup(new Name("int"))); Term indexTerm = capsulateTf(ctx, () -> getTermFactory().createTerm(indexVar)); Function leq = functions().lookup(new Name("leq")); Term fromTerm = - capsulateTf(ctx, () -> getTermFactory().createTerm(leq, rangeFrom, indexTerm)); + capsulateTf(ctx, () -> getTermFactory().createTerm(leq, rangeFrom, indexTerm)); Term toTerm = - capsulateTf(ctx, () -> getTermFactory().createTerm(leq, indexTerm, rangeTo)); + capsulateTf(ctx, () -> getTermFactory().createTerm(leq, indexTerm, rangeTo)); Term guardTerm = capsulateTf(ctx, - () -> getTermFactory().createTerm(Junctor.AND, fromTerm, toTerm)); + () -> getTermFactory().createTerm(Junctor.AND, fromTerm, toTerm)); quantifiedArrayGuard = capsulateTf(ctx, () -> getTermFactory() .createTerm(Junctor.AND, quantifiedArrayGuard, guardTerm)); // TODO check quantifiedArrayGuard! @@ -953,7 +1006,7 @@ public TermLabel visitSingle_label(KeYParser.Single_labelContext ctx) { } if (label == null) { label = getServices().getProfile().getTermLabelManager().parseLabel(labelName, - parameters, getServices()); + parameters, getServices()); } } catch (Exception ex) { throw new BuildingException(ctx, ex); @@ -980,7 +1033,7 @@ public Term visitIfThenElseTerm(KeYParser.IfThenElseTermContext ctx) { Term thenT = (Term) ctx.thenT.accept(this); Term elseT = (Term) ctx.elseT.accept(this); return capsulateTf(ctx, - () -> getTermFactory().createTerm(IfThenElse.IF_THEN_ELSE, condF, thenT, elseT)); + () -> getTermFactory().createTerm(IfThenElse.IF_THEN_ELSE, condF, thenT, elseT)); } @@ -997,7 +1050,7 @@ public Object visitIfExThenElseTerm(KeYParser.IfExThenElseTermContext ctx) { Term elseT = accept(ctx.elseT); ImmutableArray exVarsArray = new ImmutableArray<>(exVars); Term result = getTermFactory().createTerm(IfExThenElse.IF_EX_THEN_ELSE, - new Term[] { condF, thenT, elseT }, exVarsArray, null); + new Term[]{condF, thenT, elseT}, exVarsArray, null); unbindVars(orig); return result; } @@ -1015,7 +1068,7 @@ public Term visitQuantifierterm(KeYParser.QuantifiertermContext ctx) { List vs = accept(ctx.bound_variables()); Term a1 = accept(ctx.sub); Term a = getTermFactory().createTerm(op, new ImmutableArray<>(a1), - new ImmutableArray<>(vs.toArray(new QuantifiableVariable[0])), null); + new ImmutableArray<>(vs.toArray(new QuantifiableVariable[0])), null); unbindVars(orig); return a; } @@ -1049,7 +1102,7 @@ public Object visitSubstitution_term(KeYParser.Substitution_termContext ctx) { Term a2 = oneOf(ctx.atom_prefix(), ctx.unary_formula()); try { Term result = - getServices().getTermBuilder().subst(op, (QuantifiableVariable) v, a1, a2); + getServices().getTermBuilder().subst(op, (QuantifiableVariable) v, a1, a2); return result; } catch (Exception e) { throw new BuildingException(ctx, e); @@ -1081,10 +1134,10 @@ public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variable if (ts != null) { if (!(ts instanceof VariableSV)) { semanticError(ctx, - ts + " is not allowed in a quantifier. Note, that you can't " - + "use the normal syntax for quantifiers of the form \"\\exists int i;\"" - + " in taclets. You have to define the variable as a schema variable" - + " and use the syntax \"\\exists i;\" instead."); + ts + " is not allowed in a quantifier. Note, that you can't " + + "use the normal syntax for quantifiers of the form \"\\exists int i;\"" + + " in taclets. You have to define the variable as a schema variable" + + " and use the syntax \"\\exists i;\" instead."); } bindVar(); return (QuantifiableVariable) ts; @@ -1095,7 +1148,7 @@ public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variable } QuantifiableVariable result = - doLookup(new Name(ctx.id.getText()), variables()); + doLookup(new Name(ctx.id.getText()), variables()); if (result == null) { semanticError(ctx, "There is no schema variable or variable named " + id); @@ -1128,7 +1181,7 @@ public Object visitModality_term(KeYParser.Modality_termContext ctx) { } return capsulateTf(ctx, - () -> getTermFactory().createTerm(op, new Term[] { a1 }, null, sjb.javaBlock)); + () -> getTermFactory().createTerm(op, new Term[]{a1}, null, sjb.javaBlock)); } @Override @@ -1150,7 +1203,7 @@ public Object visitChar_literal(KeYParser.Char_literalContext ctx) { } } return getTermFactory().createTerm(functions().lookup(new Name("C")), - toZNotation(String.valueOf(intVal), functions()).sub(0)); + toZNotation(String.valueOf(intVal), functions()).sub(0)); } public boolean isClass(String p) { @@ -1176,7 +1229,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { assert parts != null && varfuncid != null; boolean javaReference = - parts.size() > 1 && (isPackage(parts.get(0)) || isClass(parts.get(0))); + parts.size() > 1 && (isPackage(parts.get(0)) || isClass(parts.get(0))); if (javaReference) { return splitJava(parts); @@ -1190,7 +1243,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { if (varfuncid.endsWith(LIMIT_SUFFIX)) { varfuncid = varfuncid.substring(0, varfuncid.length() - 5); op = lookupVarfuncId(ctx, varfuncid, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); if (ObserverFunction.class.isAssignableFrom(op.getClass())) { op = getServices().getSpecificationRepository() .limitObs((ObserverFunction) op).first; @@ -1199,13 +1252,13 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { } } else { String firstName = - ctx.name == null ? ctx.INT_LITERAL().getText() - : ctx.name.simple_ident(0).getText(); + ctx.name == null ? ctx.INT_LITERAL().getText() + : ctx.name.simple_ident(0).getText(); op = lookupVarfuncId(ctx, firstName, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); if (op instanceof ProgramVariable v && ctx.name.simple_ident().size() > 1) { List otherParts = - ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size()); + ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size()); Term tv = getServices().getTermFactory().createTerm(v); String memberName = otherParts.get(0).getText(); if (v.sort() == getServices().getTypeConverter().getSeqLDT().targetSort()) { @@ -1213,7 +1266,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { return getServices().getTermBuilder().seqLen(tv); } else { semanticError(ctx, "There is no attribute '%s'for sequences (Seq), only " - + "'length' is supported.", memberName); + + "'length' is supported.", memberName); } } memberName = StringUtil.trim(memberName, "()"); @@ -1221,6 +1274,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { return createAttributeTerm(tv, attr, ctx); } } + return op; } @@ -1266,7 +1320,7 @@ private Term visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { // endregion KeYJavaType kjt = - getTypeByClassName(javaPackage + (javaPackage.isEmpty() ? "" : ".") + javaClass); + getTypeByClassName(javaPackage + (javaPackage.isEmpty() ? "" : ".") + javaClass); if (ctx.call() != null) { addWarning("Call of package or class"); @@ -1290,7 +1344,7 @@ private Term visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { if (pm != null) { Term[] args = visitArguments(simpleContext.call().argument_list()); current = getJavaInfo().getStaticProgramMethodTerm(attributeName, args, - kjt.getFullName()); + kjt.getFullName()); } else { semanticError(ctx, "Unknown java attribute: %s", attributeName); } @@ -1303,7 +1357,7 @@ private Term visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { String attributeName = attrid.id.getText(); Term[] args = visitArguments(attrid.call().argument_list()); current = getServices().getJavaInfo().getStaticProgramMethodTerm(attributeName, - args, className); + args, className); if (current == null) { final Sort sort = lookupSort(className); if (sort == null) { @@ -1312,7 +1366,7 @@ private Term visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { kjt = getServices().getJavaInfo().getKeYJavaType(sort); if (kjt == null) { semanticError(ctx, "Found logic sort for " + className - + " but no corresponding java type!"); + + " but no corresponding java type!"); } } return current; @@ -1347,7 +1401,7 @@ private Term handleAttributes(Term current, List att return current; } else if (ctxSuffix instanceof KeYParser.Attribute_simpleContext) { KeYParser.Attribute_simpleContext attrid = - (KeYParser.Attribute_simpleContext) ctxSuffix; + (KeYParser.Attribute_simpleContext) ctxSuffix; String memberName = attrid.id.getText(); Sort seqSort = lookupSort("Seq"); if (current.sort() == seqSort) { @@ -1355,7 +1409,7 @@ private Term handleAttributes(Term current, List att return getServices().getTermBuilder().seqLen(current); } else { semanticError(ctxSuffix, "There is no attribute '%s'for sequences (Seq), " - + "only 'length' is supported.", memberName); + + "only 'length' is supported.", memberName); } } else { boolean isCall = attrid.call() != null; @@ -1371,7 +1425,7 @@ private Term handleAttributes(Term current, List att assert kjt != null; classRef = kjt.getFullName(); current = getServices().getJavaInfo().getProgramMethodTerm(current, - memberName, sfxargs, classRef, true); + memberName, sfxargs, classRef, true); } else { Operator attr = getAttributeInPrefixSort(current.sort(), memberName); current = createAttributeTerm(current, attr, ctxSuffix); @@ -1383,7 +1437,7 @@ private Term handleAttributes(Term current, List att } } else if (ctxSuffix instanceof KeYParser.Attribute_complexContext) { KeYParser.Attribute_complexContext attrid = - (KeYParser.Attribute_complexContext) ctxSuffix; + (KeYParser.Attribute_complexContext) ctxSuffix; Term heap = accept(attrid.heap); String classRef = attrid.sort.getText(); String memberName = attrid.id.getText(); @@ -1397,10 +1451,10 @@ private Term handleAttributes(Term current, List att assert kjt != null; classRef = kjt.getFullName(); current = getServices().getJavaInfo().getProgramMethodTerm(current, memberName, - sfxargs, classRef, false); + sfxargs, classRef, false); } else { Operator op = getAttributeInPrefixSort(getTypeByClassName(classRef).getSort(), - classRef + "::" + memberName); + classRef + "::" + memberName); current = createAttributeTerm(current, op, ctxSuffix); } @@ -1412,7 +1466,7 @@ private Term handleAttributes(Term current, List att KeYJavaType kjt = getServices().getJavaInfo().getKeYJavaType(sort); if (kjt == null) { semanticError(ctxSuffix, - "Found logic sort for %s but no corresponding java type!", classRef); + "Found logic sort for %s but no corresponding java type!", classRef); } } if (heap != null) { @@ -1449,7 +1503,7 @@ public Term visitAccessterm(KeYParser.AccesstermContext ctx) { orig = variables(); List bv = accept(ctx.call().boundVars); boundVars = - bv != null ? new ImmutableArray<>(bv.toArray(new QuantifiableVariable[0])) : null; + bv != null ? new ImmutableArray<>(bv.toArray(new QuantifiableVariable[0])) : null; args = visitArguments(ctx.call().argument_list()); if (boundVars != null) { unbindVars(orig); @@ -1464,7 +1518,7 @@ public Term visitAccessterm(KeYParser.AccesstermContext ctx) { } else if (firstName.endsWith(LIMIT_SUFFIX)) { firstName = firstName.substring(0, firstName.length() - 5); op = lookupVarfuncId(ctx, firstName, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); if (ObserverFunction.class.isAssignableFrom(op.getClass())) { op = getServices().getSpecificationRepository() .limitObs((ObserverFunction) op).first; @@ -1473,7 +1527,7 @@ public Term visitAccessterm(KeYParser.AccesstermContext ctx) { } } else { op = lookupVarfuncId(ctx, firstName, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); } Term current; @@ -1498,9 +1552,9 @@ public Term visitAccessterm(KeYParser.AccesstermContext ctx) { for (QuantifiableVariable qv : args[i].freeVars()) { if (boundVars.contains(qv)) { semanticError(ctx, - "Building function term " + op - + " with bound variables failed: " + "Variable " + qv - + " must not occur free in subterm " + args[i]); + "Building function term " + op + + " with bound variables failed: " + "Variable " + qv + + " must not occur free in subterm " + args[i]); } } } @@ -1509,7 +1563,7 @@ public Term visitAccessterm(KeYParser.AccesstermContext ctx) { // create term Term[] finalArgs1 = args; current = capsulateTf(ctx, - () -> getTermFactory().createTerm(finalOp, finalArgs1, finalBoundVars, null)); + () -> getTermFactory().createTerm(finalOp, finalArgs1, finalBoundVars, null)); } } current = handleAttributes(current, ctx.attribute()); @@ -1558,16 +1612,16 @@ private Term toCNotation(String number) { private Term toFPNotation(String number) { String decBitString = - Integer.toUnsignedString(Float.floatToIntBits(Float.parseFloat(number))); + Integer.toUnsignedString(Float.floatToIntBits(Float.parseFloat(number))); // toNum("0")); // soon to disappear return getTermFactory().createTerm(functions().lookup(new Name("FP")), toNum(decBitString)); } private Term toDFPNotation(String number) { String decBitString = - Long.toUnsignedString(Double.doubleToLongBits(Double.parseDouble(number))); + Long.toUnsignedString(Double.doubleToLongBits(Double.parseDouble(number))); return getTermFactory().createTerm(functions().lookup(new Name("DFP")), - toNum(decBitString)); // toNum("0")); // soon to disappear + toNum(decBitString)); // toNum("0")); // soon to disappear } private Term toNum(String number) { @@ -1693,7 +1747,7 @@ private boolean isIntTerm(Term reference) { } private ImmutableSet lookupOperatorSV(String opName, - ImmutableSet modalities) { + ImmutableSet modalities) { SchemaVariable sv = schemaVariables().lookup(new Name(opName)); if (!(sv instanceof ModalOperatorSV)) { semanticError(null, "Schema variable " + opName + " not defined."); @@ -1727,13 +1781,13 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) { // term); return term; } - Term[] params = new Term[] { heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2) }; + Term[] params = new Term[]{heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2)}; return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); + () -> getServices().getTermFactory().createTerm(term.op(), params)); } else if (term.op() instanceof ObserverFunction) { if (!isImplicitHeap(term.sub(0))) { semanticError(null, "Expecting program variable heap as first argument of: %s", - term); + term); } Term[] params = new Term[term.arity()]; @@ -1744,7 +1798,7 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) { } return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); + () -> getServices().getTermFactory().createTerm(term.op(), params)); } return term; @@ -1756,7 +1810,7 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) { protected Term heapSelectionSuffix(Term term, Term heap, ParserRuleContext ctx) { if (!isHeapTerm(heap)) { semanticError(null, "Expecting term of type Heap but sort is %s for term %s", - heap.sort(), term); + heap.sort(), term); } Term result = replaceHeap(term, heap, ctx); return result; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index 69785ef1614..6bfa18276df 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.nparser.builder; import java.util.List; +import java.util.Objects; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Name; @@ -11,9 +12,13 @@ import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.logic.op.SortDependingFunction; import de.uka.ilkd.key.logic.op.Transformer; +import de.uka.ilkd.key.logic.overop.FunctionMetaData; +import de.uka.ilkd.key.logic.overop.InfixMetaData; +import de.uka.ilkd.key.logic.overop.OperatorInfo; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.logic.sort.Sort; import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.pp.NotationInfo; import org.key_project.util.collection.ImmutableArray; @@ -76,6 +81,11 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { Function p = null; + ImmutableArray metaData = null; + if (ctx.functionMetaData() != null) { + metaData = accept(ctx.functionMetaData()); + } + int separatorIndex = pred_name.indexOf("::"); if (separatorIndex > 0) { String sortName = pred_name.substring(0, separatorIndex); @@ -84,16 +94,19 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { if (genSort instanceof GenericSort) { assert argSorts != null; p = SortDependingFunction.createFirstInstance((GenericSort) genSort, - new Name(baseName), Sort.FORMULA, argSorts.toArray(new Sort[0]), false); + new Name(baseName), Sort.FORMULA, argSorts.toArray(new Sort[0]), false, + metaData); } } if (p == null) { assert argSorts != null; p = new Function(new Name(pred_name), Sort.FORMULA, argSorts.toArray(new Sort[0]), - whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), false); + whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), false, + metaData); } + if (lookup(p.name()) == null) { functions().add(p); } else { @@ -103,6 +116,51 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { return null; } + @Override + public ImmutableArray visitInfixMetaData(KeYParser.InfixMetaDataContext ctx) { + return ctx.infixOperator().stream() + .filter(Objects::nonNull) + .map(it -> { + var opInfo = OperatorInfo.find(it.start); + if (opInfo != null) { + return new InfixMetaData(opInfo.getNames(), opInfo.getPrecedence()); + } else { + int prec = 0; + if (it.opEqualities() != null) + prec = NotationInfo.PRIORITY_EQUAL; + if (it.opComparison() != null) + prec = NotationInfo.PRIORITY_COMPARISON; + if (it.opStrong1() != null) + prec = NotationInfo.PRIORITY_ARITH_STRONG; + if (it.opStrong2() != null) + prec = NotationInfo.PRIORITY_ARITH_STRONG; + if (it.opWeak() != null) + prec = NotationInfo.PRIORITY_ARITH_WEAK; + if (it.opConjunction() != null) + prec = NotationInfo.PRIORITY_AND; + if (it.opDisjunction() != null) + prec = NotationInfo.PRIORITY_OR; + return new InfixMetaData(it.getText(), prec); + } + }).collect(ImmutableArray.collector()); + } + + + @Override + public Object visitPrefixMetaData(KeYParser.PrefixMetaDataContext ctx) { + return super.visitPrefixMetaData(ctx); + } + + @Override + public Object visitPostfixMetaData(KeYParser.PostfixMetaDataContext ctx) { + return super.visitPostfixMetaData(ctx); + } + + @Override + public Object visitShortcutMetaData(KeYParser.ShortcutMetaDataContext ctx) { + return super.visitShortcutMetaData(ctx); + } + @Override public Object visitFunc_decl(KeYParser.Func_declContext ctx) { boolean unique = ctx.UNIQUE() != null; @@ -116,6 +174,13 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) { semanticError(ctx, "Where-to-bind list must have same length as argument list"); } + + ImmutableArray metaData = null; + if (ctx.functionMetaData() != null) { + metaData = accept(ctx.functionMetaData()); + } + + Function f = null; assert funcName != null; int separatorIndex = funcName.indexOf("::"); @@ -125,13 +190,20 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) { Sort genSort = lookupSort(sortName); if (genSort instanceof GenericSort) { f = SortDependingFunction.createFirstInstance((GenericSort) genSort, - new Name(baseName), retSort, argSorts.toArray(new Sort[0]), unique); + new Name(baseName), + retSort, + argSorts.toArray(new Sort[0]), + unique, + metaData); } } if (f == null) { - f = new Function(new Name(funcName), retSort, argSorts.toArray(new Sort[0]), - whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), unique); + f = new Function(new Name(funcName), + retSort, argSorts.toArray(new Sort[0]), + whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), + unique, + metaData); } if (lookup(f.name()) == null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java index fd9313c37fb..77c2fb0780f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java @@ -80,28 +80,26 @@ */ public final class NotationInfo { - - // Priorities of operators (roughly corresponding to the grammatical structure in the parser. - static final int PRIORITY_TOP = 0; - static final int PRIORITY_EQUIVALENCE = 20; - static final int PRIORITY_IMP = 30; - static final int PRIORITY_OR = 40; - static final int PRIORITY_AND = 50; - static final int PRIORITY_NEGATION = 60; - static final int PRIORITY_QUANTIFIER = 60; - static final int PRIORITY_MODALITY = 60; - static final int PRIORITY_POST_MODALITY = 60; - static final int PRIORITY_EQUAL = 70; - static final int PRIORITY_COMPARISON = 80; - static final int PRIORITY_ARITH_WEAK = 90; - static final int PRIORITY_BELOW_ARITH_WEAK = 91; - static final int PRIORITY_ARITH_STRONG = 100; - static final int PRIORITY_BELOW_ARITH_STRONG = 101; - static final int PRIORITY_CAST = 120; - static final int PRIORITY_ATOM = 130; - static final int PRIORITY_BOTTOM = 140; - static final int PRIORITY_LABEL = 140; // TODO: find appropriate value + public static final int PRIORITY_TOP = 0; + public static final int PRIORITY_EQUIVALENCE = 20; + public static final int PRIORITY_IMP = 30; + public static final int PRIORITY_OR = 40; + public static final int PRIORITY_AND = 50; + public static final int PRIORITY_NEGATION = 60; + public static final int PRIORITY_QUANTIFIER = 60; + public static final int PRIORITY_MODALITY = 60; + public static final int PRIORITY_POST_MODALITY = 60; + public static final int PRIORITY_EQUAL = 70; + public static final int PRIORITY_COMPARISON = 80; + public static final int PRIORITY_ARITH_WEAK = 90; + public static final int PRIORITY_BELOW_ARITH_WEAK = 91; + public static final int PRIORITY_ARITH_STRONG = 100; + public static final int PRIORITY_BELOW_ARITH_STRONG = 101; + public static final int PRIORITY_CAST = 120; + public static final int PRIORITY_ATOM = 130; + public static final int PRIORITY_BOTTOM = 140; + public static final int PRIORITY_LABEL = 140; // TODO: find appropriate value public static boolean DEFAULT_PRETTY_SYNTAX = true; @@ -468,6 +466,10 @@ Notation getNotation(Operator op) { } } + if (op instanceof Function) { + return new Notation.FunctionNotation(); + } + return new Notation.FunctionNotation(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java index 2c584aa6fa8..51e3624aa40 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java @@ -93,6 +93,8 @@ public boolean hasErrors() { */ public void throwException() { if (hasErrors()) { + var log = LoggerFactory.getLogger(SyntaxErrorReporter.class); + errors.forEach(it -> log.error(it.toString())); throw new ParserException("", errors); } } @@ -165,6 +167,19 @@ public String showInInput(String[] lines) { public String positionAsUrl() { return String.format("file://source:%d", line); } + + @Override + public String toString() { + return "SyntaxError{" + + "recognizer=" + recognizer + + ", line=" + line + + ", offendingSymbol=" + offendingSymbol + + ", charPositionInLine=" + charPositionInLine + + ", msg='" + msg + '\'' + + ", source=" + source + + ", stack='" + stack + '\'' + + '}'; + } } public static class ParserException extends RuntimeException implements HasLocation { diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatHeader.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatHeader.key index 8a4e68bb6f8..86ae7c60a53 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatHeader.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatHeader.key @@ -36,11 +36,11 @@ float javaDivFloatForbiddenResult(float, float); // Floating-point arithmetic with IEEE 754 semantics - float addFloat(float, float); - float subFloat(float, float); - float mulFloat(float, float); - float divFloat(float, float); - float negFloat(float); + float addFloat(float, float) \infix(+); + float subFloat(float, float) \infix(-); + float mulFloat(float, float) \infix(*); + float divFloat(float, float) \infix(/); + float negFloat(float) \prefix(-); float absFloat(float); @@ -63,11 +63,11 @@ double javaDivDoubleForbiddenResult(double, double); // Double arithmetic with IEEE 754 semantics - double addDouble(double, double); - double subDouble(double, double); - double mulDouble(double, double); - double divDouble(double, double); - double negDouble(double); + double addDouble(double, double) \infix(+); + double subDouble(double, double) \infix(-); + double mulDouble(double, double) \infix(*); + double divDouble(double, double) \infix(/); + double negDouble(double) \prefix(-); double absDouble(double); @@ -86,11 +86,11 @@ \predicates { - ltFloat(float, float); - gtFloat(float, float); - leqFloat(float, float); - geqFloat(float, float); - eqFloat(float, float); + ltFloat(float, float) \infix(<); + gtFloat(float, float) \infix(>); + leqFloat(float, float) \infix(<=); + geqFloat(float, float) \infix(>=); + eqFloat(float, float) \infix(=); floatIsNaN(float); floatIsZero(float); @@ -101,11 +101,11 @@ floatIsNegative(float); floatIsNice(float); - ltDouble(double, double); - gtDouble(double, double); - leqDouble(double, double); - geqDouble(double, double); - eqDouble(double, double); + ltDouble(double, double) \infix(<); + gtDouble(double, double) \infix(>); + leqDouble(double, double) \infix(<=); + geqDouble(double, double) \infix(>=); + eqDouble(double, double) \infix(=); doubleIsNaN(double); doubleIsZero(double); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key index 73337d3d4d9..11815c064c6 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key @@ -37,13 +37,13 @@ int C(numbers); // arithmetic operators on mathematical integers - int add(int, int); + int add(int, int) \infix(+); int neg(int); - int sub(int, int); - int mul(int, int); - int div(int, int); - int mod(int, int); - int pow(int, int); + int sub(int, int) \infix(-); + int mul(int, int) \infix(*); + int div(int, int) \infix(/); + int mod(int, int) \infix(%); + int pow(int, int) \infix(**); int log(int, int); // comprehensions @@ -242,10 +242,10 @@ // from the current integer semantics. // ---------------------------------------------------------------------------- - leq(int, int); - lt(int, int); - geq(int, int); - gt(int, int); + leq(int, int) \infix(<=); + lt(int, int) \infix(<); + geq(int, int) \infix(>=); + gt(int, int) \infix(>); // ---------------------------------------------------------------------------- // The functions declared below change their semantics when switching the diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key index b1a2a9a2cd4..642ffa51230 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key @@ -16,9 +16,9 @@ // other constructors LocSet singleton(Object, Field); - LocSet union(LocSet, LocSet); - LocSet intersect(LocSet, LocSet); - LocSet setMinus(LocSet, LocSet); + LocSet union(LocSet, LocSet) \infix(\cup +); + LocSet intersect(LocSet, LocSet) \infix(\cap); + LocSet setMinus(LocSet, LocSet) \infix(\setminus -); LocSet infiniteUnion {true}(LocSet); LocSet allFields(Object); LocSet allObjects(Field); @@ -31,7 +31,7 @@ \predicates { elementOf(Object, Field, LocSet); - subset(LocSet, LocSet); + subset(LocSet, LocSet) \infix(\subseteq); disjoint(LocSet, LocSet); createdInHeap(LocSet, Heap); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key index e88d2e928ad..0616b806d5b 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key @@ -27,13 +27,13 @@ // constructors Seq seqEmpty; Seq seqSingleton(any); - Seq seqConcat(Seq, Seq); + Seq seqConcat(Seq, Seq) \infix(+); Seq seqSub(Seq, int, int); - Seq seqReverse(Seq); + Seq seqReverse(Seq) \prefix(~); Seq seqDef {false, false, true}(int, int, any); Seq seqSwap(Seq, int, int); - Seq seqRemove(Seq, int); + Seq seqRemove(Seq, int) \prefix(-); Seq seqNPermInv(Seq); Seq array2seq(Heap, Object); diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java index 125a42fe935..8946ba68675 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java @@ -4,14 +4,23 @@ package de.uka.ilkd.key.nparser; import java.io.IOException; +import java.io.PrintWriter; +import java.io.StringWriter; +import java.lang.reflect.Field; import java.net.URL; +import java.util.*; +import java.util.stream.Collectors; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.overop.OperatorInfo; +import de.uka.ilkd.key.pp.LogicPrinter; +import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.proof.init.JavaProfile; -import de.uka.ilkd.key.util.parsing.BuildingException; +import org.jspecify.annotations.NonNull; import org.junit.jupiter.api.Assumptions; +import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.CsvFileSource; import org.slf4j.Logger; @@ -27,26 +36,69 @@ public class ExprTest { private static final Logger LOGGER = LoggerFactory.getLogger(ExprTest.class); + @Test + public void printOpTable() throws IllegalAccessException { + var sw = new StringWriter(); + var out = new PrintWriter(sw); + + var map = new TreeMap>(); + for (OperatorInfo value : OperatorInfo.values()) { + if (!map.containsKey(value.getPrecedence())) + map.put(value.getPrecedence(), new LinkedList<>()); + map.get(value.getPrecedence()).add(value); + } + out.println("| Level | Operators |"); + out.println(":-: | -----------"); + var levels = Arrays.stream(NotationInfo.class.getFields()) + .filter(it -> it.getName().startsWith("PRIORITY_")) + .sorted(Comparator.comparing(it -> { + try { + return it.getInt(null); + } catch (IllegalAccessException e) { + throw new RuntimeException(e); + } + })).toList(); + + for (Field f : levels) { + int level = f.getInt(null); + var values = map.get(level); + var a = ""; + if (values != null) + a = values.stream() + .flatMap(it -> it.getNames().stream()) + .map(it -> "`" + it + "`") + .collect(Collectors.joining(" ")); + out.format("| %d | %s | %s |\n", + level, f.getName().substring(9), + a); + } + System.out.println(sw); + } + + @ParameterizedTest @CsvFileSource(resources = "exprs.txt", delimiter = '^') public void parseAndVisit(String expr) throws IOException { Assumptions.assumeFalse(expr.startsWith("#")); KeyIO io = getIo(); - try { - Term actual = io.parseExpression(expr); - assertNotNull(actual); - LOGGER.info("Term: {}", actual); - } catch (BuildingException e) { - DebugKeyLexer.debug(expr); - } + @NonNull + Term actual = io.parseExpression(expr); + assertNotNull(actual); + LOGGER.info("Actual Term: {}", actual); + + LOGGER.warn("Actual Term: {}", + LogicPrinter.quickPrintTerm(actual, io.getServices(), true, true)); } + private KeyIO io; private KeyIO getIo() throws IOException { + if(io!=null)return io; + Services services = new Services(new JavaProfile()); String p = "/de/uka/ilkd/key/proof/rules/ldt.key"; URL url = getClass().getResource(p); Assumptions.assumeTrue(url != null); - KeyIO io = new KeyIO(services); + io = new KeyIO(services); io.load(url).parseFile().loadDeclarations().loadSndDegreeDeclarations(); NamespaceBuilder nssb = new NamespaceBuilder(services.getNamespaces()); @@ -56,7 +108,6 @@ private KeyIO getIo() throws IOException { // Without this call, the LDTs are not available to the expression // builder. Probably a problem of the mocking here. (MU) services.getTypeConverter().init(); - return io; } diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exprs.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exprs.txt index 2cad0b7cffb..fcdd70ece73 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exprs.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exprs.txt @@ -33,4 +33,3 @@ seqEmpty + seqEmpty \emptyset ∪ ∅ \cap ∅ = (∅ \cup ∅) ∩ ∅ ∅ ⊆ \emptyset \emptyset ∖ \emptyset -(∅ ∊ ∅) & true \ No newline at end of file diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index aefc3822e32..aa764988fc7 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java @@ -4,11 +4,12 @@ package org.key_project.util.collection; import java.lang.reflect.Array; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.Collection; -import java.util.Iterator; -import java.util.List; +import java.util.*; +import java.util.function.BiConsumer; +import java.util.function.BinaryOperator; +import java.util.function.Function; +import java.util.function.Supplier; +import java.util.stream.Collector; import java.util.stream.Stream; import java.util.stream.StreamSupport; @@ -39,7 +40,7 @@ public ImmutableArray() { * @param arr the ProgrammElement array to wrap */ @SuppressWarnings("unchecked") - public ImmutableArray(S... arr) { + public ImmutableArray(@NonNull S... arr) { content = (S[]) Array.newInstance(arr.getClass().getComponentType(), arr.length); System.arraycopy(arr, 0, content, 0, arr.length); } @@ -65,6 +66,41 @@ public ImmutableArray(@NonNull Collection list) { content = (S[]) list.toArray(); } + /** + * A collector for the creation of {@link ImmutableArray} from streams. + */ + public static Collector, ImmutableArray> collector() { + return new Collector<>() { + @Override + public Supplier> supplier() { + return ArrayList::new; + } + + @Override + public BiConsumer, T> accumulator() { + return ArrayList::add; + } + + @Override + public BinaryOperator> combiner() { + return (a, b) -> { + a.addAll(b); + return a; + }; + } + + @Override + public Function, ImmutableArray> finisher() { + return ImmutableArray::new; + } + + @Override + public Set characteristics() { + return Set.of(); + } + }; + } + /** * gets the element at the specified position *