Skip to content

Commit 65006b4

Browse files
mattulbrichmattulbrich
committed
more on parameterised types ...
1 parent 6238304 commit 65006b4

File tree

15 files changed

+503
-155
lines changed

15 files changed

+503
-155
lines changed

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

Lines changed: 17 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -90,17 +90,28 @@ one_sort_decl
9090
:
9191
doc=DOC_COMMENT?
9292
(
93-
GENERIC sortIds=sortList
93+
GENERIC sortIds=simple_ident_dots_comma_list
9494
(ONEOF sortOneOf = oneof_sorts)?
9595
(EXTENDS sortExt = extends_sorts)? SEMI
96-
| PROXY sortIds=sortList (EXTENDS sortExt=extends_sorts)? SEMI
97-
| ABSTRACT? sortIds=sortList (EXTENDS sortExt=extends_sorts)? SEMI
96+
| PROXY sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI
97+
| ABSTRACT? (sortIds=simple_ident_dots_comma_list |
98+
parametric_sort_decl) (EXTENDS sortExt=extends_sorts)? SEMI
9899
)
99100
;
100101

101-
sortList
102+
// TODO currently you are not allowed to commatise parametric_sort_decl. Is this severe?
103+
104+
parametric_sort_decl
102105
:
103-
sortId (COMMA sortId)*
106+
simple_ident_dots
107+
OPENTYPEPARAMS
108+
formal_sort_param_decl (COMMA formal_sort_param_decl)*
109+
CLOSETYPEPARAMS
110+
;
111+
112+
formal_sort_param_decl
113+
:
114+
(PLUS | MINUS)? simple_ident
104115
;
105116

106117
simple_ident_dots
@@ -113,7 +124,6 @@ simple_ident_dots_comma_list
113124
simple_ident_dots (COMMA simple_ident_dots)*
114125
;
115126

116-
117127
extends_sorts
118128
:
119129
sortId (COMMA sortId)*
@@ -334,17 +344,10 @@ sortId
334344
id=simple_ident_dots (EMPTYBRACKETS)* formal_sort_parameters?
335345
;
336346

337-
formal_sort_variance
338-
:
339-
(PLUS | MINUS)?
340-
;
341-
342-
formal_sort_parameter: formal_sort_variance id=sortId;
343-
344347
formal_sort_parameters
345348
:
346349
OPENTYPEPARAMS
347-
formal_sort_parameter (COMMA formal_sort_parameter)*
350+
sortId (COMMA sortId)*
348351
CLOSETYPEPARAMS
349352
;
350353

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
import de.uka.ilkd.key.logic.NamespaceSet;
1010
import de.uka.ilkd.key.logic.TermServices;
1111
import de.uka.ilkd.key.logic.sort.GenericSort;
12+
import de.uka.ilkd.key.logic.sort.ParametricSortInstance;
1213
import de.uka.ilkd.key.logic.sort.ProgramSVSort;
1314

