Overloaded Operators for KeY lang

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

@@ -28,6 +28,7 @@ decls
     | schema_var_decls
     | pred_decls
     | func_decls
+    | adt_decls
     | transform_decls
     | ruleset_decls
     | contracts             // for problems
@@ -212,6 +213,7 @@ pred_decl
   pred_name = funcpred_name
   (whereToBind=where_to_bind)?
   argSorts=arg_sorts
+  functionMetaData?
   SEMI
 ;
 
@@ -228,18 +230,47 @@ func_decl
   func_name = funcpred_name
 	whereToBind=where_to_bind?
   argSorts = arg_sorts
+  functionMetaData?
   SEMI
 ;
 
+/**
+ \datatypes {
+    List = Nil | Cons(any, List);
+ }
+ */
+adt_decl
+:
+  doc=DOC_COMMENT? (UNIQUE)?
+  name=funcpred_name
+  EQUALS
+  adt_constructor (OR adt_constructor)*
+  SEMI
+;
+
+adt_constructor
+:
+    doc=DOC_COMMENT? funcpred_name                                      #adt_constructor_base
+  | doc=DOC_COMMENT? funcpred_name LPAREN sortId (COMMA sortId)* RPAREN #adt_constructor_recursion
+;
+
+functionMetaData
+:
+    INFIX LPAREN op=(PLUS|STAR|SLASH|MINUS|EXP|PERCENT|LESS|LESSEQUAL|GREATER|GREATEREQUAL|LGUILLEMETS) RPAREN
+  | PREFIX LPAREN op=(MINUS|TILDE) RPAREN
+  | POSTFIX LPAREN (/*currently no overloaded operator*/) RPAREN
+  | SHORTCUT LPAREN IDENT RPAREN
+;
+
 func_decls
-    :
-        FUNCTIONS
-        LBRACE
-        (
-            func_decl
-        ) *
-        RBRACE
-    ;
+:
+    FUNCTIONS LBRACE (func_decl)* RBRACE
+;
+
+adt_decls
+:
+  DATATYPES LBRACE adt_decl* RBRACE
+;
 
 
 // like arg_sorts but admits also the keyword "\formula"
@@ -346,10 +377,10 @@ unary_formula:
   | 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) b=weak_arith_term)?;
