Skip to content

Commit

Permalink
ERROR: less classes
Browse files Browse the repository at this point in the history
  • Loading branch information
@ice1000
ice1000 committed Sep 10, 2021
1 parent 6cc15ae commit f3335eb
Show file tree
Hide file tree
Showing 2 changed files with 38 additions and 61 deletions.
16 changes: 8 additions & 8 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Expand Up @@ -139,7 +139,7 @@ private static boolean needImplicitParamIns(@NotNull Expr expr, @NotNull FormTer
if (term == null) term = generatePi(expr);
if (term instanceof CallTerm.Hole) unifyTy(term, generatePi(expr), expr.sourcePos());
if (!(term.normalize(NormalizeMode.WHNF) instanceof FormTerm.Pi dt)) {
return fail(expr, term, new BadTypeError.Pi(expr, term));
return fail(expr, term, BadTypeError.pi(expr, term));
}
var param = expr.param();
if (param.explicit() != dt.param().explicit()) {
Expand Down Expand Up @@ -361,7 +361,7 @@ private Result unifyTyMaybeInsert(@Nullable Term upper, @NotNull Term lower, @No
@Override public Result visitNew(Expr.@NotNull NewExpr expr, @Nullable Term term) {
var struct = checkNoZonk(expr.struct(), null).wellTyped;
if (!(struct instanceof CallTerm.Struct structCall))
return fail(expr.struct(), struct, new BadTypeError.StructCon(expr, struct));
return fail(expr.struct(), struct, BadTypeError.structCon(expr, struct));
var structRef = structCall.ref();

var subst = new Substituter.TermSubst(MutableMap.create());
Expand Down Expand Up @@ -440,7 +440,7 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
var projectee = checkNoZonk(struct, null);
var whnf = projectee.type.normalize(NormalizeMode.WHNF);
if (!(whnf instanceof CallTerm.Struct structCall))
return fail(struct, whnf, new BadTypeError.StructAcc(struct, fieldName, whnf));
return fail(struct, whnf, BadTypeError.structAcc(struct, fieldName, whnf));

var structCore = structCall.ref().core;
if (structCore == null) throw new UnsupportedOperationException("TODO");
Expand All @@ -467,7 +467,7 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
var projectee = checkNoZonk(tuple, null);
var whnf = projectee.type.normalize(NormalizeMode.WHNF);
if (!(whnf instanceof FormTerm.Sigma sigma))
return fail(tuple, whnf, new BadTypeError.SigmaAcc(tuple, ix, whnf));
return fail(tuple, whnf, BadTypeError.sigmaAcc(tuple, ix, whnf));
var telescope = sigma.params();
var index = ix - 1;
if (index < 0 || index >= telescope.size()) {
Expand All @@ -491,7 +491,7 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
var f = checkNoZonk(expr.function(), null);
var app = f.wellTyped;
if (!(f.type.normalize(NormalizeMode.WHNF) instanceof FormTerm.Pi piTerm))
return fail(expr, f.type, new BadTypeError.Pi(expr, f.type));
return fail(expr, f.type, BadTypeError.pi(expr, f.type));
var pi = piTerm;
var subst = new Substituter.TermSubst(MutableMap.create());
for (var iter = expr.arguments().iterator(); iter.hasNext(); ) {
Expand All @@ -506,7 +506,7 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
app = CallTerm.make(app, new Arg<>(holeApp, false));
var newPi = instPi(pi, subst, holeApp);
if (newPi.isLeft()) pi = newPi.getLeftValue();
else return fail(expr, newPi.getRightValue(), new BadTypeError.Pi(expr, newPi.getRightValue()));
else return fail(expr, newPi.getRightValue(), BadTypeError.pi(expr, newPi.getRightValue()));
} else {
// TODO[ice]: no implicit argument expected, but inserted.
throw new TyckerException();
Expand All @@ -518,7 +518,7 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
if (iter.hasNext()) {
var newPi = instPi(pi, subst, elabArg);
if (newPi.isLeft()) pi = newPi.getLeftValue();
else return fail(expr, newPi.getRightValue(), new BadTypeError.Pi(expr, newPi.getRightValue()));
else return fail(expr, newPi.getRightValue(), BadTypeError.pi(expr, newPi.getRightValue()));
}
subst.map().put(pi.param().ref(), elabArg);
}
Expand Down Expand Up @@ -555,7 +555,7 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
resultLast.value = result.type;
});
} else if (!(term.normalize(NormalizeMode.WHNF) instanceof FormTerm.Sigma dt)) {
return fail(expr, term, new BadTypeError.SigmaCon(expr, term));
return fail(expr, term, BadTypeError.sigmaCon(expr, term));
} else {
var againstTele = dt.params().view();
var last = dt.params().last().type();
Expand Down
83 changes: 30 additions & 53 deletions base/src/main/java/org/aya/tyck/error/BadTypeError.java
View file
Expand Up @@ -11,12 +11,16 @@
import org.aya.pretty.doc.Style;
import org.jetbrains.annotations.NotNull;

public interface BadTypeError extends ExprProblem {
@Override default @NotNull Severity level() {
public record BadTypeError(
@Override @NotNull Expr expr,
@NotNull Term actualType, @NotNull Doc action,
@NotNull Doc thing, @NotNull Doc desired
) implements ExprProblem {
@Override public @NotNull Severity level() {
return Severity.ERROR;
}

private static @NotNull Doc genDescribe(@NotNull Expr expr, @NotNull Term actualType, @NotNull Doc action, @NotNull Doc thing, @NotNull Doc desired) {
@Override public @NotNull Doc describe() {
return Doc.vcat(
Doc.sep(Doc.english("Unable to"), action, Doc.english("the expression")),
Doc.par(1, expr.toDoc(DistillerOptions.DEFAULT)),
Expand All @@ -26,63 +30,36 @@ public interface BadTypeError extends ExprProblem {
);
}

record Pi(
@NotNull Expr expr,
@NotNull Term actualType
) implements BadTypeError {
@Override public @NotNull Doc describe() {
return genDescribe(expr, actualType, Doc.plain("apply"),
Doc.english("of what you applied"), Doc.english("Pi type"));
}
public static @NotNull BadTypeError pi(@NotNull Expr expr, @NotNull Term actualType) {
return new BadTypeError(expr, actualType, Doc.plain("apply"),
Doc.english("of what you applied"), Doc.english("Pi type"));
}

record SigmaAcc(
@NotNull Expr expr,
int ix,
@NotNull Term actualType
) implements BadTypeError {
@Override public @NotNull Doc describe() {
return genDescribe(expr, actualType,
Doc.sep(Doc.english("project the"), Doc.ordinal(ix), Doc.english("element of")),
Doc.english("of what you projected on"),
Doc.english("Sigma type"));
}
public static @NotNull BadTypeError sigmaAcc(@NotNull Expr expr, int ix, @NotNull Term actualType) {
return new BadTypeError(expr, actualType,
Doc.sep(Doc.english("project the"), Doc.ordinal(ix), Doc.english("element of")),
Doc.english("of what you projected on"),
Doc.english("Sigma type"));
}

record SigmaCon(
@NotNull Expr expr,
@NotNull Term actualType
) implements BadTypeError {
@Override public @NotNull Doc describe() {
return genDescribe(expr, actualType,
Doc.sep(Doc.plain("construct")),
Doc.english("you checks it against"),
Doc.english("Sigma type"));
}
public static @NotNull BadTypeError sigmaCon(@NotNull Expr expr, @NotNull Term actualType) {
return new BadTypeError(expr, actualType,
Doc.sep(Doc.plain("construct")),
Doc.english("you checks it against"),
Doc.english("Sigma type"));
}

record StructAcc(
@NotNull Expr expr,
@NotNull String fieldName,
@NotNull Term actualType
) implements BadTypeError {
@Override public @NotNull Doc describe() {
return genDescribe(expr, actualType,
Doc.sep(Doc.english("access field"), Doc.styled(Style.code(), Doc.plain(fieldName)), Doc.plain("of")),
Doc.english("of what you accessed"),
Doc.english("struct type"));
}
public static @NotNull BadTypeError structAcc(@NotNull Expr expr, @NotNull String fieldName, @NotNull Term actualType) {
return new BadTypeError(expr, actualType,
Doc.sep(Doc.english("access field"), Doc.styled(Style.code(), Doc.plain(fieldName)), Doc.plain("of")),
Doc.english("of what you accessed"),
Doc.english("struct type"));
}

record StructCon(
@NotNull Expr expr,
@NotNull Term actualType
) implements BadTypeError {
@Override public @NotNull Doc describe() {
return genDescribe(expr, actualType,
Doc.sep(Doc.plain("construct")),
Doc.english("you gave"),
Doc.english("struct type"));
}
public static @NotNull BadTypeError structCon(@NotNull Expr expr, @NotNull Term actualType) {
return new BadTypeError(expr, actualType,
Doc.sep(Doc.plain("construct")),
Doc.english("you gave"),
Doc.english("struct type"));
}
}

0 comments on commit f3335eb

Please sign in to comment.