1415
import org.key_project.logic.Name;
@@ -39,7 +40,7 @@ public final class SortDependingFunction extends JFunction {
3940

4041
private SortDependingFunction(SortDependingFunctionTemplate template, Sort sortDependingOn) {
4142
super(instantiateName(template.kind, sortDependingOn),
42-
instantiateResultSort(template, sortDependingOn),
43+
instantiateSort(template.sortDependingOn, sortDependingOn, template.sort),
4344
instantiateArgSorts(template, sortDependingOn), null, template.unique, false);
4445
this.template = template;
4546
this.sortDependingOn = Qualifier.create(sortDependingOn);
@@ -55,23 +56,22 @@ private static Name instantiateName(Name kind, Sort sortDependingOn) {
5556
}
5657

5758

58-
private static Sort instantiateResultSort(SortDependingFunctionTemplate template,
59-
Sort sortDependingOn) {
60-
return template.sort == template.sortDependingOn ? sortDependingOn : template.sort;
59+
private static Sort instantiateSort(GenericSort genericSort, Sort instanatiation,
60+
Sort toInstantiate) {
61+
// Replaces the generic sort and all occurrences in parametric sorts
62+
return ParametricSortInstance.instantiate(genericSort, instanatiation, toInstantiate);
6163
}
6264

6365

6466
private static ImmutableArray<Sort> instantiateArgSorts(SortDependingFunctionTemplate template,
6567
Sort sortDependingOn) {
6668
Sort[] result = new Sort[template.argSorts.size()];
6769
for (int i = 0; i < result.length; i++) {
68-
result[i] = (template.argSorts.get(i) == template.sortDependingOn ? sortDependingOn
69-
: template.argSorts.get(i));
70+
result[i] = ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, template.argSorts.get(i));
7071
}
7172
return new ImmutableArray<>(result);
7273
}
7374

74-
7575
// -------------------------------------------------------------------------
7676
// public interface
7777
// -------------------------------------------------------------------------

‎key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDeclaration.java‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.logic.sort;
5+
6+
import java.util.IdentityHashMap;
7+
import java.util.Map;
8+
import java.util.function.Function;
9+
10+
import de.uka.ilkd.key.ldt.JavaDLTheory;
11+
12+
import org.jspecify.annotations.NonNull;
13+
import org.jspecify.annotations.NullMarked;
14+
import org.key_project.logic.Name;
15+
import org.key_project.logic.Named;
16+
import org.key_project.logic.sort.Sort;
17+
import org.key_project.util.collection.ImmutableList;
18+
import org.key_project.util.collection.ImmutableSet;
19+
import org.key_project.util.collection.Immutables;
20+
21+
/**
22+
* Here is a short class diagram, written for PlantUML.
23+
* You can create the PNG file by feeding this SourceFile into PlantUML or
24+
* by entering the text into https://www.planttext.com/, e.g.
25+
@formatter:off
26+
@startuml
27+
interface Sort
28+
abstract class AbstractSort
29+
class SortImpl
30+
31+
class ParametricSortDeclaration
32+
class ParametricSortInstance
33+
class NullSort
34+
class GenericSort
35+
36+
Sort <|-- AbstractSort
37+
AbstractSort <|-- SortImpl
38+
AbstractSort <|-- ParametricSortInstance
39+
AbstractSort <|-- GenericSort
40+
Sort <|-- NullSort
41+
42+
ParametricSortInstance --> ParametricSortDeclaration : base
43+
ParametricSortInstance --> "*" Sort :args
44+
ParametricSortDeclaration --> "n" GenericSort : typeParameters
45+
ParametricSortDeclaration --> "*" Sort : extendsDecl
46+
ParametricSortDeclaration --> "n" Variance : variances
47+
48+
enum Variance {
49+
COVARIANT
50+
CONTRAVARIANT
51+
INVARIANT
52+
}
53+
@enduml
54+
@formatter:on
55+
*/
56+
57+
@NullMarked
58+
public class ParametricSortDeclaration implements Named {
59+
60+
private final Name name;
61+
private final boolean isAbstract;
62+
private final String documentation;
63+
private final String origin;
64+
65+
public enum Variance {
66+
COVARIANT,
67+
CONTRAVARIANT,
68+
INVARIANT;
69+
}
70+
71+
public record SortParameter(@NonNull GenericSort genericSort, @NonNull Variance variance) {
72+
}
73+
74+
private final ImmutableList<SortParameter> parameters;
75+
76+
private final ImmutableSet<Sort> extendedSorts;
77+
78+
public ParametricSortDeclaration(Name name, ImmutableSet<Sort> ext, boolean isAbstract,
79+
ImmutableList<GenericSort> parameters, ImmutableList<Variance> covariances,
80+
String documentation, String origin) {
81+
this(name, ext, isAbstract, Immutables.zip(parameters, covariances, SortParameter::new), documentation, origin);
82+
}
83+
84+
public ParametricSortDeclaration(Name name, ImmutableSet<Sort> ext, boolean isAbstract,
85+
ImmutableList<SortParameter> sortParams, String documentation, String origin) {
86+
this.name = name;
87+
this.extendedSorts = ext.isEmpty() ? Immutables.setOf(JavaDLTheory.ANY) : ext;
88+
this.isAbstract = isAbstract;
89+
this.documentation = documentation;
90+
this.origin = origin;
91+
this.parameters = sortParams;
92+
assert Immutables.isDuplicateFree(parameters.map(SortParameter::genericSort)) :
93+
"The caller should have made sure that generic sorts are not duplicated";
94+
}
95+
96+
public Function<Sort, Sort> getInstantiator(ImmutableList<Sort> args) {
97+
IdentityHashMap<GenericSort, Sort> map = new IdentityHashMap<>();
98+
99+
if (args.size() != parameters.size()) {
100+
throw new IllegalArgumentException("Parametric type " + name +
101+
" expected " + parameters.size() + " arguments, but received " +
102+
args);
103+
}
104+
105+
ImmutableList<SortParameter> p = parameters;
106+
while (!args.isEmpty()) {
107+
map.put(p.head().genericSort(), args.head());
108+
p = p.tail();
109+
args = args.tail();
110+
}
111+
112+
return new SortInstantiator(map);
113+
}
114+
115+
public static class SortInstantiator implements Function<Sort, Sort> {
116+
private final Map<GenericSort, Sort> map;
117+
118+
public SortInstantiator(Map<GenericSort, Sort> map) {
119+
this.map = map;
120+
}
121+
122+
@Override
123+
public Sort apply(Sort sort) {
124+
Sort mapped = map.get(sort);
125+
if (mapped != null) {
126+
return mapped;
127+
}
128+
if (sort instanceof ParametricSortInstance psi) {
129+
return psi.map(this);
130+
} else {
131+
return sort;
132+
}
133+
}
134+
}
135+
136+
public ImmutableList<SortParameter> getParameters() {
137+
return parameters;
138+
}
139+
140+
public ImmutableSet<Sort> getExtendedSorts() {
141+
return extendedSorts;
142+
}
143+
144+
@Override
145+
public Name name() {
146+
return name;
147+
}
148+
149+
public boolean isAbstract() {
150+
return isAbstract;
151+
}
152+
153+
public String getDocumentation() {
154+
return documentation;
155+
}
156+
157+
public String getOrigin() {
158+
return origin;
159+
}
160+
}

‎key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java‎

Lines changed: 23 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -71,10 +71,12 @@ private static ImmutableSet<Sort> computeExt(ParametricSortDeclaration base,
7171
switch(parameter.variance()) {
7272
case COVARIANT -> {
7373
// take all bases of that arg and add the modified sort as ext class
74-
for (Sort s : parameter.genericSort().extendsSorts()) {
74+
/* for (Sort s : parameter.genericSort().extendsSorts()) {
7575
ImmutableList<Sort> newArgs = parameters.replace(number, s);
7676
result = result.add(ParametricSortInstance.get(base, newArgs));
77-
}
77+
} */
78+
// throw new UnsupportedOperationException(
79+
// "Covariance currently not supported");
7880
}
7981

8082
case CONTRAVARIANT -> throw new UnsupportedOperationException(
@@ -88,7 +90,8 @@ private static ImmutableSet<Sort> computeExt(ParametricSortDeclaration base,
8890
}
8991

9092
private static Name makeName(ParametricSortDeclaration base, ImmutableList<Sort> parameters) {
91-
return new Name(base.name() + "<[" + parameters + "]>");
93+
// The [ ] are produced by the list's toString method.
94+
return new Name(base.name() + "<" + parameters + ">");
9295
}
9396

9497
public ParametricSortDeclaration getBase() {
@@ -128,6 +131,22 @@ public ImmutableSet<Sort> extendsSorts() {
128131

129132
@Override
130133
public boolean extendsTrans(Sort sort) {
131-
return false;
134+
return sort == this || extendsSorts()
135+
.exists((Sort superSort) -> superSort == sort || superSort.extendsTrans(sort));
136+
}
137+
138+
public static Sort instantiate(GenericSort genericSort, Sort instantiation, Sort toInstantiate) {
139+
if(genericSort == toInstantiate) {
140+
return instantiation;
141+
} else if(toInstantiate instanceof ParametricSortInstance psort) {
142+
return psort.instantiate(genericSort, instantiation);
143+
} else {
144+
return toInstantiate;
145+
}
146+
}
147+
148+
public Sort instantiate(GenericSort template, Sort instantiation) {
149+
ImmutableList<Sort> newParameters = parameters.map(s -> instantiate(template, instantiation, s));
150+
return get(base, newParameters);
132151
}
133152
}

0 commit comments

Comments
 (0)