+comparison_term: a=weak_arith_term (op=(LESS|LESSEQUAL|GREATER|GREATEREQUAL) b=weak_arith_term)?;
 weak_arith_term: a=strong_arith_term_1 (op+=(PLUS|MINUS) 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 ((PERCENT|SLASH) b=strong_arith_term_2)?;
+strong_arith_term_2: a=atom_prefix (op=(PERCENT|SLASH) b=strong_arith_term_2)?;
 update_term: (LBRACE u=term RBRACE) (atom_prefix | unary_formula);
 substitution_term:
  LBRACE SUBST  bv=one_bound_variable SEMI

key/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java

@@ -19,14 +19,14 @@
 import de.uka.ilkd.key.util.Debug;
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 import recoder.service.ConstantEvaluator;
-import recoder.service.KeYCrossReferenceSourceInfo;
 
 import java.util.Collection;
+import java.util.Collections;
+import java.util.Collection;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.Map;
 
@@ -112,10 +112,6 @@ public CharListLDT getCharListLDT() {
         return (CharListLDT) getLDT(CharListLDT.NAME);
     }
 
-    public Collection<LDT> getLDTs() {
-        return LDTs.values();
-    }
-
     private Term translateOperator(de.uka.ilkd.key.java.expression.Operator op, ExecutionContext ec) {
 
         final Term[] subs = new Term[op.getArity()];
@@ -395,6 +391,7 @@ private Term convertLiteralExpression(Literal lit) {
 
 
     // TODO Adapt for @Reals
+
     /**
      * performs binary numeric promotion on the argument types
      */
@@ -444,39 +441,39 @@ else if ((t1 == PrimitiveType.JAVA_BOOLEAN &&
             return type1;
         } else if (type2.equals(services.getJavaInfo().getKeYJavaType("java.lang.String"))) {
             return type2;
-    	} else if ((t2 == PrimitiveType.JAVA_FLOAT) &&
-                (t1 == PrimitiveType.JAVA_BYTE||
-                        t1 == PrimitiveType.JAVA_SHORT||
-                        t1 == PrimitiveType.JAVA_INT||
-                        t1 == PrimitiveType.JAVA_CHAR||
-                        t1 == PrimitiveType.JAVA_LONG||
-			t1 == PrimitiveType.JAVA_FLOAT)) {
+        } else if ((t2 == PrimitiveType.JAVA_FLOAT) &&
+                (t1 == PrimitiveType.JAVA_BYTE ||
+                        t1 == PrimitiveType.JAVA_SHORT ||
+                        t1 == PrimitiveType.JAVA_INT ||
+                        t1 == PrimitiveType.JAVA_CHAR ||
+                        t1 == PrimitiveType.JAVA_LONG ||
+                        t1 == PrimitiveType.JAVA_FLOAT)) {
             return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_FLOAT);
-    	} else if ((t1 == PrimitiveType.JAVA_FLOAT) &&
-                (t2 == PrimitiveType.JAVA_BYTE||
-                        t2 == PrimitiveType.JAVA_SHORT||
-                        t2 == PrimitiveType.JAVA_INT||
-                        t2 == PrimitiveType.JAVA_CHAR||
-                        t2 == PrimitiveType.JAVA_LONG||
-			t2 == PrimitiveType.JAVA_FLOAT)) {
+        } else if ((t1 == PrimitiveType.JAVA_FLOAT) &&
+                (t2 == PrimitiveType.JAVA_BYTE ||
+                        t2 == PrimitiveType.JAVA_SHORT ||
+                        t2 == PrimitiveType.JAVA_INT ||
+                        t2 == PrimitiveType.JAVA_CHAR ||
+                        t2 == PrimitiveType.JAVA_LONG ||
+                        t2 == PrimitiveType.JAVA_FLOAT)) {
             return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_FLOAT);
-    	} else if ((t2 == PrimitiveType.JAVA_DOUBLE) &&
-                (t1 == PrimitiveType.JAVA_BYTE||
-                        t1 == PrimitiveType.JAVA_SHORT||
-                        t1 == PrimitiveType.JAVA_INT||
-                        t1 == PrimitiveType.JAVA_CHAR||
-                        t1 == PrimitiveType.JAVA_LONG||
-                        t1 == PrimitiveType.JAVA_FLOAT||
-			t1 == PrimitiveType.JAVA_DOUBLE)) {
+        } else if ((t2 == PrimitiveType.JAVA_DOUBLE) &&
+                (t1 == PrimitiveType.JAVA_BYTE ||
+                        t1 == PrimitiveType.JAVA_SHORT ||
+                        t1 == PrimitiveType.JAVA_INT ||
+                        t1 == PrimitiveType.JAVA_CHAR ||
+                        t1 == PrimitiveType.JAVA_LONG ||
+                        t1 == PrimitiveType.JAVA_FLOAT ||
+                        t1 == PrimitiveType.JAVA_DOUBLE)) {
             return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_DOUBLE);
-    	} else if ((t1 == PrimitiveType.JAVA_DOUBLE) &&
-                (t2 == PrimitiveType.JAVA_BYTE||
-                        t2 == PrimitiveType.JAVA_SHORT||
-                        t2 == PrimitiveType.JAVA_INT||
-                        t2 == PrimitiveType.JAVA_CHAR||
-                        t2 == PrimitiveType.JAVA_LONG||
-                        t2 == PrimitiveType.JAVA_FLOAT||
-			t2 == PrimitiveType.JAVA_DOUBLE)) {
+        } else if ((t1 == PrimitiveType.JAVA_DOUBLE) &&
+                (t2 == PrimitiveType.JAVA_BYTE ||
+                        t2 == PrimitiveType.JAVA_SHORT ||
+                        t2 == PrimitiveType.JAVA_INT ||
+                        t2 == PrimitiveType.JAVA_CHAR ||
+                        t2 == PrimitiveType.JAVA_LONG ||
+                        t2 == PrimitiveType.JAVA_FLOAT ||
+                        t2 == PrimitiveType.JAVA_DOUBLE)) {
             return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_DOUBLE);
         } else {
             throw new RuntimeException("Could not determine promoted type "
@@ -511,10 +508,10 @@ else if (t1 == PrimitiveType.JAVA_BIGINT)
             return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_BIGINT);
         else if (t1 == PrimitiveType.JAVA_REAL)
             return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_REAL);
-	else if (t1 == PrimitiveType.JAVA_FLOAT)
-	    return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_FLOAT);
-	else if (t1 == PrimitiveType.JAVA_DOUBLE)
-	    return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_DOUBLE);
+        else if (t1 == PrimitiveType.JAVA_FLOAT)
+            return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_FLOAT);
+        else if (t1 == PrimitiveType.JAVA_DOUBLE)
+            return services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_DOUBLE);
         else throw new RuntimeException("Could not determine promoted type " +
                     "of " + type1);
     }
@@ -1024,4 +1021,7 @@ private LDT getResponsibleLDT(de.uka.ilkd.key.java.expression.Operator op, Term[
         return null;
     }
 
+    public Collection<LDT> getLDTs() {
+        return Collections.unmodifiableCollection(LDTs.values());
+    }
 }

key/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java

@@ -252,13 +252,9 @@ public final Type getType(Term t) {
 	return null;
     }
 
-    @Nullable
-    @Override
-    public Function getFunctionFor(String operationName, Services services) {
-        switch (operationName) {
-			// This is not very elegant; but seqConcat is actually in the SeqLDT.
-            case "add": return services.getNamespaces().functions().lookup("seqConcat");
-            default: return null;
-        }
-    }
+	@Nullable
+	@Override
+	public Function getFunctionFor(String operatorSymbol, Services services) {
+		return services.getTypeConverter().getSeqLDT().getFunctionFor(operatorSymbol, services);
+	}
 }

