Skip to content

Commit

Permalink
Move code from DesugarVisitor to ExpressionResolveNameVisitor (#147)
Browse files Browse the repository at this point in the history
  • Loading branch information
@ice1000
ice1000 committed Apr 3, 2020
1 parent 1b8a17c commit 9f0f355
Show file tree
Hide file tree
Showing 3 changed files with 87 additions and 87 deletions.
82 changes: 81 additions & 1 deletion base/src/main/java/org/arend/naming/resolving/visitor/ExpressionResolveNameVisitor.java
View file
Expand Up @@ -3,6 +3,8 @@
import org.arend.core.context.Utils;
import org.arend.ext.error.ErrorReporter;
import org.arend.ext.error.GeneralError;
import org.arend.ext.error.LocalError;
import org.arend.ext.error.TypecheckingError;
import org.arend.naming.BinOpParser;
import org.arend.naming.error.DuplicateNameError;
import org.arend.naming.error.NamingError;
Expand All @@ -13,7 +15,6 @@
import org.arend.term.concrete.BaseConcreteExpressionVisitor;
import org.arend.term.concrete.Concrete;
import org.arend.typechecking.error.local.ExpectedConstructorError;
import org.arend.ext.error.LocalError;
import org.arend.typechecking.provider.ConcreteProvider;

import java.util.*;
Expand Down Expand Up @@ -187,6 +188,10 @@ public Concrete.Expression visitSigma(Concrete.SigmaExpression expr, Void params

@Override
public Concrete.Expression visitCase(Concrete.CaseExpression expr, Void params) {
List<Concrete.Parameter> parameters = new ArrayList<>();
convertCaseAppHoles(expr, parameters);
if (!parameters.isEmpty())
return new Concrete.LamExpression(expr.getData(), parameters, expr).accept(this, null);
Set<Referable> eliminatedRefs = new HashSet<>();
try (Utils.ContextSaver ignored = new Utils.ContextSaver(myContext)) {
for (Concrete.CaseArgument caseArg : expr.getArguments()) {
Expand Down Expand Up @@ -226,6 +231,10 @@ public Concrete.Expression visitCase(Concrete.CaseExpression expr, Void params)

@Override
public Concrete.Expression visitBinOpSequence(Concrete.BinOpSequenceExpression expr, Void params) {
List<Concrete.Parameter> parameters = new ArrayList<>();
convertBinOpAppHoles(expr, parameters);
if (!parameters.isEmpty())
return new Concrete.LamExpression(expr.getData(), parameters, expr).accept(this, null);
Concrete.Expression result = super.visitBinOpSequence(expr, null);
return result instanceof Concrete.BinOpSequenceExpression ? new BinOpParser(myErrorReporter).parse((Concrete.BinOpSequenceExpression) result) : result;
}
Expand Down Expand Up @@ -487,4 +496,75 @@ public Concrete.Expression visitLet(Concrete.LetExpression expr, Void params) {
return expr;
}
}

@Override
public Concrete.Expression visitProj(Concrete.ProjExpression expr, Void params) {
if (expr.expression instanceof Concrete.ApplyHoleExpression) {
List<Concrete.Parameter> parameters = new ArrayList<>(1);
convertProjAppHoles(expr, parameters);
return new Concrete.LamExpression(expr.expression.getData(), parameters, expr).accept(this, null);
} else return super.visitProj(expr, params);
}

@Override
public Concrete.Expression visitApplyHole(Concrete.ApplyHoleExpression expr, Void params) {
myErrorReporter.report(new TypecheckingError("`__` not allowed here", expr));
return super.visitApplyHole(expr, params);
}

private static void convertBinOpAppHoles(Concrete.BinOpSequenceExpression expr, List<Concrete.Parameter> parameters) {
for (Concrete.BinOpSequenceElem elem : expr.getSequence())
if (elem.expression instanceof Concrete.ApplyHoleExpression) {
Object data = elem.expression.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
elem.expression = new Concrete.ReferenceExpression(data, ref);
} else convertRecursively(elem.expression, parameters);
}

private static void convertRecursively(Concrete.Expression expression, List<Concrete.Parameter> parameters) {
if (expression instanceof Concrete.AppExpression)
convertAppHoles((Concrete.AppExpression) expression, parameters);
else if (expression instanceof Concrete.ProjExpression)
convertProjAppHoles((Concrete.ProjExpression) expression, parameters);
else if (expression instanceof Concrete.BinOpSequenceExpression)
convertBinOpAppHoles((Concrete.BinOpSequenceExpression) expression, parameters);
else if (expression instanceof Concrete.CaseExpression)
convertCaseAppHoles((Concrete.CaseExpression) expression, parameters);
}

private static void convertAppHoles(Concrete.AppExpression expr, List<Concrete.Parameter> parameters) {
Concrete.Expression originalFunc = expr.getFunction();
if (originalFunc instanceof Concrete.ApplyHoleExpression) {
Object data = originalFunc.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
expr.setFunction(new Concrete.ReferenceExpression(data, ref));
}
for (Concrete.Argument argument : expr.getArguments())
if (argument.expression instanceof Concrete.ApplyHoleExpression) {
Object data = argument.expression.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
argument.expression = new Concrete.ReferenceExpression(data, ref);
}
}

private static void convertProjAppHoles(Concrete.ProjExpression proj, List<Concrete.Parameter> parameters) {
if (!(proj.expression instanceof Concrete.ApplyHoleExpression)) return;
Object data = proj.expression.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
proj.expression = new Concrete.ReferenceExpression(data, ref);
}

private static void convertCaseAppHoles(Concrete.CaseExpression expr, List<Concrete.Parameter> parameters) {
for (Concrete.CaseArgument argument : expr.getArguments())
if (argument.expression instanceof Concrete.ApplyHoleExpression) {
Object data = argument.expression.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
argument.expression = new Concrete.ReferenceExpression(data, ref);
} else convertRecursively(argument.expression, parameters);
}
}
81 changes: 0 additions & 81 deletions base/src/main/java/org/arend/typechecking/visitor/DesugarVisitor.java
View file
Expand Up @@ -4,7 +4,6 @@
import org.arend.ext.error.ErrorReporter;
import org.arend.ext.error.LocalError;
import org.arend.ext.error.TypecheckingError;
import org.arend.ext.reference.Precedence;
import org.arend.naming.reference.*;
import org.arend.naming.scope.ClassFieldImplScope;
import org.arend.prelude.Prelude;
Expand Down Expand Up @@ -228,11 +227,6 @@ public Concrete.Expression visitReference(Concrete.ReferenceExpression expr, Voi

@Override
public Concrete.Expression visitApp(Concrete.AppExpression expr, Void params) {
List<Concrete.Parameter> parameters = new ArrayList<>();
convertAppHoles(expr, parameters);
if (!parameters.isEmpty())
return new Concrete.LamExpression(expr.getData(), parameters, expr).accept(this, null);

if (!(expr.getFunction() instanceof Concrete.ReferenceExpression)) {
return super.visitApp(expr, null);
}
Expand All @@ -243,64 +237,6 @@ public Concrete.Expression visitApp(Concrete.AppExpression expr, Void params) {
return visitApp((Concrete.ReferenceExpression) expr.getFunction(), expr.getArguments(), expr, true);
}

private static void convertAppHoles(Concrete.AppExpression expr, List<Concrete.Parameter> parameters) {
Concrete.Expression originalFunc = expr.getFunction();
if (originalFunc instanceof Concrete.ApplyHoleExpression) {
Object data = originalFunc.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
expr.setFunction(new Concrete.ReferenceExpression(data, ref));
}
boolean isOp = false;
if (originalFunc instanceof Concrete.ReferenceExpression) {
Referable referable = originalFunc.getUnderlyingReferable();
if (referable instanceof GlobalReferable) {
Precedence precedence = ((GlobalReferable) referable).getPrecedence();
isOp = precedence.isInfix;
}
}
for (Concrete.Argument argument : expr.getArguments())
if (argument.expression instanceof Concrete.ApplyHoleExpression) {
Object data = argument.expression.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
argument.expression = new Concrete.ReferenceExpression(data, ref);
} else if (isOp && argument.expression instanceof Concrete.AppExpression)
convertAppHoles((Concrete.AppExpression) argument.expression, parameters);
else if (isOp && argument.expression instanceof Concrete.ProjExpression)
convertProjAppHoles((Concrete.ProjExpression) argument.expression, parameters);
else if (isOp && argument.expression instanceof Concrete.CaseExpression)
convertCaseAppHoles((Concrete.CaseExpression) argument.expression, parameters);
}

private static void convertProjAppHoles(Concrete.ProjExpression proj, List<Concrete.Parameter> parameters) {
if (!(proj.expression instanceof Concrete.ApplyHoleExpression)) return;
Object data = proj.expression.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
proj.expression = new Concrete.ReferenceExpression(data, ref);
}

private static void convertCaseAppHoles(Concrete.CaseExpression expr, List<Concrete.Parameter> parameters) {
for (Concrete.CaseArgument argument : expr.getArguments())
if (argument.expression instanceof Concrete.AppExpression)
convertAppHoles((Concrete.AppExpression) argument.expression, parameters);
else if (argument.expression instanceof Concrete.ProjExpression)
convertProjAppHoles((Concrete.ProjExpression) argument.expression, parameters);
else if (argument.expression instanceof Concrete.ApplyHoleExpression) {
Object data = argument.expression.getData();
LocalReferable ref = new LocalReferable("p" + parameters.size());
parameters.add(new Concrete.NameParameter(data, true, ref));
argument.expression = new Concrete.ReferenceExpression(data, ref);
}
}

@Override
public Concrete.Expression visitApplyHole(Concrete.ApplyHoleExpression expr, Void params) {
myErrorReporter.report(new TypecheckingError("`__` not allowed here", expr));
return super.visitApplyHole(expr, params);
}

@Override
public Concrete.Expression visitClassExt(Concrete.ClassExtExpression expr, Void params) {
Concrete.Expression classExpr = expr.getBaseClassExpression();
Expand Down Expand Up @@ -395,23 +331,6 @@ private void visitClassFieldImpl(Concrete.ClassFieldImpl classFieldImpl, List<?
}
}

@Override
public Concrete.Expression visitProj(Concrete.ProjExpression expr, Void params) {
if (expr.expression instanceof Concrete.ApplyHoleExpression) {
List<Concrete.Parameter> parameters = new ArrayList<>(1);
convertProjAppHoles(expr, parameters);
return new Concrete.LamExpression(expr.expression.getData(), parameters, expr).accept(this, null);
} else return super.visitProj(expr, params);
}

@Override
public Concrete.Expression visitCase(Concrete.CaseExpression expr, Void params) {
List<Concrete.Parameter> parameters = new ArrayList<>();
convertCaseAppHoles(expr, parameters);
return parameters.isEmpty() ? super.visitCase(expr, params)
: new Concrete.LamExpression(expr.getData(), parameters, expr).accept(this, null);
}

@Override
protected <T extends Concrete.ClassElement> void visitClassElements(List<T> elements, Void params) {
if (elements.isEmpty()) {
Expand Down
11 changes: 6 additions & 5 deletions src/test/java/org/arend/typechecking/AppHoleTest.java
View file
Expand Up @@ -68,20 +68,21 @@ public void inTuple() {
@Test
public void inApplicant() {
Expression ty = typeCheckExpr("(Nat -> Nat) -> Nat", null).expression;
Expression result = typeCheckExpr("__ 233", ty).expression;
assertTrue(result instanceof LamExpression);
assertTrue(typeCheckExpr("__ 233", ty)
.expression instanceof LamExpression);
}

@Test
public void implicit() {
assertTrue(typeCheckExpr("idp {__}", null).expression instanceof LamExpression);
assertTrue(typeCheckExpr("idp {__}", null)
.expression instanceof LamExpression);
}

@Test
public void inApp() {
Expression ty = typeCheckExpr("\\Set0 -> \\Set1", null).expression;
Expression result = typeCheckExpr("Path (\\lam _ => \\Set0) __ Nat", ty).expression;
assertTrue(result instanceof LamExpression);
assertTrue(typeCheckExpr("Path (\\lam _ => \\Set0) __ Nat", ty)
.expression instanceof LamExpression);
}

@Test
Expand Down

0 comments on commit 9f0f355

Please sign in to comment.