From 9b7d7260a90139b76ce7354ade1d9dda300b5ab4 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Thu, 22 Feb 2024 00:53:13 +0100 Subject: [PATCH 1/4] introducing the idea of mixfix parsing --- .gitmodules | 3 + java-mixfix | 1 + key.core/build.gradle | 1 + key.core/src/main/antlr4/KeYLexer.g4 | 5 + key.core/src/main/antlr4/KeYParser.g4 | 13 ++ .../java/de/uka/ilkd/key/java/Services.java | 3 + .../java/de/uka/ilkd/key/nparser/KeyIO.java | 1 - .../uka/ilkd/key/nparser/ParsingFacade.java | 14 +- .../nparser/builder/ExpressionBuilder.java | 16 ++ .../builder/FunctionPredicateBuilder.java | 8 + .../key/nparser/builder/MixFixResolver.java | 165 ++++++++++++++++++ .../key/nparser/builder/MixFixSyntax.java | 0 .../de/uka/ilkd/key/proof/rules/bigint.key | 2 +- .../de/uka/ilkd/key/proof/rules/javaRules.key | 4 +- key.ui/examples/mixfix.key | 12 ++ settings.gradle | 1 + 16 files changed, 238 insertions(+), 11 deletions(-) create mode 100644 .gitmodules create mode 160000 java-mixfix create mode 100644 key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixSyntax.java create mode 100644 key.ui/examples/mixfix.key diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000000..edeb4608aec --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "java-mixfix"] + path = java-mixfix + url = https://github.com/mattulbrich/java-mixfix.git diff --git a/java-mixfix b/java-mixfix new file mode 160000 index 00000000000..9b1404aba9d --- /dev/null +++ b/java-mixfix @@ -0,0 +1 @@ +Subproject commit 9b1404aba9dc2080933b7b8f63432358881f17b3 diff --git a/key.core/build.gradle b/key.core/build.gradle index 2f04313b771..ecad3fae2de 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -14,6 +14,7 @@ dependencies { implementation group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' implementation group: 'org.antlr', name: 'antlr-runtime', version: '3.5.3' implementation group: 'antlr', name: 'antlr', version: '2.7.7' + api project(':java-mixfix') javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' antlr group: 'org.antlr', name: 'antlr', version: '3.5.3' // use ANTLR version 3 diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 1ef3866446a..7d51836971f 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -212,6 +212,7 @@ DATATYPES : '\\datatypes'; TRANSFORMERS : '\\transformers'; UNIQUE : '\\unique'; FREE : '\\free'; +SYNTAX : '\\syntax'; RULES : '\\rules'; AXIOMS : '\\axioms'; @@ -428,6 +429,10 @@ fragment IDCHAR: LETTER | DIGIT | '_' | '#' | '$'; IDENT: ( (LETTER | '_' | '#' | '$') (IDCHAR)*); +OPERATOR: [#_$%&!~?<+>-]+ ; + +MIXFIX_HOLE: '_' '/' DIGIT+ ; + INT_LITERAL: (DIGIT | '_')+ ('l'|'L')? ; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 2a2926ea015..4eafb0ccd7c 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -227,9 +227,16 @@ func_decl func_name = funcpred_name whereToBind=where_to_bind? argSorts = arg_sorts + func_decl_syntax? SEMI ; +func_decl_syntax +: +SYNTAX + ( MIXFIX_HOLE | OPERATOR | simple_ident | LPAREN | RPAREN )+ +; + /** \datatypes { \free List = Nil | Cons(any head, List tail); @@ -418,6 +425,12 @@ primitive_term: | abbreviation | accessterm | literals + | mixfix + ; + +mixfix: + TILDE (literals | simple_ident | OPERATOR | PLUS | MINUS | + LESS | LPAREN | RPAREN /* | ... */ )+ TILDE ; /* diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java index d8232196aee..fc2a41c93dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.java.recoderext.SchemaCrossReferenceServiceConfiguration; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.OriginTermLabelFactory; +import de.uka.ilkd.key.nparser.builder.MixFixResolver; import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.Profile; @@ -88,6 +89,8 @@ public class Services implements TermServices { private final TermBuilder termBuilderWithoutCache; + public final MixFixResolver mixFixResolver = new MixFixResolver(this); + /** * creates a new Services object with a new TypeConverter and a new JavaInfo object with no * information stored at none of these. diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java index b80e260b775..a4454d07db8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java @@ -54,7 +54,6 @@ public class KeyIO { private List warnings = new LinkedList<>(); private AbbrevMap abbrevMap; - public KeyIO(@NonNull Services services, @NonNull NamespaceSet nss) { this.services = services; this.nss = nss; 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 50356a94fd5..d615cf8ee4b 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 @@ -132,15 +132,15 @@ public static KeyAst.File parseFile(CharStream stream) { p.getInterpreter().setPredictionMode(PredictionMode.SLL); // we don't want error messages or recovery during first try p.removeErrorListeners(); - p.setErrorHandler(new BailErrorStrategy()); + // p.setErrorHandler(new BailErrorStrategy()); KeYParser.FileContext ctx; - try { + // try { ctx = p.file(); - } catch (ParseCancellationException ex) { - LOGGER.warn("SLL was not enough"); - p = createParser(stream); - ctx = p.file(); - } +// } catch (ParseCancellationException ex) { +// LOGGER.warn("SLL was not enough"); +// p = createParser(stream); +// ctx = p.file(); +// } p.getErrorReporter().throwException(); return new KeyAst.File(ctx); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index 1cc53a2eda6..07386591924 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 @@ -29,9 +29,11 @@ import de.uka.ilkd.key.nparser.KeYParser.RealLiteralContext; import de.uka.ilkd.key.parser.NotDeclException; import de.uka.ilkd.key.pp.AbbrevMap; +import de.uka.ilkd.key.speclang.translation.SLTranslationException; import de.uka.ilkd.key.util.Debug; import de.uka.ilkd.key.util.parsing.BuildingException; +import edu.kit.kastel.formal.mixfix.MixFixException; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; @@ -183,6 +185,20 @@ public Term visitTermEOF(KeYParser.TermEOFContext ctx) { return accept(ctx.term()); } + @Override + public Term visitMixfix(KeYParser.MixfixContext ctx) { + try { + return services.mixFixResolver.resolve(ctx); + } catch (MixFixException e) { + Object val = e.getToken(); + if(val instanceof Token token) { + throw new BuildingException(token, "Mixfix parser error", e); + } else { + throw new BuildingException(e); + } + } + } + @Override public Term visitElementary_update_term(KeYParser.Elementary_update_termContext ctx) { Term a = accept(ctx.a); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index 69785ef1614..520ff33bcf1 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 @@ -15,6 +15,7 @@ import de.uka.ilkd.key.logic.sort.Sort; import de.uka.ilkd.key.nparser.KeYParser; +import org.antlr.v4.runtime.Token; import org.key_project.util.collection.ImmutableArray; @@ -140,6 +141,13 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) { // weigl: agreement on KaKeY meeting: this should be an error. semanticError(ctx, "Function '" + funcName + "' is already defined!"); } + + if(ctx.func_decl_syntax() != null) { + List tokens = MixFixResolver.extractTokens(ctx.func_decl_syntax()); + tokens.remove(0); + services.mixFixResolver.addMixFixRule(f, tokens); + } + return f; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java new file mode 100644 index 00000000000..1f8ae9b6e63 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java @@ -0,0 +1,165 @@ +package de.uka.ilkd.key.nparser.builder; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.Function; +import de.uka.ilkd.key.logic.op.Operator; +import de.uka.ilkd.key.nparser.KeYLexer; +import de.uka.ilkd.key.nparser.KeYParser; +import edu.kit.kastel.formal.mixfix.*; +import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.Token; +import org.antlr.v4.runtime.tree.ParseTree; +import org.antlr.v4.runtime.tree.TerminalNode; +import org.jspecify.annotations.NonNull; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +public class MixFixResolver { + + private final MixFixRuleCollection ruleCollection = new MixFixRuleCollection<>(); + + private final Services services; + + public MixFixResolver(Services services) { + this.services = services; + + // adding primary rules + ruleCollection.addRule(new IntegerRule()); + ruleCollection.addRule(new ParenthesesRule()); + ruleCollection.addRule(new IdentifierRule()); + // ... others as well + } + + public Term resolve(KeYParser.MixfixContext ctx) throws MixFixException { + List tokens = extractTokens(ctx); + // Currently there is ~ at the beginning and end of mixfix parts + tokens.remove(0); + tokens.remove(tokens.size()-1); + MixFixParser parser = new MixFixParser<>(ruleCollection); + return parser.parseExpression(tokens); + } + + public static List extractTokens(ParserRuleContext ctx) { + List result = new ArrayList(); + extractTokens(result, ctx); + return result; + } + private static void extractTokens(List tokens, ParserRuleContext ctx) { + for (ParseTree child : ctx.children) { + if (child instanceof TerminalNode tn) { + tokens.add(tn.getSymbol()); + } else { + extractTokens(tokens, (ParserRuleContext) child); + } + } + } + + public void addMixFixRule(Function functionSymbol, List mixfix) { + Matcher[] matchers = new Matcher[mixfix.size()]; + int left = extractPrecedence(mixfix.get(0)); + int right = extractPrecedence(mixfix.get(mixfix.size() - 1)); + for (int i = 0; i < matchers.length; i++) { + Token token = mixfix.get(i); + if(token != null && token.getType() != KeYLexer.MIXFIX_HOLE && !token.getText().equals("_")) { + matchers[i] = t -> t.getText().equals(token.getText()) && t.getType() == token.getType(); + } + } + ruleCollection.addRule(new KeYRule(functionSymbol, matchers, left, right)); + } + + private int extractPrecedence(Token token) { + if(token.getType() == KeYLexer.MIXFIX_HOLE) { + String num = token.getText().substring(2); + return Integer.parseInt(num); + } else { + return 0; + } + } + + class KeYRule extends SequenceRule { + + private final Function functionSymbol; + protected KeYRule(Function functionSymbol, Matcher[] sequence, int leftBinding, int rightBinding) { + super(sequence, leftBinding, rightBinding); + this.functionSymbol = functionSymbol; + } + + @Override + protected Term makeResult(@NonNull ADTList results) { + return services.getTermFactory().createTerm(functionSymbol, results.toList()); + } + } + + private class IntegerRule implements MixFixRule { + + @Override + public boolean isLeftRecursive() { + return false; + } + + @Override + public ADTList> parse(ParseContext context, int minBinding) { + Token t = context.getCurrentToken(); + DebugLog.enter(context, minBinding); + + if (t.getType() == KeYLexer.INT_LITERAL) { + context = context.consumeToken(); + context = context.setResult(services.getTermBuilder().zTerm(t.getText())); + DebugLog.leave(context); + return ADTList.singleton(context); + } else { + DebugLog.leave("nil"); + return ADTList.nil(); + } + } + } + + private static class ParenthesesRule extends SequenceRule { + + protected ParenthesesRule() { + super(Arrays.>asList( + t -> t.getType() == KeYLexer.LPAREN, + null, + t -> t.getType() == KeYLexer.RPAREN).toArray(Matcher[]::new), 0, 0); + } + + @Override + protected Term makeResult(@NonNull ADTList results) { + assert results.size() == 1; + return results.hd(); + } + } + + private class IdentifierRule implements MixFixRule { + @Override + public boolean isLeftRecursive() { + return false; + } + + @Override + public ADTList> parse(ParseContext context, int minBinding) { + Token t = context.getCurrentToken(); + DebugLog.enter(context, minBinding); + + if (t.getType() == KeYLexer.IDENT) { + String img = t.getText(); + Operator f = services.getNamespaces().functions().lookup(img); + if (f == null) { + f = services.getNamespaces().programVariables().lookup(img); + } + if (f != null) { + context = context.consumeToken(); + context = context.setResult(services.getTermFactory().createTerm(f)); + DebugLog.leave(context); + return ADTList.singleton(context); + } + } + DebugLog.leave("nil"); + return ADTList.nil(); + } + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixSyntax.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixSyntax.java new file mode 100644 index 00000000000..e69de29bb2d diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/bigint.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/bigint.key index 3d875cbd111..00e24c650c1 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/bigint.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/bigint.key @@ -260,7 +260,7 @@ \find(\modality{#allmodal}{.. #loc = - #seBigint; ...}\endmodality (post)) - \replacewith({#loc := -#seBigint} + \replacewith({#loc := - #seBigint} \modality{#allmodal}{.. ...}\endmodality (post)) \heuristics(executeIntegerAssignment) \displayname "unaryMinus" diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index 0c8a422441c..29382fb40bb 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -1568,7 +1568,7 @@ equality_comparison_new { \find(\modality{#allmodal}{.. #lhs = #senf0 == #senf1; ...}\endmodality (post)) - \replacewith(\if(!#senf0 = #senf1) + \replacewith(\if(! #senf0 = #senf1) \then(\modality{#allmodal}{.. #lhs = false; ...}\endmodality (post)) \else(\modality{#allmodal}{.. #lhs = true; ...}\endmodality (post))) \heuristics(obsolete, simplify_prog, split_if) @@ -1585,7 +1585,7 @@ inequality_comparison_new { \find(\modality{#allmodal}{.. #lhs = #senf0 != #senf1; ...}\endmodality (post)) - \replacewith(\if(!#senf0 = #senf1) \then(\modality{#allmodal}{.. #lhs = true; ...}\endmodality (post)) + \replacewith(\if(! #senf0 = #senf1) \then(\modality{#allmodal}{.. #lhs = true; ...}\endmodality (post)) \else(\modality{#allmodal}{.. #lhs = false; ...}\endmodality (post))) \heuristics(obsolete, simplify_prog, split_if) \displayname "inequality comparison" diff --git a/key.ui/examples/mixfix.key b/key.ui/examples/mixfix.key new file mode 100644 index 00000000000..05f9bdc6e50 --- /dev/null +++ b/key.ui/examples/mixfix.key @@ -0,0 +1,12 @@ +\functions { + + int myExp(int, int) \syntax _/30 !! _/30; + int mySeqGet(Seq, int) \syntax _/100 --> _ <--; + int myadd(int, int) \syntax _/40 ++ _/40; + +} + +\problem { + //~ 3 ++ 3 ~ > ~3!!4~ + ~ 3 ++ 3 !! 4 ++ (seqEmpty --> 3 <--) ~ > 0 +} diff --git a/settings.gradle b/settings.gradle index 0f65c7fe42c..b70aa2b3d69 100644 --- a/settings.gradle +++ b/settings.gradle @@ -14,3 +14,4 @@ include 'keyext.proofmanagement' include 'keyext.exploration' include 'keyext.slicing' include 'keyext.caching' +include 'java-mixfix' From a6fc7d1103ecf225da6cccc94135527c451124ee Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Thu, 22 Feb 2024 23:20:04 +0100 Subject: [PATCH 2/4] no git submodule. does not work correctly --- .gitmodules | 3 - java-mixfix | 1 - java-mixfix/LICENSE | 674 ++++++++++++++++++ java-mixfix/README.md | 2 + .../edu/kit/kastel/formal/mixfix/ADTList.java | 293 ++++++++ .../kit/kastel/formal/mixfix/DebugLog.java | 104 +++ .../edu/kit/kastel/formal/mixfix/Matcher.java | 59 ++ .../edu/kit/kastel/formal/mixfix/MaxList.java | 71 ++ .../kastel/formal/mixfix/MixFixException.java | 54 ++ .../kastel/formal/mixfix/MixFixParser.java | 231 ++++++ .../kit/kastel/formal/mixfix/MixFixRule.java | 59 ++ .../formal/mixfix/MixFixRuleCollection.java | 79 ++ .../kastel/formal/mixfix/ParseContext.java | 92 +++ .../kastel/formal/mixfix/SequenceRule.java | 215 ++++++ .../kastel/formal/mixfix/ExampleParser.java | 28 + .../kastel/formal/mixfix/IdentifierRule.java | 38 + .../formal/mixfix/NaturalNumberRule.java | 37 + .../kit/kastel/formal/mixfix/SyntaxRule.java | 59 ++ .../kit/kastel/formal/mixfix/TestADTList.java | 65 ++ .../formal/mixfix/TestMixFixParser.java | 250 +++++++ 20 files changed, 2410 insertions(+), 4 deletions(-) delete mode 160000 java-mixfix create mode 100644 java-mixfix/LICENSE create mode 100644 java-mixfix/README.md create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ADTList.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/DebugLog.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/Matcher.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MaxList.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixException.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixParser.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRule.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRuleCollection.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ParseContext.java create mode 100644 java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/SequenceRule.java create mode 100644 java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/ExampleParser.java create mode 100644 java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/IdentifierRule.java create mode 100644 java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/NaturalNumberRule.java create mode 100644 java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/SyntaxRule.java create mode 100644 java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestADTList.java create mode 100644 java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestMixFixParser.java diff --git a/.gitmodules b/.gitmodules index edeb4608aec..e69de29bb2d 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +0,0 @@ -[submodule "java-mixfix"] - path = java-mixfix - url = https://github.com/mattulbrich/java-mixfix.git diff --git a/java-mixfix b/java-mixfix deleted file mode 160000 index 9b1404aba9d..00000000000 --- a/java-mixfix +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 9b1404aba9dc2080933b7b8f63432358881f17b3 diff --git a/java-mixfix/LICENSE b/java-mixfix/LICENSE new file mode 100644 index 00000000000..f288702d2fa --- /dev/null +++ b/java-mixfix/LICENSE @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + + Copyright (C) + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + Copyright (C) + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +. diff --git a/java-mixfix/README.md b/java-mixfix/README.md new file mode 100644 index 00000000000..e69c3410fe2 --- /dev/null +++ b/java-mixfix/README.md @@ -0,0 +1,2 @@ +# java-mixfix +A generic mixfix parsing library for Java diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ADTList.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ADTList.java new file mode 100644 index 00000000000..08dab8ad179 --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ADTList.java @@ -0,0 +1,293 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +import org.jspecify.annotations.NonNull; + +import java.util.*; + +/** + * Lists as in the theory of Abstract Data Types. + *

