Add Polymorphic Sorts and Functions

key.core/src/main/antlr4/KeYLexer.g4

@@ -381,6 +381,8 @@ GREATEREQUAL
 :   '>' '=' | '\u2265'
       ;
 
+OPENTYPEPARAMS : '<[';
+CLOSETYPEPARAMS : ']>';
 
 WS:  [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace
 STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ;

key.core/src/main/antlr4/KeYLexer.tokens

@@ -0,0 +1,388 @@
+MODALITY=1
+SORTS=2
+GENERIC=3
+PROXY=4
+EXTENDS=5
+ONEOF=6
+ABSTRACT=7
+SCHEMAVARIABLES=8
+SCHEMAVAR=9
+MODALOPERATOR=10
+PROGRAM=11
+FORMULA=12
+TERM=13
+UPDATE=14
+VARIABLES=15
+VARIABLE=16
+SKOLEMTERM=17
+SKOLEMFORMULA=18
+TERMLABEL=19
+MODIFIABLE=20
+PROGRAMVARIABLES=21
+STORE_TERM_IN=22
+STORE_STMT_IN=23
+HAS_INVARIANT=24
+GET_INVARIANT=25
+GET_FREE_INVARIANT=26
+GET_VARIANT=27
+IS_LABELED=28
+SAME_OBSERVER=29
+VARCOND=30
+APPLY_UPDATE_ON_RIGID=31
+DEPENDINGON=32
+DISJOINTMODULONULL=33
+DROP_EFFECTLESS_ELEMENTARIES=34
+DROP_EFFECTLESS_STORES=35
+SIMPLIFY_IF_THEN_ELSE_UPDATE=36
+ENUM_CONST=37
+FREELABELIN=38
+HASSORT=39
+FIELDTYPE=40
+FINAL=41
+ELEMSORT=42
+HASLABEL=43
+HASSUBFORMULAS=44
+ISARRAY=45
+ISARRAYLENGTH=46
+ISCONSTANT=47
+ISENUMTYPE=48
+ISINDUCTVAR=49
+ISLOCALVARIABLE=50
+ISOBSERVER=51
+DIFFERENT=52
+METADISJOINT=53
+ISTHISREFERENCE=54
+DIFFERENTFIELDS=55
+ISREFERENCE=56
+ISREFERENCEARRAY=57
+ISSTATICFIELD=58
+ISMODELFIELD=59
+ISINSTRICTFP=60
+ISSUBTYPE=61
+EQUAL_UNIQUE=62
+NEW=63
+NEW_TYPE_OF=64
+NEW_DEPENDING_ON=65
+NEW_LOCAL_VARS=66
+HAS_ELEMENTARY_SORT=67
+NEWLABEL=68
+CONTAINS_ASSIGNMENT=69
+NOT_=70
+NOTFREEIN=71
+SAME=72
+STATIC=73
+STATICMETHODREFERENCE=74
+MAXEXPANDMETHOD=75
+STRICT=76
+TYPEOF=77
+INSTANTIATE_GENERIC=78
+FORALL=79
+EXISTS=80
+SUBST=81
+IF=82
+IFEX=83
+THEN=84
+ELSE=85
+INCLUDE=86
+INCLUDELDTS=87
+CLASSPATH=88
+BOOTCLASSPATH=89
+NODEFAULTCLASSES=90
+JAVASOURCE=91
+WITHOPTIONS=92
+OPTIONSDECL=93
+KEYSETTINGS=94
+PROFILE=95
+TRUE=96
+FALSE=97
+SAMEUPDATELEVEL=98
+INSEQUENTSTATE=99
+ANTECEDENTPOLARITY=100
+SUCCEDENTPOLARITY=101
+CLOSEGOAL=102
+HEURISTICSDECL=103
+NONINTERACTIVE=104
+DISPLAYNAME=105
+HELPTEXT=106
+REPLACEWITH=107
+ADDRULES=108
+ADDPROGVARS=109
+HEURISTICS=110
+FIND=111
+ADD=112
+ASSUMES=113
+TRIGGER=114
+AVOID=115
+PREDICATES=116
+FUNCTIONS=117
+DATATYPES=118
+TRANSFORMERS=119
+UNIQUE=120
+FREE=121
+RULES=122
+AXIOMS=123
+PROBLEM=124
+CHOOSECONTRACT=125
+PROOFOBLIGATION=126
+PROOF=127
+PROOFSCRIPT=128
+CONTRACTS=129
+INVARIANTS=130
+LEMMA=131
+IN_TYPE=132
+IS_ABSTRACT_OR_INTERFACE=133
+IS_FINAL=134
+CONTAINERTYPE=135
+UTF_PRECEDES=136
+UTF_IN=137
+UTF_EMPTY=138
+UTF_UNION=139
+UTF_INTERSECT=140
+UTF_SUBSET_EQ=141
+UTF_SUBSEQ=142
+UTF_SETMINUS=143
+SEMI=144
+SLASH=145
+COLON=146
+DOUBLECOLON=147
+ASSIGN=148
+DOT=149
+DOTRANGE=150
+COMMA=151
+LPAREN=152
+RPAREN=153
+LBRACE=154
+RBRACE=155
+LBRACKET=156
+RBRACKET=157
+EMPTYBRACKETS=158
+AT=159
+PARALLEL=160
+OR=161
+AND=162
+NOT=163
+IMP=164
+EQUALS=165
+NOT_EQUALS=166
+SEQARROW=167
+EXP=168
+TILDE=169
+PERCENT=170
+STAR=171
+MINUS=172
+PLUS=173
+GREATER=174
+GREATEREQUAL=175
+OPENTYPEPARAMS=176
+CLOSETYPEPARAMS=177
+WS=178
+STRING_LITERAL=179
+LESS=180
+LESSEQUAL=181
+LGUILLEMETS=182
+RGUILLEMETS=183
+EQV=184
+CHAR_LITERAL=185
+QUOTED_STRING_LITERAL=186
+SL_COMMENT=187
+BIN_LITERAL=188
+HEX_LITERAL=189
+IDENT=190
+INT_LITERAL=191
+FLOAT_LITERAL=192
+DOUBLE_LITERAL=193
+REAL_LITERAL=194
+ERROR_UKNOWN_ESCAPE=195
+ERROR_CHAR=196
+COMMENT_END=197
+DOC_COMMENT=198
+ML_COMMENT=199
+MODALITYD=200
+MODALITYB=201
+MODALITYBB=202
+MODAILITYGENERIC1=203
+MODAILITYGENERIC2=204
+MODAILITYGENERIC3=205
+MODAILITYGENERIC4=206
+MODAILITYGENERIC5=207
+MODAILITYGENERIC6=208
+MODAILITYGENERIC7=209
+MODALITYD_END=210
+MODALITYD_STRING=211
+MODALITYD_CHAR=212
+MODALITYG_END=213
+MODALITYB_END=214
+MODALITYBB_END=215
+'\\sorts'=2
+'\\generic'=3
+'\\proxy'=4
+'\\extends'=5
+'\\oneof'=6
+'\\abstract'=7
+'\\schemaVariables'=8
+'\\schemaVar'=9
+'\\modalOperator'=10
+'\\program'=11
+'\\formula'=12
+'\\term'=13
+'\\update'=14
+'\\variables'=15
+'\\variable'=16
+'\\skolemTerm'=17
+'\\skolemFormula'=18
+'\\termlabel'=19
+'\\modifiable'=20
+'\\programVariables'=21
+'\\storeTermIn'=22
+'\\storeStmtIn'=23
+'\\hasInvariant'=24
+'\\getInvariant'=25
+'\\getFreeInvariant'=26
+'\\getVariant'=27
+'\\isLabeled'=28
+'\\sameObserver'=29
+'\\varcond'=30
+'\\applyUpdateOnRigid'=31
+'\\dependingOn'=32
+'\\disjointModuloNull'=33
+'\\dropEffectlessElementaries'=34
+'\\dropEffectlessStores'=35
+'\\simplifyIfThenElseUpdate'=36
+'\\enumConstant'=37
+'\\freeLabelIn'=38
+'\\hasSort'=39
+'\\fieldType'=40
+'\\final'=41
+'\\elemSort'=42
+'\\hasLabel'=43
+'\\hasSubFormulas'=44
+'\\isArray'=45
+'\\isArrayLength'=46
+'\\isConstant'=47
+'\\isEnumType'=48
+'\\isInductVar'=49
+'\\isLocalVariable'=50
+'\\isObserver'=51
+'\\different'=52
+'\\metaDisjoint'=53
+'\\isThisReference'=54
+'\\differentFields'=55
+'\\isReference'=56
+'\\isReferenceArray'=57
+'\\isStaticField'=58
+'\\isModelField'=59
+'\\isInStrictFp'=60
+'\\sub'=61
+'\\equalUnique'=62
+'\\new'=63
+'\\newTypeOf'=64
+'\\newDependingOn'=65
+'\\newLocalVars'=66
+'\\hasElementarySort'=67
+'\\newLabel'=68
+'\\containsAssignment'=69
+'\\not'=70
+'\\notFreeIn'=71
+'\\same'=72
+'\\static'=73
+'\\staticMethodReference'=74
+'\\mayExpandMethod'=75
+'\\strict'=76
+'\\typeof'=77
+'\\instantiateGeneric'=78
+'\\subst'=81
+'\\if'=82
+'\\ifEx'=83
+'\\then'=84
+'\\else'=85
+'\\include'=86
+'\\includeLDTs'=87
+'\\classpath'=88
+'\\bootclasspath'=89
+'\\noDefaultClasses'=90
+'\\javaSource'=91
+'\\withOptions'=92
+'\\optionsDecl'=93
+'\\settings'=94
+'\\profile'=95
+'true'=96
+'false'=97
+'\\sameUpdateLevel'=98
+'\\inSequentState'=99
+'\\antecedentPolarity'=100
+'\\succedentPolarity'=101
+'\\closegoal'=102
+'\\heuristicsDecl'=103
+'\\noninteractive'=104
+'\\displayname'=105
+'\\helptext'=106
+'\\replacewith'=107
+'\\addrules'=108
+'\\addprogvars'=109
+'\\heuristics'=110
+'\\find'=111
+'\\add'=112
+'\\assumes'=113
+'\\trigger'=114
+'\\avoid'=115
+'\\predicates'=116
+'\\functions'=117
+'\\datatypes'=118
+'\\transformers'=119
+'\\unique'=120
+'\\free'=121
+'\\rules'=122
+'\\axioms'=123
+'\\problem'=124
+'\\chooseContract'=125
+'\\proofObligation'=126
+'\\proof'=127
+'\\proofScript'=128
+'\\contracts'=129
+'\\invariants'=130
+'\\lemma'=131
+'\\inType'=132
+'\\isAbstractOrInterface'=133
+'\\isFinal'=134
+'\\containerType'=135
+';'=144
+'/'=145
+':'=146
+'::'=147
+':='=148
+'.'=149
+','=151
+'('=152
+')'=153
+'{'=154
+'}'=155
+'['=156
+']'=157
+'@'=159
+'='=165
+'^'=168
+'~'=169
+'%'=170
+'*'=171
+'-'=172
+'+'=173
+'>'=174
+'<['=176
+']>'=177
+'<'=180
+'/*!'=198
+'/*'=199
+'\\<'=200
+'\\['=201
+'\\[['=202
+'\\box'=203
+'\\diamond'=204
+'\\diamond_transaction'=205
+'\\modality'=206
+'\\box_transaction'=207
+'\\throughout'=208
+'\\throughout_transaction'=209
+'\\>'=210
+'\\endmodality'=213
+'\\]'=214
+'\\]]'=215