Revive work on Polymorphic Sorts

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

@@ -383,6 +383,9 @@ GREATEREQUAL
 
 WS:  [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace
 STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ;
+
+OPENTYPEPARAMS:'<' '[';
+CLOSETYPEPARAMS:']' '>';
 LESS: '<';
 LESSEQUAL: '<' '=' | '\u2264';
 LGUILLEMETS: '<' '<' | '«' | '‹';

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

@@ -94,10 +94,26 @@ one_sort_decl
         (ONEOF sortOneOf = oneof_sorts)?
         (EXTENDS sortExt = extends_sorts)? SEMI
     | PROXY  sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI
-    | ABSTRACT? sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)?  SEMI
+    | ABSTRACT? (sortIds=simple_ident_dots_comma_list |
+                 parametric_sort_decl) (EXTENDS sortExt=extends_sorts)?  SEMI
   )
 ;
 
+// TODO currently you are not allowed to commatise parametric_sort_decl. Is this severe?
+
+parametric_sort_decl
+:
+    simple_ident_dots
+    OPENTYPEPARAMS
+    formal_sort_param_decl (COMMA formal_sort_param_decl)*
+    CLOSETYPEPARAMS
+;
+
+formal_sort_param_decl
+:
+    (PLUS | MINUS)? simple_ident
+;
+
 simple_ident_dots
 :
   simple_ident (DOT simple_ident)*
@@ -108,7 +124,6 @@ simple_ident_dots_comma_list
   simple_ident_dots (COMMA simple_ident_dots)*
 ;
 
-
 extends_sorts
 :
     sortId (COMMA sortId)*
@@ -243,7 +258,7 @@ datatype_decl:
   doc=DOC_COMMENT?
   // weigl: all datatypes are free!
   // FREE?
-  name=simple_ident
+  name=simple_ident formal_sort_parameters?
   EQUALS
   datatype_constructor (OR datatype_constructor)*
   SEMI
@@ -326,7 +341,14 @@ ruleset_decls
 
 sortId
 :
-    id=simple_ident_dots (EMPTYBRACKETS)*
+    id=simple_ident_dots (EMPTYBRACKETS)* formal_sort_parameters?
+;
+
+formal_sort_parameters
+:
+    OPENTYPEPARAMS
+    sortId (COMMA sortId)*
+    CLOSETYPEPARAMS
 ;
 
 id_declaration

key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java

@@ -7,6 +7,8 @@
 import de.uka.ilkd.key.logic.op.IProgramVariable;
 import de.uka.ilkd.key.logic.op.JFunction;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
+import de.uka.ilkd.key.logic.sort.ParametricSortDeclaration;
+import de.uka.ilkd.key.logic.sort.ParametricSortInstance;
 import de.uka.ilkd.key.rule.RuleSet;
 
 import org.key_project.logic.Name;
