.
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
+ *
+ * - Wieland, Jacob. Parsing Mixfix Expressions.
+ * Dealing with User-Defined Mixfix Operators Efficiently
+ * - http://effbot.org/zone/simple-top-down-parsing.htm
+ *
+ *
+ * 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
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..0d456186ad4 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';
@@ -355,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
: '\''
((' '..'&') |
@@ -428,6 +400,11 @@ fragment IDCHAR: LETTER | DIGIT | '_' | '#' | '$';
IDENT: ( (LETTER | '_' | '#' | '$') (IDCHAR)*);
+OPERATOR: ([*=#_$%&!~?<+>] | '-' | '\'' | '\u2265' | '\u2264' | '«' | '‹'
+ | '»' | '›' | '\u2194')+ ;
+
+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..75b3b355e9f 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);
@@ -363,61 +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
+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
+ )+
;
/*
@@ -471,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:
@@ -792,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/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..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
@@ -29,9 +29,14 @@
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.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;
@@ -53,7 +58,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.
@@ -80,7 +85,7 @@ public ExpressionBuilder(Services services, NamespaceSet nss) {
}
public ExpressionBuilder(Services services, NamespaceSet nss,
- Namespace schemaNamespace) {
+ Namespace schemaNamespace) {
super(services, nss);
setSchemaVariables(schemaNamespace);
}
@@ -88,8 +93,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;
@@ -168,6 +173,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());
@@ -176,13 +182,53 @@ 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) {
return accept(ctx.term());
}
+ @Override
+ public Term visitTerm(KeYParser.TermContext 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);
+ }
+ }
+ }
+
+ 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);
@@ -209,14 +255,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);
@@ -351,24 +389,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);
@@ -425,17 +445,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++) {
@@ -451,7 +471,7 @@ public Object visitBracket_term(KeYParser.Bracket_termContext ctx) {
}
return handleAttributes(t, ctx.attribute());
}
-
+ */
/*
* @Override public String
* visitStaticAttributeOrQueryReference(KeYParser.StaticAttributeOrQueryReferenceContext ctx) {
@@ -522,7 +542,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) {
@@ -604,7 +624,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);
}
@@ -659,8 +679,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));
@@ -670,7 +690,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()
@@ -711,19 +731,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;
}
@@ -772,6 +792,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);
@@ -792,6 +813,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);
@@ -811,7 +833,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);
@@ -821,7 +843,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();
@@ -983,7 +1004,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();
@@ -1057,7 +1077,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());
@@ -1067,10 +1086,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) {
@@ -1081,10 +1102,10 @@ public QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variable
if (ts != null) {
if (!(ts instanceof VariableSV)) {
semanticError(ctx,
- ts + " is not allowed in a quantifier. Note, that you can't "
- + "use the normal syntax for quantifiers of the form \"\\exists int i;\""
- + " in taclets. You have to define the variable as a schema variable"
- + " and use the syntax \"\\exists i;\" instead.");
+ ts + " is not allowed in a quantifier. Note, that you can't "
+ + "use the normal syntax for quantifiers of the form \"\\exists int i;\""
+ + " in taclets. You have to define the variable as a schema variable"
+ + " and use the syntax \"\\exists i;\" instead.");
}
bindVar();
return (QuantifiableVariable) ts;
@@ -1095,7 +1116,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);
@@ -1104,55 +1125,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;
}
@@ -1176,7 +1208,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) {
assert parts != null && varfuncid != null;
boolean javaReference =
- parts.size() > 1 && (isPackage(parts.get(0)) || isClass(parts.get(0)));
+ parts.size() > 1 && (isPackage(parts.get(0)) || isClass(parts.get(0)));
if (javaReference) {
return splitJava(parts);
@@ -1190,7 +1222,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) {
if (varfuncid.endsWith(LIMIT_SUFFIX)) {
varfuncid = varfuncid.substring(0, varfuncid.length() - 5);
op = lookupVarfuncId(ctx, varfuncid,
- ctx.sortId() != null ? ctx.sortId().getText() : null, sortId);
+ ctx.sortId() != null ? ctx.sortId().getText() : null, sortId);
if (ObserverFunction.class.isAssignableFrom(op.getClass())) {
op = getServices().getSpecificationRepository()
.limitObs((ObserverFunction) op).first;
@@ -1199,13 +1231,13 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) {
}
} else {
String firstName =
- ctx.name == null ? ctx.INT_LITERAL().getText()
- : ctx.name.simple_ident(0).getText();
+ ctx.name == null ? ctx.INT_LITERAL().getText()
+ : ctx.name.simple_ident(0).getText();
op = lookupVarfuncId(ctx, firstName,
- ctx.sortId() != null ? ctx.sortId().getText() : null, sortId);
+ ctx.sortId() != null ? ctx.sortId().getText() : null, sortId);
if (op instanceof ProgramVariable v && ctx.name.simple_ident().size() > 1) {
List otherParts =
- ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size());
+ ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size());
Term tv = getServices().getTermFactory().createTerm(v);
String memberName = otherParts.get(0).getText();
if (v.sort() == getServices().getTypeConverter().getSeqLDT().targetSort()) {
@@ -1213,7 +1245,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, "()");
@@ -1224,7 +1256,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
@@ -1323,9 +1355,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()) {
@@ -1333,8 +1365,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;
@@ -1347,7 +1379,7 @@ private Term handleAttributes(Term current, List att
return current;
} else if (ctxSuffix instanceof KeYParser.Attribute_simpleContext) {
KeYParser.Attribute_simpleContext attrid =
- (KeYParser.Attribute_simpleContext) ctxSuffix;
+ (KeYParser.Attribute_simpleContext) ctxSuffix;
String memberName = attrid.id.getText();
Sort seqSort = lookupSort("Seq");
if (current.sort() == seqSort) {
@@ -1355,7 +1387,7 @@ private Term handleAttributes(Term current, List att
return getServices().getTermBuilder().seqLen(current);
} else {
semanticError(ctxSuffix, "There is no attribute '%s'for sequences (Seq), "
- + "only 'length' is supported.", memberName);
+ + "only 'length' is supported.", memberName);
}
} else {
boolean isCall = attrid.call() != null;
@@ -1371,7 +1403,7 @@ private Term handleAttributes(Term current, List att
assert kjt != null;
classRef = kjt.getFullName();
current = getServices().getJavaInfo().getProgramMethodTerm(current,
- memberName, sfxargs, classRef, true);
+ memberName, sfxargs, classRef, true);
} else {
Operator attr = getAttributeInPrefixSort(current.sort(), memberName);
current = createAttributeTerm(current, attr, ctxSuffix);
@@ -1383,7 +1415,7 @@ private Term handleAttributes(Term current, List att
}
} else if (ctxSuffix instanceof KeYParser.Attribute_complexContext) {
KeYParser.Attribute_complexContext attrid =
- (KeYParser.Attribute_complexContext) ctxSuffix;
+ (KeYParser.Attribute_complexContext) ctxSuffix;
Term heap = accept(attrid.heap);
String classRef = attrid.sort.getText();
String memberName = attrid.id.getText();
@@ -1397,10 +1429,10 @@ private Term handleAttributes(Term current, List att
assert kjt != null;
classRef = kjt.getFullName();
current = getServices().getJavaInfo().getProgramMethodTerm(current, memberName,
- sfxargs, classRef, false);
+ sfxargs, classRef, false);
} else {
Operator op = getAttributeInPrefixSort(getTypeByClassName(classRef).getSort(),
- classRef + "::" + memberName);
+ classRef + "::" + memberName);
current = createAttributeTerm(current, op, ctxSuffix);
}
@@ -1412,7 +1444,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) {
@@ -1421,7 +1453,7 @@ private Term handleAttributes(Term current, List att
}
}
return current;
- }
+ }*/
public T defaultOnException(T defaultValue, Supplier supplier) {
try {
@@ -1431,7 +1463,7 @@ public T defaultOnException(T defaultValue, Supplier supplier) {
}
}
- @Override
+ /*@Override
public Term visitAccessterm(KeYParser.AccesstermContext ctx) {
Term t = visitAccesstermAsJava(ctx);
if (t != null) {
@@ -1515,12 +1547,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.
@@ -1537,7 +1569,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");
@@ -1558,16 +1590,16 @@ private Term toCNotation(String number) {
private Term toFPNotation(String number) {
String decBitString =
- Integer.toUnsignedString(Float.floatToIntBits(Float.parseFloat(number)));
+ Integer.toUnsignedString(Float.floatToIntBits(Float.parseFloat(number)));
// toNum("0")); // soon to disappear
return getTermFactory().createTerm(functions().lookup(new Name("FP")), toNum(decBitString));
}
private Term toDFPNotation(String number) {
String decBitString =
- Long.toUnsignedString(Double.doubleToLongBits(Double.parseDouble(number)));
+ Long.toUnsignedString(Double.doubleToLongBits(Double.parseDouble(number)));
return getTermFactory().createTerm(functions().lookup(new Name("DFP")),
- toNum(decBitString)); // toNum("0")); // soon to disappear
+ toNum(decBitString)); // toNum("0")); // soon to disappear
}
private Term toNum(String number) {
@@ -1693,7 +1725,7 @@ private boolean isIntTerm(Term reference) {
}
private ImmutableSet lookupOperatorSV(String opName,
- ImmutableSet modalities) {
+ ImmutableSet modalities) {
SchemaVariable sv = schemaVariables().lookup(new Name(opName));
if (!(sv instanceof ModalOperatorSV)) {
semanticError(null, "Schema variable " + opName + " not defined.");
@@ -1727,13 +1759,13 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) {
// term);
return term;
}
- Term[] params = new Term[] { heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2) };
+ Term[] params = new Term[]{heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2)};
return capsulateTf(ctx,
- () -> getServices().getTermFactory().createTerm(term.op(), params));
+ () -> getServices().getTermFactory().createTerm(term.op(), params));
} else if (term.op() instanceof ObserverFunction) {
if (!isImplicitHeap(term.sub(0))) {
semanticError(null, "Expecting program variable heap as first argument of: %s",
- term);
+ term);
}
Term[] params = new Term[term.arity()];
@@ -1744,7 +1776,7 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) {
}
return capsulateTf(ctx,
- () -> getServices().getTermFactory().createTerm(term.op(), params));
+ () -> getServices().getTermFactory().createTerm(term.op(), params));
}
return term;
@@ -1756,7 +1788,7 @@ private Term replaceHeap0(Term term, Term heap, ParserRuleContext ctx) {
protected Term heapSelectionSuffix(Term term, Term heap, ParserRuleContext ctx) {
if (!isHeapTerm(heap)) {
semanticError(null, "Expecting term of type Heap but sort is %s for term %s",
- heap.sort(), term);
+ heap.sort(), term);
}
Term result = replaceHeap(term, heap, ctx);
return result;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java
index 69785ef1614..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..84dee22314c
--- /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.TermContext 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<>(1024);
+ 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.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());
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'