From a6e9a4f3389deb2ad1579702f86ac209049f68d8 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 12 Jul 2024 13:11:09 -0400 Subject: [PATCH] class: code review, do not compute all the types --- .../main/java/org/aya/tyck/ExprTycker.java | 41 +++++++++---------- .../java/org/aya/tyck/error/ClassError.java | 11 ++--- .../java/org/aya/tyck/tycker/AppTycker.java | 10 ++--- .../java/org/aya/unify/TermComparator.java | 4 +- .../java/org/aya/syntax/concrete/Expr.java | 9 +--- 5 files changed, 29 insertions(+), 46 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index 41e2855ac..ed489f0f1 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.java @@ -2,11 +2,9 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.tyck; -import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; import kala.collection.immutable.ImmutableTreeSeq; import kala.collection.mutable.MutableList; -import kala.collection.mutable.MutableMap; import kala.collection.mutable.MutableStack; import kala.collection.mutable.MutableTreeSet; import kala.control.Result; @@ -15,7 +13,6 @@ import org.aya.syntax.concrete.Expr; import org.aya.syntax.core.Closure; import org.aya.syntax.core.def.DataDefLike; -import org.aya.syntax.core.def.MemberDefLike; import org.aya.syntax.core.def.PrimDef; import org.aya.syntax.core.repr.AyaShape; import org.aya.syntax.core.term.*; @@ -176,7 +173,7 @@ case PiTerm(var dom, var cod) -> { var forget = resultClazz.args().drop(clazz.args().size()); return new Jdg.Default(new ClassCastTerm(clazz.ref(), result.wellTyped(), clazz.args(), forget), type); } else { - // TODO: skip unifyTyReported below + return makeErrorResult(type, result); } } } @@ -340,15 +337,15 @@ yield subscoped(param.ref(), wellParam, () -> var type = new DataCall(def, 0, ImmutableSeq.of(elementTy)); yield new Jdg.Default(new ListTerm(results, match.recog(), type), type); } - case Expr.New neutron -> { - var wellTyped = synthesize(neutron.classCall()); + case Expr.New(var classCall) -> { + var wellTyped = synthesize(classCall); if (!(wellTyped.wellTyped() instanceof ClassCall call)) { - yield fail(expr.data(), new ClassError.NotClassCall(neutron.classCall())); + yield fail(expr.data(), new ClassError.NotClassCall(classCall)); } // check whether the call is fully applied if (call.args().size() != call.ref().members().size()) { - yield fail(expr.data(), new ClassError.NotFullyApplied(neutron.classCall())); + yield fail(expr.data(), new ClassError.NotFullyApplied(classCall)); } yield new Jdg.Default(new NewTerm(call), call); @@ -397,11 +394,11 @@ case CompiledVar(var content) -> new AppTycker<>(this, sourcePos, args.size(), l private Jdg computeArgs( @NotNull SourcePos pos, @NotNull ImmutableSeq args, - @NotNull AbstractTele params, @NotNull BiFunction k + @NotNull AbstractTele params, @NotNull BiFunction k ) throws NotPi { int argIx = 0, paramIx = 0; var result = new Term[params.telescopeSize()]; - var types = new Term[params.telescopeSize()]; + Term firstType = null; while (argIx < args.size() && paramIx < params.telescopeSize()) { var arg = args.get(argIx); var param = params.telescopeRich(paramIx, result); @@ -412,39 +409,39 @@ private Jdg computeArgs( break; } else if (arg.name() == null) { // here, arg.explicit() == true and param.explicit() == false - result[paramIx] = insertImplicit(param, arg.sourcePos()); - types[paramIx++] = param.type(); + if (paramIx == 0) firstType = param.type(); + result[paramIx++] = insertImplicit(param, arg.sourcePos()); continue; } } if (arg.name() != null && !param.nameEq(arg.name())) { - result[paramIx] = insertImplicit(param, arg.sourcePos()); - types[paramIx++] = param.type(); + if (paramIx == 0) firstType = param.type(); + result[paramIx++] = insertImplicit(param, arg.sourcePos()); continue; } var what = inherit(arg.arg(), param.type()); - result[paramIx] = what.wellTyped(); - types[paramIx++] = what.type(); + if (paramIx == 0) firstType = param.type(); + result[paramIx++] = what.wellTyped(); argIx++; } // Trailing implicits while (paramIx < params.telescopeSize()) { if (params.telescopeLicit(paramIx)) break; var param = params.telescopeRich(paramIx, result); - result[paramIx] = insertImplicit(param, pos); - types[paramIx++] = param.type(); + if (paramIx == 0) firstType = param.type(); + result[paramIx++] = insertImplicit(param, pos); } var extraParams = MutableStack.>create(); if (argIx < args.size()) { - return generateApplication(args.drop(argIx), k.apply(result, types)); + return generateApplication(args.drop(argIx), k.apply(result, firstType)); } else while (paramIx < params.telescopeSize()) { var param = params.telescopeRich(paramIx, result); var atarashiVar = LocalVar.generate(param.name()); extraParams.push(new Pair<>(atarashiVar, param.type())); - result[paramIx] = new FreeTerm(atarashiVar); - types[paramIx++] = param.type(); + if (paramIx == 0) firstType = param.type(); + result[paramIx++] = new FreeTerm(atarashiVar); } - var generated = k.apply(result, types); + var generated = k.apply(result, firstType); while (extraParams.isNotEmpty()) { var pair = extraParams.pop(); generated = new Jdg.Default( diff --git a/base/src/main/java/org/aya/tyck/error/ClassError.java b/base/src/main/java/org/aya/tyck/error/ClassError.java index 9074af807..bc6954a8a 100644 --- a/base/src/main/java/org/aya/tyck/error/ClassError.java +++ b/base/src/main/java/org/aya/tyck/error/ClassError.java @@ -12,21 +12,16 @@ public interface ClassError extends TyckError { @NotNull WithPos problemExpr(); - @Override - default @NotNull SourcePos sourcePos() { - return problemExpr().sourcePos(); - } + @Override default @NotNull SourcePos sourcePos() { return problemExpr().sourcePos(); } record NotClassCall(@Override @NotNull WithPos problemExpr) implements ClassError { - @Override - public @NotNull Doc describe(@NotNull PrettierOptions options) { + @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return Doc.sep(Doc.english("Unable to new a non-class type:"), Doc.code(problemExpr.data().toDoc(options))); } } record NotFullyApplied(@Override @NotNull WithPos problemExpr) implements ClassError { - @Override - public @NotNull Doc describe(@NotNull PrettierOptions options) { + @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return Doc.sep(Doc.english("Unable to new an incomplete class type:"), Doc.code(problemExpr.data().toDoc(options))); } } diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java index 7e5a206dd..cb0d6b96b 100644 --- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java @@ -30,14 +30,12 @@ import org.jetbrains.annotations.Nullable; import java.util.function.BiFunction; -import java.util.function.Function; public record AppTycker( @Override @NotNull TyckState state, @NotNull AbstractTycker tycker, @NotNull SourcePos pos, - int argsCount, - int lift, + int argsCount, int lift, @NotNull Factory makeArgs ) implements Stateful { /** @@ -52,7 +50,7 @@ public record AppTycker( */ @FunctionalInterface public interface Factory extends - CheckedBiFunction, Jdg, Ex> { + CheckedBiFunction, Jdg, Ex> { } public AppTycker( @@ -164,9 +162,9 @@ public AppTycker( private @NotNull Jdg checkProjCall(@NotNull MemberDefLike member) throws Ex { var signature = member.signature().lift(lift); - return makeArgs.applyChecked(signature, (args, ty) -> { + return makeArgs.applyChecked(signature, (args, fstTy) -> { assert args.length >= 1; - var ofTy = whnf(ty[0]); + var ofTy = whnf(fstTy); if (!(ofTy instanceof ClassCall classTy)) throw new UnsupportedOperationException("report"); // TODO var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]); return new Jdg.Default( diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java index 71dd1b2b9..045d4295c 100644 --- a/base/src/main/java/org/aya/unify/TermComparator.java +++ b/base/src/main/java/org/aya/unify/TermComparator.java @@ -33,7 +33,6 @@ import org.jetbrains.annotations.Nullable; import java.util.Objects; -import java.util.function.BiFunction; import java.util.function.Function; import java.util.function.Supplier; import java.util.function.UnaryOperator; @@ -178,12 +177,11 @@ private boolean checkApproxResult(@Nullable Term type, Term approxResult) { */ private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Term type) { return switch (whnf(type)) { - // TODO: ClassCall case LamTerm _, ConCallLike _, TupTerm _ -> Panic.unreachable(); case ErrorTerm _ -> true; case ClassCall classCall -> { if (classCall.args().size() == classCall.ref().members().size()) yield true; - // TODO: should we compare fields that have impl? + // TODO: skip comparing fields that already have impl specified in the type yield classCall.ref().members().allMatch(member -> { // loop invariant: first [i] members are the "same". ([i] is the loop counter, count from 0) // Note that member can only refer to first [i] members, so it is safe that we supply [lhs] or [rhs] diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java index cda6060ea..5a6916a97 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java @@ -318,9 +318,7 @@ record LitString(@NotNull String string) implements Expr { @Override public void forEach(@NotNull PosedConsumer f) { } } - record New( - @NotNull WithPos classCall - ) implements Expr { + record New(@NotNull WithPos classCall) implements Expr { public @NotNull Expr.New update(@NotNull WithPos classCall) { return classCall == classCall() ? this : new New(classCall); } @@ -329,10 +327,7 @@ record New( return update(classCall.descent(f)); } - @Override - public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) { - f.accept(classCall); - } + @Override public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) { f.accept(classCall); } } record Idiom(