@@ -21,39 +23,43 @@ public class NamespaceSet {
     private Namespace<JFunction> funcNS = new Namespace<>();
     private Namespace<RuleSet> ruleSetNS = new Namespace<>();
     private Namespace<Sort> sortNS = new Namespace<>();
+    private Namespace<ParametricSortDeclaration> parametricSortNS = new Namespace<>();
     private Namespace<Choice> choiceNS = new Namespace<>();
 
     public NamespaceSet() {
     }
 
     public NamespaceSet(Namespace<QuantifiableVariable> varNS,
             Namespace<JFunction> funcNS,
-            Namespace<Sort> sortNS, Namespace<RuleSet> ruleSetNS, Namespace<Choice> choiceNS,
+            Namespace<Sort> sortNS,
+                        Namespace<ParametricSortDeclaration> parametricSortNS,
+                        Namespace<RuleSet> ruleSetNS, Namespace<Choice> choiceNS,
             Namespace<IProgramVariable> programVarNS) {
         this.varNS = varNS;
         this.progVarNS = programVarNS;
         this.funcNS = funcNS;
         this.sortNS = sortNS;
+        this.parametricSortNS = parametricSortNS;
         this.ruleSetNS = ruleSetNS;
         this.choiceNS = choiceNS;
     }
 
     public NamespaceSet copy() {
         return new NamespaceSet(variables().copy(), functions().copy(),
-            sorts().copy(),
+            sorts().copy(), parametricSorts().copy(),
             ruleSets().copy(), choices().copy(), programVariables().copy());
     }
 
     public NamespaceSet shallowCopy() {
-        return new NamespaceSet(variables(), functions(), sorts(), ruleSets(),
-            choices(),
-            programVariables());
+        return new NamespaceSet(variables(), functions(), sorts(), parametricSorts(), ruleSets(),
+            choices(), programVariables());
     }
 
     // TODO MU: Rename into sth with wrap or similar
     public NamespaceSet copyWithParent() {
         return new NamespaceSet(new Namespace<>(variables()),
             new Namespace<>(functions()), new Namespace<>(sorts()),
+            new Namespace<>(parametricSorts()),
             new Namespace<>(ruleSets()), new Namespace<>(choices()),
             new Namespace<>(programVariables()));
     }
@@ -98,6 +104,14 @@ public void setSorts(Namespace<Sort> sortNS) {
         this.sortNS = sortNS;
     }
 
+    public Namespace<ParametricSortDeclaration> parametricSorts() {
+        return parametricSortNS;
+    }
+
+    public void setParametricSorts(Namespace<ParametricSortDeclaration> parametricSortNS) {
+        this.parametricSortNS = parametricSortNS;
+    }
+
     public Namespace<Choice> choices() {
         return choiceNS;
     }
@@ -110,6 +124,7 @@ public void add(NamespaceSet ns) {
         variables().add(ns.variables());
         programVariables().add(ns.programVariables());
         sorts().add(ns.sorts());
+        parametricSorts().add(ns.parametricSorts());
         ruleSets().add(ns.ruleSets());
         functions().add(ns.functions());
         choices().add(ns.choices());
@@ -119,7 +134,7 @@ public void add(NamespaceSet ns) {
      * returns all namespaces in an array
      */
     private Namespace<?>[] asArray() {
-        return new Namespace[] { variables(), programVariables(), sorts(), ruleSets(), functions(),
+        return new Namespace[] { variables(), programVariables(), sorts(), parametricSorts(), ruleSets(), functions(),
             choices() };
     }
 
@@ -190,23 +205,26 @@ public void seal() {
         funcNS.seal();
         ruleSetNS.seal();
         sortNS.seal();
+        parametricSortNS.seal();
         choiceNS.seal();
     }
 
     public boolean isEmpty() {
         return varNS.isEmpty() && programVariables().isEmpty() && funcNS.isEmpty()
-                && ruleSetNS.isEmpty() && sortNS.isEmpty() && choiceNS.isEmpty();
+                && ruleSetNS.isEmpty() && sortNS.isEmpty() && parametricSortNS.isEmpty() && choiceNS.isEmpty();
     }
 
 
     // create a namespace
     public NamespaceSet simplify() {
         return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(),
+            parametricSortNS.simplify(),
             ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify());
     }
 
     public NamespaceSet getCompression() {
         return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(),
+            parametricSortNS.compress(),
             ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress());
     }
 
@@ -218,6 +236,7 @@ public void flushToParent() {
 
     public NamespaceSet getParent() {
         return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(),
+            parametricSortNS.parent(),
             ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent());
     }
 

key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java

@@ -9,6 +9,7 @@
 import de.uka.ilkd.key.logic.NamespaceSet;
 import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.sort.GenericSort;
+import de.uka.ilkd.key.logic.sort.ParametricSortInstance;
 import de.uka.ilkd.key.logic.sort.ProgramSVSort;
 
 import org.key_project.logic.Name;
@@ -39,7 +40,7 @@ public final class SortDependingFunction extends JFunction {
 
     private SortDependingFunction(SortDependingFunctionTemplate template, Sort sortDependingOn) {
         super(instantiateName(template.kind, sortDependingOn),
-            instantiateResultSort(template, sortDependingOn),
+            instantiateSort(template.sortDependingOn, sortDependingOn, template.sort),
             instantiateArgSorts(template, sortDependingOn), null, template.unique, false);
         this.template = template;
         this.sortDependingOn = Qualifier.create(sortDependingOn);
@@ -55,23 +56,22 @@ private static Name instantiateName(Name kind, Sort sortDependingOn) {
     }
 
 
-    private static Sort instantiateResultSort(SortDependingFunctionTemplate template,
-            Sort sortDependingOn) {
-        return template.sort == template.sortDependingOn ? sortDependingOn : template.sort;
+    private static Sort instantiateSort(GenericSort genericSort, Sort instanatiation,
+                                        Sort toInstantiate) {
+        // Replaces the generic sort and all occurrences in parametric sorts
+        return ParametricSortInstance.instantiate(genericSort, instanatiation, toInstantiate);
     }
 
 
     private static ImmutableArray<Sort> instantiateArgSorts(SortDependingFunctionTemplate template,
             Sort sortDependingOn) {
         Sort[] result = new Sort[template.argSorts.size()];
         for (int i = 0; i < result.length; i++) {
-            result[i] = (template.argSorts.get(i) == template.sortDependingOn ? sortDependingOn
-                    : template.argSorts.get(i));
+            result[i] = ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, template.argSorts.get(i));
         }
         return new ImmutableArray<>(result);
     }
 
-
     // -------------------------------------------------------------------------
     // public interface
     // -------------------------------------------------------------------------