diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index d972dfba..b34024ea 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.java @@ -2,21 +2,19 @@ // 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.ImmutableSeq; import org.aya.generic.SortKind; import org.aya.syntax.concrete.Expr; -import org.aya.syntax.core.def.TeleDef; import org.aya.syntax.core.term.*; -import org.aya.syntax.core.term.call.Callable; import org.aya.syntax.ref.DefVar; import org.aya.syntax.ref.LocalCtx; import org.aya.syntax.ref.LocalVar; import org.aya.tyck.tycker.AbstractExprTycker; -import org.aya.tyck.tycker.ExprTyckerUtils; +import org.aya.tyck.tycker.AppTycker; +import org.aya.util.error.WithPos; import org.aya.util.reporter.Reporter; import org.jetbrains.annotations.NotNull; -import java.util.Objects; - public final class ExprTycker extends AbstractExprTycker { public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Reporter reporter) { super(state, ctx, reporter); @@ -28,22 +26,22 @@ public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Repo return term; } - public @NotNull Result inherit(@NotNull Expr expr, @NotNull Term type) { + public @NotNull Result inherit(@NotNull WithPos expr, @NotNull Term type) { return synthesize(expr); } - public @NotNull Term ty(@NotNull Expr expr) { + public @NotNull Term ty(@NotNull WithPos expr) { return doTy(expr); } - private @NotNull Term doTy(@NotNull Expr expr) { - return switch (expr) { + private @NotNull Term doTy(@NotNull WithPos expr) { + return switch (expr.data()) { case Expr.Sort sort -> new SortTerm(sort.kind(), sort.lift()); case Expr.Pi(var param, var last) -> { - var wellParam = ty(param.type().data()); + var wellParam = ty(param.type()); yield subscoped(() -> { localCtx().put(param.ref(), wellParam); - var wellLast = ty(last.data()); + var wellLast = ty(last); return new PiTerm(wellParam, wellLast); }); } @@ -51,35 +49,20 @@ yield subscoped(() -> { }; } - public @NotNull Result synthesize(@NotNull Expr expr) { + public @NotNull Result synthesize(@NotNull WithPos expr) { return doSynthesize(expr); } - private @NotNull Result doSynthesize(@NotNull Expr expr) { - return switch (expr) { - case Expr.App(var f, var a) -> { - var resultF = synthesize(f.data()); - if (!(whnf(resultF.type()) instanceof PiTerm fTy)) throw new UnsupportedOperationException("TODO"); - - var wellF = whnf(resultF.wellTyped()); - if (wellF instanceof Callable.Tele callF) { - yield checkAppOnCall(callF, fTy, a); - } - - var param = fTy.param(); - var wellArg = inherit(a.term(), param).wellTyped(); - var app = AppTerm.make(wellF, wellArg); - var ty = fTy.body().instantiate(wellArg); - - yield new Result.Default(app, ty); - } + private @NotNull Result doSynthesize(@NotNull WithPos expr) { + return switch (expr.data()) { + case Expr.App(var f, var a) -> checkApplication(f, a); case Expr.Hole hole -> throw new UnsupportedOperationException("TODO"); case Expr.Lambda(var param, var body) -> { - var paramResult = synthesize(param.type().data()); + var paramResult = synthesize(param.type()); yield subscoped(() -> { localCtx().put(param.ref(), paramResult.wellTyped()); - var bodyResult = synthesize(body.data()); + var bodyResult = synthesize(body); var lamTerm = new LamTerm(bodyResult.wellTyped().bind(param.ref())); var ty = new PiTerm( paramResult.type(), @@ -92,7 +75,7 @@ yield subscoped(() -> { case Expr.LitString litString -> throw new UnsupportedOperationException("TODO"); case Expr.Ref ref -> switch (ref.var()) { case LocalVar lVar -> new Result.Default(new FreeTerm(lVar), localCtx().get(lVar)); - case DefVar defVar -> ExprTyckerUtils.inferDef(defVar); + case DefVar defVar -> AppTycker.checkDefApplication(defVar, _ -> ImmutableSeq.empty()); default -> throw new UnsupportedOperationException("TODO"); }; case Expr.Sigma sigma -> throw new UnsupportedOperationException("TODO"); @@ -100,12 +83,12 @@ yield subscoped(() -> { var ty = ty(expr); yield new Result.Default(ty, new SortTerm(SortKind.Type, 0)); } - case Expr.Sort sort -> { - var ty = ty(sort); + case Expr.Sort _ -> { + var ty = ty(expr); yield new Result.Default(ty, ty); // FIXME: Type in Type } case Expr.Tuple(var items) -> { - var results = items.map(i -> synthesize(i.data())); + var results = items.map(this::synthesize); var wellTypeds = results.map(Result::wellTyped); var tys = results.map(Result::type); var wellTyped = new TupTerm(wellTypeds); @@ -124,41 +107,13 @@ yield subscoped(() -> { }; } + private @NotNull Result checkApplication(WithPos f, ImmutableSeq a) { + throw new UnsupportedOperationException("TODO"); + } + private @NotNull PiTerm ensurePi(Term term) { if (term instanceof PiTerm pi) return pi; // TODO throw new UnsupportedOperationException("TODO: report NotPi"); } - - private @NotNull Result checkAppOnCall(@NotNull Callable.Tele f, @NotNull PiTerm fTy, @NotNull Expr.NamedArg arg) { - var argLicit = arg.explicit(); - var tele = TeleDef.defTele(f.ref()); - var param = tele.get(f.args().size()); // always success - - while (param.explicit() != argLicit - || (arg.name() != null && Objects.equals(param.name(), arg.name()))) { - if (argLicit || arg.name() != null) { - // We need to insert hole if: - // * the parameter is implicit but the argument is explicit - // * the parameter and the argument is both implicit but the argument is an named argument, - // and the parameter is not the one. - - // do insert hole - var hole = mockTerm(param, arg.sourcePos()); - f = f.applyTo(hole); - var newTy = fTy.body().instantiate(hole); - fTy = ensurePi(newTy); - param = tele.get(f.args().size()); - } else { - // the parameter is explicit but the argument is implicit - // which is TODO not cool. - throw new UnsupportedOperationException("TODO: report not cool"); - } - } - - // for now, we can safely apply {arg} to {f} - - var wellArg = inherit(arg.term(), fTy.param()).wellTyped(); - return new Result.Default(f.applyTo(wellArg), fTy.body().instantiate(wellArg)); - } } diff --git a/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java b/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java index 7d3fab1d..44431343 100644 --- a/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java @@ -32,11 +32,11 @@ protected AbstractExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @N @Override public @NotNull TyckState state() { - return this.state; + return state; } @Override public @NotNull Reporter reporter() { - return this.reporter; + return reporter; } } diff --git a/base/src/main/java/org/aya/tyck/tycker/ExprTyckerUtils.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java similarity index 77% rename from base/src/main/java/org/aya/tyck/tycker/ExprTyckerUtils.java rename to base/src/main/java/org/aya/tyck/tycker/AppTycker.java index c2c17de1..d577c6c3 100644 --- a/base/src/main/java/org/aya/tyck/tycker/ExprTyckerUtils.java +++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java @@ -6,24 +6,31 @@ import org.aya.syntax.concrete.stmt.decl.Decl; import org.aya.syntax.concrete.stmt.decl.TeleDecl; import org.aya.syntax.core.def.*; +import org.aya.syntax.core.term.Param; +import org.aya.syntax.core.term.Term; import org.aya.syntax.core.term.call.DataCall; import org.aya.syntax.core.term.call.FnCall; import org.aya.syntax.ref.DefVar; import org.aya.tyck.Result; import org.jetbrains.annotations.NotNull; -public final class ExprTyckerUtils { - private ExprTyckerUtils() {} +import java.util.function.Function; + +public final class AppTycker { + private AppTycker() {} @SuppressWarnings("unchecked") - public static @NotNull Result inferDef(@NotNull DefVar defVar) { + public static @NotNull Result checkDefApplication( + @NotNull DefVar defVar, + Function, ImmutableSeq> makeArgs + ) { var core = defVar.core; var concrete = defVar.concrete; if (core instanceof FnDef || concrete instanceof TeleDecl.FnDecl) { var fnVar = (DefVar) defVar; new Result.Default( - new FnCall(fnVar, 0, ImmutableSeq.empty()), + new FnCall(fnVar, 0, makeArgs.apply(TeleDef.defTele(fnVar))), TeleDef.defType(fnVar) ); } else if (core instanceof DataDef || concrete instanceof TeleDecl.DataDecl) { 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 827bf0cf..c1c1861b 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java @@ -134,13 +134,14 @@ record Tuple( } } - record App(@NotNull WithPos function, @NotNull NamedArg argument) implements Expr { - public @NotNull App update(@NotNull WithPos function, @NotNull NamedArg argument) { - return function == function() && argument == argument() ? this : new App(function, argument); + record App(@NotNull WithPos function, @NotNull ImmutableSeq argument) implements Expr { + public @NotNull App update(@NotNull WithPos function, @NotNull ImmutableSeq argument) { + return function == function() && argument.sameElements(argument(), true) + ? this : new App(function, argument); } @Override public @NotNull App descent(@NotNull UnaryOperator<@NotNull Expr> f) { - return update(function.descent(f), argument.descent(f)); + return update(function.descent(f), argument.map(arg -> arg.descent(f))); } } diff --git a/syntax/src/main/java/org/aya/syntax/core/def/CtorDef.java b/syntax/src/main/java/org/aya/syntax/core/def/CtorDef.java index f48b656d..13553f76 100644 --- a/syntax/src/main/java/org/aya/syntax/core/def/CtorDef.java +++ b/syntax/src/main/java/org/aya/syntax/core/def/CtorDef.java @@ -22,10 +22,10 @@ public final class CtorDef extends SubLevelDef { */ public CtorDef( @NotNull DefVar dataRef, @NotNull DefVar ref, - @NotNull ImmutableSeq selfTele, + @NotNull ImmutableSeq ownerTele, @NotNull ImmutableSeq selfTele, @NotNull Term result, boolean coerce ) { - super(selfTele, result, coerce); + super(ownerTele, selfTele, result, coerce); ref.core = this; this.dataRef = dataRef; this.ref = ref; diff --git a/syntax/src/main/java/org/aya/syntax/core/def/SubLevelDef.java b/syntax/src/main/java/org/aya/syntax/core/def/SubLevelDef.java index 47f4f10a..6ba5e38e 100644 --- a/syntax/src/main/java/org/aya/syntax/core/def/SubLevelDef.java +++ b/syntax/src/main/java/org/aya/syntax/core/def/SubLevelDef.java @@ -14,21 +14,24 @@ * @author ice1000 */ public sealed abstract class SubLevelDef implements TeleDef permits CtorDef { + public final @NotNull ImmutableSeq ownerTele; public final @NotNull ImmutableSeq selfTele; public final @NotNull Term result; public final boolean coerce; protected SubLevelDef( + @NotNull ImmutableSeq ownerTele, @NotNull ImmutableSeq selfTele, @NotNull Term result, boolean coerce ) { + this.ownerTele = ownerTele; this.selfTele = selfTele; this.result = result; this.coerce = coerce; } public @NotNull SeqView fullTelescope() { - return selfTele.view(); + return ownerTele.view().concat(selfTele); } @Override public @NotNull Term result() { diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Param.java b/syntax/src/main/java/org/aya/syntax/core/term/Param.java index 2160ff0b..845fef94 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/Param.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/Param.java @@ -6,11 +6,7 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -public record Param( - @Nullable String name, - @NotNull Term type, - boolean explicit -) { +public record Param(@Nullable String name, @NotNull Term type, boolean explicit) { public Param(@NotNull Term type, boolean explicit) { this(null, type, explicit); } @@ -18,4 +14,8 @@ public Param(@NotNull Term type, boolean explicit) { public @NotNull Arg toArg() { return new Arg<>(type, explicit); } + + public @NotNull Param implicitize() { + return new Param(name, type, false); + } }