diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java index 0b61603b3eb..8009f5ab889 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java @@ -274,7 +274,7 @@ private Taclet genInfFlowContractApplTaclet(Goal goal, ProofObligationVars appDa tacletBuilder.setFind(schemaFind); tacletBuilder.setApplicationRestriction( new ApplicationRestriction(ApplicationRestriction.ANTECEDENT_POLARITY)); - tacletBuilder.setIfSequent(assumesSeq); + tacletBuilder.setAssumesSequent(assumesSeq); RewriteTacletGoalTemplate goalTemplate = new RewriteTacletGoalTemplate(replaceWithSeq, ImmutableSLList.nil(), schemaFind); tacletBuilder.addTacletGoalTemplate(goalTemplate); @@ -311,7 +311,7 @@ public InfFlowContractAppTaclet getRewriteTaclet() { TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(this); prefixBuilder.build(); return new InfFlowContractAppTaclet(name, - new TacletApplPart(ifseq, applicationRestriction, varsNew, varsNotFreeIn, + new TacletApplPart(assumesSeq, applicationRestriction, varsNew, varsNotFreeIn, varsNewDependingOn, variableConditions), goals, ruleSets, attrs, (JTerm) find, prefixBuilder.getPrefixMap(), diff --git a/key.core.testgen/testcases/arrayutil/actual/build.gradle.kts b/key.core.testgen/testcases/arrayutil/actual/build.gradle.kts new file mode 100644 index 00000000000..23ceacaa016 --- /dev/null +++ b/key.core.testgen/testcases/arrayutil/actual/build.gradle.kts @@ -0,0 +1,23 @@ +package de.uka.ilkd.key.tcg + +plugins { + java +} + +repositories { + mavenCentral() +} + +dependencies { + testImplementation(platform("org.junit:junit-bom:5.13.2")) + testImplementation("org.junit.jupiter:junit-jupiter-api") + testRuntimeOnly("org.junit.jupiter:junit-jupiter-engine") + testRuntimeOnly("org.junit.platform:junit-platform-launcher") + + testImplementation("org.objenesis:objenesis:3.3") + testImplementation("org.hamcrest:hamcrest-core:2.2") +} + +tasks.withType { + useJUnitPlatform() +} diff --git a/key.core.testgen/testcases/arrayutil/actual/build.xml b/key.core.testgen/testcases/arrayutil/actual/build.xml new file mode 100644 index 00000000000..04efc1915da --- /dev/null +++ b/key.core.testgen/testcases/arrayutil/actual/build.xml @@ -0,0 +1,65 @@ + + + simple example build file + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/key.core.testgen/testcases/arrayutil/actual/pom.xml b/key.core.testgen/testcases/arrayutil/actual/pom.xml new file mode 100644 index 00000000000..f3af8138868 --- /dev/null +++ b/key.core.testgen/testcases/arrayutil/actual/pom.xml @@ -0,0 +1,29 @@ + + + 4.0.0 + generated + generated + 1.0.0-SNAPSHOT + jar + + + + org.junit.jupiter + junit-jupiter-api + 5.11.3 + test + + + org.objenesis + objenesis + 3.3 + test + + + org.hamcrest + hamcrest-core + 2.2 + test + + + \ No newline at end of file diff --git a/key.core.testgen/testcases/arrayutil/actual/src/main/java/ArrayUtils.java b/key.core.testgen/testcases/arrayutil/actual/src/main/java/ArrayUtils.java new file mode 100644 index 00000000000..19b30f44f75 --- /dev/null +++ b/key.core.testgen/testcases/arrayutil/actual/src/main/java/ArrayUtils.java @@ -0,0 +1,14 @@ +/** From the second KeY book. + * https://link.springer.com/chapter/10.1007/978-3-319-49812-6_12 + * Listing 12.1 + */ +public class ArrayUtils { + /*@ public normal_behavior + @ ensures (\forall int i; 0<=i && i allBools, + Set allInts, Set allObjects, Map old) { + return ((sub1(exc, _preexc, a, _prea, self, _preself, b, _preb, allBools, allInts, allObjects, old) && inv_javalangObject(self, exc, _preexc, a, _prea, self, _preself, b, _preb, allBools, allInts, allObjects, old)) && (exc == null)); + } + + boolean inv_javalangObject(java.lang.Object o, java.lang.Throwable exc, + java.lang.Throwable _preexc, int[] a, int[] _prea, ArrayUtils self, ArrayUtils _preself, + int[] b, int[] _preb, Set allBools, Set allInts, + Set allObjects, Map old) { + return true; + } + + boolean sub1(java.lang.Throwable exc, java.lang.Throwable _preexc, int[] a, int[] _prea, + ArrayUtils self, ArrayUtils _preself, int[] b, int[] _preb, Set allBools, + Set allInts, Set allObjects, Map old) { + for(int i : allInts) { + if(!(!((0 <= i) && (i < a.length)) || (a[i] == b[i]))) { + return false; + } + } + return true; + } +} diff --git a/key.core/build.gradle b/key.core/build.gradle index eedd94a7f58..f5cfcb1106b 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -170,14 +170,15 @@ processResources.dependsOn generateVersionFiles, generateSolverPropsList, genera def antlr4OutputKey = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/nparser" tasks.register('runAntlr4Key', JavaExec) { //see incremental task api, prevents rerun if nothing has changed. - inputs.files "src/main/antlr4/KeYLexer.g4", "src/main/antlr4/KeYParser.g4" + inputs.files "src/main/antlr4/JavaKeYLexer.g4", "src/main/antlr4/JavaKeYParser.g4" outputs.dir antlr4OutputKey classpath = configurations.antlr4 mainClass.set("org.antlr.v4.Tool") args = ["-visitor", + "-lib", "../key.ncore/src/main/antlr/", "-Xexact-output-dir", "-o", antlr4OutputKey, "-package", "de.uka.ilkd.key.nparser", - "src/main/antlr4/KeYLexer.g4", "src/main/antlr4/KeYParser.g4"] + "src/main/antlr4/JavaKeYLexer.g4", "src/main/antlr4/JavaKeYParser.g4"] doFirst { file(antlr4OutputKey).mkdirs() println("create $antlr4OutputKey") diff --git a/key.core/src/main/antlr4/JavaKeYLexer.g4 b/key.core/src/main/antlr4/JavaKeYLexer.g4 new file mode 100644 index 00000000000..9ea0ac834ee --- /dev/null +++ b/key.core/src/main/antlr4/JavaKeYLexer.g4 @@ -0,0 +1,108 @@ +lexer grammar JavaKeYLexer; + +@header { +} + +@annotateclass{ @SuppressWarnings("all") } + +import KeYLexer; + +// Keywords used in schema variable declarations +TERMLABEL : '\\termlabel'; + +// used in contracts +MODIFIABLE : '\\modifiable'; + +// Keywords used in program variable declarations +PROGRAMVARIABLES : '\\programVariables'; + +// Keywords for varcond and related stuff +STORE_TERM_IN : '\\storeTermIn'; +STORE_STMT_IN : '\\storeStmtIn'; +HAS_INVARIANT : '\\hasInvariant'; +GET_INVARIANT : '\\getInvariant'; +GET_FREE_INVARIANT: '\\getFreeInvariant'; +GET_VARIANT: '\\getVariant'; +IS_LABELED: '\\isLabeled'; + +SAME_OBSERVER : '\\sameObserver'; +DEPENDINGON : '\\dependingOn'; +DISJOINTMODULONULL : '\\disjointModuloNull'; +DROP_EFFECTLESS_STORES : '\\dropEffectlessStores'; +ENUM_CONST : '\\enumConstant'; +FREELABELIN : '\\freeLabelIn'; +FIELDTYPE : '\\fieldType'; +FINAL : '\\final'; +ELEMSORT : '\\elemSort'; +HASLABEL : '\\hasLabel'; +HASSUBFORMULAS : '\\hasSubFormulas'; +ISARRAY:'\\isArray'; +ISARRAYLENGTH:'\\isArrayLength'; +ISCONSTANT: '\\isConstant'; +ISENUMTYPE:'\\isEnumType'; +ISINDUCTVAR:'\\isInductVar'; +ISLOCALVARIABLE : '\\isLocalVariable'; +ISOBSERVER : '\\isObserver'; +METADISJOINT : '\\metaDisjoint'; +ISTHISREFERENCE:'\\isThisReference'; +DIFFERENTFIELDS:'\\differentFields'; +ISREFERENCE:'\\isReference'; +ISREFERENCEARRAY:'\\isReferenceArray'; +ISSTATICFIELD : '\\isStaticField'; +ISMODELFIELD : '\\isModelField'; +ISINSTRICTFP : '\\isInStrictFp'; +NEW_DEPENDING_ON: '\\newDependingOn'; +NEW_LOCAL_VARS: '\\newLocalVars'; +NEWLABEL : '\\newLabel'; +CONTAINS_ASSIGNMENT : '\\containsAssignment'; +// label occurs again for character `!' +NOTFREEIN : '\\notFreeIn'; +STATIC : '\\static'; +STATICMETHODREFERENCE : '\\staticMethodReference'; +MAXEXPANDMETHOD : '\\mayExpandMethod'; + +// inclusion and stuff, things that (usually) come at the beginning +// of the file +CLASSPATH:'\\classpath'; +BOOTCLASSPATH:'\\bootclasspath'; +NODEFAULTCLASSES:'\\noDefaultClasses'; +JAVASOURCE:'\\javaSource'; // TODO: remove + +CHOOSECONTRACT : '\\chooseContract'; +CONTRACTS : '\\contracts'; +INVARIANTS : '\\invariants'; + +// The first three guys are not really meta operators, treated separately +IN_TYPE : '\\inType'; +IS_ABSTRACT_OR_INTERFACE : '\\isAbstractOrInterface'; +IS_FINAL : '\\isFinal'; +CONTAINERTYPE : '\\containerType'; + +// types that need to be declared as keywords +//LOCSET : '\\locset'; +//SEQ : '\\seq'; +//BIGINT : '\\bigint'; + +/** + * Here we have to accept all strings of ki01 ERROR_CHAR 0:\ nd \\[a-z_] + * and make the decision our selves as to what to do with it + * (i.e. is it a modality, keyword, or possibly something else) + */ +MODALITYBB: '\\[[' -> more, pushMode(modBoxBox); + +MODAILITYGENERIC3: '\\diamond_transaction' -> more, pushMode(modGeneric); +MODAILITYGENERIC5: '\\box_transaction' -> more, pushMode(modGeneric); +MODAILITYGENERIC6: '\\throughout' -> more, pushMode(modGeneric); +MODAILITYGENERIC7: '\\throughout_transaction' -> more, pushMode(modGeneric); + +/* weigl: not working +MODAILITYGENERIC: + ('\\modality' | '\\diamond' | '\\diamond_transaction' + '\\box' | '\\box_transaction' | '\\throughout' | '\\throughout_transaction') + -> more, pushMode(modGeneric); +*/ +//BACKSLASH: '\\'; + +DOC_COMMENT + : '/*!' -> more , pushMode (docComment) + ; diff --git a/key.core/src/main/antlr4/JavaKeYParser.g4 b/key.core/src/main/antlr4/JavaKeYParser.g4 new file mode 100644 index 00000000000..21f04607691 --- /dev/null +++ b/key.core/src/main/antlr4/JavaKeYParser.g4 @@ -0,0 +1,314 @@ +parser grammar JavaKeYParser; +import KeYParser; + +@header { + import de.uka.ilkd.key.util.parsing.*; +} + +@members { +private SyntaxErrorReporter errorReporter = new SyntaxErrorReporter(getClass()); +public SyntaxErrorReporter getErrorReporter() { return errorReporter;} +} + +options { tokenVocab=JavaKeYLexer; } // use tokens from STLexer.g4 + +decls +: + ( bootClassPath // for problems + | stlist=classPaths // for problems + | string=programSource // for problems + | one_include_statement + | options_choice + | option_decls + | sort_decls + | prog_var_decls + | schema_var_decls + | pred_decls + | func_decls + | transform_decls + | datatype_decls + | ruleset_decls + | contracts // for problems + | invariants // for problems + | rulesOrAxioms // for problems + )* +; + +//TODO Split +one_schema_var_decl +: + MODALOPERATOR one_schema_modal_op_decl + | PROGRAM + (schema_modifiers)? + id = simple_ident + (LBRACKET nameString=simple_ident EQUALS parameter=simple_ident_dots RBRACKET)? + ids=simple_ident_comma_list + | FORMULA + (schema_modifiers)? + ids = simple_ident_comma_list + | TERMLABEL + (schema_modifiers)? + ids=simple_ident_comma_list + | UPDATE + (schema_modifiers)? + ids=simple_ident_comma_list + | SKOLEMFORMULA + (schema_modifiers)? + ids=simple_ident_comma_list + | ( TERM + | (VARIABLES | VARIABLE) + | SKOLEMTERM + ) + (schema_modifiers)? + s=sortId + ids=simple_ident_comma_list +; + +arrayopid: + EMPTYBRACKETS LPAREN componentType=typemapping RPAREN +; + +/** + * In the special but important case of Taclets, we don't yet know + * whether we are going to have a term or a formula, and it is hard + * to decide a priori what we are looking at. So the `term' + * non-terminal will recognize a term or a formula. The `formula' + * reads a formula/term and throws an error if it wasn't a formula. + * This gives a rather late error message. */ + +//region terms and formulas + +literals: + boolean_literal + | char_literal + | integer + | floatnum + | string_literal + | emptyset +; + +//labeled_term: a=parallel_term (LGUILLEMETS labels=label RGUILLEMETS)?; + +atom_prefix: + update_term + | substitution_term + | locset_term + | cast_term + | unary_minus_term + | bracket_term +; +bracket_term: primitive_labeled_term (bracket_suffix_heap)* attribute*; +bracket_suffix_heap: brace_suffix (AT heap=bracket_term)?; +brace_suffix: + LBRACKET target=term ASSIGN val=term RBRACKET #bracket_access_heap_update + | LBRACKET id=simple_ident args=argument_list RBRACKET #bracket_access_heap_term + | LBRACKET STAR RBRACKET #bracket_access_star + | LBRACKET indexTerm=term (DOTRANGE rangeTo=term)? RBRACKET #bracket_access_indexrange +; +primitive_labeled_term: + primitive_term ( LGUILLEMETS labels= label RGUILLEMETS )?; + +/* +weigl, 2021-03-12: + It would be nice if the following left-recursion would work. + ANTLR4 supports left-recursion, but their implementated resolution of left-recursion + does not resolve a working grammar, that adheres the term precedence of KeY. + + We are using the old grammar rules of the KeYParser.g (ANTLR3). + Maybe someone with more understanding of ANTLR4 could solve the problem and + write a more readable grammar. + +term +: + term (LGUILLEMETS labels = label RGUILLEMETS) #termLabeled + | term PARALLEL term #parallel + | MODALITY term #termModality + | locset_term #termLocset + | quantifierterm #termQuantifier + | term STAR term #termMult + | term (SLASH | PERCENT) term #termDivisionModulo + | term (PLUS|MINUS) term #termWeakArith + | location_term #termLocation + | substitutionterm #termSubstitution + | term EQUALS term #termEquals + | term AND term #conjunction_term + | updateterm #termUpdate + | ifThenElseTerm #termIfThenElse + | ifExThenElseTerm #termIfExThenElse + | NOT term #negation + | MINUS term #unaryMinus + | term OR term #disjunction_term + | term NOT_EQUALS term #termNotEquals + | term ( LESS | LESSEQUAL | GREATER | GREATEREQUAL ) term #termCompare + | term ASSIGN term #elementary_update_term + | term IMP term #implication_term + | term EQV term #equivalence_term + | LPAREN sort=sortId RPAREN term #cast + | LPAREN term RPAREN #termParen + | AT name=simple_ident #abbreviation + | term LBRACKET target=term ASSIGN val=term RBRACKET #bracket_access_heap_upate + | term LBRACKET id=simple_ident args=argument_list RBRACKET #bracket_access_heap_term + | term LBRACKET STAR RBRACKET #bracket_access_star + | term LBRACKET indexTerm=term (DOTRANGE rangeTo=term)? RBRACKET #bracket_access_indexrange + | term DOT STAR #dotAll + | term argument_list #termCall + | term AT term #termHeap + | term DOT attrid #termAttribute //this is ambigous + | accessterm #termAccess //also handles function calls + | literals #termLiterals +; +*/ + +attribute: + DOT STAR #attribute_star + | DOT id=simple_ident call? (AT heap=bracket_term)? #attribute_simple + | DOT LPAREN sort=sortId DOUBLECOLON id=simple_ident RPAREN + call? (AT heap=bracket_term)? #attribute_complex +; + +label +: + l=single_label (COMMA l=single_label )* +; + +single_label +: + (name=IDENT + | star=STAR ) + + (LPAREN + (string_value + (COMMA string_value )* + )? + RPAREN + )? +; + +location_term +: + LPAREN obj=equivalence_term COMMA field=equivalence_term RPAREN +; + +locset_term +: + LBRACE + ( l = location_term + ( COMMA l = location_term )* )? + RBRACE +; + +char_literal: + CHAR_LITERAL; + +varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. Only for backwards compatibility. + APPLY_UPDATE_ON_RIGID + | SAME_OBSERVER + | DROP_EFFECTLESS_ELEMENTARIES + | DROP_EFFECTLESS_STORES + | DIFFERENTFIELDS + | SIMPLIFY_IF_THEN_ELSE_UPDATE + | CONTAINS_ASSIGNMENT + | ISENUMTYPE + | ISTHISREFERENCE + | STATICMETHODREFERENCE + | ISREFERENCEARRAY + | ISARRAY + | ISARRAYLENGTH + | IS_ABSTRACT_OR_INTERFACE + | IS_FINAL + | ENUM_CONST + | FINAL + | STATIC + | ISLOCALVARIABLE + | ISOBSERVER + | DIFFERENT + | METADISJOINT + | EQUAL_UNIQUE + | FREELABELIN + | ISCONSTANT + | HASLABEL + | ISSTATICFIELD + | ISMODELFIELD + | HASSUBFORMULAS + | FIELDTYPE + | NEW + | NEW_TYPE_OF + | NEW_DEPENDING_ON + | NEW_LOCAL_VARS + | HAS_ELEMENTARY_SORT + | SAME + | ISSUBTYPE + | STRICT ISSUBTYPE + | DISJOINTMODULONULL + | NOTFREEIN + | HASSORT + | NEWLABEL + | ISREFERENCE + | MAXEXPANDMETHOD + | STORE_TERM_IN + | STORE_STMT_IN + | HAS_INVARIANT + | GET_INVARIANT + | GET_FREE_INVARIANT + | GET_VARIANT + | IS_LABELED + | ISINSTRICTFP +; + +varexp_argument +: + //weigl: Ambguity between term (which can also contain simple_ident_dots and sortId) + // suggestion add an explicit keyword to request the sort by name or manually resolve later in builder + TYPEOF LPAREN y=varId RPAREN + | CONTAINERTYPE LPAREN y=varId RPAREN + | DEPENDINGON LPAREN y=varId RPAREN + | term +; + +metaTerm: + vf=metaId (LPAREN t+=term (COMMA t+=term)* RPAREN)? +; + +contracts +: + CONTRACTS + LBRACE + (one_contract)* + RBRACE +; + +invariants +: + INVARIANTS LPAREN selfVar=one_bound_variable RPAREN + LBRACE + (one_invariant)* + RBRACE +; + +one_contract +: + contractName = simple_ident LBRACE + (prog_var_decls)? + fma=term MODIFIABLE modifiableClause=term + RBRACE SEMI +; + +one_invariant +: + invName = simple_ident LBRACE + fma=term + (DISPLAYNAME displayName=string_value)? + RBRACE SEMI +; + +bootClassPath +: + BOOTCLASSPATH id=string_value SEMI +; + +classPaths +: + CLASSPATH s=string_value (COMMA s=string_value)* SEMI +; + +programSource: JAVASOURCE result=oneProgramSource SEMI; diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 deleted file mode 100644 index 3b2dd941696..00000000000 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ /dev/null @@ -1,536 +0,0 @@ -lexer grammar KeYLexer; - -@header { - import java.util.HashMap; - import java.util.LinkedHashMap; -} - -@annotateclass{ @SuppressWarnings("all") } - -@members{ - private String modalityBegin = null; - private String modalityEnd = null; - - private static HashMap modNames = new LinkedHashMap(20); - private static HashMap modPairs = new LinkedHashMap(20); - - static { - modNames.put("\\<","diamond"); - modNames.put("\\diamond","diamond"); - modNames.put("\\diamond_transaction","diamond_transaction"); - modNames.put("\\[","box"); - modNames.put("\\box","box"); - modNames.put("\\box_transaction","box_transaction"); - modNames.put("\\[[","throughout"); - modNames.put("\\throughout","throughout"); - modNames.put("\\throughout_transaction","throughout_transaction"); - - modPairs.put("\\<","\\>"); - modPairs.put("\\[","\\]"); - - //modPairs.put("\\[[","\\]]"); - - modPairs.put("\\modality","\\endmodality"); - modPairs.put("\\diamond","\\endmodality"); - modPairs.put("\\diamond_transaction","\\endmodality"); - modPairs.put("\\box","\\endmodality"); - modPairs.put("\\box_transaction","\\endmodality"); - modPairs.put("\\throughout","\\endmodality"); - modPairs.put("\\throughout_transaction","\\endmodality"); - } - - private Token tokenBackStorage = null; - @Override - public void emit(Token token) { - int MAX_K = 10; - if (token.getType() == INT_LITERAL) {//rewrite INT_LITERALs to identifier when preceeded by an '(' - for (int k = 1; k <= MAX_K; k++) { - int codePoint = _input.LA(k); - if (Character.isWhitespace(codePoint)) continue; - if (codePoint == '(') ((org.antlr.v4.runtime.CommonToken) token).setType(IDENT); - break; - } - } - if(token.getType() == PROOF) { - tokenBackStorage = super.emitEOF(); - //will later be overwritten the EOF token - } - super.emit(token); - } - - @Override - public Token nextToken() { - if(tokenBackStorage!=null) { - Token t = tokenBackStorage; - tokenBackStorage = null; - return t; - } - return super.nextToken(); - } - -} - -tokens {MODALITY} - -SORTS:'\\sorts'; -GENERIC : '\\generic'; -PROXY : '\\proxy'; -EXTENDS : '\\extends'; -ONEOF : '\\oneof'; -ABSTRACT : '\\abstract'; -ALIAS: '\\alias'; - -// Keywords used in schema variable declarations -SCHEMAVARIABLES : '\\schemaVariables'; -SCHEMAVAR : '\\schemaVar'; -MODALOPERATOR : '\\modalOperator'; -PROGRAM : '\\program'; -FORMULA : '\\formula'; -TERM : '\\term'; -UPDATE : '\\update'; -VARIABLES : '\\variables'; -VARIABLE : '\\variable'; -SKOLEMTERM : '\\skolemTerm'; -SKOLEMFORMULA : '\\skolemFormula'; -TERMLABEL : '\\termlabel'; - -// used in contracts -MODIFIABLE : '\\modifiable'; - -// Keywords used in program variable declarations -PROGRAMVARIABLES : '\\programVariables'; - -// Keywords for varcond and related stuff -STORE_TERM_IN : '\\storeTermIn'; -STORE_STMT_IN : '\\storeStmtIn'; -HAS_INVARIANT : '\\hasInvariant'; -GET_INVARIANT : '\\getInvariant'; -GET_FREE_INVARIANT: '\\getFreeInvariant'; -GET_VARIANT: '\\getVariant'; -IS_LABELED: '\\isLabeled'; - -SAME_OBSERVER : '\\sameObserver'; -VARCOND : '\\varcond'; -APPLY_UPDATE_ON_RIGID : '\\applyUpdateOnRigid'; -DEPENDINGON : '\\dependingOn'; -DISJOINTMODULONULL : '\\disjointModuloNull'; -DROP_EFFECTLESS_ELEMENTARIES : '\\dropEffectlessElementaries'; -DROP_EFFECTLESS_STORES : '\\dropEffectlessStores'; -SIMPLIFY_IF_THEN_ELSE_UPDATE : '\\simplifyIfThenElseUpdate'; -ENUM_CONST : '\\enumConstant'; -FREELABELIN : '\\freeLabelIn'; -HASSORT : '\\hasSort'; -FIELDTYPE : '\\fieldType'; -FINAL : '\\final'; -ELEMSORT : '\\elemSort'; -HASLABEL : '\\hasLabel'; -HASSUBFORMULAS : '\\hasSubFormulas'; -ISARRAY:'\\isArray'; -ISARRAYLENGTH:'\\isArrayLength'; -ISCONSTANT: '\\isConstant'; -ISENUMTYPE:'\\isEnumType'; -ISINDUCTVAR:'\\isInductVar'; -ISLOCALVARIABLE : '\\isLocalVariable'; -ISOBSERVER : '\\isObserver'; -DIFFERENT : '\\different'; -METADISJOINT : '\\metaDisjoint'; -ISTHISREFERENCE:'\\isThisReference'; -DIFFERENTFIELDS:'\\differentFields'; -ISREFERENCE:'\\isReference'; -ISREFERENCEARRAY:'\\isReferenceArray'; -ISSTATICFIELD : '\\isStaticField'; -ISMODELFIELD : '\\isModelField'; -ISINSTRICTFP : '\\isInStrictFp'; -ISSUBTYPE : '\\sub'; -EQUAL_UNIQUE : '\\equalUnique'; -NEW : '\\new'; -NEW_TYPE_OF: '\\newTypeOf'; -NEW_DEPENDING_ON: '\\newDependingOn'; -NEW_LOCAL_VARS: '\\newLocalVars'; -HAS_ELEMENTARY_SORT:'\\hasElementarySort'; -NEWLABEL : '\\newLabel'; -CONTAINS_ASSIGNMENT : '\\containsAssignment'; -// label occurs again for character `!' -NOT_ : '\\not'; -NOTFREEIN : '\\notFreeIn'; -SAME : '\\same'; -STATIC : '\\static'; -STATICMETHODREFERENCE : '\\staticMethodReference'; -MAXEXPANDMETHOD : '\\mayExpandMethod'; -STRICT : '\\strict'; -TYPEOF : '\\typeof'; -INSTANTIATE_GENERIC : '\\instantiateGeneric'; - -// Quantifiers, binding, substitution -FORALL : '\\forall' | '\u2200'; -EXISTS : '\\exists' | '\u2203'; -SUBST : '\\subst'; -IF : '\\if'; -IFEX : '\\ifEx'; -THEN : '\\then'; -ELSE : '\\else'; - -// inclusion and stuff, things that (usually) come at the beginning -// of the file -INCLUDE:'\\include'; -INCLUDELDTS:'\\includeLDTs'; -CLASSPATH:'\\classpath'; -BOOTCLASSPATH:'\\bootclasspath'; -NODEFAULTCLASSES:'\\noDefaultClasses'; -JAVASOURCE:'\\javaSource'; -WITHOPTIONS:'\\withOptions'; -OPTIONSDECL:'\\optionsDecl'; -KEYSETTINGS : '\\settings'; -PROFILE : '\\profile'; - -// Those guys can stay being keywords -TRUE : 'true'; -FALSE : 'false'; - - -// Keywords related to taclets -SAMEUPDATELEVEL : '\\sameUpdateLevel'; -INSEQUENTSTATE : '\\inSequentState'; -ANTECEDENTPOLARITY : '\\antecedentPolarity'; -SUCCEDENTPOLARITY : '\\succedentPolarity'; -CLOSEGOAL : '\\closegoal'; -HEURISTICSDECL : '\\heuristicsDecl'; -NONINTERACTIVE : '\\noninteractive'; -DISPLAYNAME : '\\displayname'; -HELPTEXT : '\\helptext'; -REPLACEWITH : '\\replacewith'; -ADDRULES : '\\addrules'; -ADDPROGVARS : '\\addprogvars'; -HEURISTICS : '\\heuristics'; -FIND : '\\find'; -ADD : '\\add'; -ASSUMES : '\\assumes'; -TRIGGER : '\\trigger'; -AVOID : '\\avoid'; - -PREDICATES : '\\predicates'; -FUNCTIONS : '\\functions'; -DATATYPES : '\\datatypes'; -TRANSFORMERS : '\\transformers'; -UNIQUE : '\\unique'; -FREE : '\\free'; - -RULES : '\\rules'; -AXIOMS : '\\axioms'; -PROBLEM : '\\problem'; -CHOOSECONTRACT : '\\chooseContract'; -PROOFOBLIGATION : '\\proofObligation'; -PROOF : '\\proof'; -PROOFSCRIPT : '\\proofScript'; -CONTRACTS : '\\contracts'; -INVARIANTS : '\\invariants'; - -// Taclet annotations (see TacletAnnotations.java for more details) -LEMMA : '\\lemma'; - -// The first three guys are not really meta operators, treated separately -IN_TYPE : '\\inType'; -IS_ABSTRACT_OR_INTERFACE : '\\isAbstractOrInterface'; -IS_FINAL : '\\isFinal'; -CONTAINERTYPE : '\\containerType'; - -// types that need to be declared as keywords -//LOCSET : '\\locset'; -//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' - ; - -IMP -: '->' | '\u2192' - ; - -EQUALS -: '=' - ; - -NOT_EQUALS -: '!=' | '\u2260' - ; - -SEQARROW -: '==>' | '\u27F9' - ; - -EXP -: '^' - ; - -TILDE -: '~' - ; - -PERCENT -: '%' - ; - -STAR -: '*' - ; - -MINUS -: '-' - ; - -PLUS -: '+' - ; - -GREATER -: '>' - ; - -GREATEREQUAL -: '>' '=' | '\u2265' - ; - -OPENTYPEPARAMS : '<' '['; -CLOSETYPEPARAMS : ']' '>'; - -WS: [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace -STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ; -LESS: '<'; -LESSEQUAL: '<' '=' | '\u2264'; -LGUILLEMETS: '<' '<' | '«' | '‹'; -RGUILLEMETS: '>''>' | '»' | '›'; - -EQV: '<->' | '\u2194'; -CHAR_LITERAL -: '\'' - ((' '..'&') | - ('('..'[') | - (']'..'~') | - ('\\' ('\'' | '\\' | 'n' | 'r' | 't' | 'b' | 'f' | '"' | 'u' HEX )) - ) - '\'' - ; - -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')?; -fragment DIGIT: '0'..'9'; -fragment HEX -: ('a'..'f'|'A'..'F'|DIGIT ) - ('a'..'f'|'A'..'F'|DIGIT ) - ('a'..'f'|'A'..'F'|DIGIT ) - ('a'..'f'|'A'..'F'|DIGIT ) - ; - -fragment LETTER: 'a'..'z'|'A'..'Z'; -fragment IDCHAR: LETTER | DIGIT | '_' | '#' | '$'; - - -IDENT: ( (LETTER | '_' | '#' | '$') (IDCHAR)*); - -INT_LITERAL: - (DIGIT | '_')+ ('l'|'L')? -; - -fragment EXP_SUFFIX: - ('e'|'E') ('+'|'-')? (DIGIT)+ - ; - -// reals, floats and doubles are all rationals here. -fragment RATIONAL_LITERAL: - (DIGIT)+ ('.' (DIGIT)*)? (EXP_SUFFIX)? - | '.' (DIGIT)+ (EXP_SUFFIX)? - ; - -FLOAT_LITERAL: - RATIONAL_LITERAL ('f' | 'F') - ; - -DOUBLE_LITERAL: - RATIONAL_LITERAL ('d' | 'D') - ; - -REAL_LITERAL: - RATIONAL_LITERAL ('r' | 'R')? - ; - - -/** - * Here we have to accept all strings of ki01 ERROR_CHAR 0:\ nd \\[a-z_] - * and make the decision our selves as to what to do with it - * (i.e. is it a modality, keyword, or possibly something else) - */ -MODALITYD: '\\<' -> more, pushMode(modDiamond); -MODALITYB: '\\[' -> more, pushMode(modBox); -MODALITYBB: '\\[[' -> more, pushMode(modBoxBox); - -MODAILITYGENERIC1: '\\box' -> more, pushMode(modGeneric); -MODAILITYGENERIC2: '\\diamond' -> more, pushMode(modGeneric); -MODAILITYGENERIC3: '\\diamond_transaction' -> more, pushMode(modGeneric); -MODAILITYGENERIC4: '\\modality' -> more, pushMode(modGeneric); -MODAILITYGENERIC5: '\\box_transaction' -> more, pushMode(modGeneric); -MODAILITYGENERIC6: '\\throughout' -> more, pushMode(modGeneric); -MODAILITYGENERIC7: '\\throughout_transaction' -> more, pushMode(modGeneric); - -/* weigl: not working -MODAILITYGENERIC: - ('\\modality' | '\\diamond' | '\\diamond_transaction' - '\\box' | '\\box_transaction' | '\\throughout' | '\\throughout_transaction') - -> more, pushMode(modGeneric); -*/ -//BACKSLASH: '\\'; -ERROR_UKNOWN_ESCAPE: '\\' IDENT; -ERROR_CHAR: .; - -mode modDiamond; -MODALITYD_END: '\\>' -> type(MODALITY), popMode; -MODALITYD_STRING : '"' -> more, pushMode(modString); -MODALITYD_CHAR : '\'' -> more, pushMode(modChar); -MODALITYD_COMMENT : [\\] [*] -> more, pushMode(modComment); -MODALITYD_ANY : . -> more; - -mode modGeneric; -MODALITYG_END: '\\endmodality' -> type(MODALITY), popMode; -MODALITYG_STRING : '"' -> more, pushMode(modString); -MODALITYG_CHAR : '\'' -> more, pushMode(modChar); -MODALITYG_COMMENT : [\\] [*] -> more, pushMode(modComment); -MODALITYG_ANY : . -> more; - -mode modBox; -MODALITYB_END: '\\]' -> type(MODALITY), popMode; -MODALITYB_STRING : '"' -> more, pushMode(modString); -MODALITYB_CHAR : '\'' -> more, pushMode(modChar); -MODALITYB_COMMENT : [\\] [*] -> more, pushMode(modComment); -MODALITYB_ANY : . -> more; - -mode modBoxBox; -MODALITYBB_END: '\\]]' -> type(MODALITY), popMode; -MODALITYBB_STRING : '"' -> more, pushMode(modString); -MODALITYBB_CHAR : '\'' -> more, pushMode(modChar); -MODALITYBB_COMMENT : [\\] [*] -> more, pushMode(modComment); -MODALITYBB_ANY : . -> more; - - -mode modString; -MOD_STRING_ESC: [\\] '"' -> more; -MOD_STRING_END: '"' -> more,popMode; -MOD_STRING_ANY: . -> more; - -mode modChar; -MOD_CHAR_END: '\'' -> more,popMode; -MOD_CHAR_ANY: . -> more; - -mode modComment; -MOD_COMMENT_END: ('*/'|EOF) -> more, popMode; -MOD_COMMENT_ANY: . -> more; - -mode COMMENT; -COMMENT_END: ('*/'|EOF) -> channel(HIDDEN), popMode; -COMMENT_ANY_CHAR: . -> more; - -mode docComment; -DOC_COMMENT_END: ('*/'|EOF) -> type(DOC_COMMENT), popMode; -DOC_COMMENT_ANY_CHAR: . -> more; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 deleted file mode 100644 index 5832a7238f7..00000000000 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ /dev/null @@ -1,934 +0,0 @@ -parser grammar KeYParser; - -@header { - import de.uka.ilkd.key.util.parsing.*; -} - -@members { -private SyntaxErrorReporter errorReporter = new SyntaxErrorReporter(getClass()); -public SyntaxErrorReporter getErrorReporter() { return errorReporter;} -} - -options { tokenVocab=KeYLexer; } // use tokens from STLexer.g4 - -file: DOC_COMMENT* (profile? preferences? decls problem? proof?) EOF; - -decls -: - ( bootClassPath // for problems - | stlist=classPaths // for problems - | string=javaSource // for problems - | one_include_statement - | options_choice - | option_decls - | sort_decls - | prog_var_decls - | schema_var_decls - | pred_decls - | func_decls - | transform_decls - | datatype_decls - | ruleset_decls - | contracts // for problems - | invariants // for problems - | rulesOrAxioms // for problems - )* -; - -problem -: - ( PROBLEM LBRACE ( t=termorseq ) RBRACE - | CHOOSECONTRACT (chooseContract=string_value SEMI)? - | PROOFOBLIGATION (proofObligation=cvalue)? SEMI? - ) - proofScriptEntry? -; - - - -one_include_statement -: - (INCLUDE | INCLUDELDTS) - one_include (COMMA one_include)* SEMI -; - -one_include -: - absfile=IDENT | relfile=string_value -; - -options_choice -: - WITHOPTIONS activated_choice (COMMA activated_choice)* SEMI -; - -activated_choice -: - cat=IDENT COLON choice_=IDENT -; - -option_decls -: - OPTIONSDECL LBRACE (choice SEMI)* RBRACE -; - -choice -: - maindoc+=DOC_COMMENT* - category=IDENT - (COLON LBRACE optionDecl (COMMA optionDecl)* RBRACE)? -; - -optionDecl: doc+=DOC_COMMENT? choice_option+=IDENT; - -sort_decls -: - SORTS LBRACE (one_sort_decl)* RBRACE -; - -one_sort_decl -: - doc=DOC_COMMENT? - ( - GENERIC sortIds=simple_ident_dots_comma_list - (ONEOF sortOneOf = oneof_sorts)? - (EXTENDS sortExt = extends_sorts)? SEMI - | PROXY sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI - | ABSTRACT? (sortIds=simple_ident_dots_comma_list | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)? SEMI - | ALIAS simple_ident_dots EQUALS sortId SEMI - ) -; - -parametric_sort_decl -: - simple_ident_dots - formal_sort_param_decls -; - -simple_ident_dots -: - simple_ident (DOT simple_ident)* -; - -simple_ident_dots_comma_list -: - simple_ident_dots (COMMA simple_ident_dots)* -; - - -extends_sorts -: - sortId (COMMA sortId)* -; - -oneof_sorts -: - LBRACE - s = sortId (COMMA s = sortId) * - RBRACE -; - -keyjavatype -: - type = simple_ident_dots (EMPTYBRACKETS)* -; - -prog_var_decls -: - PROGRAMVARIABLES - LBRACE - ( - kjt = keyjavatype - var_names = simple_ident_comma_list - SEMI - )* - RBRACE -; - -//this rule produces a StringLiteral -string_literal: id=STRING_LITERAL; - -//this rule produces a String -string_value: STRING_LITERAL; - -simple_ident -: - id=IDENT -; - -simple_ident_comma_list -: - id = simple_ident (COMMA id = simple_ident )* -; - - -schema_var_decls : - SCHEMAVARIABLES LBRACE - ( one_schema_var_decl SEMI)* - RBRACE -; - -//TODO Split -one_schema_var_decl -: - MODALOPERATOR one_schema_modal_op_decl - | PROGRAM - (schema_modifiers)? - id = simple_ident - (LBRACKET nameString=simple_ident EQUALS parameter=simple_ident_dots RBRACKET)? - ids=simple_ident_comma_list - | FORMULA - (schema_modifiers)? - ids = simple_ident_comma_list - | TERMLABEL - (schema_modifiers)? - ids=simple_ident_comma_list - | UPDATE - (schema_modifiers)? - ids=simple_ident_comma_list - | SKOLEMFORMULA - (schema_modifiers)? - ids=simple_ident_comma_list - | ( TERM - | (VARIABLES | VARIABLE) - | SKOLEMTERM - ) - (schema_modifiers)? - s=sortId - ids=simple_ident_comma_list -; - -schema_modifiers - : - LBRACKET - opts = simple_ident_comma_list - RBRACKET - - ; - -one_schema_modal_op_decl -: - (LPAREN sort = sortId RPAREN)? - LBRACE ids = simple_ident_comma_list RBRACE id = simple_ident -; - -pred_decl -: - doc=DOC_COMMENT? - pred_name = funcpred_name - formal_sort_param_decls? - (whereToBind=where_to_bind)? - argSorts=arg_sorts - SEMI -; - -pred_decls -: - PREDICATES LBRACE (pred_decl)* RBRACE -; - -func_decl -: - doc=DOC_COMMENT? - (UNIQUE)? - retSort = sortId - func_name = funcpred_name - formal_sort_param_decls? - whereToBind=where_to_bind? - argSorts = arg_sorts - SEMI -; - -/** -\datatypes { - \free List = Nil | Cons(any head, List tail); -} -*/ -datatype_decls: - DATATYPES LBRACE datatype_decl* RBRACE -; - -datatype_decl: - doc=DOC_COMMENT? - // weigl: all datatypes are free! - // FREE? - name=simple_ident formal_sort_param_decls? - EQUALS - datatype_constructor (OR datatype_constructor)* - SEMI -; - -datatype_constructor: - name=simple_ident - ( - LPAREN - (argSort+=sortId argName+=simple_ident - (COMMA argSort+=sortId argName+=simple_ident)* - )? - RPAREN - )? -; - -formal_sort_param_decls -: OPENTYPEPARAMS - formal_sort_param_decl (COMMA formal_sort_param_decl)* - CLOSETYPEPARAMS -; - -formal_sort_param_decl -: - (PLUS | MINUS)? simple_ident -; - -func_decls - : - FUNCTIONS - LBRACE - ( - func_decl - ) * - RBRACE - ; - - -// like arg_sorts but admits also the keyword "\formula" -arg_sorts_or_formula -: - ( LPAREN - arg_sorts_or_formula_helper - (COMMA arg_sorts_or_formula_helper)* - RPAREN - )? -; - -arg_sorts_or_formula_helper -: - sortId | FORMULA -; - -transform_decl -: - doc=DOC_COMMENT? - (retSort = sortId - | FORMULA - ) - - trans_name=funcpred_name - argSorts=arg_sorts_or_formula - SEMI -; - - -transform_decls: - TRANSFORMERS LBRACE (transform_decl)* RBRACE -; - -arrayopid: - EMPTYBRACKETS LPAREN componentType=keyjavatype RPAREN -; - -arg_sorts: - (LPAREN sortId (COMMA sortId)* RPAREN)? -; - -where_to_bind: - LBRACE - b+=(TRUE | FALSE) - (COMMA b+=(TRUE | FALSE) )* - RBRACE - - ; - -ruleset_decls -: - HEURISTICSDECL LBRACE (doc+=DOC_COMMENT? id+=simple_ident SEMI)* RBRACE -; - -sortId -: - id=simple_ident_dots formal_sort_args? (EMPTYBRACKETS)* -; - -formal_sort_args -: - OPENTYPEPARAMS - sortId (COMMA sortId)* - CLOSETYPEPARAMS -; - -id_declaration -: - id=IDENT ( COLON s=sortId )? -; - -funcpred_name -: - (sortId DOUBLECOLON)? (name=simple_ident_dots|num=INT_LITERAL) -; - - -/** - * In the special but important case of Taclets, we don't yet know - * whether we are going to have a term or a formula, and it is hard - * to decide a priori what we are looking at. So the `term' - * non-terminal will recognize a term or a formula. The `formula' - * reads a formula/term and throws an error if it wasn't a formula. - * This gives a rather late error message. */ - -//region terms and formulas - -termEOF: term EOF; // toplevel - -boolean_literal: TRUE | FALSE; -literals: - boolean_literal - | char_literal - | integer - | floatnum - | string_literal - | emptyset -; - -emptyset: UTF_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)*; -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)*; -update_term: (LBRACE u=parallel_term RBRACE) (atom_prefix | unary_formula); - -substitution_term: - LBRACE SUBST bv=one_bound_variable SEMI - replacement=comparison_term RBRACE - (atom_prefix|unary_formula) -; -cast_term: (LPAREN sort=sortId RPAREN) sub=atom_prefix; -unary_minus_term: MINUS sub=atom_prefix; -atom_prefix: - update_term - | substitution_term - | locset_term - | cast_term - | unary_minus_term - | bracket_term -; -bracket_term: primitive_labeled_term (bracket_suffix_heap)* attribute*; -bracket_suffix_heap: brace_suffix (AT heap=bracket_term)?; -brace_suffix: - LBRACKET target=term ASSIGN val=term RBRACKET #bracket_access_heap_update - | LBRACKET id=simple_ident args=argument_list RBRACKET #bracket_access_heap_term - | LBRACKET STAR RBRACKET #bracket_access_star - | LBRACKET indexTerm=term (DOTRANGE rangeTo=term)? RBRACKET #bracket_access_indexrange -; -primitive_labeled_term: - primitive_term ( LGUILLEMETS labels= label RGUILLEMETS )?; -termParen: LPAREN term RPAREN (attribute)*; -abbreviation: AT name=simple_ident; -primitive_term: - termParen - | ifThenElseTerm - | ifExThenElseTerm - | abbreviation - | accessterm - | literals - ; - -/* -weigl, 2021-03-12: - It would be nice if the following left-recursion would work. - ANTLR4 supports left-recursion, but their implementated resolution of left-recursion - does not resolve a working grammar, that adheres the term precedence of KeY. - - We are using the old grammar rules of the KeYParser.g (ANTLR3). - Maybe someone with more understanding of ANTLR4 could solve the problem and - write a more readable grammar. - -term -: - term (LGUILLEMETS labels = label RGUILLEMETS) #termLabeled - | term PARALLEL term #parallel - | MODALITY term #termModality - | locset_term #termLocset - | quantifierterm #termQuantifier - | term STAR term #termMult - | term (SLASH | PERCENT) term #termDivisionModulo - | term (PLUS|MINUS) term #termWeakArith - | location_term #termLocation - | substitutionterm #termSubstitution - | term EQUALS term #termEquals - | term AND term #conjunction_term - | updateterm #termUpdate - | ifThenElseTerm #termIfThenElse - | ifExThenElseTerm #termIfExThenElse - | NOT term #negation - | MINUS term #unaryMinus - | term OR term #disjunction_term - | term NOT_EQUALS term #termNotEquals - | term ( LESS | LESSEQUAL | GREATER | GREATEREQUAL ) term #termCompare - | term ASSIGN term #elementary_update_term - | term IMP term #implication_term - | term EQV term #equivalence_term - | LPAREN sort=sortId RPAREN term #cast - | LPAREN term RPAREN #termParen - | AT name=simple_ident #abbreviation - | term LBRACKET target=term ASSIGN val=term RBRACKET #bracket_access_heap_upate - | term LBRACKET id=simple_ident args=argument_list RBRACKET #bracket_access_heap_term - | term LBRACKET STAR RBRACKET #bracket_access_star - | term LBRACKET indexTerm=term (DOTRANGE rangeTo=term)? RBRACKET #bracket_access_indexrange - | term DOT STAR #dotAll - | term argument_list #termCall - | term AT term #termHeap - | term DOT attrid #termAttribute //this is ambigous - | accessterm #termAccess //also handles function calls - | literals #termLiterals -; -*/ - - -/** - * Access: a.b.c@f, T.staticQ() - */ -accessterm -: - // OLD - (sortId DOUBLECOLON)? - firstName=simple_ident - formal_sort_args? - - /*Faster version - simple_ident_dots - ( EMPTYBRACKETS* - DOUBLECOLON - simple_ident - )?*/ - call? - ( attribute )* -; - -attribute: - DOT STAR #attribute_star - | DOT id=simple_ident call? (AT heap=bracket_term)? #attribute_simple - | DOT LPAREN sort=sortId DOUBLECOLON id=simple_ident RPAREN - call? (AT heap=bracket_term)? #attribute_complex -; - -call: - ((LBRACE boundVars=bound_variables RBRACE)? argument_list) -; - -label -: - l=single_label (COMMA l=single_label )* -; - -single_label -: - (name=IDENT - | star=STAR ) - - (LPAREN - (string_value - (COMMA string_value )* - )? - RPAREN - )? -; - -location_term -: - LPAREN obj=equivalence_term COMMA field=equivalence_term RPAREN -; - -ifThenElseTerm -: - IF LPAREN condF = term RPAREN - THEN LPAREN thenT = term RPAREN - ELSE LPAREN elseT = term RPAREN -; - -ifExThenElseTerm -: - IFEX exVars = bound_variables - LPAREN condF = term RPAREN - THEN LPAREN thenT = term RPAREN - ELSE LPAREN elseT = term RPAREN -; - -locset_term -: - LBRACE - ( l = location_term - ( COMMA l = location_term )* )? - RBRACE -; - -bound_variables -: - var=one_bound_variable (COMMA var=one_bound_variable)* SEMI -; - -one_bound_variable -: - s=sortId? id=simple_ident -; - -argument_list -: - LPAREN - (term (COMMA term)*)? - RPAREN -; - -integer_with_minux: MINUS? integer; -integer: - (INT_LITERAL | HEX_LITERAL | BIN_LITERAL) -; - -floatnum: // called floatnum because "float" collide with the Java language - (MINUS)? FLOAT_LITERAL #floatLiteral - | (MINUS)? DOUBLE_LITERAL #doubleLiteral - | (MINUS)? REAL_LITERAL #realLiteral -; - -char_literal: - CHAR_LITERAL; - - -varId: id=IDENT; -varIds: ids=simple_ident_comma_list; - -triggers -: - TRIGGER - LBRACE id=simple_ident RBRACE - t=term - (AVOID avoidCond+=term - (COMMA avoidCond+=term )*)? - SEMI -; - -taclet -: - doc=DOC_COMMENT? - (LEMMA)? - name=IDENT (choices_=option_list)? - LBRACE - ( form=term - | - ( SCHEMAVAR one_schema_var_decl SEMI) * - ( ASSUMES LPAREN ifSeq=seq RPAREN ) ? - ( FIND LPAREN find=termorseq RPAREN - ( SAMEUPDATELEVEL - | INSEQUENTSTATE - | ANTECEDENTPOLARITY - | SUCCEDENTPOLARITY - )* - )? - - ( VARCOND LPAREN varexplist RPAREN )* - goalspecs - modifiers - ) - RBRACE -; - -modifiers -: - ( rs = rulesets - | NONINTERACTIVE - | DISPLAYNAME dname=string_value - | HELPTEXT htext=string_value - | triggers - ) * -; - -seq: ant=semisequent SEQARROW suc=semisequent; - -seqEOF: seq EOF; - -termorseq -: - head=term (COMMA s=seq | SEQARROW ss=semisequent) ? - | SEQARROW ss=semisequent -; - -semisequent -: - /* empty */ - | head=term ( COMMA ss=semisequent) ? -; - -varexplist : varexp (COMMA varexp)* ; - -varexp -: - negate=NOT_? - varexpId - (LBRACKET parameter+=IDENT (COMMA parameter+=IDENT)* RBRACKET)? - (LPAREN varexp_argument (COMMA varexp_argument)* RPAREN)? -; - - -varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. Only for backwards compatibility. - APPLY_UPDATE_ON_RIGID - | SAME_OBSERVER - | DROP_EFFECTLESS_ELEMENTARIES - | DROP_EFFECTLESS_STORES - | DIFFERENTFIELDS - | SIMPLIFY_IF_THEN_ELSE_UPDATE - | CONTAINS_ASSIGNMENT - | ISENUMTYPE - | ISTHISREFERENCE - | STATICMETHODREFERENCE - | ISREFERENCEARRAY - | ISARRAY - | ISARRAYLENGTH - | IS_ABSTRACT_OR_INTERFACE - | IS_FINAL - | ENUM_CONST - | FINAL - | STATIC - | ISLOCALVARIABLE - | ISOBSERVER - | DIFFERENT - | METADISJOINT - | EQUAL_UNIQUE - | FREELABELIN - | ISCONSTANT - | HASLABEL - | ISSTATICFIELD - | ISMODELFIELD - | HASSUBFORMULAS - | FIELDTYPE - | NEW - | NEW_TYPE_OF - | NEW_DEPENDING_ON - | NEW_LOCAL_VARS - | HAS_ELEMENTARY_SORT - | SAME - | ISSUBTYPE - | STRICT ISSUBTYPE - | DISJOINTMODULONULL - | NOTFREEIN - | HASSORT - | NEWLABEL - | ISREFERENCE - | MAXEXPANDMETHOD - | STORE_TERM_IN - | STORE_STMT_IN - | HAS_INVARIANT - | GET_INVARIANT - | GET_FREE_INVARIANT - | GET_VARIANT - | IS_LABELED - | ISINSTRICTFP -; - -varexp_argument -: - //weigl: Ambguity between term (which can also contain simple_ident_dots and sortId) - // suggestion add an explicit keyword to request the sort by name or manually resolve later in builder - TYPEOF LPAREN y=varId RPAREN - | CONTAINERTYPE LPAREN y=varId RPAREN - | DEPENDINGON LPAREN y=varId RPAREN - | term -; - -goalspecs: - CLOSEGOAL - | goalspecwithoption (SEMI goalspecwithoption)* -; - -goalspecwithoption - : - soc=option_list LBRACE goalspec RBRACE - | goalspec -; - -option -: - cat=IDENT COLON value=IDENT -; - -option_list -: - LPAREN - (option_expr (COMMA option_expr)*) - RPAREN -; - -option_expr -: - option_expr AND option_expr #option_expr_and - | option_expr OR option_expr #option_expr_or - | NOT option_expr #option_expr_not - | LPAREN option_expr RPAREN #option_expr_paren - | option #option_expr_prop -; - -goalspec -: - (name=string_value (LBRACKET tag=simple_ident RBRACKET)? COLON)? - ( rwObj=replacewith - addSeq=add? - addRList=addrules? - addpv=addprogvar? - | addSeq=add (addRList=addrules)? - | addRList=addrules - ) -; - -replacewith: REPLACEWITH LPAREN o=termorseq RPAREN; -add: ADD LPAREN s=seq RPAREN; -addrules: ADDRULES LPAREN lor=tacletlist RPAREN; -addprogvar: ADDPROGVARS LPAREN pvs=pvset RPAREN; -tacletlist: taclet (COMMA taclet)*; - -pvset: varId (COMMA varId)*; - -rulesets: - HEURISTICS LPAREN ruleset - (COMMA ruleset) * RPAREN -; - -ruleset: id=IDENT; - -metaId: id=simple_ident ; - -metaTerm: - vf=metaId (LPAREN t+=term (COMMA t+=term)* RPAREN)? -; - - -contracts -: - CONTRACTS - LBRACE - (one_contract)* - RBRACE -; - -invariants -: - INVARIANTS LPAREN selfVar=one_bound_variable RPAREN - LBRACE - (one_invariant)* - RBRACE -; - -one_contract -: - contractName = simple_ident LBRACE - (prog_var_decls)? - fma=term MODIFIABLE modifiableClause=term - RBRACE SEMI -; - -one_invariant -: - invName = simple_ident LBRACE - fma=term - (DISPLAYNAME displayName=string_value)? - RBRACE SEMI -; - -rulesOrAxioms: - doc=DOC_COMMENT? - (RULES|AXIOMS) - (choices = option_list)? - (LBRACE (s=taclet SEMI)* RBRACE) -; - -bootClassPath -: - BOOTCLASSPATH id=string_value SEMI -; - -classPaths -: - CLASSPATH s=string_value (COMMA s=string_value)* SEMI -; - -javaSource: JAVASOURCE result=oneJavaSource SEMI; - -oneJavaSource -: - ( string_value - | COLON - )+ -; - -profile: PROFILE name=string_value SEMI; - -preferences -: - KEYSETTINGS (LBRACE s=string_value? RBRACE - | c=cvalue ) // LBRACE, RBRACE included in cvalue#table -; - -proofScriptEntry -: - PROOFSCRIPT - ( STRING_LITERAL SEMI? - | LBRACE proofScript RBRACE - ) -; - -proofScriptEOF: proofScript EOF; -proofScript: proofScriptCommand*; -proofScriptCommand: cmd=IDENT proofScriptParameters SEMI; - -proofScriptParameters: proofScriptParameter*; -proofScriptParameter : ((pname=proofScriptParameterName (COLON|EQUALS))? expr=proofScriptExpression); -proofScriptParameterName: AT? IDENT; // someone thought, that the let-command parameters should have a leading "@" -proofScriptExpression: - boolean_literal - | char_literal - | integer - | floatnum - | string_literal - | LPAREN (term | seq) RPAREN - | simple_ident - | abbreviation - | literals - | proofScriptCodeBlock - ; - -proofScriptCodeBlock: LBRACE proofScript RBRACE; - -// PROOF -proof: PROOF EOF; - -// Config -cfile: cvalue* EOF; -//csection: LBRACKET IDENT RBRACKET; -ckv: doc=DOC_COMMENT? ckey ':' cvalue; -ckey: IDENT | STRING_LITERAL; -cvalue: - IDENT #csymbol - | STRING_LITERAL #cstring - | BIN_LITERAL #cintb - | HEX_LITERAL #cinth - | MINUS? INT_LITERAL #cintd - | MINUS? FLOAT_LITERAL #cfpf - | MINUS? DOUBLE_LITERAL #cfpd - | MINUS? REAL_LITERAL #cfpr - | (TRUE|FALSE) #cbool - | LBRACE - (ckv (COMMA ckv)*)? COMMA? - RBRACE #table - | LBRACKET (cvalue (COMMA cvalue)*)? COMMA? RBRACKET #list; diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java index 9b286c49198..bbcf25b17ab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java @@ -15,7 +15,7 @@ import de.uka.ilkd.key.logic.label.OriginTermLabel.NodeOrigin; import de.uka.ilkd.key.logic.label.OriginTermLabel.SpecType; import de.uka.ilkd.key.logic.op.*; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.parser.DefaultTermParser; import de.uka.ilkd.key.parser.IdDeclaration; @@ -192,7 +192,7 @@ private JTerm parseTerm(String s, Namespace<@NonNull QuantifiableVariable> varNS * function) */ private IdDeclaration parseIdDeclaration(String s) throws ParserException { - KeYParser.Id_declarationContext ctx = + JavaKeYParser.Id_declarationContext ctx = ParsingFacade.parseIdDeclaration(CharStreams.fromString(s)); Sort sort = ctx.s != null ? services.getNamespaces().lookupSortOrAlias(ctx.s.getText()) : null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java index 146723fcf0d..0bbe1d4c07e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java @@ -19,27 +19,27 @@ * @version 1 (03.04.23) * @see KeyAst.ConfigurationFile#asConfiguration() */ -class ConfigurationBuilder extends KeYParserBaseVisitor { +class ConfigurationBuilder extends JavaKeYParserBaseVisitor { @Override - public List visitCfile(KeYParser.CfileContext ctx) { + public List visitCfile(JavaKeYParser.CfileContext ctx) { return ctx.cvalue().stream().map(it -> it.accept(this)).collect(Collectors.toList()); } @Override - public String visitCkey(KeYParser.CkeyContext ctx) { + public String visitCkey(JavaKeYParser.CkeyContext ctx) { if (ctx.STRING_LITERAL() != null) return sanitizeStringLiteral(ctx.STRING_LITERAL().getText()); return ctx.IDENT().getText(); } @Override - public String visitCsymbol(KeYParser.CsymbolContext ctx) { + public String visitCsymbol(JavaKeYParser.CsymbolContext ctx) { return ctx.IDENT().getText(); } @Override - public String visitCstring(KeYParser.CstringContext ctx) { + public String visitCstring(JavaKeYParser.CstringContext ctx) { final var text = ctx.getText(); return sanitizeStringLiteral(text); } @@ -51,17 +51,17 @@ public String visitCstring(KeYParser.CstringContext ctx) { } @Override - public Long visitCintb(KeYParser.CintbContext ctx) { + public Long visitCintb(JavaKeYParser.CintbContext ctx) { return Long.parseLong(ctx.getText(), 2); } @Override - public Long visitCinth(KeYParser.CinthContext ctx) { + public Long visitCinth(JavaKeYParser.CinthContext ctx) { return Long.parseLong(ctx.getText(), 16); } @Override - public Long visitCintd(KeYParser.CintdContext ctx) { + public Long visitCintd(JavaKeYParser.CintdContext ctx) { final var text = ctx.getText(); if (text.endsWith("L") || text.endsWith("l")) { return Long.parseLong(text.substring(0, text.length() - 1), 10); @@ -71,29 +71,29 @@ public Long visitCintd(KeYParser.CintdContext ctx) { } @Override - public Double visitCfpf(KeYParser.CfpfContext ctx) { + public Double visitCfpf(JavaKeYParser.CfpfContext ctx) { return Double.parseDouble(ctx.getText()); } @Override - public Double visitCfpd(KeYParser.CfpdContext ctx) { + public Double visitCfpd(JavaKeYParser.CfpdContext ctx) { return Double.parseDouble(ctx.getText()); } @Override - public Double visitCfpr(KeYParser.CfprContext ctx) { + public Double visitCfpr(JavaKeYParser.CfprContext ctx) { return Double.parseDouble(ctx.getText()); } @Override - public Boolean visitCbool(KeYParser.CboolContext ctx) { + public Boolean visitCbool(JavaKeYParser.CboolContext ctx) { return Boolean.parseBoolean(ctx.getText()); } @Override - public Configuration visitTable(KeYParser.TableContext ctx) { + public Configuration visitTable(JavaKeYParser.TableContext ctx) { final var data = new LinkedHashMap(); - for (KeYParser.CkvContext context : ctx.ckv()) { + for (JavaKeYParser.CkvContext context : ctx.ckv()) { var name = context.ckey().accept(this).toString(); var val = context.cvalue().accept(this); data.put(name, val); @@ -102,9 +102,9 @@ public Configuration visitTable(KeYParser.TableContext ctx) { } @Override - public List visitList(KeYParser.ListContext ctx) { + public List visitList(JavaKeYParser.ListContext ctx) { var seq = new ArrayList<>(ctx.children.size()); - for (KeYParser.CvalueContext context : ctx.cvalue()) { + for (JavaKeYParser.CvalueContext context : ctx.cvalue()) { seq.add(context.accept(this)); } return seq; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/DebugKeyLexer.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/DebugKeyLexer.java index 5c39de74099..8ce8ef63099 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/DebugKeyLexer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/DebugKeyLexer.java @@ -30,9 +30,9 @@ public class DebugKeyLexer { private static final String DEFAULT_FORMAT = "%02d %20s %d:%-50s\n"; private final PrintStream stream; private final String format; - private final Collection lexer; + private final Collection lexer; - public DebugKeyLexer(PrintStream stream, String format, Collection lexer) { + public DebugKeyLexer(PrintStream stream, String format, Collection lexer) { this.stream = stream; this.format = format; this.lexer = lexer; @@ -78,25 +78,25 @@ public static void debug(String content) { debug(ParsingFacade.createLexer(CharStreams.fromString(content))); } - public static void debug(KeYLexer lexer) { + public static void debug(JavaKeYLexer lexer) { DebugKeyLexer dkl = new DebugKeyLexer(System.out, DEFAULT_FORMAT, Collections.singleton(lexer)); dkl.run(); } public void run() { - for (KeYLexer l : lexer) { + for (JavaKeYLexer l : lexer) { run(l); } } - private void run(KeYLexer toks) { + private void run(JavaKeYLexer toks) { Token t; do { t = toks.nextToken(); stream.format(format, toks.getLine(), toks.getVocabulary().getSymbolicName(t.getType()), toks._mode, t.getText().replace("\n", "\\n")); - if (t.getType() == KeYLexer.ERROR_CHAR) { + if (t.getType() == JavaKeYLexer.ERROR_CHAR) { stream.println("!!ERROR!!"); } } while (t.getType() != CommonToken.EOF); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 22a4e64f10d..8bc16632f64 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -78,8 +78,8 @@ public String getText() { } /// An AST representing a complete KeY file. - public static class File extends KeyAst { - File(KeYParser.FileContext ctx) { + public static class File extends KeyAst { + File(JavaKeYParser.FileContext ctx) { super(ctx); } @@ -110,7 +110,7 @@ public static class File extends KeyAst { */ public @Nullable ProofScript findProofScript() { if (ctx.problem() != null && ctx.problem().proofScriptEntry() != null) { - KeYParser.ProofScriptEntryContext pctx = ctx.problem().proofScriptEntry(); + JavaKeYParser.ProofScriptEntryContext pctx = ctx.problem().proofScriptEntry(); if (pctx.STRING_LITERAL() != null) { var ctx = pctx.STRING_LITERAL().getSymbol(); @@ -156,7 +156,7 @@ public ProblemInformation getProblemInformation() { /// This token also marks the end of the parse tree (EOF) but not the end of the file. /// Positional information of the token is used to set up the proof replayer. public @Nullable Token findProof() { - KeYParser.ProofContext a = ctx.proof(); + JavaKeYParser.ProofContext a = ctx.proof(); if (a != null) { return a.PROOF().getSymbol(); } @@ -169,16 +169,16 @@ public ProblemInformation getProblemInformation() { * the regular classpath, the Java source file to load, * include statements to load other files, configuration of options, * declarations of sorts, program variables, schema variables, predicates, and more. - * See the grammar (KeYParser.g4) for more possible elements. + * See the grammar (JavaKeYParser.g4) for more possible elements. */ public KeyAst.@Nullable Declarations getProblemHeader() { - final KeYParser.DeclsContext decls = ctx.decls(); + final JavaKeYParser.DeclsContext decls = ctx.decls(); return new KeyAst.Declarations(decls); } } - public static class ConfigurationFile extends KeyAst { - ConfigurationFile(KeYParser.CfileContext ctx) { + public static class ConfigurationFile extends KeyAst { + ConfigurationFile(JavaKeYParser.CfileContext ctx) { super(ctx); } @@ -214,20 +214,20 @@ public Expression(JmlParser.@NonNull ExpressionContext ctx) { } - public static class Term extends KeyAst { - Term(KeYParser.TermContext ctx) { + public static class Term extends KeyAst { + Term(JavaKeYParser.TermContext ctx) { super(ctx); } } - public static class Seq extends KeyAst { - Seq(KeYParser.SeqContext ctx) { + public static class Seq extends KeyAst { + Seq(JavaKeYParser.SeqContext ctx) { super(ctx); } } - public static class Taclet extends KeyAst { - public Taclet(KeYParser.TacletContext taclet) { + public static class Taclet extends KeyAst { + public Taclet(JavaKeYParser.TacletContext taclet) { super(taclet); } } @@ -238,8 +238,8 @@ public Taclet(KeYParser.TacletContext taclet) { * @author Alexander Weigl * @version 1 (23.04.24) */ - public static class ProofScript extends KeyAst { - ProofScript(KeYParser.@NonNull ProofScriptContext ctx) { + public static class ProofScript extends KeyAst { + ProofScript(JavaKeYParser.@NonNull ProofScriptContext ctx) { super(ctx); } @@ -269,12 +269,12 @@ public List asAst() { } private static List asAst(URI file, - List cmds) { + List cmds) { return cmds.stream().map(it -> asAst(file, it)).toList(); } public static @NonNull ScriptBlock asAst(URI file, - KeYParser.ProofScriptCodeBlockContext ctx) { + JavaKeYParser.ProofScriptCodeBlockContext ctx) { var loc = new Location(file, Position.fromToken(ctx.start)); final var proofScriptCommandContexts = ctx.proofScript().proofScriptCommand(); final List list = @@ -285,7 +285,7 @@ private static List asAst(URI file, } private static @NonNull ScriptCommandAst asAst(URI file, - KeYParser.ProofScriptCommandContext it) { + JavaKeYParser.ProofScriptCommandContext it) { var loc = new Location(file, Position.fromToken(it.start)); var nargs = new HashMap(); var pargs = new ArrayList<>(); @@ -313,15 +313,15 @@ private static List asAst(URI file, /// Represents the user declarations in a KeY file. /// /// @author weigl - public static class Declarations extends KeyAst { - protected Declarations(KeYParser.DeclsContext ctx) { + public static class Declarations extends KeyAst { + protected Declarations(JavaKeYParser.DeclsContext ctx) { super(ctx); } public java.io.@Nullable File getJavaSourceLocation() { try { - KeYParser.String_valueContext value = - ctx.javaSource(0).oneJavaSource().string_value(0); + JavaKeYParser.String_valueContext value = + ctx.programSource(0).oneProgramSource().string_value(0); String v = ParsingFacade.getValueDocumentation(value); return new java.io.File(v); } catch (NullPointerException | IndexOutOfBoundsException e) { @@ -333,9 +333,9 @@ protected Declarations(KeYParser.DeclsContext ctx) { /// Prints the definitions, independent of paths, to the given {@link PrintWriter}. public void printDefinitions(PrintWriter out) { - ctx.accept(new KeYParserBaseVisitor<@Nullable Object>() { + ctx.accept(new JavaKeYParserBaseVisitor<@Nullable Object>() { @Override - public @Nullable Object visitOne_include(KeYParser.One_includeContext ctx) { + public @Nullable Object visitOne_include(JavaKeYParser.One_includeContext ctx) { if (ctx.absfile != null) { out.printf("\\include %s;", ctx.absfile.getText()); } @@ -343,82 +343,86 @@ public void printDefinitions(PrintWriter out) { } @Override - public @Nullable Object visitOptions_choice(KeYParser.Options_choiceContext ctx) { + public @Nullable Object visitOptions_choice( + JavaKeYParser.Options_choiceContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitOption_decls(KeYParser.Option_declsContext ctx) { + public @Nullable Object visitOption_decls(JavaKeYParser.Option_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitSort_decls(KeYParser.Sort_declsContext ctx) { + public @Nullable Object visitSort_decls(JavaKeYParser.Sort_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { + public @Nullable Object visitProg_var_decls( + JavaKeYParser.Prog_var_declsContext ctx) { printAsIs(ctx); return null; } @Override public @Nullable Object visitSchema_var_decls( - KeYParser.Schema_var_declsContext ctx) { + JavaKeYParser.Schema_var_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitPred_decls(KeYParser.Pred_declsContext ctx) { + public @Nullable Object visitPred_decls(JavaKeYParser.Pred_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitFunc_decls(KeYParser.Func_declsContext ctx) { + public @Nullable Object visitFunc_decls(JavaKeYParser.Func_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitTransform_decls(KeYParser.Transform_declsContext ctx) { + public @Nullable Object visitTransform_decls( + JavaKeYParser.Transform_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitDatatype_decls(KeYParser.Datatype_declsContext ctx) { + public @Nullable Object visitDatatype_decls( + JavaKeYParser.Datatype_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitRuleset_decls(KeYParser.Ruleset_declsContext ctx) { + public @Nullable Object visitRuleset_decls(JavaKeYParser.Ruleset_declsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitContracts(KeYParser.ContractsContext ctx) { + public @Nullable Object visitContracts(JavaKeYParser.ContractsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitInvariants(KeYParser.InvariantsContext ctx) { + public @Nullable Object visitInvariants(JavaKeYParser.InvariantsContext ctx) { printAsIs(ctx); return null; } @Override - public @Nullable Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) { + public @Nullable Object visitRulesOrAxioms(JavaKeYParser.RulesOrAxiomsContext ctx) { printAsIs(ctx); return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java index b758e24d92e..b86472b9215 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java @@ -100,27 +100,27 @@ public static List parseFiles(URL url) throws IOException { return ci; } - private static KeYParser createParser(TokenSource lexer) { - KeYParser p = new KeYParser(new CommonTokenStream(lexer)); + private static JavaKeYParser createParser(TokenSource lexer) { + JavaKeYParser p = new JavaKeYParser(new CommonTokenStream(lexer)); p.removeErrorListeners(); p.addErrorListener(p.getErrorReporter()); return p; } - private static KeYParser createParser(CharStream stream) { + private static JavaKeYParser createParser(CharStream stream) { return createParser(createLexer(stream)); } - public static KeYLexer createLexer(Path file) throws IOException { + public static JavaKeYLexer createLexer(Path file) throws IOException { return createLexer(CharStreams.fromPath(file)); } - public static KeYLexer createLexer(CharStream stream) { - return new KeYLexer(stream); + public static JavaKeYLexer createLexer(CharStream stream) { + return new JavaKeYLexer(stream); } - public static @NonNull KeYLexer createLexer(@NonNull PositionedString ps) { + public static @NonNull JavaKeYLexer createLexer(@NonNull PositionedString ps) { var position = ps.getLocation().getPosition(); var uri = ps.getLocation().fileUri().toString(); @@ -153,12 +153,12 @@ public static KeyAst.File parseFile(File file) throws IOException { } public static KeyAst.File parseFile(CharStream stream) { - KeYParser p = createParser(stream); + JavaKeYParser p = createParser(stream); p.getInterpreter().setPredictionMode(PredictionMode.SLL); p.removeErrorListeners(); p.setErrorHandler(new BailErrorStrategy()); - KeYParser.FileContext ctx; + JavaKeYParser.FileContext ctx; try { ctx = p.file(); } catch (ParseCancellationException ex) { @@ -177,14 +177,14 @@ public static KeyAst.File parseFile(CharStream stream) { } public static KeyAst.Term parseExpression(CharStream stream) { - KeYParser p = createParser(stream); - KeYParser.TermContext term = p.termEOF().term(); + JavaKeYParser p = createParser(stream); + JavaKeYParser.TermContext term = p.termEOF().term(); p.getErrorReporter().throwException(); return new KeyAst.Term(term); } public static KeyAst.Seq parseSequent(CharStream stream) { - KeYParser p = createParser(stream); + JavaKeYParser p = createParser(stream); KeyAst.Seq seq = new KeyAst.Seq(p.seqEOF().seq()); p.getErrorReporter().throwException(); return seq; @@ -220,7 +220,7 @@ public static KeyAst.ProofScript parseScript(String text) { * @return non-null string */ public static @NonNull String getValueDocumentation( - KeYParser.@NonNull String_valueContext ctx) { + JavaKeYParser.@NonNull String_valueContext ctx) { return ctx.getText().substring(1, ctx.getText().length() - 1).replace("\\\"", "\"") .replace("\\\\", "\\"); } @@ -233,8 +233,8 @@ public static KeyAst.ProofScript parseScript(String text) { * @deprecated */ @Deprecated - public static KeYParser.Id_declarationContext parseIdDeclaration(CharStream stream) { - KeYParser p = createParser(stream); + public static JavaKeYParser.Id_declarationContext parseIdDeclaration(CharStream stream) { + JavaKeYParser p = createParser(stream); return p.id_declaration(); } @@ -252,7 +252,7 @@ public static KeyAst.Taclet parseTaclet(String source) { } public static KeyAst.Taclet parseTaclet(CharStream source) { - KeYParser p = createParser(source); + JavaKeYParser p = createParser(source); var term = p.taclet(); p.getErrorReporter().throwException(); return new KeyAst.Taclet(term); @@ -262,7 +262,8 @@ public static KeyAst.Taclet parseTaclet(CharStream source) { /** * Parses the configuration determined by the given {@code file}. - * A configuration corresponds to the grammar rule {@code cfile} in the {@code KeYParser.g4}. + * A configuration corresponds to the grammar rule {@code cfile} in the + * {@code JavaKeYParser.g4}. * * @param file non-null {@link Path} object * @return monad that encapsluate the ParserRuleContext @@ -284,14 +285,15 @@ public static KeyAst.ConfigurationFile parseConfigurationFile(File file) throws /** * Parses the configuration determined by the given {@code stream}. - * A configuration corresponds to the grammar rule {@code cfile} in the {@code KeYParser.g4}. + * A configuration corresponds to the grammar rule {@code cfile} in the + * {@code JavaKeYParser.g4}. * * @param stream non-null {@link CharStream} object * @return monad that encapsluate the ParserRuleContext * @throws BuildingException if the file is syntactical broken. */ public static KeyAst.ConfigurationFile parseConfigurationFile(CharStream stream) { - KeYParser p = createParser(stream); + JavaKeYParser p = createParser(stream); var ctx = p.cfile(); p.getErrorReporter().throwException(); return new KeyAst.ConfigurationFile(ctx); @@ -299,7 +301,8 @@ public static KeyAst.ConfigurationFile parseConfigurationFile(CharStream stream) /** * Parses the configuration determined by the given {@code stream}. - * A configuration corresponds to the grammar rule {@code cfile} in the {@code KeYParser.g4}. + * A configuration corresponds to the grammar rule {@code cfile} in the + * {@code JavaKeYParser.g4}. * * @param input non-null {@link CharStream} object * @return a configuration object with the data deserialize from the given file @@ -325,7 +328,7 @@ public static Configuration readConfigurationFile(File file) throws IOException return readConfigurationFile(file.toPath()); } - public static Configuration getConfiguration(KeYParser.TableContext ctx) { + public static Configuration getConfiguration(JavaKeYParser.TableContext ctx) { final var cfg = new ConfigurationBuilder(); return cfg.visitTable(ctx); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java index d4989e8336d..5e04812875e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java @@ -19,8 +19,8 @@ /** * A short little hack, but completely working and fast, for replaying proofs inside KeY files. *

- * This class avoids using the {@link KeYParser} and building a parse tree. It uses only the - * {@link KeYLexer} to analyze the sexpr which described the applied taclet application. + * This class avoids using the {@link JavaKeYParser} and building a parse tree. It uses only the + * {@link JavaKeYLexer} to analyze the sexpr which described the applied taclet application. * * @author Alexander Weigl * @version 1 (12/5/19) @@ -59,7 +59,8 @@ public static void run(@NonNull Token token, CharStream input, IProofFileParser } /** - * Replays the proof behind the given {@code input}. This method uses the {@link KeYLexer} to + * Replays the proof behind the given {@code input}. This method uses the {@link JavaKeYLexer} + * to * lex input stream, and parse them manually by consuming the tokens. It singals to the given * {@link IProofFileParser} at start or end of an expr. *

@@ -72,7 +73,7 @@ public static void run(@NonNull Token token, CharStream input, IProofFileParser */ public static void run(CharStream input, IProofFileParser prl, final int startLine, URI source) { - KeYLexer lexer = ParsingFacade.createLexer(input); + JavaKeYLexer lexer = ParsingFacade.createLexer(input); CommonTokenStream stream = new CommonTokenStream(lexer); ArrayDeque stack = new ArrayDeque<>(); // currently open // proof @@ -81,7 +82,7 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi while (true) { int type = stream.LA(1); // current token type switch (type) { - case KeYLexer.LPAREN -> { + case JavaKeYLexer.LPAREN -> { // expected "(" ["string"] stream.consume(); // consume the "(" Token idToken = stream.LT(1); // element id @@ -97,7 +98,7 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi stream.consume(); String arg = null; int pos = idToken.getLine() + startLine; - if (stream.LA(1) == KeYLexer.STRING_LITERAL) { + if (stream.LA(1) == JavaKeYLexer.STRING_LITERAL) { // argument was given arg = stream.LT(1).getText(); arg = unescape(arg.substring(1, arg.length() - 1)); @@ -107,11 +108,11 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi stack.push(cur); posStack.push(pos); } - case KeYLexer.RPAREN -> { + case JavaKeYLexer.RPAREN -> { prl.endExpr(stack.pop(), posStack.pop()); stream.consume(); } - case KeYLexer.EOF -> { + case JavaKeYLexer.EOF -> { return; } default -> stream.consume(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java index 61e425b8129..ce761f97c49 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java @@ -6,7 +6,7 @@ import java.util.*; import java.util.stream.Collectors; -import de.uka.ilkd.key.nparser.KeYParserBaseVisitor; +import de.uka.ilkd.key.nparser.JavaKeYParserBaseVisitor; import de.uka.ilkd.key.util.parsing.BuildingException; import de.uka.ilkd.key.util.parsing.BuildingIssue; @@ -31,7 +31,7 @@ * @author Alexander Weigl */ @SuppressWarnings("unchecked") -abstract class AbstractBuilder extends KeYParserBaseVisitor { +abstract class AbstractBuilder extends JavaKeYParserBaseVisitor { private static final Logger LOGGER = LoggerFactory.getLogger(AbstractBuilder.class); private @Nullable List buildingIssues = null; private @Nullable Stack parameters = null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java index 06da0a1a4d8..5b85032692d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java @@ -6,7 +6,7 @@ import java.util.*; import de.uka.ilkd.key.nparser.ChoiceInformation; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import org.key_project.logic.Choice; import org.key_project.logic.Name; @@ -39,14 +39,14 @@ public ChoiceFinder(Namespace choices) { } @Override - public Object visitDecls(KeYParser.DeclsContext ctx) { + public Object visitDecls(JavaKeYParser.DeclsContext ctx) { ctx.option_decls().forEach(this::accept); ctx.options_choice().forEach(this::accept); return null; } @Override - public Object visitChoice(KeYParser.ChoiceContext ctx) { + public Object visitChoice(JavaKeYParser.ChoiceContext ctx) { String category = ctx.category.getText(); List options = new ArrayList<>(ctx.optionDecl().size()); ctx.optionDecl().forEach(it -> options.add(it.IDENT.getText())); @@ -62,7 +62,7 @@ public Object visitChoice(KeYParser.ChoiceContext ctx) { } @Override - public Choice visitActivated_choice(KeYParser.Activated_choiceContext ctx) { + public Choice visitActivated_choice(JavaKeYParser.Activated_choiceContext ctx) { String cat = ctx.cat.getText(); String ch = ctx.choice_.getText(); if (activatedChoicesCategories().contains(cat)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ContractsAndInvariantsFinder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ContractsAndInvariantsFinder.java index b5212df34b6..dd630f69b6d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ContractsAndInvariantsFinder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ContractsAndInvariantsFinder.java @@ -11,7 +11,7 @@ import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.speclang.ClassInvariant; @@ -52,19 +52,19 @@ public ContractsAndInvariantsFinder(Services services, NamespaceSet nss) { } @Override - public Object visitDecls(KeYParser.DeclsContext ctx) { + public Object visitDecls(JavaKeYParser.DeclsContext ctx) { mapOf(ctx.contracts()); mapOf(ctx.invariants()); return null; } @Override - public Object visitContracts(KeYParser.ContractsContext ctx) { + public Object visitContracts(JavaKeYParser.ContractsContext ctx) { return mapOf(ctx.one_contract()); } @Override - public Object visitOne_contract(KeYParser.One_contractContext ctx) { + public Object visitOne_contract(JavaKeYParser.One_contractContext ctx) { String contractName = visitSimple_ident(ctx.contractName); // for program variable declarations Namespace oldProgVars = namespaces().programVariables(); @@ -87,7 +87,7 @@ public Object visitOne_contract(KeYParser.One_contractContext ctx) { @Override - public Object visitInvariants(KeYParser.InvariantsContext ctx) { + public Object visitInvariants(JavaKeYParser.InvariantsContext ctx) { Namespace orig = variables(); selfVar = (LocationVariable) ctx.selfVar.accept(this); ctx.one_invariant().forEach(it -> it.accept(this)); @@ -96,7 +96,7 @@ public Object visitInvariants(KeYParser.InvariantsContext ctx) { } @Override - public Object visitOne_invariant(KeYParser.One_invariantContext ctx) { + public Object visitOne_invariant(JavaKeYParser.One_invariantContext ctx) { String invName = visitSimple_ident(ctx.simple_ident()); JTerm fma = accept(ctx.fma); String displayName = ctx.displayName != null ? ctx.displayName.getText() : null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index b9d4c467101..ffbc703a831 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java @@ -12,7 +12,7 @@ import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.logic.sort.*; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.nparser.ParsingFacade; import org.key_project.logic.Choice; @@ -54,7 +54,7 @@ public DeclarationBuilder(Services services, NamespaceSet nss) { } @Override - public Object visitDecls(KeYParser.DeclsContext ctx) { + public Object visitDecls(JavaKeYParser.DeclsContext ctx) { mapMapOf(ctx.option_decls(), ctx.options_choice(), ctx.ruleset_decls(), ctx.sort_decls(), ctx.datatype_decls(), ctx.prog_var_decls(), ctx.schema_var_decls()); @@ -62,7 +62,7 @@ public Object visitDecls(KeYParser.DeclsContext ctx) { } @Override - public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { + public Object visitDatatype_decl(JavaKeYParser.Datatype_declContext ctx) { // boolean freeAdt = ctx.FREE() != null; var name = ctx.name.getText(); var doc = ctx.DOC_COMMENT() != null @@ -88,10 +88,10 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { } @Override - public Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { + public Object visitProg_var_decls(JavaKeYParser.Prog_var_declsContext ctx) { for (int i = 0; i < ctx.simple_ident_comma_list().size(); i++) { List varNames = accept(ctx.simple_ident_comma_list(i)); - KeYJavaType kjt = accept(ctx.keyjavatype(i)); + KeYJavaType kjt = accept(ctx.typemapping(i)); assert varNames != null; for (String varName : varNames) { if (varName.equals("null")) { @@ -118,9 +118,9 @@ public Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { @Override - public Object visitChoice(KeYParser.ChoiceContext ctx) { + public Object visitChoice(JavaKeYParser.ChoiceContext ctx) { String cat = ctx.category.getText(); - for (KeYParser.OptionDeclContext optdecl : ctx.optionDecl()) { + for (JavaKeYParser.OptionDeclContext optdecl : ctx.optionDecl()) { Token catctx = optdecl.IDENT; String name = cat + ":" + catctx.getText(); Choice c = choices().lookup(new Name(name)); @@ -139,15 +139,15 @@ public Object visitChoice(KeYParser.ChoiceContext ctx) { } @Override - public Object visitSort_decls(KeYParser.Sort_declsContext ctx) { - for (KeYParser.One_sort_declContext c : ctx.one_sort_decl()) { + public Object visitSort_decls(JavaKeYParser.Sort_declsContext ctx) { + for (JavaKeYParser.One_sort_declContext c : ctx.one_sort_decl()) { c.accept(this); } return null; } @Override - public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { + public Object visitOne_sort_decl(JavaKeYParser.One_sort_declContext ctx) { List sortOneOf = accept(ctx.sortOneOf); List sortExt = accept(ctx.sortExt); boolean isGenericSort = ctx.GENERIC() != null; @@ -251,23 +251,23 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { } @Override - public Object visitOption_decls(KeYParser.Option_declsContext ctx) { + public Object visitOption_decls(JavaKeYParser.Option_declsContext ctx) { return mapOf(ctx.choice()); } @Override - public List visitExtends_sorts(KeYParser.Extends_sortsContext ctx) { + public List visitExtends_sorts(JavaKeYParser.Extends_sortsContext ctx) { return mapOf(ctx.sortId()); } @Override - public List visitOneof_sorts(KeYParser.Oneof_sortsContext ctx) { + public List visitOneof_sorts(JavaKeYParser.Oneof_sortsContext ctx) { return mapOf(ctx.sortId()); } @Override - public Object visitRuleset_decls(KeYParser.Ruleset_declsContext ctx) { + public Object visitRuleset_decls(JavaKeYParser.Ruleset_declsContext ctx) { for (String id : this.mapOf(ctx.simple_ident())) { RuleSet h = new RuleSet(new Name(id)); if (ruleSets().lookup(new Name(id)) == null) { @@ -279,7 +279,7 @@ public Object visitRuleset_decls(KeYParser.Ruleset_declsContext ctx) { @Override - public Object visitOptions_choice(KeYParser.Options_choiceContext ctx) { + public Object visitOptions_choice(JavaKeYParser.Options_choiceContext ctx) { return null; } 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 edeffedf972..6eb96c12083 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 @@ -19,7 +19,7 @@ import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.*; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import org.key_project.logic.*; import org.key_project.logic.op.Function; @@ -62,17 +62,17 @@ public DefaultBuilder(Services services, NamespaceSet nss) { } @Override - public List visitPvset(KeYParser.PvsetContext ctx) { + public List visitPvset(JavaKeYParser.PvsetContext ctx) { return mapOf(ctx.varId()); } @Override - public List visitRulesets(KeYParser.RulesetsContext ctx) { + public List visitRulesets(JavaKeYParser.RulesetsContext ctx) { return mapOf(ctx.ruleset()); } @Override - public RuleSet visitRuleset(KeYParser.RulesetContext ctx) { + public RuleSet visitRuleset(JavaKeYParser.RulesetContext ctx) { String id = ctx.IDENT().getText(); RuleSet h = ruleSets().lookup(new Name(id)); if (h == null) { @@ -82,7 +82,7 @@ public RuleSet visitRuleset(KeYParser.RulesetContext ctx) { } @Override - public String visitSimple_ident_dots(KeYParser.Simple_ident_dotsContext ctx) { + public String visitSimple_ident_dots(JavaKeYParser.Simple_ident_dotsContext ctx) { return ctx.getText(); } @@ -110,7 +110,8 @@ protected void unbindVars(Namespace orig) { } /* - * @Override public Integer visitLocation_ident(KeYParser.Location_identContext ctx) { var id = + * @Override public Integer visitLocation_ident(JavaKeYParser.Location_identContext ctx) { var + * id = * accept(ctx.simple_ident()); if ("Location".equals(id)) { return LOCATION_MODIFIER; } else if * (!"Location".equals(id)) { semanticError(ctx, * "%s Attribute of a Non Rigid Function can only be 'Location'", id); } return NORMAL_NONRIGID; @@ -118,12 +119,13 @@ protected void unbindVars(Namespace orig) { */ @Override - public List visitArg_sorts_or_formula(KeYParser.Arg_sorts_or_formulaContext ctx) { + public List visitArg_sorts_or_formula(JavaKeYParser.Arg_sorts_or_formulaContext ctx) { return mapOf(ctx.arg_sorts_or_formula_helper()); } @Override - public Sort visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_helperContext ctx) { + public Sort visitArg_sorts_or_formula_helper( + JavaKeYParser.Arg_sorts_or_formula_helperContext ctx) { if (ctx.FORMULA() != null) { return JavaDLTheory.FORMULA; } else { @@ -132,7 +134,8 @@ public Sort visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_help } /* - * @Override public Sort visitAny_sortId(KeYParser.Any_sortIdContext ctx) { Pair p = + * @Override public Sort visitAny_sortId(JavaKeYParser.Any_sortIdContext ctx) { Pair + * p = * accept(ctx.any_sortId_help()); return toArraySort(p, ctx.EMPTYBRACKETS().size()); } */ @@ -144,7 +147,7 @@ public Sort visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_help * the String with the symbols name */ protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, - KeYParser.Formal_sort_argsContext genericArgsCtxt) { + JavaKeYParser.Formal_sort_argsContext genericArgsCtxt) { Name name = new Name(varfuncName); Operator[] operators = { schemaVariables().lookup(name), variables().lookup(name), @@ -249,7 +252,7 @@ protected Namespace choices() { } @Override - public String visitString_value(KeYParser.String_valueContext ctx) { + public String visitString_value(JavaKeYParser.String_valueContext ctx) { return ctx.getText().substring(1, ctx.getText().length() - 1); } @@ -270,7 +273,7 @@ public void setSchemaVariables(Namespace ns) { } @Override - public Object visitVarIds(KeYParser.VarIdsContext ctx) { + public Object visitVarIds(JavaKeYParser.VarIdsContext ctx) { Collection ids = accept(ctx.simple_ident_comma_list()); List list = new ArrayList<>(ids.size()); for (String id : ids) { @@ -286,34 +289,35 @@ public Object visitVarIds(KeYParser.VarIdsContext ctx) { @Override public Object visitSimple_ident_dots_comma_list( - KeYParser.Simple_ident_dots_comma_listContext ctx) { + JavaKeYParser.Simple_ident_dots_comma_listContext ctx) { return mapOf(ctx.simple_ident_dots()); } @Override - public String visitSimple_ident(KeYParser.Simple_identContext ctx) { + public String visitSimple_ident(JavaKeYParser.Simple_identContext ctx) { return ctx.IDENT().getText(); } @Override - public List visitSimple_ident_comma_list(KeYParser.Simple_ident_comma_listContext ctx) { + public List visitSimple_ident_comma_list( + JavaKeYParser.Simple_ident_comma_listContext ctx) { return mapOf(ctx.simple_ident()); } @Override - public List visitWhere_to_bind(KeYParser.Where_to_bindContext ctx) { + public List visitWhere_to_bind(JavaKeYParser.Where_to_bindContext ctx) { List list = new ArrayList<>(ctx.children.size()); ctx.b.forEach(it -> list.add(it.getText().equalsIgnoreCase("true"))); return list; } @Override - public List visitArg_sorts(KeYParser.Arg_sortsContext ctx) { + public List visitArg_sorts(JavaKeYParser.Arg_sortsContext ctx) { return mapOf(ctx.sortId()); } @Override - public Sort visitSortId(KeYParser.SortIdContext ctx) { + public Sort visitSortId(JavaKeYParser.SortIdContext ctx) { String primitiveName = ctx.id.getText(); if (ctx.formal_sort_args() != null) { // parametric sorts should be instantiated @@ -362,7 +366,7 @@ public Sort visitSortId(KeYParser.SortIdContext ctx) { return s; } - private ImmutableList getGenericArgs(KeYParser.Formal_sort_argsContext ctx, + private ImmutableList getGenericArgs(JavaKeYParser.Formal_sort_argsContext ctx, ImmutableList params) { if (ctx.sortId().size() != params.size()) { semanticError(ctx, "Expected %d sort arguments, got only %d", @@ -378,7 +382,7 @@ private ImmutableList getGenericArgs(KeYParser.Formal_sort_args } @Override - public KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) { + public KeYJavaType visitTypemapping(JavaKeYParser.TypemappingContext ctx) { boolean array = false; StringBuilder type = new StringBuilder(visitSimple_ident_dots(ctx.simple_ident_dots())); for (int i = 0; i < ctx.EMPTYBRACKETS().size(); i++) { @@ -424,19 +428,19 @@ public KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) { } @Override - public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { + public Object visitFuncpred_name(JavaKeYParser.Funcpred_nameContext ctx) { return ctx.getText(); } @Override public @Nullable List visitFormal_sort_param_decls( - KeYParser.Formal_sort_param_declsContext ctx) { + JavaKeYParser.Formal_sort_param_declsContext ctx) { return mapOf(ctx.formal_sort_param_decl()); } @Override public @Nullable GenericParameter visitFormal_sort_param_decl( - KeYParser.Formal_sort_param_declContext ctx) { + JavaKeYParser.Formal_sort_param_declContext ctx) { GenericParameter.Variance variance; if (ctx.PLUS() != null) { 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 b5b27874d6d..6e7d88c7980 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 @@ -19,11 +19,11 @@ import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.ProgramSVSort; -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; -import de.uka.ilkd.key.nparser.KeYParser.RealLiteralContext; +import de.uka.ilkd.key.nparser.JavaKeYLexer; +import de.uka.ilkd.key.nparser.JavaKeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser.DoubleLiteralContext; +import de.uka.ilkd.key.nparser.JavaKeYParser.FloatLiteralContext; +import de.uka.ilkd.key.nparser.JavaKeYParser.RealLiteralContext; import de.uka.ilkd.key.parser.NotDeclException; import de.uka.ilkd.key.pp.AbbrevMap; import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; @@ -181,7 +181,7 @@ private static boolean isSelectTerm(JTerm term) { } @Override - public JTerm visitParallel_term(KeYParser.Parallel_termContext ctx) { + public JTerm visitParallel_term(JavaKeYParser.Parallel_termContext ctx) { List t = mapOf(ctx.elementary_update_term()); JTerm a = t.get(0); for (int i = 1; i < t.size(); i++) { @@ -191,12 +191,12 @@ public JTerm visitParallel_term(KeYParser.Parallel_termContext ctx) { } @Override - public JTerm visitTermEOF(KeYParser.TermEOFContext ctx) { + public JTerm visitTermEOF(JavaKeYParser.TermEOFContext ctx) { return accept(ctx.term()); } @Override - public JTerm visitElementary_update_term(KeYParser.Elementary_update_termContext ctx) { + public JTerm visitElementary_update_term(JavaKeYParser.Elementary_update_termContext ctx) { JTerm a = accept(ctx.a); JTerm b = accept(ctx.b); if (b != null) { @@ -206,14 +206,14 @@ public JTerm visitElementary_update_term(KeYParser.Elementary_update_termContext } @Override - public JTerm visitEquivalence_term(KeYParser.Equivalence_termContext ctx) { + public JTerm visitEquivalence_term(JavaKeYParser.Equivalence_termContext ctx) { JTerm a = accept(ctx.a); if (ctx.b.isEmpty()) { return a; } JTerm cur = a; - for (KeYParser.Implication_termContext context : ctx.b) { + for (JavaKeYParser.Implication_termContext context : ctx.b) { JTerm b = accept(context); cur = binaryTerm(ctx, Equality.EQV, cur, b); @@ -232,25 +232,25 @@ private JTerm binaryTerm(ParserRuleContext ctx, Operator operator, } @Override - public JTerm visitImplication_term(KeYParser.Implication_termContext ctx) { + public JTerm visitImplication_term(JavaKeYParser.Implication_termContext ctx) { JTerm termL = accept(ctx.a); JTerm termR = accept(ctx.b); return binaryTerm(ctx, Junctor.IMP, termL, termR); } @Override - public JTerm visitDisjunction_term(KeYParser.Disjunction_termContext ctx) { + public JTerm visitDisjunction_term(JavaKeYParser.Disjunction_termContext ctx) { JTerm t = accept(ctx.a); - for (KeYParser.Conjunction_termContext c : ctx.b) { + for (JavaKeYParser.Conjunction_termContext c : ctx.b) { t = binaryTerm(ctx, Junctor.OR, t, accept(c)); } return t; } @Override - public JTerm visitConjunction_term(KeYParser.Conjunction_termContext ctx) { + public JTerm visitConjunction_term(JavaKeYParser.Conjunction_termContext ctx) { JTerm t = accept(ctx.a); - for (KeYParser.Term60Context c : ctx.b) { + for (JavaKeYParser.Term60Context c : ctx.b) { t = binaryTerm(ctx, Junctor.AND, t, accept(c)); } return t; @@ -259,14 +259,14 @@ public JTerm visitConjunction_term(KeYParser.Conjunction_termContext ctx) { } @Override - public Object visitUnary_minus_term(KeYParser.Unary_minus_termContext ctx) { + public Object visitUnary_minus_term(JavaKeYParser.Unary_minus_termContext ctx) { JTerm result = accept(ctx.sub); assert result != null; if (ctx.MINUS() != null) { Function Z = functions().lookup("Z"); if (result.op() == Z) { // weigl: rewrite neg(Z(1(#)) to Z(neglit(1(#)) - // This mimics the old KeyParser behaviour. Unknown if necessary. + // This mimics the old JavaKeYParser behaviour. Unknown if necessary. final Function neglit = functions().lookup("neglit"); final JTerm num = result.sub(0); return capsulateTf(ctx, @@ -294,7 +294,7 @@ public Object visitUnary_minus_term(KeYParser.Unary_minus_termContext ctx) { } @Override - public JTerm visitNegation_term(KeYParser.Negation_termContext ctx) { + public JTerm visitNegation_term(JavaKeYParser.Negation_termContext ctx) { JTerm termL = accept(ctx.sub); if (ctx.NOT() != null) { return capsulateTf(ctx, () -> getTermFactory().createTerm(Junctor.NOT, termL)); @@ -304,7 +304,7 @@ public JTerm visitNegation_term(KeYParser.Negation_termContext ctx) { } @Override - public JTerm visitEquality_term(KeYParser.Equality_termContext ctx) { + public JTerm visitEquality_term(JavaKeYParser.Equality_termContext ctx) { JTerm termL = accept(ctx.a); JTerm termR = accept(ctx.b); JTerm eq = binaryTerm(ctx, Equality.EQUALS, termL, termR); @@ -315,7 +315,7 @@ public JTerm visitEquality_term(KeYParser.Equality_termContext ctx) { } @Override - public Object visitComparison_term(KeYParser.Comparison_termContext ctx) { + public Object visitComparison_term(JavaKeYParser.Comparison_termContext ctx) { JTerm termL = accept(ctx.a); JTerm termR = accept(ctx.b); @@ -341,7 +341,7 @@ public Object visitComparison_term(KeYParser.Comparison_termContext ctx) { } @Override - public Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx) { + public Object visitWeak_arith_term(JavaKeYParser.Weak_arith_termContext ctx) { JTerm termL = Objects.requireNonNull(accept(ctx.a)); if (ctx.op.isEmpty()) { return updateOrigin(termL, ctx, services); @@ -352,11 +352,11 @@ public Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx) { for (int i = 0; i < terms.size(); i++) { String opname = ""; switch (ctx.op.get(i).getType()) { - case KeYLexer.UTF_INTERSECT -> opname = LocSetLDT.INTERSECT_STRING; - case KeYLexer.UTF_SETMINUS -> opname = LocSetLDT.SETMINUS_STRING; - case KeYLexer.UTF_UNION -> opname = LocSetLDT.UNION_STRING; - case KeYLexer.PLUS -> opname = IntegerLDT.ADD_STRING; - case KeYLexer.MINUS -> opname = IntegerLDT.SUB_STRING; + case JavaKeYLexer.UTF_INTERSECT -> opname = LocSetLDT.INTERSECT_STRING; + case JavaKeYLexer.UTF_SETMINUS -> opname = LocSetLDT.SETMINUS_STRING; + case JavaKeYLexer.UTF_UNION -> opname = LocSetLDT.UNION_STRING; + case JavaKeYLexer.PLUS -> opname = IntegerLDT.ADD_STRING; + case JavaKeYLexer.MINUS -> opname = IntegerLDT.SUB_STRING; default -> semanticError(ctx, "Unexpected token: %s", ctx.op.get(i)); } JTerm cur = terms.get(i); @@ -385,7 +385,7 @@ private JTerm binaryLDTSpecificTerm(ParserRuleContext ctx, String opname, JTerm @Override - public Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx) { + public Object visitStrong_arith_term_1(JavaKeYParser.Strong_arith_term_1Context ctx) { JTerm termL = accept(ctx.a); if (ctx.b.isEmpty()) { return updateOrigin(termL, ctx, services); @@ -399,19 +399,20 @@ public Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx) } @Override - public Object visitEmptyset(KeYParser.EmptysetContext ctx) { + public Object visitEmptyset(JavaKeYParser.EmptysetContext ctx) { var op = services.getTypeConverter().getLocSetLDT().getEmpty(); return updateOrigin(getTermFactory().createTerm(op), ctx, services); } @Override - public Object visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx) { + public Object visitStrong_arith_term_2(JavaKeYParser.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" : + // List opName = ctx.op.stream().map(it -> it.getType()== JavaKeYLexer.PERCENT ? + // "mod" : // "div").collect(Collectors.toList()); JTerm term = accept(ctx.a); @@ -430,7 +431,7 @@ public Object visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx) 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"; + var opName = ctx.op.get(i).getType() == JavaKeYLexer.PERCENT ? "mod" : "div"; Function op = ldt.getFunctionFor(opName, services); if (op == null) { semanticError(ctx, "Could not find function symbol '%s' for sort '%s'.", opName, @@ -451,10 +452,11 @@ protected JTerm capsulateTf(ParserRuleContext ctx, Supplier termSupplier) } @Override - public Object visitBracket_term(KeYParser.Bracket_termContext ctx) { + public Object visitBracket_term(JavaKeYParser.Bracket_termContext ctx) { JTerm t = accept(ctx.primitive_labeled_term()); for (int i = 0; i < ctx.bracket_suffix_heap().size(); i++) { - KeYParser.Brace_suffixContext brace_suffix = ctx.bracket_suffix_heap(i).brace_suffix(); + JavaKeYParser.Brace_suffixContext brace_suffix = + ctx.bracket_suffix_heap(i).brace_suffix(); ParserRuleContext heap = ctx.bracket_suffix_heap(i).heap; t = accept(brace_suffix, t); if (heap != null) { @@ -469,7 +471,8 @@ public Object visitBracket_term(KeYParser.Bracket_termContext ctx) { /* * @Override public String - * visitStaticAttributeOrQueryReference(KeYParser.StaticAttributeOrQueryReferenceContext ctx) { + * visitStaticAttributeOrQueryReference(JavaKeYParser.StaticAttributeOrQueryReferenceContext + * ctx) { * //TODO weigl: this rule is a total grammar blower. String attrReference = ctx.id.getText(); * for (int i = 0; i < ctx.EMPTYBRACKETS().size(); i++) { attrReference += "[]"; } * @@ -483,7 +486,8 @@ public Object visitBracket_term(KeYParser.Bracket_termContext ctx) { // } /* - * @Override public Term visitStatic_attribute_suffix(KeYParser.Static_attribute_suffixContext + * @Override public Term + * visitStatic_attribute_suffix(JavaKeYParser.Static_attribute_suffixContext * ctx) { Operator v = null; String attributeName = * accept(ctx.staticAttributeOrQueryReference()); String className; if * (attributeName.indexOf(':') != -1) { className = attributeName.substring(0, @@ -549,19 +553,19 @@ private JTerm toZNotation(BigInteger bi, Namespace functions) { } @Override - public Sequent visitSeq(KeYParser.SeqContext ctx) { + public Sequent visitSeq(JavaKeYParser.SeqContext ctx) { ImmutableList ant = accept(ctx.ant); ImmutableList suc = accept(ctx.suc); return JavaDLSequentKit.createSequent(ant, suc); } @Override - public Sequent visitSeqEOF(KeYParser.SeqEOFContext ctx) { + public Sequent visitSeqEOF(JavaKeYParser.SeqEOFContext ctx) { return accept(ctx.seq()); } @Override - public Object visitTermorseq(KeYParser.TermorseqContext ctx) { + public Object visitTermorseq(JavaKeYParser.TermorseqContext ctx) { JTerm head = accept(ctx.head); Sequent s = accept(ctx.s); ImmutableList ss = accept(ctx.ss); @@ -586,7 +590,7 @@ public Object visitTermorseq(KeYParser.TermorseqContext ctx) { } @Override - public ImmutableList visitSemisequent(KeYParser.SemisequentContext ctx) { + public ImmutableList visitSemisequent(JavaKeYParser.SemisequentContext ctx) { ImmutableList ss = accept(ctx.ss); if (ss == null) { ss = ImmutableSLList.nil(); @@ -628,7 +632,7 @@ private PairOfStringAndJavaBlock getJavaBlock(Token t) { } @Override - public Object visitMetaId(KeYParser.MetaIdContext ctx) { + public Object visitMetaId(JavaKeYParser.MetaIdContext ctx) { String id = visitSimple_ident(ctx.simple_ident()); TermTransformer v = AbstractTermTransformer.name2metaop(id); if (v == null) { @@ -638,7 +642,7 @@ public Object visitMetaId(KeYParser.MetaIdContext ctx) { } @Override - public JTerm visitMetaTerm(KeYParser.MetaTermContext ctx) { + public JTerm visitMetaTerm(JavaKeYParser.MetaTermContext ctx) { Operator metaId = accept(ctx.metaId()); List t = mapOf(ctx.term()); return capsulateTf(ctx, () -> getTermFactory().createTerm(metaId, t)); @@ -733,7 +737,8 @@ private Operator getAttributeInPrefixSort(Sort prefixSort, String attributeName) } /* - * @Override public String visitAttrid(KeYParser.AttridContext ctx) { return ctx.getText(); } + * @Override public String visitAttrid(JavaKeYParser.AttridContext ctx) { return ctx.getText(); + * } */ private String unescapeString(String string) { @@ -760,13 +765,13 @@ private String unescapeString(String string) { } @Override - public JTerm visitString_literal(KeYParser.String_literalContext ctx) { + public JTerm visitString_literal(JavaKeYParser.String_literalContext ctx) { String s = unescapeString(ctx.id.getText()); return getServices().getTypeConverter().convertToLogicElement(new StringLiteral(s)); } @Override - public Object visitCast_term(KeYParser.Cast_termContext ctx) { + public Object visitCast_term(JavaKeYParser.Cast_termContext ctx) { JTerm result = accept(ctx.sub); if (ctx.sortId() == null) { return result; @@ -795,7 +800,8 @@ private void markHeapAsExplicit(JTerm a) { } /* - * private Term createStaticAttributeOrMethod(JavaQuery jq, KeYParser.AccesstermContext ctx) { + * private Term createStaticAttributeOrMethod(JavaQuery jq, JavaKeYParser.AccesstermContext ctx) + * { * final var kjt = jq.kjt; String mn = jq.attributeNames; if (jq.maybeAttr != null) { * ProgramVariable maybeAttr = getJavaInfo().getAttribute(mn, kjt); if (maybeAttr != null) { var * op = getAttributeInPrefixSort(kjt.getSort(), mn); return createAttributeTerm(null, op, ctx); @@ -808,7 +814,8 @@ private void markHeapAsExplicit(JTerm a) { */ @Override - public Object visitBracket_access_heap_update(KeYParser.Bracket_access_heap_updateContext ctx) { + public Object visitBracket_access_heap_update( + JavaKeYParser.Bracket_access_heap_updateContext ctx) { JTerm heap = pop(); JTerm target = accept(ctx.target); JTerm val = accept(ctx.val); @@ -819,7 +826,7 @@ public Object visitBracket_access_heap_update(KeYParser.Bracket_access_heap_upda @Override - public Object visitBracket_access_heap_term(KeYParser.Bracket_access_heap_termContext ctx) { + public Object visitBracket_access_heap_term(JavaKeYParser.Bracket_access_heap_termContext ctx) { JTerm heap = pop(); String id = accept(ctx.simple_ident()); @@ -840,7 +847,7 @@ public Object visitBracket_access_heap_term(KeYParser.Bracket_access_heap_termCo } @Override - public Object visitBracket_access_star(KeYParser.Bracket_access_starContext ctx) { + public Object visitBracket_access_star(JavaKeYParser.Bracket_access_starContext ctx) { JTerm reference = pop(); JTerm rangeFrom = toZNotation("0", functions()); JTerm lt = getServices().getTermBuilder().dotLength(reference); @@ -852,7 +859,8 @@ public Object visitBracket_access_star(KeYParser.Bracket_access_starContext ctx) } @Override - public Object visitBracket_access_indexrange(KeYParser.Bracket_access_indexrangeContext ctx) { + public Object visitBracket_access_indexrange( + JavaKeYParser.Bracket_access_indexrangeContext ctx) { // | term LBRACKET indexTerm=term (DOTRANGE rangeTo=term)? RBRACKET // #bracket_access_indexrange JTerm term = pop(); @@ -902,7 +910,7 @@ public Object visitBracket_access_indexrange(KeYParser.Bracket_access_indexrange } @Override - public Object visitBoolean_literal(KeYParser.Boolean_literalContext ctx) { + public Object visitBoolean_literal(JavaKeYParser.Boolean_literalContext ctx) { if (ctx.TRUE() != null) { return capsulateTf(ctx, () -> getTermFactory().createTerm(Junctor.TRUE)); } else { @@ -911,7 +919,7 @@ public Object visitBoolean_literal(KeYParser.Boolean_literalContext ctx) { } @Override - public Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContext ctx) { + public Object visitPrimitive_labeled_term(JavaKeYParser.Primitive_labeled_termContext ctx) { JTerm t = accept(ctx.primitive_term()); if (ctx.LGUILLEMETS() != null) { ImmutableArray labels = accept(ctx.label()); @@ -923,13 +931,13 @@ public Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContex } @Override - public ImmutableArray visitLabel(KeYParser.LabelContext ctx) { + public ImmutableArray visitLabel(JavaKeYParser.LabelContext ctx) { List labels = mapOf(ctx.single_label()); return new ImmutableArray<>(labels); } @Override - public TermLabel visitSingle_label(KeYParser.Single_labelContext ctx) { + public TermLabel visitSingle_label(JavaKeYParser.Single_labelContext ctx) { String labelName = ""; TermLabel left = null; TermLabel right = null; @@ -959,7 +967,7 @@ public TermLabel visitSingle_label(KeYParser.Single_labelContext ctx) { } @Override - public Object visitAbbreviation(KeYParser.AbbreviationContext ctx) { + public Object visitAbbreviation(JavaKeYParser.AbbreviationContext ctx) { String sc = accept(ctx.name); JTerm a = abbrevMap.getTerm(sc); if (a == null) { @@ -969,7 +977,7 @@ public Object visitAbbreviation(KeYParser.AbbreviationContext ctx) { } @Override - public JTerm visitIfThenElseTerm(KeYParser.IfThenElseTermContext ctx) { + public JTerm visitIfThenElseTerm(JavaKeYParser.IfThenElseTermContext ctx) { JTerm condF = (JTerm) ctx.condF.accept(this); if (condF.sort() != JavaDLTheory.FORMULA) { semanticError(ctx, "Condition of an \\if-then-else term has to be a formula."); @@ -982,7 +990,7 @@ public JTerm visitIfThenElseTerm(KeYParser.IfThenElseTermContext ctx) { @Override - public Object visitIfExThenElseTerm(KeYParser.IfExThenElseTermContext ctx) { + public Object visitIfExThenElseTerm(JavaKeYParser.IfExThenElseTermContext ctx) { Namespace orig = variables(); List exVars = accept(ctx.bound_variables()); JTerm condF = accept(ctx.condF); @@ -1000,7 +1008,7 @@ public Object visitIfExThenElseTerm(KeYParser.IfExThenElseTermContext ctx) { } @Override - public JTerm visitQuantifierterm(KeYParser.QuantifiertermContext ctx) { + public JTerm visitQuantifierterm(JavaKeYParser.QuantifiertermContext ctx) { Operator op = null; Namespace orig = variables(); if (ctx.FORALL() != null) { @@ -1018,20 +1026,20 @@ public JTerm visitQuantifierterm(KeYParser.QuantifiertermContext ctx) { } @Override - public JTerm visitLocset_term(KeYParser.Locset_termContext ctx) { + public JTerm visitLocset_term(JavaKeYParser.Locset_termContext ctx) { List terms = mapOf(ctx.location_term()); return getServices().getTermBuilder().union(terms); } @Override - public Object visitLocation_term(KeYParser.Location_termContext ctx) { + public Object visitLocation_term(JavaKeYParser.Location_termContext ctx) { JTerm obj = accept(ctx.obj); JTerm field = accept(ctx.field); return getServices().getTermBuilder().singleton(obj, field); } @Override - public Object visitSubstitution_term(KeYParser.Substitution_termContext ctx) { + public Object visitSubstitution_term(JavaKeYParser.Substitution_termContext ctx) { SubstOp op = WarySubstOp.SUBST; Namespace orig = variables(); JAbstractSortedOperator v = accept(ctx.bv); @@ -1056,7 +1064,7 @@ public Object visitSubstitution_term(KeYParser.Substitution_termContext ctx) { } @Override - public Object visitUpdate_term(KeYParser.Update_termContext ctx) { + public Object visitUpdate_term(JavaKeYParser.Update_termContext ctx) { JTerm t = oneOf(ctx.atom_prefix(), ctx.unary_formula()); if (ctx.u.isEmpty()) { return t; @@ -1065,12 +1073,14 @@ public Object visitUpdate_term(KeYParser.Update_termContext ctx) { return getTermFactory().createTerm(UpdateApplication.UPDATE_APPLICATION, u, t); } - public List visitBound_variables(KeYParser.Bound_variablesContext ctx) { + public List visitBound_variables( + JavaKeYParser.Bound_variablesContext ctx) { return mapOf(ctx.one_bound_variable()); } @Override - public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variableContext ctx) { + public QuantifiableVariable visitOne_bound_variable( + JavaKeYParser.One_bound_variableContext ctx) { String id = accept(ctx.simple_ident()); Sort sort = accept(ctx.sortId()); @@ -1103,7 +1113,7 @@ public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variable @Override - public Object visitModality_term(KeYParser.Modality_termContext ctx) { + public Object visitModality_term(JavaKeYParser.Modality_termContext ctx) { JTerm a1 = accept(ctx.sub); if (ctx.MODALITY() == null) { return a1; @@ -1132,12 +1142,12 @@ public Object visitModality_term(KeYParser.Modality_termContext ctx) { } @Override - public List visitArgument_list(KeYParser.Argument_listContext ctx) { + public List visitArgument_list(JavaKeYParser.Argument_listContext ctx) { return mapOf(ctx.term()); } @Override - public Object visitChar_literal(KeYParser.Char_literalContext ctx) { + public Object visitChar_literal(JavaKeYParser.Char_literalContext ctx) { String s = ctx.CHAR_LITERAL().getText(); int intVal = 0; if (s.length() == 3) { @@ -1164,7 +1174,7 @@ public boolean isClass(String p) { * @return a Term or an operator, depending on the referenced object. */ @Override - public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { + public Object visitFuncpred_name(JavaKeYParser.Funcpred_nameContext ctx) { List parts = mapOf(ctx.name.simple_ident()); String varfuncid = ctx.name.getText(); @@ -1203,7 +1213,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { op = lookupVarfuncId(ctx, firstName, null); if (op instanceof ProgramVariable v && ctx.name.simple_ident().size() > 1) { - List otherParts = + List otherParts = ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size()); JTerm tv = getServices().getTermFactory().createTerm(v); String memberName = otherParts.get(0).getText(); @@ -1223,7 +1233,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { return op; } - private JTerm visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { + private JTerm visitAccesstermAsJava(JavaKeYParser.AccesstermContext ctx) { String firstName = accept(ctx.firstName); if (isPackage(firstName) || isClass(firstName)) { // consume suffix as long as it is part of a java class or package @@ -1236,7 +1246,7 @@ private JTerm visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { // region split up package and class name while (startWithPackage && ctx.attribute( - currentSuffix) instanceof KeYParser.Attribute_simpleContext a) { + currentSuffix) instanceof JavaKeYParser.Attribute_simpleContext a) { if (a.heap != null) { break; // No heap on java package allowed } @@ -1250,7 +1260,8 @@ private JTerm visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { } } - while (ctx.attribute(currentSuffix) instanceof KeYParser.Attribute_simpleContext a) { + while (ctx + .attribute(currentSuffix) instanceof JavaKeYParser.Attribute_simpleContext a) { if (a.heap != null) { break; // No heap on java Class name allowed } @@ -1274,10 +1285,10 @@ private JTerm visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { JTerm current = null; for (int i = currentSuffix; i < ctx.attribute().size(); i++) { - KeYParser.AttributeContext attrib = ctx.attribute(i); + JavaKeYParser.AttributeContext attrib = ctx.attribute(i); boolean isLast = i == ctx.attribute().size() - 1; - if (attrib instanceof KeYParser.Attribute_simpleContext simpleContext) { + if (attrib instanceof JavaKeYParser.Attribute_simpleContext simpleContext) { boolean isCall = simpleContext.call() != null; ParserRuleContext heap = simpleContext.heap; // TODO? String attributeName = accept(simpleContext.id); @@ -1298,7 +1309,7 @@ private JTerm visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { addWarning(""); return current; } - } else if (attrib instanceof KeYParser.Attribute_complexContext attrid) { + } else if (attrib instanceof JavaKeYParser.Attribute_complexContext attrid) { String className = attrid.sort.getText(); String attributeName = attrid.id.getText(); JTerm[] args = visitArguments(attrid.call().argument_list()); @@ -1316,7 +1327,7 @@ private JTerm visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { } } return current; - } else if (attrib instanceof KeYParser.Attribute_starContext) { + } else if (attrib instanceof JavaKeYParser.Attribute_starContext) { // TODO } } @@ -1326,7 +1337,7 @@ private JTerm visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { } @Override - public Object visitTermParen(KeYParser.TermParenContext ctx) { + public Object visitTermParen(JavaKeYParser.TermParenContext ctx) { JTerm base = accept(ctx.term()); if (ctx.attribute().isEmpty()) { return base; @@ -1334,18 +1345,18 @@ public Object visitTermParen(KeYParser.TermParenContext ctx) { return handleAttributes(base, ctx.attribute()); } - private JTerm handleAttributes(JTerm current, List attribute) { + private JTerm handleAttributes(JTerm current, List attribute) { for (int i = 0; i < attribute.size(); i++) { - KeYParser.AttributeContext ctxSuffix = attribute.get(i); + JavaKeYParser.AttributeContext ctxSuffix = attribute.get(i); boolean isLast = i == attribute.size() - 1; - if (ctxSuffix instanceof KeYParser.Attribute_starContext) { + if (ctxSuffix instanceof JavaKeYParser.Attribute_starContext) { current = services.getTermBuilder().allFields(current); if (!isLast) { addWarning(""); } return current; - } else if (ctxSuffix instanceof KeYParser.Attribute_simpleContext attrid) { + } else if (ctxSuffix instanceof JavaKeYParser.Attribute_simpleContext attrid) { String memberName = attrid.id.getText(); Sort seqSort = lookupSort("Seq"); if (current.sort() == seqSort) { @@ -1379,7 +1390,7 @@ private JTerm handleAttributes(JTerm current, List a current = replaceHeap(current, heap, ctxSuffix); } } - } else if (ctxSuffix instanceof KeYParser.Attribute_complexContext attrid) { + } else if (ctxSuffix instanceof JavaKeYParser.Attribute_complexContext attrid) { JTerm heap = accept(attrid.heap); String classRef = attrid.sort.getText(); String memberName = attrid.id.getText(); @@ -1428,7 +1439,7 @@ public T defaultOnException(T defaultValue, Supplier supplier) { } @Override - public JTerm visitAccessterm(KeYParser.AccesstermContext ctx) { + public JTerm visitAccessterm(JavaKeYParser.AccesstermContext ctx) { JTerm t = visitAccesstermAsJava(ctx); if (t != null) { return t; @@ -1440,7 +1451,7 @@ public JTerm visitAccessterm(KeYParser.AccesstermContext ctx) { ImmutableArray boundVars = null; Namespace orig = null; - KeYParser.Formal_sort_argsContext genericArgsCtxt = null; + JavaKeYParser.Formal_sort_argsContext genericArgsCtxt = null; if (ctx.formal_sort_args() != null) { genericArgsCtxt = ctx.formal_sort_args(); } @@ -1519,7 +1530,7 @@ public JTerm visitAccessterm(KeYParser.AccesstermContext ctx) { return current; } - private @Nullable JTerm[] visitArguments(KeYParser.@Nullable Argument_listContext call) { + private @Nullable JTerm[] visitArguments(JavaKeYParser.@Nullable Argument_listContext call) { List arguments = accept(call); return arguments == null ? null : arguments.toArray(new JTerm[0]); } @@ -1548,7 +1559,7 @@ public Object visitRealLiteral(RealLiteralContext ctx) { } @Override - public Object visitInteger(KeYParser.IntegerContext ctx) { + public Object visitInteger(JavaKeYParser.IntegerContext ctx) { return toZNotation(ctx.getText()); } @@ -1826,7 +1837,7 @@ private JavaQuery splitJava(List parts) { } @Override - public Object visitProofScript(KeYParser.ProofScriptContext ctx) { + public Object visitProofScript(JavaKeYParser.ProofScriptContext ctx) { return null;// Do not traverse into proof scripts. } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FindProblemInformation.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FindProblemInformation.java index 67b92a0bca3..4a6e80110ac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FindProblemInformation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FindProblemInformation.java @@ -6,7 +6,7 @@ import java.util.List; import java.util.Objects; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.nparser.ProblemInformation; @@ -24,7 +24,7 @@ public class FindProblemInformation extends AbstractBuilder { private final @NonNull ProblemInformation information = new ProblemInformation(); @Override - public Object visitFile(KeYParser.FileContext ctx) { + public Object visitFile(JavaKeYParser.FileContext ctx) { if (ctx.profile() != null) { information.setProfile(accept(ctx.profile())); } @@ -36,16 +36,16 @@ public Object visitFile(KeYParser.FileContext ctx) { } @Override - public Object visitDecls(KeYParser.DeclsContext ctx) { + public Object visitDecls(JavaKeYParser.DeclsContext ctx) { information.setBootClassPath(acceptFirst(ctx.bootClassPath())); ctx.classPaths().forEach( it -> information.getClasspath().addAll(Objects.requireNonNull(accept(it)))); - information.setJavaSource(acceptFirst(ctx.javaSource())); + information.setJavaSource(acceptFirst(ctx.programSource())); return null; } @Override - public Object visitProblem(KeYParser.ProblemContext ctx) { + public Object visitProblem(JavaKeYParser.ProblemContext ctx) { if (ctx.CHOOSECONTRACT() != null) { if (ctx.chooseContract != null) { information.setChooseContract(accept(ctx.chooseContract)); @@ -66,38 +66,37 @@ public Object visitProblem(KeYParser.ProblemContext ctx) { @Override - public String visitBootClassPath(KeYParser.BootClassPathContext ctx) { + public String visitBootClassPath(JavaKeYParser.BootClassPathContext ctx) { return accept(ctx.string_value()); } @Override - public List visitClassPaths(KeYParser.ClassPathsContext ctx) { + public List visitClassPaths(JavaKeYParser.ClassPathsContext ctx) { return mapOf(ctx.string_value()); } @Override - public String visitString_value(KeYParser.String_valueContext ctx) { + public String visitString_value(JavaKeYParser.String_valueContext ctx) { return ParsingFacade.getValueDocumentation(ctx); } - @Override - public String visitJavaSource(KeYParser.JavaSourceContext ctx) { - return ctx.oneJavaSource() != null ? (String) accept(ctx.oneJavaSource()) : null; + public String visitProgramSource(JavaKeYParser.ProgramSourceContext ctx) { + return ctx.oneProgramSource() != null ? (String) accept(ctx.oneProgramSource()) : null; } @Override - public String visitOneJavaSource(KeYParser.OneJavaSourceContext ctx) { + public String visitOneProgramSource(JavaKeYParser.OneProgramSourceContext ctx) { return StringUtil.trim(ctx.getText(), '"'); } @Override - public Object visitProfile(KeYParser.ProfileContext ctx) { + public Object visitProfile(JavaKeYParser.ProfileContext ctx) { return accept(ctx.name); } @Override - public String visitPreferences(KeYParser.PreferencesContext ctx) { + public String visitPreferences(JavaKeYParser.PreferencesContext ctx) { return ctx.s != null ? (String) accept(ctx.s) : null; } 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 9e84343c123..dc0b6b1bb20 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 @@ -12,7 +12,7 @@ import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.ParametricSortInstance; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import org.key_project.logic.Name; import org.key_project.logic.Namespace; @@ -44,18 +44,18 @@ public FunctionPredicateBuilder(Services services, NamespaceSet nss) { } @Override - public Object visitFile(KeYParser.FileContext ctx) { + public Object visitFile(JavaKeYParser.FileContext ctx) { return accept(ctx.decls()); } @Override - public Object visitDecls(KeYParser.DeclsContext ctx) { + public Object visitDecls(JavaKeYParser.DeclsContext ctx) { mapMapOf(ctx.pred_decls(), ctx.func_decls(), ctx.transform_decls(), ctx.datatype_decls()); return null; } @Override - public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { + public Object visitDatatype_decl(JavaKeYParser.Datatype_declContext ctx) { // weigl: all datatypes are free ==> functions are unique! // boolean freeAdt = ctx.FREE() != null; Sort sort; @@ -77,7 +77,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { sort = sorts().lookup(ctx.name.getText()); genericParams = null; } - for (KeYParser.Datatype_constructorContext constructorContext : ctx + for (JavaKeYParser.Datatype_constructorContext constructorContext : ctx .datatype_constructor()) { Name name = new Name(constructorContext.name.getText()); Sort[] args = new Sort[constructorContext.sortId().size()]; @@ -142,7 +142,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { } @Override - public Object visitPred_decl(KeYParser.Pred_declContext ctx) { + public Object visitPred_decl(JavaKeYParser.Pred_declContext ctx) { String pred_name = accept(ctx.funcpred_name()); List params = ctx.formal_sort_param_decls() == null ? null : visitFormal_sort_param_decls(ctx.formal_sort_param_decls()); @@ -190,7 +190,7 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { } @Override - public Object visitFunc_decl(KeYParser.Func_declContext ctx) { + public Object visitFunc_decl(JavaKeYParser.Func_declContext ctx) { boolean unique = ctx.UNIQUE() != null; Sort retSort = accept(ctx.sortId()); String funcName = accept(ctx.funcpred_name()); @@ -240,13 +240,13 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) { } @Override - public Object visitFunc_decls(KeYParser.Func_declsContext ctx) { + public Object visitFunc_decls(JavaKeYParser.Func_declsContext ctx) { return mapOf(ctx.func_decl()); } @Override - public Object visitTransform_decl(KeYParser.Transform_declContext ctx) { + public Object visitTransform_decl(JavaKeYParser.Transform_declContext ctx) { Sort retSort = ctx.FORMULA() != null ? JavaDLTheory.FORMULA : accept(ctx.sortId()); String trans_name = accept(ctx.funcpred_name()); List argSorts = accept(ctx.arg_sorts_or_formula()); @@ -260,13 +260,13 @@ public Object visitTransform_decl(KeYParser.Transform_declContext ctx) { @Override - public Object visitTransform_decls(KeYParser.Transform_declsContext ctx) { + public Object visitTransform_decls(JavaKeYParser.Transform_declsContext ctx) { return mapOf(ctx.transform_decl()); } @Override - public Object visitPred_decls(KeYParser.Pred_declsContext ctx) { + public Object visitPred_decls(JavaKeYParser.Pred_declsContext ctx) { return mapOf(ctx.pred_decl()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/IncludeFinder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/IncludeFinder.java index 6bd25460ab1..7996c22433d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/IncludeFinder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/IncludeFinder.java @@ -7,7 +7,7 @@ import java.net.MalformedURLException; import java.nio.file.Path; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.proof.init.Includes; import de.uka.ilkd.key.proof.io.RuleSource; import de.uka.ilkd.key.proof.io.RuleSourceFactory; @@ -31,14 +31,14 @@ public IncludeFinder(Path base) { } @Override - public Void visitOne_include_statement(KeYParser.One_include_statementContext ctx) { + public Void visitOne_include_statement(JavaKeYParser.One_include_statementContext ctx) { ldt = ctx.INCLUDELDTS() != null; mapOf(ctx.one_include()); return null; } @Override - public Void visitOne_include(KeYParser.One_includeContext ctx) { + public Void visitOne_include(JavaKeYParser.One_includeContext ctx) { String value = StringUtil.trim(ctx.getText(), "\"'"); try { addInclude(value); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java index f79f810304b..15f09b2cea6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.*; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; import de.uka.ilkd.key.settings.Configuration; @@ -40,14 +40,14 @@ public ProblemFinder(Services services, NamespaceSet nss) { } @Override - public @Nullable Object visitFile(KeYParser.FileContext ctx) { + public @Nullable Object visitFile(JavaKeYParser.FileContext ctx) { each(ctx.problem()); return null; } @Override - public @Nullable KeYJavaType visitArrayopid(KeYParser.ArrayopidContext ctx) { - return accept(ctx.keyjavatype()); + public @Nullable KeYJavaType visitArrayopid(JavaKeYParser.ArrayopidContext ctx) { + return accept(ctx.typemapping()); } /** @@ -66,7 +66,7 @@ public ProblemFinder(Services services, NamespaceSet nss) { * if the */ @Override - public @Nullable JTerm visitProblem(KeYParser.ProblemContext ctx) { + public @Nullable JTerm visitProblem(JavaKeYParser.ProblemContext ctx) { if (ctx.CHOOSECONTRACT() != null) { if (ctx.chooseContract != null) { chooseContract = ParsingFacade.getValueDocumentation(ctx.chooseContract); @@ -78,7 +78,7 @@ public ProblemFinder(Services services, NamespaceSet nss) { } if (ctx.PROOFOBLIGATION() != null) { var obl = ctx.proofObligation; - if (obl instanceof KeYParser.CstringContext stringContext) { + if (obl instanceof JavaKeYParser.CstringContext stringContext) { try { Properties p = new Properties(); var value = stringContext.STRING_LITERAL().getText(); @@ -92,7 +92,7 @@ public ProblemFinder(Services services, NamespaceSet nss) { "as a property file due to an error in the properties format", e); } - } else if (obl instanceof KeYParser.TableContext tbl) { + } else if (obl instanceof JavaKeYParser.TableContext tbl) { proofObligation = ParsingFacade.getConfiguration(tbl); } else { throw new BuildingException(ctx, @@ -106,7 +106,7 @@ public ProblemFinder(Services services, NamespaceSet nss) { } @Override - public @Nullable Sequent visitTermorseq(KeYParser.TermorseqContext ctx) { + public @Nullable Sequent visitTermorseq(JavaKeYParser.TermorseqContext ctx) { var obj = super.visitTermorseq(ctx); if (obj instanceof Sequent s) return s; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 47f7a06730e..179620bd733 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -16,7 +16,7 @@ import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import de.uka.ilkd.key.logic.sort.ProgramSVSort; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.nparser.varexp.ArgumentType; import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommand; import de.uka.ilkd.key.nparser.varexp.TacletBuilderManipulators; @@ -86,7 +86,7 @@ public TacletPBuilder(Services services, NamespaceSet namespaces, } @Override - public Object visitDecls(KeYParser.DeclsContext ctx) { + public Object visitDecls(JavaKeYParser.DeclsContext ctx) { mapOf(ctx.schema_var_decls()); mapOf(ctx.rulesOrAxioms()); mapOf(ctx.datatype_decls()); @@ -94,7 +94,7 @@ public Object visitDecls(KeYParser.DeclsContext ctx) { } @Override - public Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) { + public Object visitRulesOrAxioms(JavaKeYParser.RulesOrAxiomsContext ctx) { enableJavaSchemaMode(); if (ctx.RULES() != null) { axiomMode = false; @@ -111,7 +111,7 @@ public Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) { } @Override - public Object visitOne_schema_modal_op_decl(KeYParser.One_schema_modal_op_declContext ctx) { + public Object visitOne_schema_modal_op_decl(JavaKeYParser.One_schema_modal_op_declContext ctx) { ImmutableSet modalities = DefaultImmutableSet.nil(); Sort sort = accept(ctx.sort); if (sort != null && sort != JavaDLTheory.FORMULA) { @@ -130,7 +130,7 @@ public Object visitOne_schema_modal_op_decl(KeYParser.One_schema_modal_op_declCo } @Override - public TacletBuilder visitTriggers(KeYParser.TriggersContext ctx) { + public TacletBuilder visitTriggers(JavaKeYParser.TriggersContext ctx) { String id = (String) ctx.id.accept(this); JOperatorSV triggerVar = (JOperatorSV) schemaVariables().lookup(new Name(id)); if (triggerVar == null) { @@ -144,8 +144,8 @@ public TacletBuilder visitTriggers(KeYParser.TriggersContext ctx) { } @Override - public Taclet visitTaclet(KeYParser.TacletContext ctx) { - Sequent ifSeq = JavaDLSequentKit.getInstance().getEmptySequent(); + public Taclet visitTaclet(JavaKeYParser.TacletContext ctx) { + Sequent assumesSeq = JavaDLSequentKit.getInstance().getEmptySequent(); ImmutableSet tacletAnnotations = DefaultImmutableSet.nil(); if (ctx.LEMMA() != null) { tacletAnnotations = tacletAnnotations.add(TacletAnnotation.LEMMA); @@ -183,8 +183,8 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { setSchemaVariables(new Namespace<>(schemaVariables())); mapOf(ctx.one_schema_var_decl()); - if (ctx.ifSeq != null) { - ifSeq = accept(ctx.ifSeq); + if (ctx.assumesSeq != null) { + assumesSeq = accept(ctx.assumesSeq); } @Nullable @@ -211,7 +211,7 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { TacletBuilder b = createTacletBuilderFor(find, applicationRestriction, ctx); currentTBuilder.push(b); - b.setIfSequent(ifSeq); + b.setAssumesSequent(assumesSeq); b.setName(new Name(name)); accept(ctx.goalspecs()); mapOf(ctx.varexplist()); @@ -230,7 +230,7 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { } } - private void registerTaclet(KeYParser.Datatype_declContext ctx, TacletBuilder tb) { + private void registerTaclet(JavaKeYParser.Datatype_declContext ctx, TacletBuilder tb) { var taclet = tb.getTaclet(); taclet2Builder.put(taclet, peekTBuilder()); topLevelTaclets.add(taclet); @@ -250,7 +250,7 @@ private TacletBuilder peekTBuilder() { @Override - public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { + public Object visitDatatype_decl(JavaKeYParser.Datatype_declContext ctx) { var genParams = ctx.formal_sort_param_decls() == null ? null : visitFormal_sort_param_decls(ctx.formal_sort_param_decls()); final Sort sort; @@ -291,7 +291,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { } private TacletBuilder createDeconstructorTaclet( - KeYParser.Datatype_constructorContext constructor, String argName, int argIndex, + JavaKeYParser.Datatype_constructorContext constructor, String argName, int argIndex, Sort dtSort) { var tacletBuilder = new RewriteTacletBuilder<>(); tacletBuilder @@ -330,7 +330,7 @@ private TacletBuilder createDeconstructorTaclet( } private TacletBuilder createDeconstructorEQTaclet( - KeYParser.Datatype_constructorContext constructor, String argName, int argIndex, + JavaKeYParser.Datatype_constructorContext constructor, String argName, int argIndex, Sort dtSort) { var tacletBuilder = new RewriteTacletBuilder<>(); tacletBuilder.setName( @@ -362,7 +362,7 @@ private TacletBuilder createDeconstructorEQTaclet( var res = schemaVariables[argIndex]; tacletBuilder.setFind(tb.func(function, tb.var(x))); - tacletBuilder.setIfSequent(JavaDLSequentKit.createAnteSequent( + tacletBuilder.setAssumesSequent(JavaDLSequentKit.createAnteSequent( ImmutableSLList .singleton(new SequentFormula(tb.equals(tb.func(consFn, args), tb.var(x)))))); tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(tb.var(res))); @@ -394,7 +394,7 @@ private Sort getPossiblyParametricSort(String name, Sort sort) { } private TacletBuilder createInductionTaclet( - KeYParser.Datatype_declContext ctx, Sort sort) { + JavaKeYParser.Datatype_declContext ctx, Sort sort) { var tacletBuilder = new NoFindTacletBuilder(); var phi = declareSchemaVariable(ctx, "phi", JavaDLTheory.FORMULA, true, false, false, new SchemaVariableModifierSet.FormulaSV()); @@ -429,7 +429,7 @@ private TacletBuilder createInductionTaclet( return tacletBuilder; } - private GoalTemplAndVars createGoalDtConstructor(KeYParser.Datatype_constructorContext it, + private GoalTemplAndVars createGoalDtConstructor(JavaKeYParser.Datatype_constructorContext it, VariableSV qvar, JTerm var, Sort sort) { var constr = createQuantifiedFormula(it, qvar, var, sort); var goal = new TacletGoalTemplate( @@ -445,7 +445,7 @@ private record GoalTemplAndVars(TacletGoalTemplate tgt, } private TacletBuilder createAxiomTaclet( - KeYParser.Datatype_declContext ctx, Sort sort) { + JavaKeYParser.Datatype_declContext ctx, Sort sort) { var tacletBuilder = new NoFindTacletBuilder(); var phi = declareSchemaVariable(ctx, "phi", JavaDLTheory.FORMULA, true, false, false, new SchemaVariableModifierSet.FormulaSV()); @@ -480,7 +480,7 @@ private TacletBuilder createAxiomTaclet( return tacletBuilder; } - private TermAndVars createQuantifiedFormula(KeYParser.Datatype_constructorContext context, + private TermAndVars createQuantifiedFormula(JavaKeYParser.Datatype_constructorContext context, QuantifiableVariable qvX, JTerm phi, Sort dt) { var tb = services.getTermBuilder(); var fn = getPossiblyParametricFunction(context.name.getText(), dt); @@ -524,13 +524,13 @@ private record TermAndVars(JTerm term, @Nullable List vars } private RewriteTacletBuilder createConstructorSplit( - KeYParser.Datatype_declContext ctx, Sort sort) { + JavaKeYParser.Datatype_declContext ctx, Sort sort) { final var tb = services.getTermBuilder(); final String prefix = ctx.name.getText() + "_"; Map variables = new HashMap<>(); - for (KeYParser.Datatype_constructorContext context : ctx.datatype_constructor()) { + for (JavaKeYParser.Datatype_constructorContext context : ctx.datatype_constructor()) { for (int i = 0; i < context.argName.size(); i++) { var name = context.argName.get(i).getText(); var argSort = getPossiblyParametricSort( @@ -553,7 +553,7 @@ private RewriteTacletBuilder createConstructorSplit( false, false, false, new SchemaVariableModifierSet.TermSV()); b.setFind(tb.var(phi)); - for (KeYParser.Datatype_constructorContext context : ctx.datatype_constructor()) { + for (JavaKeYParser.Datatype_constructorContext context : ctx.datatype_constructor()) { var func = getPossiblyParametricFunction(context.name.getText(), sort); JTerm[] args = new JTerm[context.argName.size()]; for (int i = 0; i < args.length; i++) { @@ -569,7 +569,7 @@ private RewriteTacletBuilder createConstructorSplit( } @Override - public Object visitModifiers(KeYParser.ModifiersContext ctx) { + public Object visitModifiers(JavaKeYParser.ModifiersContext ctx) { TacletBuilder b = peekTBuilder(); List rs = accept(ctx.rs); if (!ctx.NONINTERACTIVE().isEmpty()) { @@ -593,15 +593,15 @@ public Object visitModifiers(KeYParser.ModifiersContext ctx) { } @Override - public Object visitVarexplist(KeYParser.VarexplistContext ctx) { + public Object visitVarexplist(JavaKeYParser.VarexplistContext ctx) { return mapOf(ctx.varexp()); } @Override - public Object visitVarexp(KeYParser.VarexpContext ctx) { + public Object visitVarexp(JavaKeYParser.VarexpContext ctx) { boolean negated = ctx.NOT_() != null; String name = ctx.varexpId().getText(); - List arguments = ctx.varexp_argument(); + List arguments = ctx.varexp_argument(); List suitableManipulators = TacletBuilderManipulators.getConditionBuildersFor(name); List parameters = @@ -624,7 +624,7 @@ public Object visitVarexp(KeYParser.VarexpContext ctx) { } private boolean applyManipulator(boolean negated, Object[] args, - TacletBuilderCommand manipulator, List arguments, + TacletBuilderCommand manipulator, List arguments, List parameters) { assert args.length == arguments.size(); ArgumentType[] types = manipulator.getArgumentTypes(); @@ -644,7 +644,7 @@ private boolean applyManipulator(boolean negated, Object[] args, } private Object evaluateVarcondArgument(ArgumentType expectedType, Object prevValue, - KeYParser.Varexp_argumentContext ctx) { + JavaKeYParser.Varexp_argumentContext ctx) { if (prevValue != null && expectedType.clazz.isAssignableFrom(prevValue.getClass())) { return prevValue; // previous value is of suitable type, we do not re-evaluate } @@ -702,7 +702,7 @@ private KeYJavaType getOrCreateJavaType(String sortId, ParserRuleContext ctx) { } - public Object buildTypeResolver(KeYParser.Varexp_argumentContext ctx) { + public Object buildTypeResolver(JavaKeYParser.Varexp_argumentContext ctx) { SchemaVariable y = accept(ctx.varId()); if (ctx.TYPEOF() != null) { return TypeResolver.createElementTypeResolver(y); @@ -725,12 +725,12 @@ public Object buildTypeResolver(KeYParser.Varexp_argumentContext ctx) { } @Override - public Object visitGoalspecs(KeYParser.GoalspecsContext ctx) { + public Object visitGoalspecs(JavaKeYParser.GoalspecsContext ctx) { return mapOf(ctx.goalspecwithoption()); } @Override - public Object visitGoalspecwithoption(KeYParser.GoalspecwithoptionContext ctx) { + public Object visitGoalspecwithoption(JavaKeYParser.GoalspecwithoptionContext ctx) { ChoiceExpr expr = accept(ctx.option_list()); goalChoice = expr == null ? ChoiceExpr.TRUE : expr; accept(ctx.goalspec()); @@ -738,7 +738,7 @@ public Object visitGoalspecwithoption(KeYParser.GoalspecwithoptionContext ctx) { } @Override - public Choice visitOption(KeYParser.OptionContext ctx) { + public Choice visitOption(JavaKeYParser.OptionContext ctx) { String choice = ctx.getText(); Choice c = choices().lookup(choice); if (c == null) { @@ -748,7 +748,7 @@ public Choice visitOption(KeYParser.OptionContext ctx) { } @Override - public ChoiceExpr visitOption_list(KeYParser.Option_listContext ctx) { + public ChoiceExpr visitOption_list(JavaKeYParser.Option_listContext ctx) { return ctx.option_expr().stream() .map(it -> (ChoiceExpr) accept(it)) .reduce(ChoiceExpr::and) @@ -756,17 +756,17 @@ public ChoiceExpr visitOption_list(KeYParser.Option_listContext ctx) { } @Override - public ChoiceExpr visitOption_expr_or(KeYParser.Option_expr_orContext ctx) { + public ChoiceExpr visitOption_expr_or(JavaKeYParser.Option_expr_orContext ctx) { return ChoiceExpr.or(accept(ctx.option_expr(0)), accept(ctx.option_expr(1))); } @Override - public ChoiceExpr visitOption_expr_paren(KeYParser.Option_expr_parenContext ctx) { + public ChoiceExpr visitOption_expr_paren(JavaKeYParser.Option_expr_parenContext ctx) { return accept(ctx.option_expr()); } @Override - public ChoiceExpr visitOption_expr_prop(KeYParser.Option_expr_propContext ctx) { + public ChoiceExpr visitOption_expr_prop(JavaKeYParser.Option_expr_propContext ctx) { String category = ctx.option().cat.getText(); String value = ctx.option().value.getText(); String choiceStr = category + ":" + value; @@ -783,17 +783,17 @@ public ChoiceExpr visitOption_expr_prop(KeYParser.Option_expr_propContext ctx) { } @Override - public ChoiceExpr visitOption_expr_not(KeYParser.Option_expr_notContext ctx) { + public ChoiceExpr visitOption_expr_not(JavaKeYParser.Option_expr_notContext ctx) { return ChoiceExpr.not(accept(ctx.option_expr())); } @Override - public ChoiceExpr visitOption_expr_and(KeYParser.Option_expr_andContext ctx) { + public ChoiceExpr visitOption_expr_and(JavaKeYParser.Option_expr_andContext ctx) { return ChoiceExpr.and(accept(ctx.option_expr(0)), accept(ctx.option_expr(1))); } @Override - public Object visitGoalspec(KeYParser.GoalspecContext ctx) { + public Object visitGoalspec(JavaKeYParser.GoalspecContext ctx) { var soc = this.goalChoice; String name = accept(ctx.string_value()); @@ -821,28 +821,28 @@ public Object visitGoalspec(KeYParser.GoalspecContext ctx) { } @Override - public Object visitReplacewith(KeYParser.ReplacewithContext ctx) { + public Object visitReplacewith(JavaKeYParser.ReplacewithContext ctx) { return accept(ctx.o); } @Override - public Object visitAdd(KeYParser.AddContext ctx) { + public Object visitAdd(JavaKeYParser.AddContext ctx) { return accept(ctx.s); } @Override - public Object visitAddrules(KeYParser.AddrulesContext ctx) { + public Object visitAddrules(JavaKeYParser.AddrulesContext ctx) { return accept(ctx.lor); } @Override - public ImmutableSet visitAddprogvar(KeYParser.AddprogvarContext ctx) { + public ImmutableSet visitAddprogvar(JavaKeYParser.AddprogvarContext ctx) { final Collection accept = accept(ctx.pvs); return Immutables.createSetFrom(Objects.requireNonNull(accept)); } @Override - public ImmutableList visitTacletlist(KeYParser.TacletlistContext ctx) { + public ImmutableList visitTacletlist(JavaKeYParser.TacletlistContext ctx) { List taclets = mapOf(ctx.taclet()); return ImmutableList.fromList(taclets); } @@ -921,7 +921,7 @@ private void addGoalTemplate(String id, Object rwObj, Sequent addSeq, } @Override - public SchemaVariable visitVarId(KeYParser.VarIdContext ctx) { + public SchemaVariable visitVarId(JavaKeYParser.VarIdContext ctx) { String id = ctx.id.getText(); return varId(ctx, id); } @@ -936,7 +936,7 @@ public SchemaVariable visitVarId(KeYParser.VarIdContext ctx) { } @Override - public Object visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx) { + public Object visitOne_schema_var_decl(JavaKeYParser.One_schema_var_declContext ctx) { boolean makeVariableSV = false; boolean makeSkolemTermSV = false; boolean makeTermLabelSV = false; @@ -1012,7 +1012,7 @@ public Object visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx) } @Override - public Object visitSchema_modifiers(KeYParser.Schema_modifiersContext ctx) { + public Object visitSchema_modifiers(JavaKeYParser.Schema_modifiersContext ctx) { SchemaVariableModifierSet mods = pop(); List ids = visitSimple_ident_comma_list(ctx.simple_ident_comma_list()); for (String id : ids) { @@ -1025,7 +1025,7 @@ public Object visitSchema_modifiers(KeYParser.Schema_modifiersContext ctx) { } @Override - public Object visitSchema_var_decls(KeYParser.Schema_var_declsContext ctx) { + public Object visitSchema_var_decls(JavaKeYParser.Schema_var_declsContext ctx) { return this.mapOf(ctx.one_schema_var_decl()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index 851cfa8320b..fb30b35d5a5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -12,7 +12,7 @@ import java.util.zip.ZipFile; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.nparser.KeYLexer; +import de.uka.ilkd.key.nparser.JavaKeYLexer; import de.uka.ilkd.key.nparser.KeyAst.ProofScript; import de.uka.ilkd.key.nparser.ProofScriptEntry; import de.uka.ilkd.key.proof.Node; @@ -190,12 +190,12 @@ public boolean hasErrors() { private static final Map missedErrors = new HashMap<>(); static { - mismatchErrors.put(new Pair<>(KeYLexer.SEMI, KeYLexer.COMMA), + mismatchErrors.put(new Pair<>(JavaKeYLexer.SEMI, JavaKeYLexer.COMMA), "there may be only one declaration per line"); - missedErrors.put(KeYLexer.RPAREN, "closing parenthesis"); - missedErrors.put(KeYLexer.RBRACE, "closing brace"); - missedErrors.put(KeYLexer.SEMI, "semicolon"); + missedErrors.put(JavaKeYLexer.RPAREN, "closing parenthesis"); + missedErrors.put(JavaKeYLexer.RBRACE, "closing brace"); + missedErrors.put(JavaKeYLexer.SEMI, "semicolon"); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java index 9359af7621b..aea5f993727 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java @@ -85,7 +85,7 @@ public AntecTaclet getAntecTaclet() { prefixBuilder.build(); AntecTaclet t = new AntecTaclet(name, - new TacletApplPart(ifseq, + new TacletApplPart(assumesSeq, applicationRestriction.combine(ApplicationRestriction.ANTECEDENT_POLARITY), varsNew, varsNotFreeIn, varsNewDependingOn, variableConditions), diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java index e2d1f630b39..2abf4d6c915 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java @@ -32,7 +32,7 @@ public NoFindTaclet getNoFindTaclet() { TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(this); prefixBuilder.build(); NoFindTaclet t = new NoFindTaclet(this.name, - new TacletApplPart(ifseq, + new TacletApplPart(assumesSeq, new ApplicationRestriction(ApplicationRestriction.IN_SEQUENT_STATE), varsNew, varsNotFreeIn, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java index bc5ab5239b2..e7d46cd2e89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java @@ -50,7 +50,7 @@ public T getRewriteTaclet() { TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(this); prefixBuilder.build(); RewriteTaclet t = new RewriteTaclet(name, - new TacletApplPart(ifseq, applicationRestriction, varsNew, varsNotFreeIn, + new TacletApplPart(assumesSeq, applicationRestriction, varsNew, varsNotFreeIn, varsNewDependingOn, variableConditions), goals, ruleSets, attrs, (JTerm) find, prefixBuilder.getPrefixMap(), diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java index 1954f7713b1..59568cd61b6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java @@ -69,7 +69,7 @@ public SuccTaclet getSuccTaclet() { final TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(this); prefixBuilder.build(); SuccTaclet t = new SuccTaclet(name, - new TacletApplPart(ifseq, + new TacletApplPart(assumesSeq, applicationRestriction.combine(ApplicationRestriction.SUCCEDENT_POLARITY), varsNew, varsNotFreeIn, varsNewDependingOn, variableConditions), diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java index bcfd38f2692..45ecdcb0c42 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java @@ -45,7 +45,7 @@ public abstract class TacletBuilder { protected Taclet taclet; protected Name name = NONAME; - protected Sequent ifseq = JavaDLSequentKit.getInstance().getEmptySequent(); + protected Sequent assumesSeq = JavaDLSequentKit.getInstance().getEmptySequent(); protected ImmutableList varsNew = ImmutableSLList.nil(); protected ImmutableList varsNotFreeIn = ImmutableSLList.nil(); protected ImmutableList varsNewDependingOn = ImmutableSLList.nil(); @@ -133,11 +133,11 @@ public void setDisplayName(@NonNull String s) { } /** - * sets the ifseq of the Taclet to be built + * sets the assumesSeq of the Taclet to be built */ - public void setIfSequent(Sequent seq) { + public void setAssumesSequent(Sequent seq) { checkContainsFreeVarSV(seq, getName(), "sequent"); - this.ifseq = seq; + this.assumesSeq = seq; } /** @@ -278,7 +278,7 @@ public void setRuleSets(ImmutableList rs) { } public Sequent ifSequent() { - return ifseq; + return assumesSeq; } public ImmutableList goalTemplates() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index 077d8ec8aaa..f5e93f4219d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java @@ -321,7 +321,7 @@ public ImmutableSet generateFunctionalRepresentsTaclets(Name name, * tacletBuilder.addTacletGoalTemplate (tgc); } */ if (ifSeq != null) { - tacletBuilder.setIfSequent(ifSeq); + tacletBuilder.setAssumesSequent(ifSeq); } tacletBuilder.setName(name); tacletBuilder.addRuleSet(new RuleSet(new Name("classAxiom"))); @@ -728,14 +728,14 @@ public ImmutableSet generatePartialInvTaclet(Name name, List hea final var succ = ImmutableSLList.singleton(eqNullSF); final Sequent ifSeq = JavaDLSequentKit.createSequent(antec, succ); - tacletBuilder.setIfSequent(ifSeq); + tacletBuilder.setAssumesSequent(ifSeq); } else if (!isStatic) { // \assumes( ==> self = null ) final JTerm selfNull = TB.equals(TB.var(selfSV), TB.NULL()); final SequentFormula selfNullSF = new SequentFormula(selfNull); final Sequent ifSeq = JavaDLSequentKit.createSuccSequent(ImmutableSLList.singleton(selfNullSF)); - tacletBuilder.setIfSequent(ifSeq); + tacletBuilder.setAssumesSequent(ifSeq); } result = result.add(tacletBuilder.getTaclet()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java index ad91a17dca5..068969558dd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java @@ -14,7 +14,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.NamespaceSet; -import de.uka.ilkd.key.nparser.KeYParser.ProofScriptExpressionContext; +import de.uka.ilkd.key.nparser.JavaKeYParser.ProofScriptExpressionContext; import de.uka.ilkd.key.nparser.KeyIO; import de.uka.ilkd.key.parser.ParserException; import de.uka.ilkd.key.pp.AbbrevMap; diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExprEvaluator.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExprEvaluator.java index 4862f59dcad..11a7f2a11d8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExprEvaluator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExprEvaluator.java @@ -5,9 +5,9 @@ import java.net.URI; -import de.uka.ilkd.key.nparser.KeYParser; -import de.uka.ilkd.key.nparser.KeYParser.*; -import de.uka.ilkd.key.nparser.KeYParserBaseVisitor; +import de.uka.ilkd.key.nparser.JavaKeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser.*; +import de.uka.ilkd.key.nparser.JavaKeYParserBaseVisitor; import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.nparser.builder.ExpressionBuilder; @@ -30,8 +30,8 @@ /// /// @author Alexander Weigl /// @version 1 (18.01.25) -/// @see de.uka.ilkd.key.nparser.KeYParser.ProofScriptExpressionContext -class ExprEvaluator extends KeYParserBaseVisitor { +/// @see de.uka.ilkd.key.nparser.JavaKeYParser.ProofScriptExpressionContext +class ExprEvaluator extends JavaKeYParserBaseVisitor { private static final Logger LOGGER = LoggerFactory.getLogger(ExprEvaluator.class); private final EngineState state; @@ -51,7 +51,7 @@ public Object visitBoolean_literal(Boolean_literalContext ctx) { } @Override - public Object visitChar_literal(KeYParser.Char_literalContext ctx) { + public Object visitChar_literal(JavaKeYParser.Char_literalContext ctx) { return ctx.getText().charAt(1); // skip "'" } @@ -61,7 +61,7 @@ public Object visitInteger(IntegerContext ctx) { } @Override - public Object visitFloatLiteral(KeYParser.FloatLiteralContext ctx) { + public Object visitFloatLiteral(JavaKeYParser.FloatLiteralContext ctx) { return Float.parseFloat(ctx.getText()); } @@ -94,7 +94,7 @@ public Object visitSimple_ident(Simple_identContext ctx) { } @Override - public Object visitTerm(KeYParser.TermContext ctx) { + public Object visitTerm(JavaKeYParser.TermContext ctx) { return evaluateExpression(ctx); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/LetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/LetCommand.java index 14a4aa1cfe9..1384a7931e6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/LetCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/LetCommand.java @@ -8,7 +8,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.pp.AbbrevMap; import de.uka.ilkd.key.scripts.meta.ProofScriptArgument; @@ -64,7 +64,7 @@ public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst arg throw new ScriptException(key + " is already fixed in this script"); } try { - final var termCtx = (KeYParser.ProofScriptExpressionContext) entry.getValue(); + final var termCtx = (JavaKeYParser.ProofScriptExpressionContext) entry.getValue(); final var value = termCtx.accept(stateMap.getEvaluator()); final var term = stateMap.getValueInjector().convert(value, JTerm.class); abbrMap.put(term, key, true); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java index 4212e60ec03..f0968e21082 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java @@ -13,7 +13,7 @@ import java.util.stream.Collectors; import de.uka.ilkd.key.control.AbstractUserInterfaceControl; -import de.uka.ilkd.key.nparser.KeYParser; +import de.uka.ilkd.key.nparser.JavaKeYParser; import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.parser.Location; @@ -189,7 +189,7 @@ public void execute(AbstractUserInterfaceControl uiControl, List getTaclets(ImmutableSet schemaVariables = new Namespace<>(); Namespace programVariables = new Namespace<>(); @@ -91,9 +91,9 @@ private void findModalities(KeYParser.FileContext ctx) { TacletPBuilder tpb = new TacletPBuilder(services, nss); tpb.setSchemaVariables(schemaVariables); - class FindMods extends KeYParserBaseVisitor { + class FindMods extends JavaKeYParserBaseVisitor { @Override - public Void visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx) { + public Void visitOne_schema_var_decl(JavaKeYParser.One_schema_var_declContext ctx) { if (ctx.PROGRAM() != null) try { ctx.accept(tpb); @@ -103,7 +103,7 @@ public Void visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx) { } @Override - public Void visitModality_term(KeYParser.Modality_termContext ctx) { + public Void visitModality_term(JavaKeYParser.Modality_termContext ctx) { final var e = ExpressionBuilder.trimJavaBlock(ctx.MODALITY().getText()); final var cleaned = e.trim().replace('\n', ' ') .replaceAll(" {2,}", " "); diff --git a/key.core/src/test/java/de/uka/ilkd/key/parser/TestTacletParser.java b/key.core/src/test/java/de/uka/ilkd/key/parser/TestTacletParser.java index e4d4113b97e..05ec20f6923 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/parser/TestTacletParser.java +++ b/key.core/src/test/java/de/uka/ilkd/key/parser/TestTacletParser.java @@ -187,7 +187,7 @@ public void testClose() { // if (b=>) find(=>b) SuccTacletBuilder builder = new SuccTacletBuilder(); builder.setFind(parseFma("b")); - builder.setIfSequent(sequent("b", null)); + builder.setAssumesSequent(sequent("b", null)); builder.setName(new Name("close_goal")); Taclet close = builder.getSuccTaclet(); String closeString = "close_goal{\\assumes (b==>) \\find(==>b) \\closegoal}"; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/tacletbuilder/TestTacletBuild.java b/key.core/src/test/java/de/uka/ilkd/key/rule/tacletbuilder/TestTacletBuild.java index ba5068422a3..1a4e425f423 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/tacletbuilder/TestTacletBuild.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/tacletbuilder/TestTacletBuild.java @@ -89,7 +89,7 @@ public void testUniquenessOfIfAndFindVarSVsInIfAndFind() { JavaDLSequentKit.createSuccSequent(ImmutableSLList.singleton(new SequentFormula(t1))); JTerm t2 = tb.ex((QuantifiableVariable) u, A); SuccTacletBuilder sb = new SuccTacletBuilder(); - sb.setIfSequent(seq); + sb.setAssumesSequent(seq); sb.setFind(t2); try { sb.getTaclet(); @@ -112,7 +112,7 @@ public void testUniquenessOfIfAndFindVarSVBothInIf() { .createSuccSequent(ImmutableSLList.singleton(new SequentFormula(t2)) .prepend(new SequentFormula(t1))); SuccTacletBuilder sb = new SuccTacletBuilder(); - sb.setIfSequent(seq); + sb.setAssumesSequent(seq); sb.setFind(A); try { sb.getTaclet(); diff --git a/key.ncore/build.gradle b/key.ncore/build.gradle index 65139ef4138..fd7b213713a 100644 --- a/key.ncore/build.gradle +++ b/key.ncore/build.gradle @@ -3,13 +3,41 @@ plugins { description = "Generic data strutures for terms and formulas without dependencies to a specific target programming language" -configurations { } +configurations { antlr4 } + +repositories { + mavenCentral() +} dependencies { api project(':key.util') - implementation 'org.jspecify:jspecify:1.0.0' + implementation('org.jspecify:jspecify:1.0.0') + antlr4 "org.antlr:antlr4:4.13.2" + api "org.antlr:antlr4-runtime:4.13.2" } +def antlr4OutputKey = String.valueOf(projectDir) + '/build/generated-src/antlr/main/org/key_project/parser' + +tasks.register('runAntlr4Key', JavaExec) { + //see incremental task api, prevents rerun if nothing has changed. + inputs.files "src/main/antlr/KeYLexer.g4", "src/main/antlr/KeYParser.g4" + outputs.dir antlr4OutputKey + classpath = configurations.antlr4 + mainClass.set("org.antlr.v4.Tool") + args = ["-visitor", + "-Xexact-output-dir", "-o", antlr4OutputKey, + //"-package", "org.key_project.rusty.parser", + "src/main/antlr/KeYLexer.g4", + "src/main/antlr/KeYParser.g4"] + doFirst { + file(antlr4OutputKey).mkdirs() + println("create $antlr4OutputKey") + } +} +compileJava.dependsOn runAntlr4Key + +sourceSets.main.java.srcDirs(String.valueOf(projectDir) + '/build/generated-src/antlr/main/') + tasks.withType(Test).configureEach { enableAssertions = true } diff --git a/key.ncore/src/main/antlr/KeYCommonParser.g4 b/key.ncore/src/main/antlr/KeYCommonParser.g4 index 944be53539f..e6a366fb1fd 100644 --- a/key.ncore/src/main/antlr/KeYCommonParser.g4 +++ b/key.ncore/src/main/antlr/KeYCommonParser.g4 @@ -1,6 +1,5 @@ parser grammar KeYCommonParser; - options { tokenVocab = KeYLexer; } simple_ident : id = IDENT @@ -11,8 +10,16 @@ simple_ident_comma_list ; sortId - : id = simple_ident_dots (EMPTYBRACKETS)* - ; +: + id=simple_ident_dots formal_sort_args? (EMPTYBRACKETS)* +; + +formal_sort_args +: + OPENTYPEPARAMS + sortId (COMMA sortId)* + CLOSETYPEPARAMS +; simple_ident_dots : simple_ident (DOT simple_ident)* @@ -23,7 +30,7 @@ simple_ident_dots_comma_list ; funcpred_name - : (sortId DOUBLECOLON)? (name = simple_ident_dots | num = INT_LITERAL) + : (simple_ident_dots DOUBLECOLON)? (name = simple_ident_dots | num = INT_LITERAL) ; varId diff --git a/key.ncore/src/main/antlr/KeYGlobalDeclParser.g4 b/key.ncore/src/main/antlr/KeYGlobalDeclParser.g4 index 5d6a5511533..4d518c7e4dd 100644 --- a/key.ncore/src/main/antlr/KeYGlobalDeclParser.g4 +++ b/key.ncore/src/main/antlr/KeYGlobalDeclParser.g4 @@ -5,8 +5,7 @@ import KeYTacletParser; options { tokenVocab = KeYLexer; } decls : (string = programSource // for problems - | one_include_statement | options_choice | option_decls | sort_decls | prog_var_decls | schema_var_decls | pred_decls | func_decls | transform_decls | datatype_decls | ruleset_decls | contracts // for problems - | invariants // for problems + | one_include_statement | options_choice | option_decls | sort_decls | prog_var_decls | schema_var_decls | pred_decls | func_decls | transform_decls | datatype_decls | ruleset_decls | rulesOrAxioms // for problems )* ; @@ -44,8 +43,19 @@ schema_var_decls : SCHEMAVARIABLES LBRACE (one_schema_var_decl SEMI)* RBRACE ; +formal_sort_param_decls +: OPENTYPEPARAMS + formal_sort_param_decl (COMMA formal_sort_param_decl)* + CLOSETYPEPARAMS +; + +formal_sort_param_decl +: + (PLUS | MINUS)? simple_ident +; + pred_decl - : doc = DOC_COMMENT? pred_name = funcpred_name (whereToBind = where_to_bind)? argSorts = arg_sorts SEMI + : doc = DOC_COMMENT? pred_name = funcpred_name formal_sort_param_decls? (whereToBind = where_to_bind)? argSorts = arg_sorts SEMI ; pred_decls @@ -53,7 +63,7 @@ pred_decls ; func_decl - : doc = DOC_COMMENT? (UNIQUE)? retSort = sortId func_name = funcpred_name whereToBind = where_to_bind? argSorts = arg_sorts SEMI + : doc = DOC_COMMENT? (UNIQUE)? retSort = sortId func_name = funcpred_name formal_sort_param_decls? whereToBind = where_to_bind? argSorts = arg_sorts SEMI ; /** @@ -69,7 +79,7 @@ datatype_decl // weigl: all datatypes are free! // FREE? - name = simple_ident EQUALS datatype_constructor (OR datatype_constructor)* SEMI + name = simple_ident formal_sort_param_decls? EQUALS datatype_constructor (OR datatype_constructor)* SEMI ; datatype_constructor @@ -80,22 +90,6 @@ func_decls : FUNCTIONS LBRACE (func_decl)* RBRACE ; -contracts - : CONTRACTS LBRACE (one_contract)* RBRACE - ; - -invariants - : INVARIANTS LPAREN selfVar = one_bound_variable RPAREN LBRACE (one_invariant)* RBRACE - ; - -one_contract - : contractName = simple_ident LBRACE (prog_var_decls)? fma = term MODIFIES modifiesClause = term RBRACE SEMI - ; - -one_invariant - : invName = simple_ident LBRACE fma = term (DISPLAYNAME displayName = string_value)? RBRACE SEMI - ; - prog_var_decls : PROGRAMVARIABLES LBRACE (kjt = typemapping var_names = simple_ident_comma_list SEMI)* RBRACE ; @@ -121,8 +115,23 @@ sort_decls ; one_sort_decl - : doc = DOC_COMMENT? (GENERIC sortIds = simple_ident_dots_comma_list (ONEOF sortOneOf = oneof_sorts)? (EXTENDS sortExt = extends_sorts)? SEMI | PROXY sortIds = simple_ident_dots_comma_list (EXTENDS sortExt = extends_sorts)? SEMI | ABSTRACT? sortIds = simple_ident_dots_comma_list (EXTENDS sortExt = extends_sorts)? SEMI) - ; +: + doc=DOC_COMMENT? + ( + GENERIC sortIds=simple_ident_dots_comma_list + (ONEOF sortOneOf = oneof_sorts)? + (EXTENDS sortExt = extends_sorts)? SEMI + | PROXY sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI + | ABSTRACT? (sortIds=simple_ident_dots_comma_list | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)? SEMI + | ALIAS simple_ident_dots EQUALS sortId SEMI + ) +; + +parametric_sort_decl +: + simple_ident_dots + formal_sort_param_decls +; extends_sorts : sortId (COMMA sortId)* diff --git a/key.ncore/src/main/antlr/KeYLexer.g4 b/key.ncore/src/main/antlr/KeYLexer.g4 index 82999d2f805..25816a3b351 100644 --- a/key.ncore/src/main/antlr/KeYLexer.g4 +++ b/key.ncore/src/main/antlr/KeYLexer.g4 @@ -18,23 +18,20 @@ lexer grammar KeYLexer; static { modNames.put("\\<","diamond"); modNames.put("\\diamond","diamond"); - modNames.put("\\diamond_transaction","diamond_transaction"); modNames.put("\\[","box"); modNames.put("\\box","box"); + + modPairs.put("\\modality","\\endmodality"); + modPairs.put("\\diamond","\\endmodality"); + modPairs.put("\\box","\\endmodality"); + + modNames.put("\\diamond_transaction","diamond_transaction"); modNames.put("\\box_transaction","box_transaction"); modNames.put("\\[[","throughout"); modNames.put("\\throughout","throughout"); modNames.put("\\throughout_transaction","throughout_transaction"); - modPairs.put("\\<","\\>"); - modPairs.put("\\[","\\]"); - - //modPairs.put("\\[[","\\]]"); - - modPairs.put("\\modality","\\endmodality"); - modPairs.put("\\diamond","\\endmodality"); modPairs.put("\\diamond_transaction","\\endmodality"); - modPairs.put("\\box","\\endmodality"); modPairs.put("\\box_transaction","\\endmodality"); modPairs.put("\\throughout","\\endmodality"); modPairs.put("\\throughout_transaction","\\endmodality"); @@ -44,7 +41,7 @@ lexer grammar KeYLexer; @Override public void emit(Token token) { int MAX_K = 10; - if (token.getType() == INT_LITERAL) {//rewrite INT_LITERALs to identifier when preceeded by an '(' + if (token.getType() == INT_LITERAL) {//rewrite INT_LITERALs to identifier when preceded by an '(' for (int k = 1; k <= MAX_K; k++) { int codePoint = _input.LA(k); if (Character.isWhitespace(codePoint)) continue; @@ -94,8 +91,10 @@ ONEOF ABSTRACT : '\\abstract' ; +ALIAS: '\\alias'; + // Keywords used in schema variable declarations - + SCHEMAVARIABLES : '\\schemaVariables' ; @@ -139,20 +138,11 @@ SKOLEMTERM SKOLEMFORMULA : '\\skolemFormula' ; - -TERMLABEL - : '\\termlabel' - ; - // Keywords used in program variable declarations PROGRAMVARIABLES : '\\programVariables' ; -SAME_OBSERVER - : '\\sameObserver' - ; - VARCOND : '\\varcond' ; @@ -161,22 +151,10 @@ APPLY_UPDATE_ON_RIGID : '\\applyUpdateOnRigid' ; -DEPENDINGON - : '\\dependingOn' - ; - -DISJOINTMODULONULL - : '\\disjointModuloNull' - ; - DROP_EFFECTLESS_ELEMENTARIES : '\\dropEffectlessElementaries' ; -DROP_EFFECTLESS_STORES - : '\\dropEffectlessStores' - ; - SIMPLIFY_IF_THEN_ELSE_UPDATE : '\\simplifyIfThenElseUpdate' ; @@ -189,10 +167,6 @@ ISINDUCTVAR : '\\isInductVar' ; -ISOBSERVER - : '\\isObserver' - ; - DIFFERENT : '\\different' ; @@ -213,10 +187,6 @@ NEW_TYPE_OF : '\\newTypeOf' ; -NEW_DEPENDING_ON - : '\\newDependingOn' - ; - HAS_ELEMENTARY_SORT : '\\hasElementarySort' ; @@ -226,10 +196,6 @@ NOT_ : '\\not' ; -NOTFREEIN - : '\\notFreeIn' - ; - SAME : '\\same' ; @@ -631,6 +597,9 @@ GREATEREQUAL | '\u2265' ; +OPENTYPEPARAMS : '<' '['; +CLOSETYPEPARAMS : ']' '>'; + WS : [ \t\n\r\u00a0]+ -> channel (HIDDEN) ; //U+00A0 = non breakable whitespace @@ -760,10 +729,6 @@ MODALITYB : '\\[' -> more , pushMode (modBox) ; -MODALITYBB - : '\\[[' -> more , pushMode (modBoxBox) - ; - MODAILITYGENERIC1 : '\\box' -> more , pushMode (modGeneric) ; @@ -776,11 +741,8 @@ MODAILITYGENERIC4 : '\\modality' -> more , pushMode (modGeneric) ; -MODAILITYGENERIC6 - : '\\throughout' -> more , pushMode (modGeneric) - ; - //BACKSLASH: '\\'; - +ERROR_UKNOWN_ESCAPE: '\\' IDENT; + ERROR_CHAR : . ; diff --git a/key.ncore/src/main/antlr/KeYParser.g4 b/key.ncore/src/main/antlr/KeYParser.g4 index b0b906910c0..6d738508b8d 100644 --- a/key.ncore/src/main/antlr/KeYParser.g4 +++ b/key.ncore/src/main/antlr/KeYParser.g4 @@ -15,11 +15,7 @@ file ; problem - : (PROBLEM LBRACE (t = termorseq) RBRACE | CHOOSECONTRACT (chooseContract = string_value SEMI)? | PROOFOBLIGATION (proofObligation = cvalue)? SEMI?) proofScript? - ; - -arrayopid - : EMPTYBRACKETS LPAREN componentType = typemapping RPAREN + : (PROBLEM LBRACE (t = termorseq) RBRACE | CHOOSECONTRACT (chooseContract = string_value SEMI)? | PROOFOBLIGATION (proofObligation = cvalue)? SEMI?) proofScriptEntry? ; /** @@ -88,14 +84,36 @@ term preferences : KEYSETTINGS (LBRACE s = string_value? RBRACE | c = cvalue) // LBRACE, RBRACE included in cvalue#table - ; -proofScript - : PROOFSCRIPT ps = STRING_LITERAL - ; - // PROOF - +proofScriptEntry +: + PROOFSCRIPT + ( STRING_LITERAL SEMI? + | LBRACE proofScript RBRACE + ) +; + +proofScriptEOF: proofScript EOF; +proofScript: proofScriptCommand*; +proofScriptCommand: cmd=IDENT proofScriptParameters SEMI; + +proofScriptParameters: proofScriptParameter*; +proofScriptParameter : ((pname=proofScriptParameterName (COLON|EQUALS))? expr=proofScriptExpression); +proofScriptParameterName: AT? IDENT; // someone thought, that the let-command parameters should have a leading "@" +proofScriptExpression: + boolean_literal + | integer + | floatnum + | string_literal + | LPAREN (term | seq) RPAREN + | simple_ident + | abbreviation + | literals + | proofScriptCodeBlock + ; +proofScriptCodeBlock: LBRACE proofScript RBRACE; + proof : PROOF EOF ; diff --git a/key.ncore/src/main/antlr/KeYSequentParser.g4 b/key.ncore/src/main/antlr/KeYSequentParser.g4 index 1b790fca539..c105fc7e9a4 100644 --- a/key.ncore/src/main/antlr/KeYSequentParser.g4 +++ b/key.ncore/src/main/antlr/KeYSequentParser.g4 @@ -19,7 +19,7 @@ termorseq semisequent : /* empty */ - + | head = term (COMMA ss = semisequent)? ; diff --git a/key.ncore/src/main/antlr/KeYTacletParser.g4 b/key.ncore/src/main/antlr/KeYTacletParser.g4 index d149c1f0b3c..4bcd24275f4 100644 --- a/key.ncore/src/main/antlr/KeYTacletParser.g4 +++ b/key.ncore/src/main/antlr/KeYTacletParser.g4 @@ -4,7 +4,7 @@ import KeYSequentParser; options { tokenVocab = KeYLexer; } taclet - : doc = DOC_COMMENT? (LEMMA)? name = IDENT (choices_ = option_list)? LBRACE (form = term | (SCHEMAVAR one_schema_var_decl SEMI)* (ASSUMES LPAREN ifSeq = seq RPAREN)? (FIND LPAREN find = termorseq RPAREN (SAMEUPDATELEVEL | INSEQUENTSTATE | ANTECEDENTPOLARITY | SUCCEDENTPOLARITY)*)? (VARCOND LPAREN varexplist RPAREN)* goalspecs modifiers) RBRACE + : doc = DOC_COMMENT? (LEMMA)? name = IDENT (choices_ = option_list)? LBRACE (form = term | (SCHEMAVAR one_schema_var_decl SEMI)* (ASSUMES LPAREN assumesSeq = seq RPAREN)? (FIND LPAREN find = termorseq RPAREN (SAMEUPDATELEVEL | INSEQUENTSTATE | ANTECEDENTPOLARITY | SUCCEDENTPOLARITY)*)? (VARCOND LPAREN varexplist RPAREN)* goalspecs modifiers) RBRACE ; option_list @@ -24,7 +24,7 @@ option_expr ; goalspec - : (name = string_value COLON)? (rwObj = replacewith addSeq = add? addRList = addrules? addpv = addprogvar? | addSeq = add (addRList = addrules)? | addRList = addrules) + : (name = string_value (LBRACKET tag=simple_ident RBRACKET)? COLON)? (rwObj = replacewith addSeq = add? addRList = addrules? addpv = addprogvar? | addSeq = add (addRList = addrules)? | addRList = addrules) ; replacewith @@ -63,10 +63,6 @@ metaId : id = simple_ident ; -metaTerm - : vf = metaId (LPAREN t += term (COMMA t += term)* RPAREN)? - ; - varexplist : varexp (COMMA varexp)* ; @@ -78,55 +74,17 @@ varexp varexpId : // weigl, 2021-03-12: This will be later just an arbitrary identifier. Only for backwards compatibility. APPLY_UPDATE_ON_RIGID - | SAME_OBSERVER | DROP_EFFECTLESS_ELEMENTARIES - | DROP_EFFECTLESS_STORES - | DIFFERENTFIELDS | SIMPLIFY_IF_THEN_ELSE_UPDATE - | CONTAINS_ASSIGNMENT - | ISENUMTYPE - | ISTHISREFERENCE - | STATICMETHODREFERENCE - | ISREFERENCEARRAY - | ISARRAY - | ISARRAYLENGTH - | IS_ABSTRACT_OR_INTERFACE - | ENUM_CONST - | FINAL - | STATIC - | ISLOCALVARIABLE - | ISOBSERVER | DIFFERENT - | METADISJOINT | EQUAL_UNIQUE - | FREELABELIN - | ISCONSTANT - | HASLABEL - | ISSTATICFIELD - | ISMODELFIELD - | HASSUBFORMULAS - | FIELDTYPE | NEW | NEW_TYPE_OF - | NEW_DEPENDING_ON | HAS_ELEMENTARY_SORT | SAME | ISSUBTYPE | STRICT ISSUBTYPE - | DISJOINTMODULONULL - | NOTFREEIN | HASSORT - | NEWLABEL - | ISREFERENCE - | MAXEXPANDMETHOD - | STORE_TERM_IN - | STORE_STMT_IN - | HAS_INVARIANT - | GET_INVARIANT - | GET_FREE_INVARIANT - | GET_VARIANT - | IS_LABELED - | ISINSTRICTFP ; varexp_argument @@ -135,8 +93,6 @@ varexp_argument // suggestion add an explicit keyword to request the sort by name or manually resolve later in builder TYPEOF LPAREN y = varId RPAREN - | CONTAINERTYPE LPAREN y = varId RPAREN - | DEPENDINGON LPAREN y = varId RPAREN | term ; @@ -163,7 +119,6 @@ one_schema_var_decl : MODALOPERATOR one_schema_modal_op_decl | PROGRAM (schema_modifiers)? id = simple_ident (LBRACKET nameString = simple_ident EQUALS parameter = simple_ident_dots RBRACKET)? ids = simple_ident_comma_list | FORMULA (schema_modifiers)? ids = simple_ident_comma_list - | TERMLABEL (schema_modifiers)? ids = simple_ident_comma_list | UPDATE (schema_modifiers)? ids = simple_ident_comma_list | SKOLEMFORMULA (schema_modifiers)? ids = simple_ident_comma_list | (TERM | (VARIABLES | VARIABLE) | SKOLEMTERM) (schema_modifiers)? s = sortId ids = simple_ident_comma_list diff --git a/key.ncore/src/main/antlr/KeYTermParser.g4 b/key.ncore/src/main/antlr/KeYTermParser.g4 index fec891d611a..a32a1b495a8 100644 --- a/key.ncore/src/main/antlr/KeYTermParser.g4 +++ b/key.ncore/src/main/antlr/KeYTermParser.g4 @@ -7,8 +7,6 @@ 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)* ; @@ -83,29 +81,13 @@ unary_minus_term atom_prefix : update_term | substitution_term - | locset_term | cast_term | unary_minus_term | bracket_term ; bracket_term - : primitive_labeled_term (bracket_suffix_heap)* attribute* - ; - -bracket_suffix_heap - : brace_suffix (AT heap = bracket_term)? - ; - -brace_suffix - : LBRACKET target = term ASSIGN val = term RBRACKET # bracket_access_heap_update - | LBRACKET id = simple_ident args = argument_list RBRACKET # bracket_access_heap_term - | LBRACKET STAR RBRACKET # bracket_access_star - | LBRACKET indexTerm = term (DOTRANGE rangeTo = term)? RBRACKET # bracket_access_indexrange - ; - -primitive_labeled_term - : primitive_term (LGUILLEMETS labels = label RGUILLEMETS)? + : primitive_term attribute* ; termParen @@ -136,7 +118,6 @@ boolean_literal literals : boolean_literal - | char_literal | integer | floatnum | string_literal @@ -164,10 +145,6 @@ argument_list : LPAREN (term (COMMA term)*)? RPAREN ; -integer_with_minux - : MINUS? integer - ; - integer : (INT_LITERAL | HEX_LITERAL | BIN_LITERAL) ; @@ -179,14 +156,6 @@ floatnum | (MINUS)? REAL_LITERAL # realLiteral ; -char_literal - : CHAR_LITERAL - ; - -location_term - : LPAREN obj = equivalence_term COMMA field = equivalence_term RPAREN - ; - ifThenElseTerm : IF LPAREN condF = term RPAREN THEN LPAREN thenT = term RPAREN ELSE LPAREN elseT = term RPAREN ; @@ -195,16 +164,12 @@ ifExThenElseTerm : IFEX exVars = bound_variables LPAREN condF = term RPAREN THEN LPAREN thenT = term RPAREN ELSE LPAREN elseT = term RPAREN ; -locset_term - : LBRACE (l = location_term (COMMA l = location_term)*)? RBRACE - ; - /** * Access: a.b.c@f, T.staticQ() */ accessterm : // OLD - (sortId DOUBLECOLON)? firstName = simple_ident + (sortId DOUBLECOLON)? firstName = simple_ident formal_sort_args? /*Faster version simple_ident_dots ( EMPTYBRACKETS* @@ -217,19 +182,10 @@ locset_term attribute : DOT STAR # attribute_star - | DOT id = simple_ident call? (AT heap = bracket_term)? # attribute_simple - | DOT LPAREN sort = sortId DOUBLECOLON id = simple_ident RPAREN call? (AT heap = bracket_term)? # attribute_complex + | DOT id = simple_ident call? # attribute_simple + | DOT LPAREN sort = sortId DOUBLECOLON id = simple_ident RPAREN call? # attribute_complex ; call : ((LBRACE boundVars = bound_variables RBRACE)? argument_list) ; - -label - : l = single_label (COMMA l = single_label)* - ; - -single_label - : (name = IDENT | star = STAR) (LPAREN (string_value (COMMA string_value)*)? RPAREN)? - ; - diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java index 3240e1d3bdd..52f7e8ed14c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java @@ -11,15 +11,15 @@ import javax.swing.text.StyleConstants; import de.uka.ilkd.key.gui.colors.ColorSettings; -import de.uka.ilkd.key.nparser.KeYLexer; +import de.uka.ilkd.key.nparser.JavaKeYLexer; import org.antlr.v4.runtime.CharStreams; -import static de.uka.ilkd.key.nparser.KeYLexer.*; +import static de.uka.ilkd.key.nparser.JavaKeYLexer.*; /** * This is a lexer class used by a {@link SourceHighlightDocument} to highlight KeY code. - * It uses the ANTLR lexer {@link KeYLexer} to tokenize the text. + * It uses the ANTLR lexer {@link JavaKeYLexer} to tokenize the text. * * Secondary keywords are highlighted in a different color. These are schema variables kinds, * variable conditions etc. @@ -143,7 +143,7 @@ private SimpleAttributeSet getAttributes(int type) { @Override public List applyTo(String text) { - KeYLexer keYLexer = new KeYLexer(CharStreams.fromString(text)); + JavaKeYLexer keYLexer = new JavaKeYLexer(CharStreams.fromString(text)); List result = new ArrayList<>(); var t = keYLexer.nextToken(); while (t.getType() != -1) {