Skip to content

Commit

Permalink
Make \where variables implicit
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Feb 5, 2024
1 parent d13fd4c commit 32bafde
Show file tree
Hide file tree
Showing 5 changed files with 601 additions and 488 deletions.
8 changes: 7 additions & 1 deletion base/src/main/java/org/arend/term/concrete/Concrete.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -384,6 +384,12 @@ public boolean isExplicit() {
}
}

public static class GeneratedArgument extends Argument {
public GeneratedArgument(Expression expression) {
super(expression, false);
}
}

public static class TypedExpression extends Expression implements ConcreteTypedExpression {
public static final byte PREC = 0;
public Expression expression;
Expand Down Expand Up @@ -2952,7 +2958,7 @@ public static class UnparsedConstructorPattern extends Pattern implements Patter

public UnparsedConstructorPattern(@Nullable Object data, boolean isExplicit, @NotNull List<BinOpSequenceElem<Pattern>> patterns, @Nullable TypedReferable asReferable) {
super(data, asReferable);
assert patterns.size() > 0;
assert !patterns.isEmpty();
myUnparsedPatterns = List.copyOf(patterns);
setExplicit(isExplicit);
}
Expand Down
43 changes: 5 additions & 38 deletions base/src/main/java/org/arend/typechecking/visitor/ClassFieldChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,7 @@
import org.arend.term.concrete.Concrete;
import org.arend.ext.error.LocalError;

import java.util.ArrayDeque;
import java.util.Collection;
import java.util.List;
import java.util.Set;
import java.util.*;

public class ClassFieldChecker extends BaseConcreteExpressionVisitor<Void> {
private Referable myThisParameter;
Expand Down Expand Up @@ -101,16 +98,6 @@ public Concrete.Expression visitTyped(Concrete.TypedExpression expr, Void params
}
}

private int getFirstArgumentIndex(Concrete.ReferenceExpression refExpr, List<Concrete.Argument> args) {
Referable ref = refExpr.getReferent();
if (ref instanceof TCDefReferable) {
Definition def = ((TCDefReferable) ref).getTypechecked();
int index = def == null ? 0 : def.getParametersOriginalDefinitions().size();
return index <= args.size() ? index : 0;
}
return 0;
}

@Override
public Concrete.Expression visitApp(Concrete.AppExpression expr, Void params) {
if (expr.getFunction() instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) expr.getFunction()).getReferent() instanceof MetaReferable) {
Expand All @@ -126,31 +113,11 @@ public Concrete.Expression visitApp(Concrete.AppExpression expr, Void params) {
return expr;
}
}
} else if (expr.getFunction() instanceof Concrete.ReferenceExpression refExpr) {
int index = getFirstArgumentIndex(refExpr, expr.getArguments());
if (index >= expr.getArguments().size() || !expr.getArguments().get(index).isExplicit()) {
if (index < expr.getArguments().size() && expr.getArguments().get(index).expression instanceof Concrete.HoleExpression) {
Referable ref = refExpr.getReferent();
if (ref instanceof TCDefReferable) {
Definition def = ((TCDefReferable) ref).getTypechecked();
if (def != null && def.getEnclosingClass() != null && def.getEnclosingClass().getReferable() == myClassReferable) {
if (expr.getArguments().size() == 1) {
return expr.getFunction().accept(this, null);
} else {
expr.getArguments().remove(0);
return super.visitApp(expr, null);
}
}
}
}
for (Concrete.Argument argument : expr.getArguments()) {
argument.expression = argument.expression.accept(this, params);
}
if (index >= expr.getArguments().size()) {
return Concrete.AppExpression.make(expr.getData(), visitReference(refExpr, null), expr.getArguments());
}
return expr;
} else if (expr.getFunction() instanceof Concrete.ReferenceExpression && !expr.getArguments().get(0).isExplicit() && !(expr.getArguments().get(0) instanceof Concrete.GeneratedArgument)) {
for (Concrete.Argument argument : expr.getArguments()) {
argument.expression = argument.expression.accept(this, params);
}
return expr;
}

return super.visitApp(expr, params);
Expand Down
31 changes: 19 additions & 12 deletions base/src/main/java/org/arend/typechecking/visitor/WhereVarsFixVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@

public class WhereVarsFixVisitor extends BaseConcreteExpressionVisitor<Void> {
private final Concrete.Definition myDefinition;
private final Map<TCDefReferable, List<Concrete.Argument>> mySelfArgs;
private final Map<TCDefReferable, List<Referable>> mySelfArgs;
private final Map<ParameterReferable, Referable> myReferableMap = new HashMap<>();

private WhereVarsFixVisitor(Concrete.Definition definition, Map<TCDefReferable, List<Concrete.Argument>> selfArgs) {
private WhereVarsFixVisitor(Concrete.Definition definition, Map<TCDefReferable, List<Referable>> selfArgs) {
myDefinition = definition;
mySelfArgs = selfArgs;
}
Expand All @@ -38,7 +38,7 @@ private static int getReferableLevel(LocatedReferable referable) {

public static void fixDefinition(Collection<? extends Concrete.Definition> definitions, ErrorReporter errorReporter) {
var whereVars = WhereVarsCollector.findWhereVars(definitions);
Map<TCDefReferable, List<Concrete.Argument>> selfArgsMap = new HashMap<>();
Map<TCDefReferable, List<Referable>> selfArgsMap = new HashMap<>();
Map<TCDefReferable, Pair<List<Concrete.Parameter>, List<Pair<TCDefReferable, Integer>>>> paramsMap = new HashMap<>();
for (Concrete.Definition definition : definitions) {
List<Concrete.Parameter> newParams = Collections.emptyList();
Expand Down Expand Up @@ -111,7 +111,7 @@ record ParamData(TCDefReferable definition, Concrete.Parameter parameter, int in
if (params != null) {
Pair<Concrete.Parameter, Referable> param = Concrete.getParameter(params.parameters, data.proj2);
if (param != null) {
newParams.add(new Concrete.TelescopeParameter(definition.getData(), param.proj1.isExplicit(), Collections.singletonList(param.proj2), param.proj1.getType() == null ? null : param.proj1.getType(), param.proj1.isProperty()));
newParams.add(new Concrete.TelescopeParameter(definition.getData(), false, Collections.singletonList(param.proj2), param.proj1.getType() == null ? null : param.proj1.getType(), param.proj1.isProperty()));
}
}
}
Expand All @@ -132,11 +132,9 @@ record ParamData(TCDefReferable definition, Concrete.Parameter parameter, int in
}
newParams = newNewParams;

List<Concrete.Argument> selfArgs = new ArrayList<>();
List<Referable> selfArgs = new ArrayList<>();
for (Concrete.Parameter param : newParams) {
for (Referable referable : param.getReferableList()) {
selfArgs.add(new Concrete.Argument(new Concrete.ReferenceExpression(null, referable), param.isExplicit()));
}
selfArgs.addAll(param.getReferableList());
}
selfArgsMap.put(definition.getData(), selfArgs);

Expand Down Expand Up @@ -259,7 +257,16 @@ public Concrete.Expression visitApp(Concrete.AppExpression expr, Void params) {
return expr;
}
}
} else if (expr.getFunction() instanceof Concrete.ReferenceExpression refExpr && !expr.getArguments().get(0).isExplicit()) {
if (refExpr.getReferent() instanceof ParameterReferable) {
visitReference(refExpr, null);
}
for (Concrete.Argument argument : expr.getArguments()) {
argument.expression = argument.expression.accept(this, params);
}
return expr;
}

return super.visitApp(expr, params);
}

Expand Down Expand Up @@ -290,17 +297,17 @@ public Concrete.Expression visitReference(Concrete.ReferenceExpression expr, Voi
if (parameters != null) {
Pair<Concrete.Parameter, Referable> paramRef = Concrete.getParameter(parameters, pair.proj2);
if (paramRef != null) {
args.add(new Concrete.Argument(new Concrete.ReferenceExpression(expr.getData(), paramRef.proj2), paramRef.proj1.isExplicit()));
args.add(new Concrete.GeneratedArgument(new Concrete.ReferenceExpression(expr.getData(), paramRef.proj2)));
}
}
}
return Concrete.AppExpression.make(expr.getData(), expr, args);
} else {
List<Concrete.Argument> selfArgs = mySelfArgs.get(ref);
List<Referable> selfArgs = mySelfArgs.get(ref);
if (selfArgs != null) {
List<Concrete.Argument> args = new ArrayList<>(selfArgs.size());
for (Concrete.Argument arg : selfArgs) {
args.add(new Concrete.Argument(new Concrete.ReferenceExpression(expr.getData(), ((Concrete.ReferenceExpression) arg.expression).getReferent()), arg.isExplicit()));
for (Referable selfArg : selfArgs) {
args.add(new Concrete.GeneratedArgument(new Concrete.ReferenceExpression(expr.getData(), selfArg)));
}
return Concrete.AppExpression.make(expr.getData(), expr, args);
}
Expand Down
Loading

0 comments on commit 32bafde

Please sign in to comment.