Skip to content

Commit

Permalink
Implement expression prettifier and local expression prettifier
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Apr 16, 2024
1 parent 39c1879 commit d379740
Show file tree
Hide file tree
Showing 18 changed files with 99 additions and 129 deletions.
19 changes: 10 additions & 9 deletions meta/src/main/java/org/arend/lib/error/LinearSolverError.java
View file
Expand Up @@ -3,6 +3,7 @@
import org.arend.ext.concrete.ConcreteSourceNode;
import org.arend.ext.core.expr.CoreExpression;
import org.arend.ext.error.TypecheckingError;
import org.arend.ext.prettifier.ExpressionPrettifier;
import org.arend.ext.prettyprinting.PrettyPrinterConfig;
import org.arend.ext.prettyprinting.doc.Doc;
import org.arend.lib.meta.linear.Equation;
Expand All @@ -14,10 +15,12 @@
import static org.arend.ext.prettyprinting.doc.DocFactory.*;

public class LinearSolverError extends TypecheckingError {
private final ExpressionPrettifier prettifier;
private final List<? extends Equation<CoreExpression>> equations;

public LinearSolverError(boolean isContradiction, List<? extends Equation<CoreExpression>> equations, @Nullable ConcreteSourceNode cause) {
public LinearSolverError(ExpressionPrettifier prettifier, boolean isContradiction, List<? extends Equation<CoreExpression>> equations, @Nullable ConcreteSourceNode cause) {
super(isContradiction ? "Cannot infer a contradiction" : "Cannot solve the equation", cause);
this.prettifier = prettifier;
this.equations = equations;
}

Expand All @@ -26,14 +29,12 @@ public Doc getBodyDoc(PrettyPrinterConfig ppConfig) {
if (equations.isEmpty()) return nullDoc();
List<Doc> docs = new ArrayList<>(equations.size());
for (Equation<CoreExpression> equation : equations) {
String op;
switch (equation.operation) {
case LESS: op = "<";break;
case LESS_OR_EQUALS: op = "<="; break;
case EQUALS: op = "="; break;
default: throw new IllegalStateException();
}
docs.add(hang(termDoc(equation.lhsTerm, ppConfig), hang(text(op), termDoc(equation.rhsTerm, ppConfig))));
String op = switch (equation.operation) {
case LESS -> "<";
case LESS_OR_EQUALS -> "<=";
case EQUALS -> "=";
};
docs.add(hang(termDoc(equation.lhsTerm, prettifier, ppConfig), hang(text(op), termDoc(equation.rhsTerm, prettifier, ppConfig))));
}
return hang(text("Assumptions:"), vList(docs));
}
Expand Down
7 changes: 5 additions & 2 deletions meta/src/main/java/org/arend/lib/error/MetaDidNotFailError.java
View file
Expand Up @@ -3,21 +3,24 @@
import org.arend.ext.concrete.ConcreteSourceNode;
import org.arend.ext.core.expr.CoreExpression;
import org.arend.ext.error.TypecheckingError;
import org.arend.ext.prettifier.ExpressionPrettifier;
import org.arend.ext.prettyprinting.PrettyPrinterConfig;
import org.arend.ext.prettyprinting.doc.Doc;
import org.arend.ext.prettyprinting.doc.DocFactory;
import org.jetbrains.annotations.Nullable;

public class MetaDidNotFailError extends TypecheckingError {
private final ExpressionPrettifier prettifier;
public final CoreExpression result;

public MetaDidNotFailError(CoreExpression result, @Nullable ConcreteSourceNode cause) {
public MetaDidNotFailError(ExpressionPrettifier prettifier, CoreExpression result, @Nullable ConcreteSourceNode cause) {
super("Meta did not fail", cause);
this.prettifier = prettifier;
this.result = result;
}

@Override
public Doc getBodyDoc(PrettyPrinterConfig ppConfig) {
return DocFactory.hang(DocFactory.text("Result:"), DocFactory.termDoc(result, ppConfig));
return DocFactory.hang(DocFactory.text("Result:"), DocFactory.termDoc(result, prettifier, ppConfig));
}
}
9 changes: 6 additions & 3 deletions meta/src/main/java/org/arend/lib/error/SimplifyError.java
View file
Expand Up @@ -3,6 +3,7 @@
import org.arend.ext.concrete.ConcreteSourceNode;
import org.arend.ext.core.expr.CoreExpression;
import org.arend.ext.error.TypecheckingError;
import org.arend.ext.prettifier.ExpressionPrettifier;
import org.arend.ext.prettyprinting.PrettyPrinterConfig;
import org.arend.ext.prettyprinting.doc.Doc;
import org.jetbrains.annotations.Nullable;
Expand All @@ -13,20 +14,22 @@
import static org.arend.ext.prettyprinting.doc.DocFactory.termDoc;

public class SimplifyError extends TypecheckingError {
private final ExpressionPrettifier prettifier;
private final List<CoreExpression> subexprList;
private final CoreExpression type;

public SimplifyError(List<CoreExpression> subexprList, CoreExpression type, @Nullable ConcreteSourceNode cause) {
public SimplifyError(ExpressionPrettifier prettifier, List<CoreExpression> subexprList, CoreExpression type, @Nullable ConcreteSourceNode cause) {
super("Cannot simplify subexpressions", cause);
this.prettifier = prettifier;
this.subexprList = subexprList;
this.type = type;
}

@Override
public Doc getBodyDoc(PrettyPrinterConfig ppConfig) {
return vList(
hang(text("Subexpressions:"), hSep(text(", "), subexprList.stream().map(x -> termLine(x, ppConfig)).toList())),
hang(text("Type:"), termDoc(type, ppConfig)));
hang(text("Subexpressions:"), hSep(text(", "), subexprList.stream().map(x -> termLine(x, prettifier, ppConfig)).toList())),
hang(text("Type:"), termDoc(type, prettifier, ppConfig)));
}

@Override
Expand Down
12 changes: 7 additions & 5 deletions meta/src/main/java/org/arend/lib/error/SubexprError.java
View file
Expand Up @@ -3,33 +3,35 @@
import org.arend.ext.concrete.ConcreteSourceNode;
import org.arend.ext.core.expr.CoreExpression;
import org.arend.ext.error.TypecheckingError;
import org.arend.ext.prettifier.ExpressionPrettifier;
import org.arend.ext.prettyprinting.PrettyPrinterConfig;
import org.arend.ext.prettyprinting.doc.Doc;
import org.jetbrains.annotations.Nullable;

import java.util.List;
import java.util.stream.Collectors;

import static org.arend.ext.prettyprinting.doc.DocFactory.*;

public class SubexprError extends TypecheckingError {
private final ExpressionPrettifier prettifier;
private final CoreExpression subexpr;
private final CoreExpression subexprType;
private final CoreExpression expr;

public SubexprError(List<Integer> occurrences, CoreExpression subexpr, CoreExpression subexprType, CoreExpression expr, @Nullable ConcreteSourceNode cause) {
super("Cannot find subexpression" + (occurrences == null ? "" : " at " + occurrences.stream().map(x -> x + 1).collect(Collectors.toList())), cause);
public SubexprError(ExpressionPrettifier prettifier, List<Integer> occurrences, CoreExpression subexpr, CoreExpression subexprType, CoreExpression expr, @Nullable ConcreteSourceNode cause) {
super("Cannot find subexpression" + (occurrences == null ? "" : " at " + occurrences.stream().map(x -> x + 1).toList()), cause);
this.prettifier = prettifier;
this.expr = expr;
this.subexpr = subexpr;
this.subexprType = subexprType;
}

@Override
public Doc getBodyDoc(PrettyPrinterConfig ppConfig) {
Doc expectedDoc = hang(text("Subexpression:"), subexprType == null ? termDoc(subexpr, ppConfig) : hang(termDoc(subexpr, ppConfig), hang(text(":"), termDoc(subexprType, ppConfig))));
Doc expectedDoc = hang(text("Subexpression:"), subexprType == null ? termDoc(subexpr, prettifier, ppConfig) : hang(termDoc(subexpr, prettifier, ppConfig), hang(text(":"), termDoc(subexprType, prettifier, ppConfig))));
return vList(
expectedDoc,
hang(text(expectedDoc.getHeight() == 1 ? " Expression:" : "Expression:"), termDoc(expr, ppConfig)));
hang(text(expectedDoc.getHeight() == 1 ? " Expression:" : "Expression:"), termDoc(expr, prettifier, ppConfig)));
}

@Override
Expand Down
7 changes: 5 additions & 2 deletions meta/src/main/java/org/arend/lib/error/TypeError.java
View file
Expand Up @@ -3,22 +3,25 @@
import org.arend.ext.concrete.ConcreteSourceNode;
import org.arend.ext.core.expr.UncheckedExpression;
import org.arend.ext.error.TypecheckingError;
import org.arend.ext.prettifier.ExpressionPrettifier;
import org.arend.ext.prettyprinting.PrettyPrinterConfig;
import org.arend.ext.prettyprinting.doc.Doc;
import org.arend.ext.prettyprinting.doc.DocFactory;
import org.jetbrains.annotations.Nullable;

public class TypeError extends TypecheckingError {
public final ExpressionPrettifier prettifier;
public final UncheckedExpression type;

public TypeError(String message, UncheckedExpression type, @Nullable ConcreteSourceNode cause) {
public TypeError(ExpressionPrettifier prettifier, String message, UncheckedExpression type, @Nullable ConcreteSourceNode cause) {
super(message, cause);
this.prettifier = prettifier;
this.type = type;
}

@Override
public Doc getBodyDoc(PrettyPrinterConfig ppConfig) {
return DocFactory.hang(DocFactory.text("Type:"), DocFactory.termDoc(type, ppConfig));
return DocFactory.hang(DocFactory.text("Type:"), DocFactory.termDoc(type, prettifier, ppConfig));
}

@Override
Expand Down
4 changes: 2 additions & 2 deletions meta/src/main/java/org/arend/lib/meta/ConstructorMeta.java
View file
Expand Up @@ -124,7 +124,7 @@ public boolean requireExpectedType() {
if (type instanceof CoreDataCallExpression) {
List<CoreConstructor> constructors = ((CoreDataCallExpression) type).computeMatchedConstructors();
if (constructors == null) {
typechecker.getErrorReporter().report(new TypeError("Cannot compute constructors of data type", type, contextData.getMarker()));
typechecker.getErrorReporter().report(new TypeError(typechecker.getExpressionPrettifier(), "Cannot compute constructors of data type", type, contextData.getMarker()));
return null;
}

Expand Down Expand Up @@ -160,7 +160,7 @@ public boolean requireExpectedType() {
}
}

typechecker.getErrorReporter().report(new TypeError("Expected a type with 1 constructor", type, contextData.getMarker()));
typechecker.getErrorReporter().report(new TypeError(typechecker.getExpressionPrettifier(), "Expected a type with 1 constructor", type, contextData.getMarker()));
return null;
}
}
128 changes: 43 additions & 85 deletions meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java
View file
Expand Up @@ -70,66 +70,51 @@ private static class EqType extends RType {
}
}

private static class Negation {
final List<RType> assumptions;
final CoreExpression type;
final Function<Deque<ConcreteExpression>, ConcreteExpression> proof;

private Negation(List<RType> assumptions, CoreExpression type, Function<Deque<ConcreteExpression>, ConcreteExpression> proof) {
this.assumptions = assumptions;
this.type = type;
this.proof = proof;
}
}
private record Negation(List<RType> assumptions, CoreExpression type, Function<Deque<ConcreteExpression>, ConcreteExpression> proof) {}

private static RType makeRType(CoreBinding binding, CoreExpression paramType) {
CoreFunCallExpression equality = paramType.toEquality();
return equality != null ? new EqType(binding, equality, equality.getDefCallArguments().get(1), equality.getDefCallArguments().get(2)) : new RType(binding, paramType);
}

private static class NegationData {
final List<RType> types;
final Deque<Object> instructions; // either CoreConstructor or not; the latter indicates a variable

NegationData(List<RType> types, Deque<Object> instructions) {
this.types = types;
this.instructions = instructions;
}

/**
* @param instructions either CoreConstructor or not; the latter indicates a variable
*/
private record NegationData(List<RType> types, Deque<Object> instructions) {
private ConcreteExpression makeExpression(Deque<ConcreteExpression> arguments, CoreConstructor constructor, ConcreteFactory factory) {
List<ConcreteArgument> args = new ArrayList<>();
CoreParameter param = constructor.getParameters();
if (param.hasNext() && !param.isExplicit()) {
for (CoreParameter dataParam = constructor.getDataType().getParameters(); dataParam.hasNext(); dataParam = dataParam.getNext()) {
args.add(factory.arg(factory.hole(), false));
}
}
for (; param.hasNext(); param = param.getNext()) {
Object con = instructions.removeFirst();
if (con instanceof CoreConstructor) {
args.add(factory.arg(makeExpression(arguments, (CoreConstructor) con, factory), param.isExplicit()));
} else {
args.add(factory.arg(arguments.removeFirst(), param.isExplicit()));
}
}
return factory.app(factory.ref(constructor.getRef()), args);
}

Negation make(List<CoreParameter> parameters, CoreExpression codomain, ConcreteExpression proof, ConcreteFactory factory) {
return new Negation(types, codomain, arguments -> {
List<ConcreteArgument> args = new ArrayList<>();
for (CoreParameter param : parameters) {
CoreParameter param = constructor.getParameters();
if (param.hasNext() && !param.isExplicit()) {
for (CoreParameter dataParam = constructor.getDataType().getParameters(); dataParam.hasNext(); dataParam = dataParam.getNext()) {
args.add(factory.arg(factory.hole(), false));
}
}
for (; param.hasNext(); param = param.getNext()) {
Object con = instructions.removeFirst();
if (con instanceof CoreConstructor) {
args.add(factory.arg(makeExpression(arguments, (CoreConstructor) con, factory), param.isExplicit()));
} else {
args.add(factory.arg(arguments.removeFirst(), param.isExplicit()));
}
}
return factory.app(proof, args);
});
return factory.app(factory.ref(constructor.getRef()), args);
}

Negation make(List<CoreParameter> parameters, CoreExpression codomain, ConcreteExpression proof, ConcreteFactory factory) {
return new Negation(types, codomain, arguments -> {
List<ConcreteArgument> args = new ArrayList<>();
for (CoreParameter param : parameters) {
Object con = instructions.removeFirst();
if (con instanceof CoreConstructor) {
args.add(factory.arg(makeExpression(arguments, (CoreConstructor) con, factory), param.isExplicit()));
} else {
args.add(factory.arg(arguments.removeFirst(), param.isExplicit()));
}
}
return factory.app(proof, args);
});
}
}
}

private boolean isAppropriateDataCall(CoreExpression type) {
if (!(type instanceof CoreDataCallExpression)) {
Expand Down Expand Up @@ -177,32 +162,21 @@ private void makeNegationData(Deque<CoreParameter> parameters, CoreExpression co
result.add(negationData);
}

private static class Triple {
final CoreFieldCallExpression fun;
final CoreExpression arg1;
final CoreExpression arg2;

Triple(CoreFieldCallExpression fun, CoreExpression arg1, CoreExpression arg2) {
this.fun = fun;
this.arg1 = arg1;
this.arg2 = arg2;
}
private record Triple(CoreFieldCallExpression fun, CoreExpression arg1, CoreExpression arg2) {

public static Triple make(CoreExpression expr) {
if (!(expr instanceof CoreAppExpression)) {
return null;
}
if (!(expr instanceof CoreAppExpression app2)) {
return null;
}

CoreAppExpression app2 = (CoreAppExpression) expr;
if (!(app2.getFunction() instanceof CoreAppExpression)) {
return null;
}
if (!(app2.getFunction() instanceof CoreAppExpression app1)) {
return null;
}

CoreAppExpression app1 = (CoreAppExpression) app2.getFunction();
CoreExpression fun = app1.getFunction();
return fun instanceof CoreFieldCallExpression ? new Triple((CoreFieldCallExpression) fun, app1.getArgument(), app2.getArgument()) : null;
CoreExpression fun = app1.getFunction();
return fun instanceof CoreFieldCallExpression ? new Triple((CoreFieldCallExpression) fun, app1.getArgument(), app2.getArgument()) : null;
}
}
}

private boolean makeNegation(CoreExpression type, ConcreteExpression proof, ConcreteFactory factory, List<Negation> negations, Values<UncheckedExpression> values, Map<CoreClassField, Map<Integer, List<Edge<Integer>>>> transGraphs) {
List<CoreParameter> parameters;
Expand Down Expand Up @@ -234,10 +208,8 @@ private boolean makeNegation(CoreExpression type, ConcreteExpression proof, Conc
negations.add(negationData.make(parameters, type, proof, factory));
}
return true;
} else if (parameters.isEmpty() && type instanceof CoreAppExpression) {
CoreAppExpression app2 = (CoreAppExpression) type;
if (app2.getFunction() instanceof CoreAppExpression) {
CoreAppExpression app1 = (CoreAppExpression) app2.getFunction();
} else if (parameters.isEmpty() && type instanceof CoreAppExpression app2) {
if (app2.getFunction() instanceof CoreAppExpression app1) {
CoreExpression fun = app1.getFunction();
if (fun instanceof CoreFieldCallExpression) {
CoreClassField field = ((CoreFieldCallExpression) fun).getDefinition();
Expand Down Expand Up @@ -313,21 +285,7 @@ public ConcreteExpression check(Context context, ConcreteExpression argument, Co

private enum EdgeKind { EQ, EQ_INV, LESS, LESS_OR_EQ }

private static class Edge<V> {
final V source;
final V target;
final ConcreteExpression proof;
final EdgeKind kind;
final ConcreteExpression leftApp;

Edge(V source, V target, ConcreteExpression proof, EdgeKind kind, ConcreteExpression leftApp) {
this.source = source;
this.target = target;
this.proof = proof;
this.kind = kind;
this.leftApp = leftApp;
}
}
private record Edge<V>(V source, V target, ConcreteExpression proof, EdgeKind kind, ConcreteExpression leftApp) {}

/**
* Finds the shortest path from {@code first} to {@code last} that contains a LESS edge.
Expand Down Expand Up @@ -415,7 +373,7 @@ private ConcreteExpression checkInternal(Context context, ConcreteExpression arg
contr = factory.core(contradiction);
} else {
if (!makeNegation(type, factory.core(contradiction), factory, negations, values, transGraphs)) {
typechecker.getErrorReporter().report(new TypeError("The expression does not prove a contradiction", type, argument));
typechecker.getErrorReporter().report(new TypeError(typechecker.getExpressionPrettifier(), "The expression does not prove a contradiction", type, argument));
return null;
}
}
Expand Down
2 changes: 1 addition & 1 deletion meta/src/main/java/org/arend/lib/meta/ExtMeta.java
View file
Expand Up @@ -703,7 +703,7 @@ public void solve(@NotNull ExpressionTypechecker typechecker, @NotNull ConcreteG
return haveClauses.isEmpty() ? let : factory.letExpr(true, false, haveClauses, let);
}

typechecker.getErrorReporter().report(new TypeError("Cannot apply extensionality", type, marker));
typechecker.getErrorReporter().report(new TypeError(typechecker.getExpressionPrettifier(), "Cannot apply extensionality", type, marker));
return null;
}
}
Expand Down

0 comments on commit d379740

Please sign in to comment.