Skip to content

Add Polymorphic Sorts and Functions #3652

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Drodt merged 34 commits into from
Mar 13, 2026
Merged

Add Polymorphic Sorts and Functions #3652

Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
f6b9328
Start on polymorphic sorts and functions
Drodt Aug 4, 2025
d8083c9
Fix SortDepFn and add test
Drodt Aug 13, 2025
d271eec
Merge branch 'main' into drodt/polymorphic
Drodt Aug 13, 2025
7a45443
Fix fns and preds parsing; add test
Drodt Aug 13, 2025
a73bcdd
Finish example; slight fixes
Drodt Aug 14, 2025
2071d12
Spotless
Drodt Aug 14, 2025
be13de6
Merge branch 'main' into drodt/polymorphic
Drodt Aug 18, 2025
04c4de8
Merge branch 'main' into drodt/polymorphic
Drodt Sep 24, 2025
46f7c7a
Prepare datatype handling
Drodt Sep 24, 2025
4f540f5
Fix taclets for datatypes w/ polymorphic params
Drodt Sep 25, 2025
412e84a
Slightly improve error messages
Drodt Sep 25, 2025
d1555e5
Fix test classes
Drodt Sep 25, 2025
f8aceda
Some documentation
Drodt Sep 25, 2025
cb55569
Fix proof loading/storing when generics are instantiated in NoFindTac…
Drodt Sep 26, 2025
8115a30
Fix parsing of proof files
Drodt Oct 30, 2025
1e7d61b
Merge branch 'main' into drodt/polymorphic
Drodt Oct 30, 2025
0f8b28a
Fix inst with sort depending fn
Drodt Oct 30, 2025
6eee25a
Start on polymorphic sorts and functions
Drodt Aug 4, 2025
67a3d0e
Fix SortDepFn and add test
Drodt Aug 13, 2025
ed34645
Fix fns and preds parsing; add test
Drodt Aug 13, 2025
76d7f62
Finish example; slight fixes
Drodt Aug 14, 2025
2d48890
Spotless
Drodt Aug 14, 2025
64cb56a
Prepare datatype handling
Drodt Sep 24, 2025
597336c
Fix taclets for datatypes w/ polymorphic params
Drodt Sep 25, 2025
6017886
Slightly improve error messages
Drodt Sep 25, 2025
39d3d92
Fix test classes
Drodt Sep 25, 2025
bbc0945
Some documentation
Drodt Sep 25, 2025
5d64af9
Fix proof loading/storing when generics are instantiated in NoFindTac…
Drodt Sep 26, 2025
7c0fb9d
Fix parsing of proof files
Drodt Oct 30, 2025
5f9de0a
Fix inst with sort depending fn
Drodt Oct 30, 2025
91e0e5c
Remove tokens file
Drodt Mar 10, 2026
2e6f515
Simplify
Drodt Mar 10, 2026
79ce7cc
Merge branch 'drodt/polymorphic' of https://github.com/KeYProject/key…
Drodt Mar 12, 2026
c20131d
Add containsGenerics method to sort
Drodt Mar 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions key.core/src/main/antlr4/KeYLexer.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -381,6 +381,8 @@ GREATEREQUAL
: '>' '=' | '\u2265'
;

OPENTYPEPARAMS : '<[';
CLOSETYPEPARAMS : ']>';

WS: [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace
STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ;
Expand Down
388 changes: 388 additions & 0 deletions key.core/src/main/antlr4/KeYLexer.tokens
View file
Open in desktop
Comment thread
Drodt marked this conversation as resolved.
Original file line number Diff line number Diff line change
@@ -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
Loading
Loading