Skip to content

Commit

Permalink
fixing merge errors
Browse files Browse the repository at this point in the history
  • Loading branch information
@wadoon
wadoon committed Jan 12, 2024
1 parent cf34505 commit 623b941
Show file tree
Hide file tree
Showing 11 changed files with 224 additions and 2,094 deletions.
7 changes: 4 additions & 3 deletions key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSort.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,15 +62,16 @@ public enum Variance {
private final ImmutableList<Variance> covariances;

public ParametricSort(Name name, ImmutableSet<Sort> ext, boolean isAbstract,
ImmutableList<GenericSort> parameters, ImmutableList<Variance> covariances) {
super(name, ext, isAbstract);
ImmutableList<GenericSort> parameters, ImmutableList<Variance> covariances,
String documentation, String origin) {
super(name, ext, isAbstract, documentation, origin);
this.parameters = parameters;
this.covariances = covariances;
}

public ParametricSort(Name name, ImmutableSet<Sort> ext, boolean isAbstract,
ImmutableList<Pair<GenericSort, Variance>> sortParams) {
this(name, ext, isAbstract, sortParams.map(x->x.first), sortParams.map(x->x.second));
this(name, ext, isAbstract, sortParams.map(x -> x.first), sortParams.map(x -> x.second), null, null);
}

public Function<Sort, Sort> getInstantiation(ImmutableList<Sort> args) {
Expand Down
17 changes: 10 additions & 7 deletions key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package de.uka.ilkd.key.logic.sort;

import de.uka.ilkd.key.logic.Name;
import org.jspecify.annotations.Nullable;
import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSet;
Expand All @@ -18,8 +19,9 @@ public class ParametricSortInstance extends AbstractSort {

private final ParametricSort base;

public static ParametricSortInstance get(ParametricSort base, ImmutableList<Sort> parameters) {
ParametricSortInstance sort = new ParametricSortInstance(base, parameters);
public static ParametricSortInstance get(ParametricSort base, ImmutableList<Sort> parameters,
@Nullable String documentation, @Nullable String origin) {
ParametricSortInstance sort = new ParametricSortInstance(base, parameters, documentation, origin);
ParametricSortInstance cached = CACHE.get(sort);
if (cached != null) {
return cached;
Expand All @@ -29,9 +31,10 @@ public static ParametricSortInstance get(ParametricSort base, ImmutableList<Sort
}
}

private ParametricSortInstance(ParametricSort base, ImmutableList<Sort> parameters) {
super(makeName(base, parameters),
computeExt(base, parameters), base.isAbstract());
private ParametricSortInstance(ParametricSort base, ImmutableList<Sort> parameters,
String documentation, String origin) {
super(makeName(base, parameters), computeExt(base, parameters), base.isAbstract(),
documentation, origin);

this.base = base;
this.parameters = parameters;
Expand All @@ -58,7 +61,7 @@ private static ImmutableSet<Sort> computeExt(ParametricSort base, ImmutableList<
// take all bases of that arg and add the modified sort as ext class
for (Sort s : parameters.get(i).extendsSorts()) {
ImmutableList<Sort> newArgs = parameters.replace(i, s);
result = result.add(ParametricSortInstance.get(base, newArgs));
result = result.add(ParametricSortInstance.get(base, newArgs, null, null));
}
break;

Expand Down Expand Up @@ -90,7 +93,7 @@ public ImmutableList<Sort> getParameters() {
public ParametricSortInstance map(Function<Sort, Sort> f) {
ImmutableList<Sort> newParameters = parameters.map(f);
// The cache ensures that no unnecessary duplicates are kept.
return get(base, newParameters);
return get(base, newParameters, null, null);
}

@Override
Expand Down
39 changes: 18 additions & 21 deletions key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ public Object visitSort_decls(KeYParser.Sort_declsContext ctx) {
return null;
}


@Override
public List<Pair<String, List<Pair<ParametricSort.Variance, Sort>>>> visitSortList(KeYParser.SortListContext ctx) {
List<Pair<String, List<Pair<ParametricSort.Variance, Sort>>>> seq = new ArrayList<>();
Expand All @@ -145,22 +146,23 @@ public List<Pair<String, List<Pair<ParametricSort.Variance, Sort>>>> visitSortLi

@Override
public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
List<Pair<String, List<Pair<ParametricSort.Variance, Sort>>>> sortIds = accept(ctx.sortIds);
//List<Pair<String, List<Pair<ParametricSort.Variance, Sort>>>> sortIds = accept(ctx.sortIds);
List<Sort> sortOneOf = accept(ctx.sortOneOf);
List<Sort> sortExt = accept(ctx.sortExt);
boolean isGenericSort = ctx.GENERIC() != null;
boolean isProxySort = ctx.PROXY() != null;
boolean isAbstractSort = ctx.ABSTRACT() != null;
List<Sort> createdSorts = new LinkedList<>();
assert sortIds != null;
//assert sortIds != null;

for (Pair<String, List<Pair<ParametricSort.Variance, Sort>>> sortId : sortIds) {
Name sortName = new Name(sortId.first);
boolean isParametricSort = !sortId.second.isEmpty();
var documentation = ParsingFacade.getValueDocumentation(ctx.DOC_COMMENT());
for (var idCtx : ctx.sortIds.simple_ident_dots()) {
String sortId = accept(idCtx);
Name sortName = new Name(sortId);
for(var idCtx : ctx.sortIds.sortId()){
//for (Pair<String, List<Pair<ParametricSort.Variance, Sort>>> sortId : sortIds) {
var name = idCtx.simple_ident_dots().getText();
var brackets = StringUtil.repeat("[]", idCtx.EMPTYBRACKETS().size());
List<Pair<ParametricSort.Variance, Sort>> typeParams = accept(idCtx.formal_sort_parameters());
Name sortName = new Name(name);

Check notice on line 164 in key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java

View workflow job for this annotation

GitHub Actions / qodana

Constant conditions & exceptions 

Value `name` is always 'null'
boolean isParametricSort = typeParams != null && !typeParams.isEmpty();

ImmutableSet<Sort> ext = sortExt == null ? ImmutableSet.empty()
: DefaultImmutableSet.fromCollection(sortExt);
Expand All @@ -175,39 +177,34 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
semanticError(ctx, "Generic sorts are not allowed to have type parameters.");
}

for (Pair<ParametricSort.Variance, Sort> param : sortId.second) {
for (Pair<ParametricSort.Variance, Sort> param : typeParams) {
if (!(param.second instanceof GenericSort)) {
semanticError(ctx, "Type parameters must be generic sorts. Given type '%s' is %s",
param.second.name(), param.second.getClass().getName());
}
}

ImmutableList<Pair<GenericSort, ParametricSort.Variance>> typeParams =
sortId.second.stream().map(it ->
ImmutableList<Pair<GenericSort, ParametricSort.Variance>> params =
typeParams.stream().map(it ->
new Pair<>((GenericSort) it.second, it.first))
.collect(ImmutableSLList.toImmutableList());
s = new ParametricSort(sortName, ext, isAbstractSort, typeParams);
s = new ParametricSort(sortName, ext, isAbstractSort, params);
}else if (isGenericSort) {
int i;

try {
var gs = new GenericSort(sortName, ext, oneOf, documentation,
BuilderHelpers.getPosition(idCtx));
s = gs;
s = new GenericSort(sortName, ext, oneOf, documentation,
BuilderHelpers.getPosition(ctx));
} catch (GenericSupersortException e) {
semanticError(ctx, "Illegal sort given");
}
} else if (new Name("any").equals(sortName)) {
s = Sort.ANY;
} else {
if (isProxySort) {
var ps = new ProxySort(sortName, ext, documentation,
s = new ProxySort(sortName, ext, documentation,
BuilderHelpers.getPosition(idCtx));
s = ps;
} else {
var si = new SortImpl(sortName, ext, isAbstractSort,
s = new SortImpl(sortName, ext, isAbstractSort,
documentation, BuilderHelpers.getPosition(idCtx));
s = si;
}
}
assert s != null;
Expand Down
7 changes: 3 additions & 4 deletions key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ protected <T> T doLookup(Name n, Namespace<?>... lookups) {
if (lookup != null && (l = lookup.lookup(n)) != null) {
try {
return (T) l;
} catch (ClassCastException e) {
} catch (ClassCastException ignored) {
}
}
}
Expand Down Expand Up @@ -353,10 +353,9 @@ public Sort visitSortId(KeYParser.SortIdContext ctx) {

//parametric sorts should be instantiated
if (ctx.formal_sort_parameters() != null) {
if (s instanceof ParametricSort) {
ParametricSort ps = (ParametricSort) s;
if (s instanceof ParametricSort ps) {
ImmutableList<Sort> parameters = getSorts(ctx.formal_sort_parameters());
s = ParametricSortInstance.get(ps, parameters);
s = ParametricSortInstance.get(ps, parameters, null, null);
} else {
semanticError(ctx, "Not a polymorphic sort: %s", s);
}
Expand Down
Loading

0 comments on commit 623b941

Please sign in to comment.