Skip to content

Commit c837095

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

File tree

14 files changed

+343
-155
lines changed

14 files changed

+343
-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/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
}

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

Lines changed: 96 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,10 @@
2020
import org.key_project.logic.Name;
2121
import org.key_project.logic.Named;
2222
import org.key_project.logic.sort.Sort;
23-
import org.key_project.util.collection.ImmutableList;
24-
import org.key_project.util.collection.ImmutableSLList;
25-
import org.key_project.util.collection.ImmutableSet;
26-
import org.key_project.util.collection.Immutables;
23+
import org.key_project.util.collection.*;
2724

2825
import org.antlr.v4.runtime.Token;
26+
import org.key_project.util.java.CollectionUtil;
2927
import org.slf4j.Logger;
3028
import org.slf4j.LoggerFactory;
3129

@@ -64,7 +62,7 @@ public Object visitDecls(KeYParser.DeclsContext ctx) {
6462
@Override
6563
public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
6664
var name = ctx.name.getText();
67-
List<FormalSortParameter> typeParameters = accept(ctx.formal_sort_parameters());
65+
List<SortParameter> typeParameters = accept(ctx.formal_sort_parameters());
6866
var doc = ctx.DOC_COMMENT() != null
6967
? ctx.DOC_COMMENT().getText()
7068
: null;
@@ -73,10 +71,15 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
7371
var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin);
7472
sorts().addSafely(s);
7573
} else {
76-
var tp = typeParameters.stream().map(it -> (GenericSort) it.second())
74+
var tp = typeParameters.stream().map(SortParameter::genericSort)
7775
.collect(ImmutableList.collector());
76+
var doubled = CollectionUtil.findDuplicates(tp);
77+
if (!doubled.isEmpty()) {
78+
semanticError(ctx.formal_sort_parameters(),
79+
"Type parameters must be unique within a declaration. Found duplicate: %s", doubled.getFirst());
80+
}
7881
var variance =
79-
typeParameters.stream().map(FormalSortParameter::first)
82+
typeParameters.stream().map(SortParameter::variance)
8083
.collect(ImmutableList.collector());
8184
var s = new ParametricSortDeclaration(
8285
new Name(name), ImmutableSet.empty(), false, tp, variance,
@@ -146,20 +149,20 @@ public Object visitSort_decls(KeYParser.Sort_declsContext ctx) {
146149
}
147150

148151

149-
public record NamedFormalSortParameter(String name, List<FormalSortParameter> parameters) {}
152+
public record NamedFormalSortParameter(String name, List<SortParameter> parameters) {}
150153

151-
@Override
152-
public List<NamedFormalSortParameter> visitSortList(KeYParser.SortListContext ctx) {
153-
List<NamedFormalSortParameter> seq = new ArrayList<>();
154-
for (KeYParser.SortIdContext context : ctx.sortId()) {
155-
String sortName = context.simple_ident_dots().getText();
156-
// String brackets = StringUtil.repeat("[]", context.EMPTYBRACKETS().size());
157-
List<FormalSortParameter> typeParams = accept(context.formal_sort_parameters());
158-
seq.add(new NamedFormalSortParameter(sortName,
159-
typeParams != null ? typeParams : Collections.emptyList()));
160-
}
161-
return seq;
162-
}
154+
// @Override
155+
// public List<NamedFormalSortParameter> visitSortList(KeYParser.SortListContext ctx) {
156+
// List<NamedFormalSortParameter> seq = new ArrayList<>();
157+
// for (KeYParser.SortIdContext context : ctx.sortId()) {
158+
// String sortName = context.simple_ident_dots().getText();
159+
// // String brackets = StringUtil.repeat("[]", context.EMPTYBRACKETS().size());
160+
// List<SortParameter> typeParams = accept(context.formal_sort_parameters());
161+
// seq.add(new NamedFormalSortParameter(sortName,
162+
// typeParams != null ? typeParams : Collections.emptyList()));
163+
// }
164+
// return seq;
165+
// }
163166

164167

165168
@Override
@@ -174,80 +177,95 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
174177
List<Sort> createdSorts = new LinkedList<>();
175178
// assert sortIds != null;
176179

180+
ImmutableSet<Sort> ext = sortExt == null ? ImmutableSet.empty()
181+
: Immutables.setOf(sortExt);
182+
ImmutableSet<Sort> oneOf = sortOneOf == null ? ImmutableSet.empty()
183+
: Immutables.setOf(sortOneOf);
184+
177185
var documentation = ParsingFacade.getValueDocumentation(ctx.DOC_COMMENT());
178-
for (var idCtx : ctx.sortIds.sortId()) {
179-
// for (Pair<String, List<Pair<ParametricSort.Variance, Sort>>> sortId : sortIds) {
180-
var name = idCtx.simple_ident_dots().getText();
181-
// var brackets = StringUtil.repeat("[]", idCtx.EMPTYBRACKETS().size());
182-
List<FormalSortParameter> typeParams = accept(idCtx.formal_sort_parameters());
186+
187+
if(ctx.sortIds == null) {
188+
// parametrised sorts
189+
var declCtx = ctx.parametric_sort_decl();
190+
assert declCtx != null : "One of the two must be present";
191+
List<SortParameter> typeParams = mapOf(declCtx.formal_sort_param_decl());
192+
ImmutableList<SortParameter> params = Immutables.listOf(typeParams);
193+
var doubled = CollectionUtil.findDuplicates(params.map(SortParameter::genericSort));
194+
if (!doubled.isEmpty()) {
195+
semanticError(declCtx,
196+
"Type parameters must be unique within a declaration. Found duplicate: %s", doubled.getFirst());
197+
}
198+
String name = declCtx.simple_ident_dots().getText();
183199
Name sortName = new Name(name);
184-
boolean isParametricSort = typeParams != null && !typeParams.isEmpty();
185-
186-
ImmutableSet<Sort> ext = sortExt == null ? ImmutableSet.empty()
187-
: Immutables.createSetFrom(sortExt);
188-
ImmutableSet<Sort> oneOf = sortOneOf == null ? ImmutableSet.empty()
189-
: Immutables.createSetFrom(sortOneOf);
190-
191-
// attention: no expand to java.lang here!
192-
Sort existingSort = sorts().lookup(sortName);
193-
if (existingSort == null) {
194-
Sort s = null;
195-
if (isParametricSort) {
196-
if (isGenericSort) {
197-
semanticError(ctx,
198-
"Generic sorts are not allowed to have type parameters.");
199-
}
200+
var sortDecl = new ParametricSortDeclaration(sortName, ext, isAbstractSort, params, documentation, BuilderHelpers.getPosition(declCtx));
201+
namespaces().parametricSorts().add(sortDecl);
200202

201-
for (FormalSortParameter param : typeParams) {
202-
if (!(param.second() instanceof GenericSort)) {
203-
semanticError(ctx,
204-
"Type parameters must be generic sorts. Given type '%s' is %s",
205-
param.second().name(), param.second().getClass().getName());
206-
}
207-
}
203+
} else {
204+
for (var idCtx : ctx.sortIds.simple_ident_dots()) {
205+
var name = idCtx.getText();
206+
Name sortName = new Name(name);
208207

209-
ImmutableList<SortParameter> params =
210-
typeParams.stream()
211-
.map(it -> new SortParameter((GenericSort) it.second(), it.first()))
212-
.collect(ImmutableSLList.toImmutableList());
213-
var sortDecl = new ParametricSortDeclaration(sortName, ext, isAbstractSort, params, documentation, BuilderHelpers.getPosition(idCtx));
214-
namespaces().parametricSorts().add(sortDecl);
215-
} else if (isGenericSort) {
216-
try {
217-
s = new GenericSort(sortName, ext, oneOf, documentation,
218-
BuilderHelpers.getPosition(ctx));
219-
} catch (GenericSupersortException e) {
220-
semanticError(ctx, "Illegal sort given");
221-
}
222-
} else if (new Name("any").equals(sortName)) {
223-
s = JavaDLTheory.ANY;
224-
} else {
225-
if (isProxySort) {
226-
s = new ProxySort(sortName, ext, documentation,
227-
BuilderHelpers.getPosition(idCtx));
208+
// attention: no expand to java.lang here!
209+
Sort existingSort = sorts().lookup(sortName);
210+
if (existingSort == null) {
211+
Sort s = null;
212+
if (isGenericSort) {
213+
try {
214+
s = new GenericSort(sortName, ext, oneOf, documentation,
215+
BuilderHelpers.getPosition(ctx));
216+
} catch (GenericSupersortException e) {
217+
semanticError(ctx, "Illegal sort given");
218+
}
219+
} else if (new Name("any").equals(sortName)) {
220+
s = JavaDLTheory.ANY;
228221
} else {
229-
s = new SortImpl(sortName, ext, isAbstractSort,
230-
documentation, BuilderHelpers.getPosition(idCtx));
222+
if (isProxySort) {
223+
s = new ProxySort(sortName, ext, documentation,
224+
BuilderHelpers.getPosition(idCtx));
225+
} else {
226+
s = new SortImpl(sortName, ext, isAbstractSort,
227+
documentation, BuilderHelpers.getPosition(idCtx));
228+
}
231229
}
232-
}
233-
if(!isParametricSort) {
234230
// parametric sort declarations are not sorts themselves.
235231
assert s != null;
236232
sorts().add(s);
237233
createdSorts.add(s);
234+
} else {
235+
// weigl: agreement on KaKeY meeting: this should be ignored until we finally have
236+
// local namespaces for generic sorts
237+
// addWarning(ctx, "Sort declaration is ignored, due to collision.");
238+
LOGGER.debug("Sort declaration of {} in {} is ignored due to collision (already "
239+
+ "present in {}).", sortName, BuilderHelpers.getPosition(ctx),
240+
existingSort.getOrigin());
238241
}
239-
} else {
240-
// weigl: agreement on KaKeY meeting: this should be ignored until we finally have
241-
// local namespaces for generic sorts
242-
// addWarning(ctx, "Sort declaration is ignored, due to collision.");
243-
LOGGER.debug("Sort declaration of {} in {} is ignored due to collision (already "
244-
+ "present in {}).", sortName, BuilderHelpers.getPosition(ctx),
245-
existingSort.getOrigin());
246242
}
247243
}
248244
return createdSorts;
249245
}
250246

247+
@Override
248+
public SortParameter visitFormal_sort_param_decl(KeYParser.Formal_sort_param_declContext ctx) {
249+
ParametricSortDeclaration.Variance variance;
250+
if (ctx.PLUS() != null)
251+
variance = ParametricSortDeclaration.Variance.COVARIANT;
252+
else if (ctx.MINUS() != null)
253+
variance = ParametricSortDeclaration.Variance.CONTRAVARIANT;
254+
else
255+
variance = ParametricSortDeclaration.Variance.INVARIANT;
256+
257+
var name = ctx.simple_ident().getText();
258+
Sort paramSort = sorts().lookup(name);
259+
if(paramSort == null) {
260+
semanticError(ctx, "Parameter sort %s not found", name);
261+
}
262+
if(!(paramSort instanceof GenericSort)) {
263+
semanticError(ctx, "Parameter sort %s is not a generic sort", name);
264+
}
265+
266+
return new SortParameter((GenericSort) paramSort, variance);
267+
}
268+
251269
@Override
252270
public Object visitOption_decls(KeYParser.Option_declsContext ctx) {
253271
return mapOf(ctx.choice());

0 commit comments

Comments
 (0)