+ * In contrast to {@link java.util.List}, objects of this class are immutable. + * New instances are returned by calls to {@link #cons(Object)}. + *

+ * The list is implemented used a singly-linked list. + *

+ * {@link ADTList} is iterable. The order of the iteration herein is + * "newest elements first". + * + * @author mattias ulbrich + */ +public class ADTList implements Iterable { + + /** + * The value stored in this entry + */ + private T head; + + /** + * The remainder of the list. + */ + private ADTList tail; + + /** + * The number of elements in this list. Is non-negative. + */ + private final int size; + + /** + * The Constant NIL is the only object with size == 0. + */ + @SuppressWarnings({"rawtypes"}) + private static final ADTList NIL = new ADTList(); + + public List toList() { + if(this==NIL){ + return new LinkedList<>(); + } + var seq = tail.toList(); + seq.add(0, head); + return seq; + } + + /** + * The private iterator class. + */ + private static class It implements Iterator { + + /** + * The current list element to take data from, may be NIL or null. + */ + private ADTList cur; + + /** + * Instantiates a new it with a list object + * + * @param adtList + * the list to iterate + */ + public It(ADTList adtList) { + cur = adtList; + } + + /** + * {@inheritDoc} + * + * If the current list is not null and has data, then the iterator has + * more to iterate. + */ + public boolean hasNext() { + return cur != null && cur.size() > 0; + } + + /** + * {@inheritDoc} + * + * If the iterator has more to iterate, return the head of the current + * list and advance the list pointer to its tail. + *

+ * Throw an exception if no data is available. + */ + @Override + public T next() { + if (!hasNext()) + throw new NoSuchElementException(); + + T t = cur.head; + cur = cur.tail; + return t; + } + + /** + * Not supported in this implementation. + */ + @Override + public void remove() { + throw new UnsupportedOperationException( + "remove is not supported by this iterator."); + } + } + + /* + * (non-Javadoc) + * + * @see java.lang.Iterable#iterator() + */ + @Override @NonNull + public Iterator iterator() { + return new It<>(this); + } + + /* + * Used to create the NIL object + */ + private ADTList() { + size = 0; + } + + /** + * Instantiates a new list from an element another list. + * + * @param head + * the element to set as head. + * @param tail + * the list to use as tail. + */ + public ADTList(T head, ADTList tail) { + this.head = head; + this.size = tail.size + 1; + this.tail = tail; + } + + /** + * Retrieves a type parametrised version of an empty list. + * + * @return a reference to {@link #NIL} + */ + @SuppressWarnings("unchecked") + public static ADTList nil() { + return NIL; + } + + /** + * Create a singleton list. + *

+ * The resulting list has length 1 and contains the given element. + * + * @param head + * the element to wrap in a singleton list. + * + * @return a list of length 1. + */ + public static ADTList singleton(T head) { + return ADTList. nil().cons(head); + } + + /** + * Create a new list from an element. + *

+ * The new list's head is the element and its tail is this + * list. Equivalent to calling new ADTList<T>(head, this) + * . + * + * @param head + * the element to add. + * + * @return a list which is longer by one entry. + */ + public ADTList cons(T head) { + return new ADTList<>(head, this); + } + + /** + * create a list which has element from the iterable collection added to + * this list. + *

+ * The collection is iterated and in that order the elements are added to + * the new list. + * + * @param collection + * the collection to add all elements from + * + * @return a list which contains all elements from collection and from this. + */ + public ADTList consAll(Iterable collection) { + ADTList result = this; + for (T t : collection) { + result = result.cons(t); + } + + return result; + } + + /** + * Gets the data element stored in this list entry. May be null. + * + * @return the head of the list + */ + public T hd() { + return head; + } + + /** + * Gets the remaining list referred to by this list. Is null + * iff size==0. + * + * @return the tail of the list. + */ + public ADTList tl() { + return tail; + } + + /** + * Gets the number of elements stored in this list. + * + * @return a non-negative number + */ + public int size() { + return size; + } + + /** + * Checks if this is empty. + *

+ * Same as size() == 0. + * + * @return true, iff is empty + */ + public boolean isEmpty() { + return size == 0; + } + + /** + * Reverses the list. + * + * @return a list with the same elements but in the opposite order. + */ + public ADTList rev() { + return ADTList. nil().consAll(this); + } + + /** + * {@inheritDoc} + * + * This is equal to another {@link ADTList} if and only if their sizes are + * equal, and they contain equal elements at each position + */ + @Override + public boolean equals(Object obj) { + if (obj instanceof ADTList list) { + return size == list.size + && (Objects.equals(head, list.head)) + && (Objects.equals(tail, list.tail)); + } + return false; + } + + /* + * (non-Javadoc) + * + * @see java.lang.Object#toString() + * @see java.util.List#toString() + */ + @Override + public String toString() { + StringBuilder sb = new StringBuilder("["); + Iterator it = iterator(); + while (it.hasNext()) { + sb.append(it.next()); + if (it.hasNext()) + sb.append(","); + } + sb.append("]"); + + return sb.toString(); + } + +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/DebugLog.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/DebugLog.java new file mode 100644 index 00000000000..cecd9ab0968 --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/DebugLog.java @@ -0,0 +1,104 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +import java.util.Arrays; +import java.util.Stack; + +/** + * The Class DebugLog is a class with only static functions which allows to + * simply trace memory entries and leaving. + * + * It is not multi-thread-compatible. + * + * When used and switched on (see {@link #DEBUG}) the methods + * {@link #enter(Object...)} and {@link #leave(Object)} allow to add trace + * statements to your code. Together with arguments and return values method + * entries and leavings will then be printed with indention to the standard + * output. + * + * @author mattias ulbrich + */ +public class DebugLog { + + + /** + * The stack of method calls. + */ + private static Stack methodStack = new Stack(); + + /** + * The master switch to turn on and off. + */ + private static boolean DEBUG = true; + + /** + * If enter and leave are unmatched, this fails. run this to check the + * failure! + */ + private static final boolean ENSURE_GOOD = true; + + /** + * Enter a method. + * + * @param args + * the arguments to the method. + */ + public static void enter(Object... args) { + if (!DEBUG) { + return; + } + + Exception ex = new Exception(); + StackTraceElement ste = ex.getStackTrace()[1]; + String method = ste.getClassName() + "." + ste.getMethodName(); + indent(); + System.out.println("> " + method); + indent(); + System.out.println(" " + Arrays.asList(args)); + methodStack.push(method); + } + + /** + * Leave a method. + * + * @param returned + * the returned value. + */ + public static void leave(Object returned) { + if (!DEBUG) { + return; + } + + String method = methodStack.pop(); + + if (ENSURE_GOOD) { + Exception ex = new Exception(); + StackTraceElement ste = ex.getStackTrace()[1]; + String methodExpected = ste.getClassName() + "." + ste.getMethodName(); + if(!method.equals(methodExpected)) { + throw new Error("Entered " + method + " but left " + methodExpected); + } + } + + indent(); + System.out.println("< " + method); + indent(); + System.out.println(" " + returned); + } + + /** + * Indentation by level + */ + private static void indent() { + for (int i = 0; i < methodStack.size(); i++) { + System.out.print(" "); + } + } + +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/Matcher.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/Matcher.java new file mode 100644 index 00000000000..44312b6be74 --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/Matcher.java @@ -0,0 +1,59 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +/** + * The interface Matcher models a predicate which allows to match tokens of a type. + * + * The class {@link SequenceRule} has a sequence of token options against which + * the input stream is matched. This sequence is made up of {@link Matcher} + * objects. + * + * A simple matcher for strings which checks for equality would be: + * + * 

+ * class EqMatcher implements Matcher<String> {
+ *     String expect;
+ * 
+ *     public EqMatcher(String string) {
+ *         expect = string;
+ *     }
+ * 
+ *     @Override
+ *     public boolean matches(String t) {
+ *         return expect.equals(t);
+ *     }
+ * }
+ *
+ * + * A matcher which allows for either tokens (of some unknown class Token) with id 42 or + * whose content is "42": + * 
+ * class SomeMatcher implements Matcher<Token> {
+ *     @Override
+ *     public boolean matches(Token t) {
+ *         return t.id == 42 || "42".equals(t.content);
+ *     }
+ * }
+ *
+ * + * @author mattias ulbrich + */ +public interface Matcher { + + /** + * Checks whether a token matches fulfils some condition. + * + * @param token + * the token to check. + * + * @return true, if successful + */ + boolean matches(T token); + +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MaxList.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MaxList.java new file mode 100644 index 00000000000..af6e42728b9 --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MaxList.java @@ -0,0 +1,71 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ + +package edu.kit.kastel.formal.mixfix; + +import java.util.AbstractList; +import java.util.List; + +/** + * The MaxList is a wrapper around an arbitrary {@link List} object which + * records reading accesses and allows to query for the maximum index to be + * read. + * + * @author mattias ulbrich + */ +public class MaxList extends AbstractList { + + /** + * The wrapped list. + */ + private final List wrappedList; + /** + * The maximum index read so far. -1 indicates that no entry has been read + * yet. + */ + private int maxIndex = -1; + + /** + * Gets the maximum index read so far. + * + * -1 is returned if no reading has been done yet from this list. + * + * @return an integer value greater or equal to -1. + */ + public int getMaxReadIndex() { + return maxIndex; + } + + /** + * Instantiates a new max list by w + * + * @param wrappedList + * the wrapped list + */ + public MaxList(List wrappedList) { + this.wrappedList = wrappedList; + } + + /* (non-Javadoc) + * @see java.util.AbstractList#get(int) + */ + @Override + public E get(int index) { + maxIndex = Math.max(index, maxIndex); + return wrappedList.get(index); + } + + /* (non-Javadoc) + * @see java.util.AbstractCollection#size() + */ + @Override + public int size() { + return wrappedList.size(); + } + +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixException.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixException.java new file mode 100644 index 00000000000..b71a1cf78c6 --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixException.java @@ -0,0 +1,54 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +/** + * MixFixException are thrown by {@link MixFixParser} when the result of a + * parsing process is erroneous. + * + * They always contain a reference to a token (retrieve via {@link #getToken()}) + * to which the parser pinned the execption. This assignment is not always + * accurate. + * + * If the exception stems from an instance of type + * MixFixParser<T>, {@link #getToken()} is guaranteed to be + * of type T also. + * + * @author mattias ulbrich + */ +public class MixFixException extends Exception { + private static final long serialVersionUID = -7898251715665380761L; + + private Object token; + + public MixFixException() { + super(); + } + + public MixFixException(String message, Throwable cause) { + super(message, cause); + } + + public MixFixException(String message) { + super(message); + } + + public MixFixException(Throwable cause) { + super(cause); + } + + public MixFixException(String string, Object token) { + super(string); + this.token = token; + } + + public Object getToken() { + return token; + } + +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixParser.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixParser.java new file mode 100644 index 00000000000..b04e9b8b9df --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixParser.java @@ -0,0 +1,231 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +import org.jspecify.annotations.NonNull; + +import java.util.List; + +/* + * def expression(rbp=0): + global token + t = token + token = next() + left = t.nud() + while rbp < token.lbp: + t = token + token = next() + left = t.led(left) + + return left + */ + +/** + * A MixFixParser allows to parse arbitrary operator grammars with + * rule-based precedences even if they are ambiguous. + * + * Top down recursive descent is used to parse a stream of tokens. + * + * The set of rules is given dynamically (at runtime) by an instance of + * {@link MixFixRuleCollection}. + * + * A grammar is called is called operator grammar if in no right hand side of a + * production two consequent non-terminal symbols appear. A grammar is called a + * (per-terminal) precedence grammar if certain relations on the terminal + * symbols can be established which allows easy parsing. This is the case for + * most expression grammars. We aim for more generality and allow therefore + * rules with different precedences for one symbol. + * + * The runtime performance of this system is theoretically poor since the + * backtracking implies an exponential runtime. In reality, however, only very + * little is backtracked. + * + * The rules are instances of the interface {@link MixFixRule}. They are called + * using the method {@link MixFixRule#parse(ParseContext, int)} to return a + * value of the result type. + * + * Simple rules (especially identifiers and some built-in rules) will directly + * implement the rule interface. Most compound rules for operators can extends + * {@link SequenceRule} however. + * + *

Further reading

+ *
    + *
  1. Wieland, Jacob. Parsing Mixfix Expressions. + * Dealing with User-Defined Mixfix Operators Efficiently
    2. + *
  2. http://effbot.org/zone/simple-top-down-parsing.htm
    3. + *
+ * + *

Remarks

+ * NUD is short for null denotation, LED for left denotation. + * + * @param R + * the result type of the parsing process. + * + * @param T + * the type of the tokens to be used for parsing. + * + * @author mattias ulbrich + * + */ +public class MixFixParser { + + /** + * The collection of rules to be used. + */ + private final MixFixRuleCollection rules; + + /** + * Instantiates a new mix fix parser. + * + * @param rules + * the rules collection + */ + public MixFixParser(MixFixRuleCollection rules) { + super(); + this.rules = rules; + } + + /** + * Parses an expression from a stream of tokens. + * + * The parser can be used to parse more than one stream (even at the same + * time). + * + * @param tokenStream + * the token stream to examine. + * + * @return the resulting object. + * + * @throws MixFixException + * in case of syntax errors + */ + public R parseExpression(List tokenStream) throws MixFixException { + + if (tokenStream.isEmpty()) { + throw new MixFixException("Empty token stream"); + } + + MaxList tokenMaxStream = new MaxList(tokenStream); + ParseContext context = new ParseContext(this, + tokenMaxStream); + ADTList> results = parseExpression(context, 0); + + if (results.isEmpty()) { + int max = tokenMaxStream.getMaxReadIndex(); + T token = null; + if(max != -1) { + token = tokenMaxStream.get(max); + } + // TODO toekn may be null + throw new MixFixException("Syntax error near " + token, token); + } + + ParseContext goodResult = null; + int maxPos = 0; + + // System.out.println(results); + + for (ParseContext ctx : results) { + if (ctx.hasFinished()) { + if (goodResult == null) { + goodResult = ctx; + } else { + throw new MixFixException( + "Ambiguous parse results. Two results are:\n" + + goodResult.getResult() + ",\n" + + ctx.getResult(), tokenStream.get(0)); + } + } + maxPos = Math.max(maxPos, ctx.getCurrentPosition()); + } + + if (goodResult == null) { + int max = tokenMaxStream.getMaxReadIndex(); + T token = tokenMaxStream.get(max); + throw new MixFixException("Syntax error near " + token, token); + } + + return goodResult.getResult(); + } + + /** + * Parses an expression which has a minimum left binding. + * + * The method is package visible to allow for call backs from + * {@link ParseContext}. + * + * This is the point were NUD-rules are queried. + * + * @param context + * the context to use + * @param minBinding + * the minimum left binding for the first operator + * + * @return a list of contexts to proceed with + */ + ADTList> parseExpression(@NonNull ParseContext context, int minBinding) { + + DebugLog.enter(context, minBinding); + ADTList> result = ADTList.nil(); + + // Bugfix: The max binding needs to be removed here + context = context.resetMaxBinding(); + + List> nudRules = rules.getNUDRules(); + for (MixFixRule rule : nudRules) { + ADTList> resultCtxs = rule.parse(context, + minBinding); + for (ParseContext resultCtx : resultCtxs) { + result = result.consAll(continueParsing(resultCtx, minBinding)); + } + } + + DebugLog.leave(result); + return result; + } + + /** + * Continue parsing with a left-recursive rule. + * + * This is the point were LED-rules are queried. + * + * @param context + * the context to use + * @param minBinding + * the minimum left binding for the first operator + * + * @return a list of contexts to proceed with + */ + private ADTList> continueParsing( + @NonNull ParseContext context, int minBinding) { + + DebugLog.enter(context, minBinding); + ADTList> result = ADTList.singleton(context); + + // end of input -> return the given context, which is valid + if (context.hasFinished()) { + DebugLog.leave(result); + return result; + } + + // check all possible led rules if they match + List> ledRules = rules.getLEDRules(); + for (MixFixRule rule : ledRules) { + ADTList> resultCtxs = rule.parse(context, + minBinding); + for (ParseContext resultCtx : resultCtxs) { + // TODO should this not be resultCtx.getLastBinding? + result = result.consAll(continueParsing(resultCtx, minBinding)); + } + } + + DebugLog.leave(result); + return result; + } + +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRule.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRule.java new file mode 100644 index 00000000000..860338153d0 --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRule.java @@ -0,0 +1,59 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +public interface MixFixRule { + + /** + * Determines the type of the rule. + * + *

+ * A rule is left recursive iff its representation as a production starts + * with a non-terminal. + * + *

+ * Or equivalently: A rule is left recursive iff it is used in a left + * denotation context (see {@link MixFixRuleCollection}). + * + * @return true iff this rule is left recursive + */ + public boolean isLeftRecursive(); + + /** + * Continues parsing with this rule in a given context. + * + *

+ * If this rule is left recursive you can retrieve the result of the + * recursion using {@link ParseContext#getResult()}. The method should + * return a collection of all possible parsing contexts in which this rule + * can finish on the given input context. This is the empty list if this + * rule cannot be applied in the context. It can return more than one + * context if the grammar is ambiguous. + * + *

+ * If the (left-)binding of the first terminal of this rule is + *

+ *
less than minBinding,
+ *
the previously encountered terminal binds stronger and this rule + * cannot be applied (in this context)
+ *
greater than context.getLastBinding()
+ *
the result in context is only possible if this rule cannot will not + * be applied (in this context)
+ *
+ * In both cases, an implementing method must return {@link ADTList#nil()} + * + * @param context + * the context to use + * @param minBinding + * the minimum left binding for the first operator + * + * @return a non-null (possibly empty) list of parse-contexts. + */ + public ADTList> parse(ParseContext context, int minBinding); + +} \ No newline at end of file diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRuleCollection.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRuleCollection.java new file mode 100644 index 00000000000..955c9c564fe --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/MixFixRuleCollection.java @@ -0,0 +1,79 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + + +/** + * This class serves as a collection of rules used by a {@link MixFixParser}. + * + *

+ * There two kind of rules: + *

+ *
left-denotation rules (LED)
+ *
rule which expect a left hand side argument already parsed in the context + * when given control. They are also called left-recursive and represent the set + * of rules which - represented as a production - begin with a non terminal + * symbol
+ *
null-denotation rule (NUD)
+ *
rules which parse their first token from the stream themselves and do not + * use/rely on a result present in the context. They correspond - represented as + * productions - to those production which start with a terminal symbol. + *
+ * + * There is only one generic method {@link #addRule(MixFixRule)} which uses the + * query {@link MixFixRule#isLeftRecursive()} to categorise an added rule. Rules + * can be retrieved using either {@link #getLEDRules()} or + * {@link #getNUDRules()}. + */ +public class MixFixRuleCollection { + + /** + * The internal collection of left denotation rules. monotonously growing. + */ + private List> ledRules = new ArrayList>(); + + /** + * The internal collection of null denotation rules. monotonously growing. + */ + private List> nudRules = new ArrayList>(); + + /** + * Gets the set of left denotation rules of this collection. + * + * @return an immutable list of rules, not null + */ + public List> getLEDRules() { + return Collections.unmodifiableList(ledRules); + } + + /** + * Gets the set of null denotation rules of this collection. + * + * @return an immutable list of rules, not null + */ + public List> getNUDRules() { + return Collections.unmodifiableList(nudRules); + } + + /** + * Adds a rule to the collection + * + * @param rule + * the rule to add, not null + */ + public void addRule(MixFixRule rule) { + if (rule.isLeftRecursive()) + ledRules.add(rule); + else + nudRules.add(rule); + } +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ParseContext.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ParseContext.java new file mode 100644 index 00000000000..31ca9f2811f --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/ParseContext.java @@ -0,0 +1,92 @@ +package edu.kit.kastel.formal.mixfix; + +import java.util.List; +// TODO: Auto-generated Javadoc +public class ParseContext { + + private final MixFixParser parser; + private final List tokenStream; + private int curPos; + private int maxBinding; + private R result; + + public ParseContext(MixFixParser parser, List tokenStream) { + this.tokenStream = tokenStream; + this.parser = parser; + this.maxBinding = Integer.MAX_VALUE; + } + + private ParseContext(ParseContext copyFrom) { + this.parser = copyFrom.parser; + this.curPos = copyFrom.curPos; + this.tokenStream = copyFrom.tokenStream; + this.maxBinding = copyFrom.maxBinding; + this.result = copyFrom.result; + } + + /** + * @return the result + */ + public R getResult() { + return result; + } + + // do not change last binding but keep it! -> for closed-rhs rules + public ParseContext setResult(R result) { + ParseContext res = new ParseContext(this); + res.result = result; + return res; + } + + public T getCurrentToken() { + if (hasFinished()) { + throw new IllegalStateException("Context already at its end"); + } + + return tokenStream.get(curPos); + } + + public int getMaxBinding() { + return maxBinding; + } + + public ParseContext setMaxBinding(int maxBinding) { + ParseContext res = new ParseContext(this); + res.maxBinding = maxBinding; + return res; + } + + public ParseContext resetMaxBinding() { + return setMaxBinding(Integer.MAX_VALUE); + } + + public ADTList> parseExpression(int minBinding) { + // TODO Memoization of parsing results, with (curPos, minBinding and/or lastBinding) + return parser.parseExpression(this, minBinding); + } + + public ParseContext consumeToken() { + ParseContext res = new ParseContext(this); + res.curPos++; + return res; + } + + public boolean hasFinished() { + return curPos >= tokenStream.size(); + } + + /* (non-Javadoc) + * @see java.lang.Object#toString() + */ + @Override + public String toString() { + return "ParseContext [curPos=" + curPos + ", maxBinding=" + getMaxBinding() + + ", result=" + result + "]"; + } + + public int getCurrentPosition() { + return curPos; + } + + +} diff --git a/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/SequenceRule.java b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/SequenceRule.java new file mode 100644 index 00000000000..519410183bd --- /dev/null +++ b/java-mixfix/src/main/java/edu/kit/kastel/formal/mixfix/SequenceRule.java @@ -0,0 +1,215 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ + +package edu.kit.kastel.formal.mixfix; + +// TODO Finish Javadoc + +import org.jspecify.annotations.NonNull; + +/** + * The Class SequenceRule. + */ +public abstract class SequenceRule implements MixFixRule { + + /** + * The sequence. + */ + private final Matcher[] sequence; + + /** + * The left binding. + */ + private final int leftBinding; + + /** + * The right binding. + */ + private final int rightBinding; + + /** + * Instantiates a new sequence rule. + * + *

+ * Please note that the array is not deep copied and that you should + * not change it after the invocation of this constructor + * + * @param sequence + * the sequence + * @param leftBinding + * the left binding + * @param rightBinding + * the right binding + */ + protected SequenceRule(Matcher[] sequence, int leftBinding, int rightBinding) { + super(); + this.sequence = sequence; + this.leftBinding = leftBinding; + this.rightBinding = rightBinding; + } + + /* + * (non-Javadoc) + * + * @see de.uka.iti.mixfix.MixFixRule#getLeftBinding() + */ + /** + * Gets the left binding. + * + * @return the left binding + */ + public int getLeftBinding() { + return leftBinding; + } + + /* + * (non-Javadoc) + * + * @see de.uka.iti.mixfix.MixFixRule#getRightBinding() + */ + /** + * Gets the right binding. + * + * @return the right binding + */ + public int getRightBinding() { + return rightBinding; + } + + /* + * (non-Javadoc) + * + * @see de.uka.iti.mixfix.MixFixRule#isLeftRecursive() + */@Override + public boolean isLeftRecursive() { + return sequence[0] == null; + } + + private boolean isRightRecursive() { + return sequence[sequence.length - 1] == null; + } + + /* + * (non-Javadoc) + * + * @see de.uka.iti.mixfix.MixFixRule#parse(de.uka.iti.mixfix.ParseContext) + */ + @Override + public ADTList> parse(@NonNull ParseContext context, int minBinding) { + + DebugLog.enter(this, context, minBinding); + + ADTList results = ADTList.nil(); + int origMaxBinding = context.getMaxBinding(); + + if (isLeftRecursive()) { + + if (getLeftBinding() > context.getMaxBinding() + || getLeftBinding() < minBinding) { + DebugLog.leave(ADTList.nil()); + return ADTList.nil(); + } + + results = results.cons(context.getResult()); + ADTList> returnValue = continueParsing(context, 1, results, origMaxBinding); + DebugLog.leave(returnValue); + return returnValue; + } else { + ADTList> returnValue = continueParsing(context, 0, results, origMaxBinding); + DebugLog.leave(returnValue); + return returnValue; + } + } + + /** + * Continue parsing. + * + * @param context + * the context + * @param seqPos + * the seq pos + * @param results + * the results + * @param origMaxBinding + * + * @return the aDT list< parse context< r, t>> + */ + private ADTList> continueParsing( + @NonNull ParseContext context, int seqPos, + @NonNull ADTList results, int origMaxBinding) { + + DebugLog.enter(this, context, seqPos, results); + + // consume the non-placeholder positions of the rule + while (seqPos < sequence.length && sequence[seqPos] != null && !context.hasFinished()) { + if (!sequence[seqPos].matches(context.getCurrentToken())) { + DebugLog.leave(ADTList.nil()); + return ADTList.nil(); + } + + context = context.consumeToken(); + seqPos++; + } + + if (seqPos < sequence.length) { + + // TODO To have fewer ambiguous grammars: Allow for "inner bindings" to use here. + // Then: minBinding = getPositionBinding(seqPos) + 1 (essentially) + int minBinding = 0; + if (seqPos == sequence.length - 1 && isRightRecursive()) { + // use right binding only in last position if that is nonterminal + minBinding = getRightBinding()+1; + } + + + if(context.hasFinished()) { + DebugLog.leave("[]"); + return ADTList.nil(); + } + + ADTList> resultCtxs = ADTList.nil(); + ADTList> parseRes = context + .parseExpression(minBinding); + + for (ParseContext parseContext : parseRes) { + ADTList newRes = results.cons(parseContext.getResult()); + resultCtxs = resultCtxs.consAll(continueParsing(parseContext, + seqPos + 1, newRes, origMaxBinding)); + } + + DebugLog.leave(resultCtxs); + return resultCtxs; + + } else { + + R r = makeResult(results.rev()); + context = context.setResult(r); + if(isRightRecursive()) { + context = context.setMaxBinding( + Math.min(getRightBinding(), context.getMaxBinding())); + } else { + context = context.setMaxBinding(origMaxBinding); + } + DebugLog.leave(context); + return ADTList.singleton(context); + + } + + } + + /** + * Make result. + * + * @param results + * the results + * + * @return the r + */ + protected abstract R makeResult(@NonNull ADTList results); + +} diff --git a/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/ExampleParser.java b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/ExampleParser.java new file mode 100644 index 00000000000..97dcc41dad9 --- /dev/null +++ b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/ExampleParser.java @@ -0,0 +1,28 @@ +package de.uka.iti.mixfix.test; + + +//public class ExampleParser { +// +// private static MixFixParser parser; +// private static MixFixRuleCollection coll; +// +// public static void main(String[] args) throws IOException { +// coll = new MixFixRuleCollection(); +// TestMixFixParser.addComplexGrammar(coll); +// parser = new MixFixParser(coll); +// BufferedReader br = new BufferedReader(new InputStreamReader(System.in)); +// String line = br.readLine(); +// while(line != null && line.length() > 0) { +// try { +// String result = parser.parseExpression(Arrays.asList(line.split(" +"))); +// System.out.println(result); +// } catch (MixFixException e) { +// System.err.println(e); +// System.err.println(e.getToken()); +// // System.err.println(e.getPosition()); +// } +// line = br.readLine(); +// } +// } +// +//} diff --git a/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/IdentifierRule.java b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/IdentifierRule.java new file mode 100644 index 00000000000..c3d0d185e31 --- /dev/null +++ b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/IdentifierRule.java @@ -0,0 +1,38 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +/** + * Very simple sample implementation for a rule which matches certain strings. + */ +public class IdentifierRule implements MixFixRule { + + @Override + public boolean isLeftRecursive() { + return false; + } + + @Override + public ADTList> parse( + ParseContext context, int minBinding) { + + DebugLog.enter(context, minBinding); + + String t = context.getCurrentToken(); + if(t.matches("[a-z]+")) { + context = context.consumeToken(); + context = context.setResult(t); + DebugLog.leave(context); + return ADTList.singleton(context); + } else { + DebugLog.leave("nil"); + return ADTList.nil(); + } + } + +} diff --git a/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/NaturalNumberRule.java b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/NaturalNumberRule.java new file mode 100644 index 00000000000..827f6e61a07 --- /dev/null +++ b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/NaturalNumberRule.java @@ -0,0 +1,37 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +/** + * Very simple sample implementation for a rule which matches certain strings. + */ +public class NaturalNumberRule implements MixFixRule { + + @Override + public boolean isLeftRecursive() { + return false; + } + + @Override + public ADTList> parse( + ParseContext context, int minBinding) { + DebugLog.enter(context, minBinding); + + String t = context.getCurrentToken(); + + if (t.matches("[0-9]+")) { + context = context.consumeToken(); + context = context.setResult(t); + DebugLog.leave(context); + return ADTList.singleton(context); + } else { + DebugLog.leave("nil"); + return ADTList.nil(); + } + } +} diff --git a/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/SyntaxRule.java b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/SyntaxRule.java new file mode 100644 index 00000000000..a33145dd4ea --- /dev/null +++ b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/SyntaxRule.java @@ -0,0 +1,59 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + + +/** + * Simple sample implementation + */ +public class SyntaxRule extends SequenceRule { + + private String name; + private String description; + + public SyntaxRule(String name, String description, int left, int right) { + super(decompose(description), left, right); + this.name = name; + this.description = description; + } + + private static class EqMatcher implements Matcher { + String expect; + + public EqMatcher(String string) { + expect = string; + } + + @Override + public boolean matches(String t) { + return expect.equals(t); + } + } + + private static Matcher[] decompose(String description) { + String[] parts = description.split(" +"); + EqMatcher[] result = new EqMatcher[parts.length]; + for (int i = 0; i < parts.length; i++) { + if (!"_".equals(parts[i])) { + result[i] = new EqMatcher(parts[i]); + } + } + return result; + } + + @Override + protected String makeResult(ADTList parameters) { + return name + parameters; + } + + @Override + public String toString() { + return name + " - " + description; + } + +} diff --git a/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestADTList.java b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestADTList.java new file mode 100644 index 00000000000..2f73a40616d --- /dev/null +++ b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestADTList.java @@ -0,0 +1,65 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +import org.junit.Test; + +import static org.junit.Assert.*; + +/** + * Test cases for the class {@link ADTList}. + */ +public class TestADTList { + + private ADTList list123 = ADTList.nil().cons("1").cons("2").cons("3"); + + public void testEquals() throws Exception { + + ADTList listCopy = ADTList.nil().cons("1").cons("2").cons("3"); + ADTList list1234 = listCopy.cons("4"); + + assertTrue(ADTList.nil().equals(ADTList.nil())); + assertTrue(list123.equals(listCopy)); + assertFalse(list123.equals(list1234)); + } + + @Test + public void testToString() throws Exception { + ADTList list1 = ADTList.nil().cons("1").cons("2").cons("3"); + assertEquals("[3,2,1]", list1.toString()); + assertEquals("[]", ADTList.nil().toString()); + } + + + @Test + public void testIterator() throws Exception { + for (@SuppressWarnings("unused") Object o : ADTList.nil()) { + fail("Must never be reached"); + } + + String s = ""; + for (String string : list123) { + s = s + string; + } + assertEquals("321", s); + } + + @Test + public void testSize() throws Exception { + assertEquals(0, ADTList.nil().size()); + assertEquals(3, list123.size()); + } + + @Test + public void testRev() { + ADTList list321 = ADTList.nil().cons("3").cons("2").cons("1"); + assertEquals(list321, list123.rev()); + } + +} + diff --git a/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestMixFixParser.java b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestMixFixParser.java new file mode 100644 index 00000000000..94198b5519b --- /dev/null +++ b/java-mixfix/src/test/java/edu/kit/kastel/formal/mixfix/TestMixFixParser.java @@ -0,0 +1,250 @@ +/* + * Copyright (C) 2010 Universitaet Karlsruhe, Germany + * written by Mattias Ulbrich + * + * The system is protected by the GNU General Public License. + * See LICENSE.TXT for details. + */ +package edu.kit.kastel.formal.mixfix; + +import org.junit.Before; +import org.junit.Test; + +import java.util.Arrays; +import static org.junit.Assert.*; + +/** + * Test cases for the {@link MixFixParser}. + */ +public class TestMixFixParser { + + private MixFixParser parser; + private MixFixRuleCollection coll; + + @Before + public void setUp() throws Exception { + coll = new MixFixRuleCollection(); + parser = new MixFixParser(coll); + } + + private String parse(String arg) throws MixFixException { + String[] arr = arg.split(" "); + String result = parser.parseExpression(Arrays.asList(arr)); + System.out.println(arg + " ==> " + result); + return result; + } + + public static void addComplexGrammar(MixFixRuleCollection coll) { + coll.addRule(new IdentifierRule()); + coll.addRule(new NaturalNumberRule()); + coll.addRule(new SyntaxRule("plus", "_ + _", 10, 10)); + coll.addRule(new SyntaxRule("subs", "_ - _", 10, 10)); + coll.addRule(new SyntaxRule("minus", "- _", 100, 100)); + coll.addRule(new SyntaxRule("mult", "_ * _", 20, 20)); + coll.addRule(new SyntaxRule("exp", "_ ^ _", 30, 28)); + coll.addRule(new SyntaxRule("paren", "( _ )", 100, 100)); + + coll.addRule(new SyntaxRule("update", "{ _ := _ } _", 100, 100)); + coll.addRule(new SyntaxRule("setex", "{ _ . _ | _ }", 100, 100)); + coll.addRule(new SyntaxRule("setex2", "{ _ | _ } ", 100, 100)); + coll.addRule(new SyntaxRule("shannon", "_ ? _ : _ ", 5, 5)); + + coll.addRule(new SyntaxRule("heap", "_ . _ @ _", 30, 30)); + + coll.addRule(new SyntaxRule("fcall", " f ( _ )", 30, 30)); + } + + @Test + public void testPrecedences() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("plus", "_ + _", 10, 10)); + coll.addRule(new SyntaxRule("mult", "_ * _", 20, 20)); + + assertEquals("plus[a,b]", parse("a + b")); + assertEquals("plus[a,mult[b,c]]", parse("a + b * c")); + assertEquals("plus[mult[a,b],c]", parse("a * b + c")); + assertEquals("mult[mult[a,b],c]", parse("a * b * c")); + } + + @Test + public void testComplexGrammar() throws Exception { + try { + addComplexGrammar(coll); + + assertEquals("plus[1,2]", parse("1 + 2")); + assertEquals("plus[7,mult[5,2]]", parse("7 + 5 * 2")); + assertEquals("plus[mult[7,5],2]", parse("7 * 5 + 2")); + assertEquals("mult[paren[plus[7,5]],2]", parse("( 7 + 5 ) * 2")); + assertEquals("plus[update[a,5,b],a]", parse("{ a := 5 } b + a")); + assertEquals("setex[a,subs[a,0],plus[a,5]]", parse("{ a . a - 0 | a + 5 }")); + assertEquals("shannon[plus[a,b],plus[c,d],plus[e,f]]", parse("a + b ? c + d : e + f")); + assertEquals("heap[paren[heap[o,f,h]],g,i]", parse("( o . f @ h ) . g @ i")); + assertEquals("heap[heap[o,f,h],g,i]", parse("o . f @ h . g @ i")); + assertEquals("plus[plus[1,1],1]", parse("1 + 1 + 1")); + assertEquals("exp[1,exp[1,1]]", parse("1 ^ 1 ^ 1")); + assertEquals("plus[a,mult[exp[b,c],d]]", parse("a + b ^ c * d")); + assertEquals("plus[mult[a,exp[b,c]],d]", parse("a * b ^ c + d")); + assertEquals("plus[a,mult[b,exp[c,d]]]", parse("a + b * c ^ d")); + assertEquals("mult[exp[a,b],c]", parse("a ^ b * c")); + assertEquals("mult[exp[a,minus[b]],c]", parse("a ^ - b * c")); + } catch (MixFixException mfe) { + System.err.println(mfe.getToken()); + throw mfe; + } + } + + @Test + public void testDevious() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("low", "_ + _ LOW", 10, 10)); + coll.addRule(new SyntaxRule("mult", "_ * _", 20, 20)); + coll.addRule(new SyntaxRule("high", "_ + _ HIGH", 40, 40)); + coll.addRule(new SyntaxRule("suffix", "_ +", 30, 1000)); + + assertEquals("low[a,b]", parse("a + b LOW")); + assertEquals("mult[a,high[b,c]]", parse("a * b + c HIGH")); + assertEquals("low[mult[a,b],c]", parse("a * b + c LOW")); + assertEquals("suffix[a]", parse("a +")); + assertEquals("mult[a,suffix[b]]", parse("a * b +")); + + assertEquals("mult[high[suffix[b],c],c]", parse("b + + c HIGH * c")); + } + + /* + * What if an inner token is the same as the beginning (led) token of an + * outer sequence? + * + * This is ambiguous: + * pre[b,inf[c,d]] and pre[inf[b,c],d] are both valid parse trees + */ + @Test + public void testInnerOuter() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("pre", "! _ : _ ", 5, 5)); + coll.addRule(new SyntaxRule("inf", "_ : _ ", 10, 10)); + + try { + parse("! b : c : d"); + fail("Grammar is ambiguous, should be noticed"); + } catch(MixFixException ex) { + } + } + + /* + * This is ambiguous: + * pre[inf[b,c], d] and inf[pre[b,c],d] are both valid parse trees + */ + @Test + public void testInnerOuter2() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("pre", "! _ : _ ", 50, 50)); + coll.addRule(new SyntaxRule("inf", "_ : _ ", 10, 10)); + + try { + parse("! b : c : d"); + fail("Grammar is ambiguous, should be noticed"); + } catch(MixFixException ex) { + } + } + + @Test + public void testInnerBinding() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("p", "_ + _", 20, 20)); + coll.addRule(new SyntaxRule("s", "_ | _ | _", 100, 100)); + + assertEquals("p[p[a,s[b,p[c,d],e]],f]", parse("a + b | c + d | e + f")); + } + + @Test + public void testAmbiguous() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("p", "_ + _", 20, 18)); + + assertEquals("p[a,p[b,c]]", parse("a + b + c")); + } + + @Test + public void testFunctions() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("funct_app", "F ( _ )", 50, 50)); + coll.addRule(new SyntaxRule("paren", "( _ )", 50, 50)); + coll.addRule(new SyntaxRule("prefix_F", "F _", 50, 50)); + + try { + parse("F ( x )"); + fail("Grammar is ambiguous, should be noticed"); + } catch(MixFixException ex) { + } + } + + @Test + public void testContinuation() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("eq", "_ = _", 50, 50)); + coll.addRule(new SyntaxRule("not", "! _", 45, 45)); + coll.addRule(new SyntaxRule("anot", "_ !! _", 100, 45)); + + assertEquals("eq[a,anot[x,eq[a,a]]]", parse("a = x !! a = a")); + assertEquals("eq[a,not[eq[a,a]]]", parse("a = ! a = a")); + } + + @Test + public void testSequenceParse() throws Exception { + coll.addRule(new IdentifierRule()); + SyntaxRule plusRule = new SyntaxRule("plus", "_ + _", 10, 10); + coll.addRule(plusRule); + coll.addRule(new SyntaxRule("mult", "_ * _", 20, 20)); + + ParseContext pc = + new ParseContext(parser, Arrays.asList("a + b * c".split(" "))) + .consumeToken().setResult("a"); + + ADTList> result = plusRule.parse(pc, 0); + assertEquals("ParseContext [curPos=5, maxBinding=10, result=plus[a,mult[b,c]]]", + result.hd().toString()); + assertEquals("ParseContext [curPos=3, maxBinding=10, result=plus[a,b]]", + result.tl().hd().toString()); + } + + @Test + public void testIfThenElse() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("ite", "if _ then _ else _", 0, 0)); + coll.addRule(new SyntaxRule("wite", "weakif _ then _ else _", 0, 40)); + coll.addRule(new SyntaxRule("plus", "_ + _", 20, 20)); + + assertEquals("ite[plus[a,b],plus[a,b],plus[a,b]]", + parse("if a + b then a + b else a + b")); + + assertEquals("plus[wite[plus[a,b],plus[a,b],a],b]", + parse("weakif a + b then a + b else a + b")); + } + + @Test + public void testVeryLargeGrammar() throws Exception { + for (int i = 0; i < 100; i++) { + coll.addRule(new SyntaxRule("lit-" + i, ""+i, 0, 0)); + coll.addRule(new SyntaxRule("no-" + i, "_ -" + i + "- _", i, i)); + } + + assertEquals("no-22[no-22[lit-1[],no-33[lit-2[],lit-3[]]],lit-4[]]", + parse("1 -22- 2 -33- 3 -22- 4")); + assertEquals("no-11[no-22[no-22[lit-1[],no-33[lit-2[],lit-3[]]]," + + "lit-4[]],no-77[no-99[lit-5[],lit-5[]],lit-1[]]]", + parse("1 -22- 2 -33- 3 -22- 4 -11- 5 -99- 5 -77- 1")); + } + + // was a bug + @Test + public void testLongerExpression() throws Exception { + coll.addRule(new IdentifierRule()); + coll.addRule(new SyntaxRule("plus", "_ + _", 10, 10)); + coll.addRule(new SyntaxRule("mult", "_ * _", 20, 20)); + + assertEquals("plus[plus[plus[plus[plus[a,mult[b,c]],d],e],f],g]", + parse("a + b * c + d + e + f + g")); + assertEquals("plus[plus[plus[plus[plus[a,b],mult[c,d]],e],f],g]", + parse("a + b + c * d + e + f + g")); + } +} \ No newline at end of file From e2483eea0796cbcdb2fb44a21104cfdf5d66fb93 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Thu, 22 Feb 2024 23:20:26 +0100 Subject: [PATCH 3/4] repair compile error and prepare grammar for mixfix --- key.core/src/main/antlr4/KeYLexer.g4 | 32 +- key.core/src/main/antlr4/KeYParser.g4 | 183 ++--------- .../nparser/builder/ExpressionBuilder.java | 283 +++++++++--------- .../key/nparser/builder/MixFixResolver.java | 2 +- 4 files changed, 174 insertions(+), 326 deletions(-) diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 7d51836971f..0d456186ad4 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -356,41 +356,12 @@ TILDE : '~' ; -PERCENT -: '%' - ; - -STAR -: '*' - ; - -MINUS -: '-' - ; - -PLUS -: '+' - ; - -GREATER -: '>' - ; - -GREATEREQUAL -: '>' '=' | '\u2265' - ; WS: [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ; -LESS: '<'; -LESSEQUAL: '<' '=' | '\u2264'; -LGUILLEMETS: '<' '<' | '«' | '‹'; -RGUILLEMETS: '>''>' | '»' | '›'; IMPLICIT_IDENT: '<' (LETTER)+ '>' ('$lmtd')? -> type(IDENT); -EQV: '<->' | '\u2194'; -PRIMES: ('\'')+; CHAR_LITERAL : '\'' ((' '..'&') | @@ -429,7 +400,8 @@ fragment IDCHAR: LETTER | DIGIT | '_' | '#' | '$'; IDENT: ( (LETTER | '_' | '#' | '$') (IDCHAR)*); -OPERATOR: [#_$%&!~?<+>-]+ ; +OPERATOR: ([*=#_$%&!~?<+>] | '-' | '\'' | '\u2265' | '\u2264' | '«' | '‹' + | '»' | '›' | '\u2194')+ ; MIXFIX_HOLE: '_' '/' DIGIT+ ; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 4eafb0ccd7c..75b3b355e9f 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -370,67 +370,17 @@ literals: ; 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 - | mixfix - ; - -mixfix: - TILDE (literals | simple_ident | OPERATOR | PLUS | MINUS | - LESS | LPAREN | RPAREN /* | ... */ )+ TILDE +term: + (literals | simple_ident | OPERATOR + | EQUALS | NOT_EQUALS | TILDE | EXP | SEMI | COMMA + | FORALL | EXISTS | SUBST | IF | IFEX | THEN | ELSE + | COLON | DOUBLECOLON | AND | OR | NOT | IMP | DOT + | MODALITY + // special case need to handled recursively because RBRACE and RPAREN are part + // of the FOLLOW set of term. + | LPAREN term RPAREN + | LBRACE term RBRACE + )+ ; /* @@ -484,109 +434,14 @@ term ; */ - -/** - * Access: a.b.c@f, T.staticQ() - */ -accessterm -: - // OLD - (sortId DOUBLECOLON)? - firstName=simple_ident - - /*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 + FLOAT_LITERAL #floatLiteral + | DOUBLE_LITERAL #doubleLiteral + | REAL_LITERAL #realLiteral ; char_literal: @@ -805,9 +660,17 @@ contracts RBRACE ; + +one_bound_variable +: + s=sortId? id=simple_ident +; + + invariants : - INVARIANTS LPAREN selfVar=one_bound_variable RPAREN + INVARIANTS LPAREN selfVar=one_bound_variable + RPAREN LBRACE (one_invariant)* RBRACE 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 07386591924..a79cc432552 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 @@ -55,7 +55,7 @@ public class ExpressionBuilder extends DefaultBuilder { public static final Logger LOGGER = LoggerFactory.getLogger(ExpressionBuilder.class); public static final String NO_HEAP_EXPRESSION_BEFORE_AT_EXCEPTION_MESSAGE = - "Expecting select term before '@', not: "; + "Expecting select term before '@', not: "; /** * The current abbreviation used for resolving "@name" terms. @@ -82,7 +82,7 @@ public ExpressionBuilder(Services services, NamespaceSet nss) { } public ExpressionBuilder(Services services, NamespaceSet nss, - Namespace schemaNamespace) { + Namespace schemaNamespace) { super(services, nss); setSchemaVariables(schemaNamespace); } @@ -90,8 +90,8 @@ public ExpressionBuilder(Services services, NamespaceSet nss, public static Term updateOrigin(Term t, ParserRuleContext ctx, Services services) { try { t = services.getTermFactory().createTermWithOrigin(t, - ctx.start.getTokenSource().getSourceName() + "@" + ctx.start.getLine() - + ":" + ctx.start.getCharPositionInLine() + 1); + ctx.start.getTokenSource().getSourceName() + "@" + ctx.start.getLine() + + ":" + ctx.start.getCharPositionInLine() + 1); } catch (ClassCastException ignored) { } return t; @@ -170,6 +170,7 @@ private static boolean isSelectTerm(Term term) { return term.op().name().toString().endsWith("::select") && term.arity() == 3; } + /* @Override public Term visitParallel_term(KeYParser.Parallel_termContext ctx) { List t = mapOf(ctx.elementary_update_term()); @@ -178,7 +179,7 @@ public Term visitParallel_term(KeYParser.Parallel_termContext ctx) { a = getTermFactory().createTerm(UpdateJunctor.PARALLEL_UPDATE, a, t.get(i)); } return updateOrigin(a, ctx, services); - } + }*/ @Override public Term visitTermEOF(KeYParser.TermEOFContext ctx) { @@ -186,12 +187,12 @@ public Term visitTermEOF(KeYParser.TermEOFContext ctx) { } @Override - public Term visitMixfix(KeYParser.MixfixContext ctx) { + public Term visitTerm(KeYParser.TermContext ctx) { try { return services.mixFixResolver.resolve(ctx); } catch (MixFixException e) { Object val = e.getToken(); - if(val instanceof Token token) { + if (val instanceof Token token) { throw new BuildingException(token, "Mixfix parser error", e); } else { throw new BuildingException(e); @@ -199,6 +200,32 @@ public Term visitMixfix(KeYParser.MixfixContext ctx) { } } + private Term binaryTerm(ParserRuleContext ctx, Operator operator, Term left, Term right) { + if (right == null) { + return updateOrigin(left, ctx, services); + } + return capsulateTf(ctx, + () -> updateOrigin(getTermFactory().createTerm(operator, left, right), ctx, services)); + } + + private Term binaryLDTSpecificTerm(ParserRuleContext ctx, String opname, Term last, Term cur) { + Sort sort = last.sort(); + if (sort == null) { + semanticError(ctx, "No sort for %s", last); + } + LDT ldt = services.getTypeConverter().getLDTFor(sort); + if (ldt == null) { + // falling back to integer ldt (for instance for untyped schema variables) + ldt = services.getTypeConverter().getIntegerLDT(); + } + Function op = ldt.getFunctionFor(opname, services); + if (op == null) { + semanticError(ctx, "Could not find function symbol '%s' for sort '%s'.", opname, sort); + } + return binaryTerm(ctx, op, last, cur); + } + + /* @Override public Term visitElementary_update_term(KeYParser.Elementary_update_termContext ctx) { Term a = accept(ctx.a); @@ -225,14 +252,6 @@ public Term visitEquivalence_term(KeYParser.Equivalence_termContext ctx) { return cur; } - private Term binaryTerm(ParserRuleContext ctx, Operator operator, Term left, Term right) { - if (right == null) { - return updateOrigin(left, ctx, services); - } - return capsulateTf(ctx, - () -> updateOrigin(getTermFactory().createTerm(operator, left, right), ctx, services)); - } - @Override public Term visitImplication_term(KeYParser.Implication_termContext ctx) { Term termL = accept(ctx.a); @@ -367,24 +386,6 @@ public Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx) { return last; } - private Term binaryLDTSpecificTerm(ParserRuleContext ctx, String opname, Term last, Term cur) { - Sort sort = last.sort(); - if (sort == null) { - semanticError(ctx, "No sort for %s", last); - } - LDT ldt = services.getTypeConverter().getLDTFor(sort); - if (ldt == null) { - // falling back to integer ldt (for instance for untyped schema variables) - ldt = services.getTypeConverter().getIntegerLDT(); - } - Function op = ldt.getFunctionFor(opname, services); - if (op == null) { - semanticError(ctx, "Could not find function symbol '%s' for sort '%s'.", opname, sort); - } - return binaryTerm(ctx, op, last, cur); - } - - @Override public Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx) { Term termL = accept(ctx.a); @@ -441,17 +442,17 @@ public Object visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx) } return term; } - + */ protected Term capsulateTf(ParserRuleContext ctx, Supplier termSupplier) { try { return termSupplier.get(); } catch (TermCreationException e) { throw new BuildingException(ctx, - String.format("Could not build term on: %s", ctx.getText()), e); + String.format("Could not build term on: %s", ctx.getText()), e); } } - @Override + /*@Override public Object visitBracket_term(KeYParser.Bracket_termContext ctx) { Term t = accept(ctx.primitive_labeled_term()); for (int i = 0; i < ctx.bracket_suffix_heap().size(); i++) { @@ -467,7 +468,7 @@ public Object visitBracket_term(KeYParser.Bracket_termContext ctx) { } return handleAttributes(t, ctx.attribute()); } - + */ /* * @Override public String * visitStaticAttributeOrQueryReference(KeYParser.StaticAttributeOrQueryReferenceContext ctx) { @@ -538,7 +539,7 @@ private Term toZNotation(BigInteger bi, Namespace functions) { for (int i = 0; i < s.length(); i++) { result = getTermFactory().createTerm(functions.lookup(new Name(s.substring(i, i + 1))), - result); + result); } if (negative) { @@ -620,7 +621,7 @@ private PairOfStringAndJavaBlock getJavaBlock(Token t) { jr.setSVNamespace(schemaVariables()); try { sjb.javaBlock = - jr.readBlockWithProgramVariables(programVariables(), cleanJava); + jr.readBlockWithProgramVariables(programVariables(), cleanJava); } catch (Exception e) { sjb.javaBlock = jr.readBlockWithEmptyContext(cleanJava); } @@ -675,8 +676,8 @@ public Term createAttributeTerm(Term prefix, Operator attribute, ParserRuleConte semanticError(null, "Cannot use schema variable " + sv + " as an attribute"); } result = getServices().getTermBuilder().select(sv.sort(), - getServices().getTermBuilder().getBaseHeap(), prefix, - capsulateTf(ctx, () -> getTermFactory().createTerm(attribute))); + getServices().getTermBuilder().getBaseHeap(), prefix, + capsulateTf(ctx, () -> getTermFactory().createTerm(attribute))); } else { if (attribute instanceof LogicVariable) { Term attrTerm = capsulateTf(ctx, () -> getTermFactory().createTerm(attribute)); @@ -686,7 +687,7 @@ public Term createAttributeTerm(Term prefix, Operator attribute, ParserRuleConte } else if (attribute == getServices().getJavaInfo().getArrayLength()) { Term finalResult = result; result = - capsulateTf(ctx, () -> getServices().getTermBuilder().dotLength(finalResult)); + capsulateTf(ctx, () -> getServices().getTermBuilder().dotLength(finalResult)); } else { ProgramVariable pv = (ProgramVariable) attribute; Function fieldSymbol = getServices().getTypeConverter().getHeapLDT() @@ -727,19 +728,19 @@ private Operator getAttributeInPrefixSort(Sort prefixSort, String attributeName) final KeYJavaType prefixKJT = javaInfo.getKeYJavaType(prefixSort); if (prefixKJT == null) { semanticError(null, - "Could not find type '" + prefixSort + "'. Maybe mispelled or " - + "you use an array or object type in a .key-file with missing " - + "\\javaSource section."); + "Could not find type '" + prefixSort + "'. Maybe mispelled or " + + "you use an array or object type in a .key-file with missing " + + "\\javaSource section."); } ProgramVariable var = - javaInfo.getCanonicalFieldProgramVariable(attributeName, prefixKJT); + javaInfo.getCanonicalFieldProgramVariable(attributeName, prefixKJT); if (var == null) { LogicVariable logicalvar = - (LogicVariable) namespaces().variables().lookup(attributeName); + (LogicVariable) namespaces().variables().lookup(attributeName); if (logicalvar == null) { semanticError(null, "There is no attribute '%s' declared in type '%s' and no " - + "logical variable of that name.", attributeName, prefixSort); + + "logical variable of that name.", attributeName, prefixSort); } else { result = logicalvar; } @@ -788,6 +789,7 @@ public Term visitString_literal(KeYParser.String_literalContext ctx) { return getServices().getTypeConverter().convertToLogicElement(new StringLiteral(s)); } + /* @Override public Object visitCast_term(KeYParser.Cast_termContext ctx) { Term result = accept(ctx.sub); @@ -808,6 +810,7 @@ public Object visitCast_term(KeYParser.Cast_termContext ctx) { SortDependingFunction castSymbol = s.getCastSymbol(getServices()); return getTermFactory().createTerm(castSymbol, result); } + */ private void markHeapAsExplicit(Term a) { explicitHeap.add(a); @@ -827,7 +830,7 @@ private void markHeapAsExplicit(Term a) { * kjt.getFullName()); } } } assert false; return null; } */ - @Override + /*@Override public Object visitBracket_access_heap_update(KeYParser.Bracket_access_heap_updateContext ctx) { Term heap = pop(); Term target = accept(ctx.target); @@ -837,7 +840,6 @@ public Object visitBracket_access_heap_update(KeYParser.Bracket_access_heap_upda return getServices().getTermBuilder().store(heap, objectTerm, fieldTerm, val); } - @Override public Object visitBracket_access_heap_term(KeYParser.Bracket_access_heap_termContext ctx) { Term heap = pop(); @@ -999,7 +1001,6 @@ public Term visitIfThenElseTerm(KeYParser.IfThenElseTermContext ctx) { () -> getTermFactory().createTerm(IfThenElse.IF_THEN_ELSE, condF, thenT, elseT)); } - @Override public Object visitIfExThenElseTerm(KeYParser.IfExThenElseTermContext ctx) { Namespace orig = variables(); @@ -1073,7 +1074,6 @@ public Object visitSubstitution_term(KeYParser.Substitution_termContext ctx) { unbindVars(orig); } } - @Override public Object visitUpdate_term(KeYParser.Update_termContext ctx) { Term t = oneOf(ctx.atom_prefix(), ctx.unary_formula()); @@ -1083,10 +1083,12 @@ public Object visitUpdate_term(KeYParser.Update_termContext ctx) { Term u = accept(ctx.u); return getTermFactory().createTerm(UpdateApplication.UPDATE_APPLICATION, u, t); } + */ + /* public List visitBound_variables(KeYParser.Bound_variablesContext ctx) { - return mapOf(ctx.one_bound_variable()); - } + return mapOf(ctx.one_bound_variable()); + }*/ @Override public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variableContext ctx) { @@ -1097,10 +1099,10 @@ public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variable if (ts != null) { if (!(ts instanceof VariableSV)) { semanticError(ctx, - ts + " is not allowed in a quantifier. Note, that you can't " - + "use the normal syntax for quantifiers of the form \"\\exists int i;\"" - + " in taclets. You have to define the variable as a schema variable" - + " and use the syntax \"\\exists i;\" instead."); + ts + " is not allowed in a quantifier. Note, that you can't " + + "use the normal syntax for quantifiers of the form \"\\exists int i;\"" + + " in taclets. You have to define the variable as a schema variable" + + " and use the syntax \"\\exists i;\" instead."); } bindVar(); return (QuantifiableVariable) ts; @@ -1111,7 +1113,7 @@ public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variable } QuantifiableVariable result = - doLookup(new Name(ctx.id.getText()), variables()); + doLookup(new Name(ctx.id.getText()), variables()); if (result == null) { semanticError(ctx, "There is no schema variable or variable named " + id); @@ -1120,55 +1122,66 @@ public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variable return result; } + /* + @Override + public Object visitModality_term(KeYParser.Modality_termContext ctx) { + Term a1 = accept(ctx.sub); + if (ctx.MODALITY() == null) { + return a1; + } - @Override - public Object visitModality_term(KeYParser.Modality_termContext ctx) { - Term a1 = accept(ctx.sub); - if (ctx.MODALITY() == null) { - return a1; - } + PairOfStringAndJavaBlock sjb = getJavaBlock(ctx.MODALITY().getSymbol()); + Operator op; + if (sjb.opName.charAt(0) == '#') { + op = - PairOfStringAndJavaBlock sjb = getJavaBlock(ctx.MODALITY().getSymbol()); - Operator op; - if (sjb.opName.charAt(0) == '#') { - /* - * if (!inSchemaMode()) { semanticError(ctx, - * "No schema elements allowed outside taclet declarations (" + sjb.opName + ")"); } - */ - op = schemaVariables().lookup(new Name(sjb.opName)); - } else { - op = Modality.getModality(sjb.opName); - } - if (op == null) { - semanticError(ctx, "Unknown modal operator: " + sjb.opName); - } + schemaVariables(). - return capsulateTf(ctx, - () -> getTermFactory().createTerm(op, new Term[] { a1 }, null, sjb.javaBlock)); - } + lookup(new Name(sjb.opName)); + } else{ + op =Modality. - @Override - public List visitArgument_list(KeYParser.Argument_listContext ctx) { - return mapOf(ctx.term()); - } + getModality(sjb.opName); + } + if(op ==null){ - @Override - public Object visitChar_literal(KeYParser.Char_literalContext ctx) { - String s = ctx.CHAR_LITERAL().getText(); - int intVal = 0; - if (s.length() == 3) { - intVal = s.charAt(1); - } else { - try { - intVal = Integer.parseInt(s.substring(3, s.length() - 1), 16); - } catch (NumberFormatException ex) { - semanticError(ctx, "'" + s + "' is not a valid character."); + semanticError(ctx, "Unknown modal operator: "+sjb.opName); } - } - return getTermFactory().createTerm(functions().lookup(new Name("C")), - toZNotation(String.valueOf(intVal), functions()).sub(0)); - } + return + + capsulateTf(ctx, + () -> + + getTermFactory(). + + createTerm(op, new Term[] { + a1 + },null,sjb.javaBlock)); + } + + /* @Override + public List visitArgument_list(KeYParser.Argument_listContext ctx) { + return mapOf(ctx.term()); + } + + @Override + public Object visitChar_literal(KeYParser.Char_literalContext ctx) { + String s = ctx.CHAR_LITERAL().getText(); + int intVal = 0; + if (s.length() == 3) { + intVal = s.charAt(1); + } else { + try { + intVal = Integer.parseInt(s.substring(3, s.length() - 1), 16); + } catch (NumberFormatException ex) { + semanticError(ctx, "'" + s + "' is not a valid character."); + } + } + return getTermFactory().createTerm(functions().lookup(new Name("C")), + toZNotation(String.valueOf(intVal), functions()).sub(0)); + } + */ public boolean isClass(String p) { return getJavaInfo().getTypeByClassName(p) != null; } @@ -1192,7 +1205,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { assert parts != null && varfuncid != null; boolean javaReference = - parts.size() > 1 && (isPackage(parts.get(0)) || isClass(parts.get(0))); + parts.size() > 1 && (isPackage(parts.get(0)) || isClass(parts.get(0))); if (javaReference) { return splitJava(parts); @@ -1206,7 +1219,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { if (varfuncid.endsWith(LIMIT_SUFFIX)) { varfuncid = varfuncid.substring(0, varfuncid.length() - 5); op = lookupVarfuncId(ctx, varfuncid, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); if (ObserverFunction.class.isAssignableFrom(op.getClass())) { op = getServices().getSpecificationRepository() .limitObs((ObserverFunction) op).first; @@ -1215,13 +1228,13 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { } } else { String firstName = - ctx.name == null ? ctx.INT_LITERAL().getText() - : ctx.name.simple_ident(0).getText(); + ctx.name == null ? ctx.INT_LITERAL().getText() + : ctx.name.simple_ident(0).getText(); op = lookupVarfuncId(ctx, firstName, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); if (op instanceof ProgramVariable v && ctx.name.simple_ident().size() > 1) { List otherParts = - ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size()); + ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size()); Term tv = getServices().getTermFactory().createTerm(v); String memberName = otherParts.get(0).getText(); if (v.sort() == getServices().getTypeConverter().getSeqLDT().targetSort()) { @@ -1229,7 +1242,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { return getServices().getTermBuilder().seqLen(tv); } else { semanticError(ctx, "There is no attribute '%s'for sequences (Seq), only " - + "'length' is supported.", memberName); + + "'length' is supported.", memberName); } } memberName = StringUtil.trim(memberName, "()"); @@ -1240,7 +1253,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { return op; } - private Term visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { + /*private Term visitAccesstermAsJava(KeYParser.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 @@ -1339,9 +1352,9 @@ private Term visitAccesstermAsJava(KeYParser.AccesstermContext ctx) { return current; } return null; - } + }*/ - @Override + /*@Override public Object visitTermParen(KeYParser.TermParenContext ctx) { Term base = accept(ctx.term()); if (ctx.attribute().isEmpty()) { @@ -1349,8 +1362,8 @@ public Object visitTermParen(KeYParser.TermParenContext ctx) { } return handleAttributes(base, ctx.attribute()); } - - private Term handleAttributes(Term current, List attribute) { + */ + /*private Term handleAttributes(Term current, List attribute) { for (int i = 0; i < attribute.size(); i++) { KeYParser.AttributeContext ctxSuffix = attribute.get(i); boolean isLast = i == attribute.size() - 1; @@ -1363,7 +1376,7 @@ private Term handleAttributes(Term current, List att return current; } else if (ctxSuffix instanceof KeYParser.Attribute_simpleContext) { KeYParser.Attribute_simpleContext attrid = - (KeYParser.Attribute_simpleContext) ctxSuffix; + (KeYParser.Attribute_simpleContext) ctxSuffix; String memberName = attrid.id.getText(); Sort seqSort = lookupSort("Seq"); if (current.sort() == seqSort) { @@ -1371,7 +1384,7 @@ private Term handleAttributes(Term current, List att return getServices().getTermBuilder().seqLen(current); } else { semanticError(ctxSuffix, "There is no attribute '%s'for sequences (Seq), " - + "only 'length' is supported.", memberName); + + "only 'length' is supported.", memberName); } } else { boolean isCall = attrid.call() != null; @@ -1387,7 +1400,7 @@ private Term handleAttributes(Term current, List att assert kjt != null; classRef = kjt.getFullName(); current = getServices().getJavaInfo().getProgramMethodTerm(current, - memberName, sfxargs, classRef, true); + memberName, sfxargs, classRef, true); } else { Operator attr = getAttributeInPrefixSort(current.sort(), memberName); current = createAttributeTerm(current, attr, ctxSuffix); @@ -1399,7 +1412,7 @@ private Term handleAttributes(Term current, List att } } else if (ctxSuffix instanceof KeYParser.Attribute_complexContext) { KeYParser.Attribute_complexContext attrid = - (KeYParser.Attribute_complexContext) ctxSuffix; + (KeYParser.Attribute_complexContext) ctxSuffix; Term heap = accept(attrid.heap); String classRef = attrid.sort.getText(); String memberName = attrid.id.getText(); @@ -1413,10 +1426,10 @@ private Term handleAttributes(Term current, List att assert kjt != null; classRef = kjt.getFullName(); current = getServices().getJavaInfo().getProgramMethodTerm(current, memberName, - sfxargs, classRef, false); + sfxargs, classRef, false); } else { Operator op = getAttributeInPrefixSort(getTypeByClassName(classRef).getSort(), - classRef + "::" + memberName); + classRef + "::" + memberName); current = createAttributeTerm(current, op, ctxSuffix); } @@ -1428,7 +1441,7 @@ private Term handleAttributes(Term current, List att KeYJavaType kjt = getServices().getJavaInfo().getKeYJavaType(sort); if (kjt == null) { semanticError(ctxSuffix, - "Found logic sort for %s but no corresponding java type!", classRef); + "Found logic sort for %s but no corresponding java type!", classRef); } } if (heap != null) { @@ -1437,7 +1450,7 @@ private Term handleAttributes(Term current, List att } } return current; - } + }*/ public T defaultOnException(T defaultValue, Supplier supplier) { try { @@ -1447,7 +1460,7 @@ public T defaultOnException(T defaultValue, Supplier supplier) { } } - @Override + /*@Override public Term visitAccessterm(KeYParser.AccesstermContext ctx) { Term t = visitAccesstermAsJava(ctx); if (t != null) { @@ -1531,12 +1544,12 @@ public Term visitAccessterm(KeYParser.AccesstermContext ctx) { current = handleAttributes(current, ctx.attribute()); return current; } - - private @Nullable Term[] visitArguments(KeYParser. @Nullable Argument_listContext call) { + */ + /*private @Nullable Term[] visitArguments(KeYParser.@Nullable Argument_listContext call) { List arguments = accept(call); return arguments == null ? null : arguments.toArray(new Term[0]); } - +*/ @Override public Object visitFloatLiteral(FloatLiteralContext ctx) { String txt = ctx.getText(); // full text of node incl. unary minus. @@ -1553,7 +1566,7 @@ public Object visitDoubleLiteral(DoubleLiteralContext ctx) { public Object visitRealLiteral(RealLiteralContext ctx) { String txt = ctx.getText(); // full text of node incl. unary minus. char lastChar = txt.charAt(txt.length() - 1); - if(lastChar == 'R' || lastChar == 'r') { + if (lastChar == 'R' || lastChar == 'r') { semanticError(ctx, "The given float literal does not have a suffix. This is essential to determine its exact meaning. You probably want to add 'r' as a suffix."); } throw new Error("not yet implemented"); @@ -1574,16 +1587,16 @@ private Term toCNotation(String number) { private Term toFPNotation(String number) { String decBitString = - Integer.toUnsignedString(Float.floatToIntBits(Float.parseFloat(number))); + Integer.toUnsignedString(Float.floatToIntBits(Float.parseFloat(number))); // toNum("0")); // soon to disappear return getTermFactory().createTerm(functions().lookup(new Name("FP")), toNum(decBitString)); } private Term toDFPNotation(String number) { String decBitString = - Long.toUnsignedString(Double.doubleToLongBits(Double.parseDouble(number))); + Long.toUnsignedString(Double.doubleToLongBits(Double.parseDouble(number))); return getTermFactory().createTerm(functions().lookup(new Name("DFP")), - toNum(decBitString)); // toNum("0")); // soon to disappear + toNum(decBitString)); // toNum("0")); // soon to disappear } private Term toNum(String number) { @@ -1709,7 +1722,7 @@ private boolean isIntTerm(Term reference) { } private ImmutableSet lookupOperatorSV(String opName, - ImmutableSet modalities) { + ImmutableSet modalities) { SchemaVariable sv = schemaVariables().lookup(new Name(opName)); if (!(sv instanceof ModalOperatorSV)) { semanticError(null, "Schema variable " + opName + " not defined."); @@ -1743,13 +1756,13 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) { // term); return term; } - Term[] params = new Term[] { heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2) }; + Term[] params = new Term[]{heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2)}; return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); + () -> getServices().getTermFactory().createTerm(term.op(), params)); } else if (term.op() instanceof ObserverFunction) { if (!isImplicitHeap(term.sub(0))) { semanticError(null, "Expecting program variable heap as first argument of: %s", - term); + term); } Term[] params = new Term[term.arity()]; @@ -1760,7 +1773,7 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) { } return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); + () -> getServices().getTermFactory().createTerm(term.op(), params)); } return term; @@ -1772,7 +1785,7 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) { protected Term heapSelectionSuffix(Term term, Term heap, ParserRuleContext ctx) { if (!isHeapTerm(heap)) { semanticError(null, "Expecting term of type Heap but sort is %s for term %s", - heap.sort(), term); + heap.sort(), term); } Term result = replaceHeap(term, heap, ctx); return result; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java index 1f8ae9b6e63..4a85caa0b56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java @@ -33,7 +33,7 @@ public MixFixResolver(Services services) { // ... others as well } - public Term resolve(KeYParser.MixfixContext ctx) throws MixFixException { + public Term resolve(KeYParser.TermContext ctx) throws MixFixException { List tokens = extractTokens(ctx); // Currently there is ~ at the beginning and end of mixfix parts tokens.remove(0); From 0c67fd61ff41bb3a1fcc855342498d4ec71d465c Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Thu, 22 Feb 2024 23:30:55 +0100 Subject: [PATCH 4/4] faster de.uka.ilkd.key.nparser.ExprTest --- .../de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java | 3 +++ .../de/uka/ilkd/key/nparser/builder/MixFixResolver.java | 2 +- .../src/test/java/de/uka/ilkd/key/nparser/ExprTest.java | 6 +++++- 3 files changed, 9 insertions(+), 2 deletions(-) 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 a79cc432552..4209fd74287 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 @@ -34,6 +34,9 @@ import de.uka.ilkd.key.util.parsing.BuildingException; import edu.kit.kastel.formal.mixfix.MixFixException; +import org.antlr.v4.runtime.RuleContext; +import org.antlr.v4.runtime.tree.ParseTree; +import org.antlr.v4.runtime.tree.TerminalNode; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java index 4a85caa0b56..84dee22314c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/MixFixResolver.java @@ -43,7 +43,7 @@ public Term resolve(KeYParser.TermContext ctx) throws MixFixException { } public static List extractTokens(ParserRuleContext ctx) { - List result = new ArrayList(); + List result = new ArrayList<>(1024); extractTokens(result, ctx); return result; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java index 125a42fe935..876017bedfd 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java @@ -41,12 +41,16 @@ public void parseAndVisit(String expr) throws IOException { } } + public static KeyIO io; + private KeyIO getIo() throws IOException { + if(io!=null) return io; + Services services = new Services(new JavaProfile()); String p = "/de/uka/ilkd/key/proof/rules/ldt.key"; URL url = getClass().getResource(p); Assumptions.assumeTrue(url != null); - KeyIO io = new KeyIO(services); + io = new KeyIO(services); io.load(url).parseFile().loadDeclarations().loadSndDegreeDeclarations(); NamespaceBuilder nssb = new NamespaceBuilder(services.getNamespaces());