key/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java

@@ -164,19 +164,9 @@ public Term translateLiteral(Literal lit, Services services) {
         return services.getTermBuilder().dfpTerm(doubleVal);
     }
 
-    @Override
-    public Function getFunctionFor(String op, Services services) {
-        switch (op) {
-            case "gt": return getGreaterThan();
-            case "geq": return getGreaterOrEquals();
-            case "lt": return getLessThan();
-            case "leq": return getLessOrEquals();
-            case "div": return getDiv();
-            case "mul": return getMul();
-            case "add": return getAdd();
-            case "sub": return getSub();
-            case "neg": return getNeg();
 
+/*    @Override
+    public Function getFunctionFor(String operatorSymbol, Services services) {
             // Floating point extensions with "\fp_"
             case "nan": return getIsNaN();
             case "zero": return getIsZero();
@@ -189,7 +179,7 @@ public Function getFunctionFor(String op, Services services) {
             case "normal": return getIsNormal();
         }
         return null;
-    }
+    }*/
 
     @Override
     public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op,

key/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java

@@ -174,19 +174,8 @@ public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op,
         }
     }
 
-    @Override
-    public Function getFunctionFor(String op, Services services) {
-        switch (op) {
-            case "gt": return getGreaterThan();
-            case "geq": return getGreaterOrEquals();
-            case "lt": return getLessThan();
-            case "leq": return getLessOrEquals();
-            case "div": return getDiv();
-            case "mul": return getMul();
-            case "add": return getAdd();
-            case "sub": return getSub();
-            case "neg": return getNeg();
-            // Floating point extensions with "\fp_"
+/*    @Override
+    public Function getFunctionFor(String operatorSymbol, Services services) {
             case "nan": return getIsNaN();
             case "zero": return getIsZero();
             case "infinite": return getIsInfinite();
@@ -195,10 +184,13 @@ public Function getFunctionFor(String op, Services services) {
             case "negative": return getIsNegative();
             case "positive": return getIsPositive();
             case "subnormal": return getIsSubnormal();
-            case "normal": return getIsNormal();
+
+                        case "normal": return getIsNormal();
+
         }
         return null;
     }
+ */
 
     @Override
     public boolean hasLiteralFunction(Function f) {

key/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java

@@ -484,23 +484,6 @@ public Function getFunctionFor(
         }
     }
 
-    @Nullable
-    @Override
-    public Function getFunctionFor(String op, Services services) {
-        switch (op) {
-            case "gt": return getGreaterThan();
-            case "geq": return getGreaterOrEquals();
-            case "lt": return getLessThan();
-            case "leq": return getLessOrEquals();
-            case "div": return getDiv();
-            case "mul": return getMul();
-            case "add": return getAdd();
-            case "sub": return getSub();
-            case "mod": return getMod();
-            case "neg": return getNeg();
-        }
-        return null;
-    }
 
     @Override
     public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, 

key/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java

@@ -1,8 +1,10 @@
 package de.uka.ilkd.key.ldt;
 
+import java.util.Collection;
 import java.util.Map;
 import java.util.TreeMap;
 
+import de.uka.ilkd.key.logic.op.MixFitInfo;
 import org.key_project.util.ExtList;
 
 import de.uka.ilkd.key.java.Expression;
@@ -235,21 +237,35 @@ public abstract Function getFunctionFor(
 
     /**
      * get the function in this LDT for an operation identified by generic
-     * operationName. If the LDT does not support this named function, it should
+     * operatorSymbol. If the LDT does not support this named function, it should
      * return null.
      *
      * This is used to resolve overloaded symbols.
      *
      * For example: "+" may map to "add" for integers, and to "addFloat" for
      * floats.
      *
-     * @param operationName non-null operationName for a generic function
+     * @param operatorSymbol non-null operatorSymbol for a generic function
      * @param services      services to use
      * @return reference to the respective LDT-specific function for the
      * operation, null if not available
      */
-    public @Nullable Function getFunctionFor(String operationName, Services services) {
-        // by default an LDT does not support overloaded symbols
+    public @Nullable Function getFunctionFor(String operatorSymbol, Services services) {
+        return getFunctionFor(operatorSymbol, MixFitInfo.Kind.INFIX, services);
+
+    }
+    public @Nullable Function getFunctionFor(String operatorSymbol, MixFitInfo.Kind kind, Services services) {
+        for (Operator operator : functions.allElements()) {
+            if(operator instanceof Function) {
+                var op = (Function) operator;
+                if (op.getMixFitInfo() != null) {
+                    var mfi = op.getMixFitInfo();
+                    if (kind == mfi.getKind() && mfi.symbol.equals(operatorSymbol)) {
+                        return op;
+                    }
+                }
+            }
+        }
         return null;
     }
 
@@ -259,4 +275,8 @@ public abstract Function getFunctionFor(
     public abstract Expression translateTerm(Term t, ExtList children, Services services);
 
     public abstract Type getType(Term t);
+
+    public Collection<Operator> getFunctions() {
+        return functions.allElements();
+    }
 }