Skip to content

Commit

Permalink
class: code review, do not compute all the types
Browse files Browse the repository at this point in the history
  • Loading branch information
@ice1000
ice1000 committed Jul 12, 2024
1 parent 397a6f6 commit a6e9a4f
Show file tree
Hide file tree
Showing 5 changed files with 29 additions and 46 deletions.
41 changes: 19 additions & 22 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.*;
Expand Down Expand Up @@ -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);
}
}
}
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -397,11 +394,11 @@ case CompiledVar(var content) -> new AppTycker<>(this, sourcePos, args.size(), l

private Jdg computeArgs(
@NotNull SourcePos pos, @NotNull ImmutableSeq<Expr.NamedArg> args,
@NotNull AbstractTele params, @NotNull BiFunction<Term[], Term[], Jdg> k
@NotNull AbstractTele params, @NotNull BiFunction<Term[], Term, Jdg> 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);
Expand All @@ -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.<Pair<LocalVar, Term>>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(
Expand Down
11 changes: 3 additions & 8 deletions base/src/main/java/org/aya/tyck/error/ClassError.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,21 +12,16 @@
public interface ClassError extends TyckError {
@NotNull WithPos<Expr> problemExpr();

@Override
default @NotNull SourcePos sourcePos() {
return problemExpr().sourcePos();
}
@Override default @NotNull SourcePos sourcePos() { return problemExpr().sourcePos(); }

record NotClassCall(@Override @NotNull WithPos<Expr> 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<Expr> 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)));
}
}
Expand Down
10 changes: 4 additions & 6 deletions base/src/main/java/org/aya/tyck/tycker/AppTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,14 +30,12 @@
import org.jetbrains.annotations.Nullable;

import java.util.function.BiFunction;
import java.util.function.Function;

public record AppTycker<Ex extends Exception>(
@Override @NotNull TyckState state,
@NotNull AbstractTycker tycker,
@NotNull SourcePos pos,
int argsCount,
int lift,
int argsCount, int lift,
@NotNull Factory<Ex> makeArgs
) implements Stateful {
/**
Expand All @@ -52,7 +50,7 @@ public record AppTycker<Ex extends Exception>(
*/
@FunctionalInterface
public interface Factory<Ex extends Exception> extends
CheckedBiFunction<AbstractTele, BiFunction<Term[], Term[], Jdg>, Jdg, Ex> {
CheckedBiFunction<AbstractTele, BiFunction<Term[], Term, Jdg>, Jdg, Ex> {
}

public AppTycker(
Expand Down Expand Up @@ -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(
Expand Down
4 changes: 1 addition & 3 deletions base/src/main/java/org/aya/unify/TermComparator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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]
Expand Down
9 changes: 2 additions & 7 deletions syntax/src/main/java/org/aya/syntax/concrete/Expr.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -318,9 +318,7 @@ record LitString(@NotNull String string) implements Expr {
@Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
}

record New(
@NotNull WithPos<Expr> classCall
) implements Expr {
record New(@NotNull WithPos<Expr> classCall) implements Expr {
public @NotNull Expr.New update(@NotNull WithPos<Expr> classCall) {
return classCall == classCall() ? this : new New(classCall);
}
Expand All @@ -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(
Expand Down

0 comments on commit a6e9a4f

Please sign in to comment.