implement the discussion of KaKeY

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java

@@ -18,10 +18,14 @@
 import de.uka.ilkd.key.nparser.ParsingFacade;
 import de.uka.ilkd.key.rule.RuleSet;
 
+import de.uka.ilkd.key.util.parsing.BuildingIssue;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableSet;
 
 import org.antlr.v4.runtime.Token;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+import recoder.util.Debug;
 
 /**
  * This visitor evaluates all basic (level 0) declarations. This includes:
@@ -41,6 +45,7 @@
  */
 public class DeclarationBuilder extends DefaultBuilder {
     private final Map<String, String> category2Default = new HashMap<>();
+    private static final Logger LOGGER = LoggerFactory.getLogger(DeclarationBuilder.class);
 
     public DeclarationBuilder(Services services, NamespaceSet nss) {
         super(services, nss);
@@ -154,7 +159,11 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
                 sorts().add(s);
                 createdSorts.add(s);
             } else {
-                addWarning(ctx, "Sort declaration is ignored, due to collision.");
+                // weigl: agreement on KaKeY meeting: this should be ignored until we finally have local namespaces
+                // for generic sorts
+                //addWarning(ctx, "Sort declaration is ignored, due to collision.");
+                LOGGER.info("Sort declaration is ignored, due to collision in {}",
+                        BuilderHelpers.getPosition(ctx));
             }
         }
         return createdSorts;

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java

@@ -86,7 +86,7 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) {
     public Object visitFunc_decl(KeYParser.Func_declContext ctx) {
         boolean unique = ctx.UNIQUE() != null;
         Sort retSort = accept(ctx.sortId());
-        String func_name = accept(ctx.funcpred_name());
+        String funcName = accept(ctx.funcpred_name());
         List<Boolean[]> whereToBind = accept(ctx.where_to_bind());
         List<Sort> argSorts = accept(ctx.arg_sorts());
         assert argSorts != null;
@@ -96,11 +96,11 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) {
         }
 
         Function f = null;
-        assert func_name != null;
-        int separatorIndex = func_name.indexOf("::");
+        assert funcName != null;
+        int separatorIndex = funcName.indexOf("::");
         if (separatorIndex > 0) {
-            String sortName = func_name.substring(0, separatorIndex);
-            String baseName = func_name.substring(separatorIndex + 2);
+            String sortName = funcName.substring(0, separatorIndex);
+            String baseName = funcName.substring(separatorIndex + 2);
             Sort genSort = lookupSort(sortName);
             if (genSort instanceof GenericSort) {
                 f = SortDependingFunction.createFirstInstance((GenericSort) genSort,
@@ -109,14 +109,15 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) {
         }
 
         if (f == null) {
-            f = new Function(new Name(func_name), retSort, argSorts.toArray(new Sort[0]),
+            f = new Function(new Name(funcName), retSort, argSorts.toArray(new Sort[0]),
                 whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), unique);
         }
 
         if (lookup(f.name()) == null) {
             functions().add(f);
         } else {
-            addWarning(ctx, "Function '" + func_name + "' is already defined!");
+            // weigl: agreement on KaKeY meeting: this should be an error.
+            semanticError(ctx, "Function '" + funcName + "' is already defined!");
         }
         return f;
     }