Skip to content
This repository has been archived by the owner on May 27, 2024. It is now read-only.

Commit

Permalink
tyck: NotPi
Browse files Browse the repository at this point in the history 
Co-authored-by: HoshinoTented <hoshinotented@qq.com>
  • Loading branch information
@ice1000 @HoshinoTented
ice1000 and HoshinoTented committed Mar 8, 2024
1 parent 56d58ad commit 145e98e
Show file tree
Hide file tree
Showing 6 changed files with 95 additions and 51 deletions.
74 changes: 56 additions & 18 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,15 @@
import org.aya.generic.SortKind;
import org.aya.syntax.concrete.Expr;
import org.aya.syntax.core.term.*;
import org.aya.syntax.ref.*;
import org.aya.syntax.ref.AnyVar;
import org.aya.syntax.ref.DefVar;
import org.aya.syntax.ref.LocalCtx;
import org.aya.syntax.ref.LocalVar;
import org.aya.tyck.error.BadTypeError;
import org.aya.tyck.error.LicitError;
import org.aya.tyck.tycker.AbstractExprTycker;
import org.aya.tyck.tycker.AppTycker;
import org.aya.util.error.SourcePos;
import org.aya.util.error.WithPos;
import org.aya.util.reporter.Reporter;
import org.jetbrains.annotations.NotNull;
Expand Down Expand Up @@ -58,7 +64,7 @@ yield subscoped(() -> {
return switch (expr.data()) {
case Expr.App(var f, var a) -> {
if (!(f.data() instanceof Expr.Ref(var ref))) throw new IllegalStateException("function must be Expr.Ref");
yield checkApplication(ref, a);
yield checkApplication(ref, expr.sourcePos(), a);
}
case Expr.Hole hole -> throw new UnsupportedOperationException("TODO");
case Expr.Lambda(var param, var body) -> {
Expand All @@ -77,13 +83,13 @@ yield subscoped(() -> {
}
case Expr.LitInt litInt -> throw new UnsupportedOperationException("TODO");
case Expr.LitString litString -> throw new UnsupportedOperationException("TODO");
case Expr.Ref(var ref) -> checkApplication(ref, ImmutableSeq.empty());
case Expr.Ref(var ref) -> checkApplication(ref, expr.sourcePos(), ImmutableSeq.empty());
case Expr.Sigma _ -> {
var ty = ty(expr);
// TODO: type level
yield new Result.Default(ty, new SortTerm(SortKind.Type, 0));
}
case Expr.Pi _ -> {
case Expr.Pi _ -> {
var ty = ty(expr);
// TODO: type level
yield new Result.Default(ty, new SortTerm(SortKind.Type, 0));
Expand All @@ -109,15 +115,25 @@ yield subscoped(() -> {
};
}

private @NotNull Result checkApplication(@NotNull AnyVar f, @NotNull ImmutableSeq<Expr.NamedArg> args) {
private @NotNull Result checkApplication(
@NotNull AnyVar f, @NotNull SourcePos sourcePos,
@NotNull ImmutableSeq<Expr.NamedArg> args
) {
try {
return doCheckApplication(f, args);
} catch (NotPi notPi) {
var expr = new Expr.App(new WithPos<>(sourcePos, new Expr.Ref(f)), args);
return fail(expr, BadTypeError.pi(state, sourcePos, expr, notPi.actual));
}
}

private @NotNull Result doCheckApplication(
@NotNull AnyVar f, @NotNull ImmutableSeq<Expr.NamedArg> args
) throws NotPi {
return switch (f) {
case LocalVar lVar -> args.foldLeft(new Result.Default(new FreeTerm(lVar), localCtx().get(lVar)), (acc, arg) -> {
if (arg.name() != null || !arg.explicit()) throw new UnsupportedOperationException("TODO: named arg");
var pi = ensurePi(acc.type());
var wellTy = inherit(arg.arg(), pi.param()).wellTyped();
return new Result.Default(new AppTerm(acc.wellTyped(), wellTy), pi.substBody(wellTy));
});
case DefVar<?, ?> defVar -> AppTycker.checkDefApplication(defVar, params -> {
case LocalVar lVar -> generateApplication(args,
new Result.Default(new FreeTerm(lVar), localCtx().get(lVar)));
case DefVar<?, ?> defVar -> AppTycker.checkDefApplication(defVar, (params, k) -> {
int argIx = 0, paramIx = 0;
var result = MutableList.<Term>create();
while (argIx < args.size() && paramIx < params.size()) {
Expand All @@ -126,7 +142,8 @@ yield subscoped(() -> {
// Implicit insertion
if (arg.explicit() != param.explicit()) {
if (!arg.explicit()) {
throw new UnsupportedOperationException("TODO: implicit application to explicit param");
reporter.report(new LicitError.BadImplicitArg(arg));
break;
} else if (arg.name() == null) {
// here, arg.explicit() == true and param.explicit() == false
result.append(mockTerm(param, arg.sourcePos()));
Expand All @@ -139,7 +156,7 @@ yield subscoped(() -> {
}
// ^ insert implicits before the named argument
if (paramIx == params.size()) {
// report TODO: named arg not found
reporter.report(new LicitError.BadImplicitArg(arg));
break;
}
}
Expand All @@ -148,16 +165,37 @@ yield subscoped(() -> {
argIx++;
paramIx++;
}
return result.toImmutableSeq();
if (argIx < args.size()) {
generateApplication(args.drop(argIx), k.apply(result.toImmutableSeq()));
} else if (paramIx < params.size()) {
// TODO: eta-expand
throw new UnsupportedOperationException("TODO");
}
return k.apply(result.toImmutableSeq());
});
default -> throw new UnsupportedOperationException("TODO");
};
}

private Result generateApplication(@NotNull ImmutableSeq<Expr.NamedArg> args, Result start) throws NotPi {
return args.foldLeftChecked(start, (acc, arg) -> {
if (arg.name() != null || !arg.explicit()) reporter.report(new LicitError.BadNamedArg(arg));
var pi = ensurePi(acc.type());
var wellTy = inherit(arg.arg(), pi.param()).wellTyped();
return new Result.Default(new AppTerm(acc.wellTyped(), wellTy), pi.substBody(wellTy));
});
}

private @NotNull PiTerm ensurePi(Term term) {
protected static final class NotPi extends Exception {
public final @NotNull Term actual;

public NotPi(@NotNull Term actual) {
this.actual = actual;
}
}

private @NotNull PiTerm ensurePi(Term term) throws NotPi {
if (term instanceof PiTerm pi) return pi;
// TODO
throw new UnsupportedOperationException("TODO: report NotPi");
throw new NotPi(term);
}
}
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/tyck/error/CounterexampleError.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
package org.aya.tyck.error;

import org.aya.pretty.doc.Doc;
import org.aya.ref.AnyVar;
import org.aya.syntax.ref.AnyVar;
import org.aya.util.error.SourcePos;
import org.aya.util.prettier.PrettierOptions;
import org.jetbrains.annotations.NotNull;
Expand Down
33 changes: 13 additions & 20 deletions base/src/main/java/org/aya/tyck/error/LicitError.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,39 +4,32 @@

import org.aya.pretty.doc.Doc;
import org.aya.syntax.concrete.Expr;
import org.aya.syntax.core.term.Term;
import org.aya.util.error.SourcePos;
import org.aya.util.prettier.PrettierOptions;
import org.aya.util.reporter.Problem;
import org.jetbrains.annotations.NotNull;

public sealed interface LicitError extends Problem {
@Override default @NotNull Severity level() {return Severity.ERROR;}
@Override default @NotNull Stage stage() {return Stage.TYCK;}
public sealed interface LicitError extends TyckError {
record BadImplicitArg(@Override @NotNull Expr.NamedArg expr) implements LicitError {
@Override public @NotNull SourcePos sourcePos() {
return expr.sourcePos();
}

record LicitMismatch(
@Override @NotNull Expr expr,
@Override @NotNull SourcePos sourcePos,
@NotNull Term type
) implements LicitError {
@Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
return Doc.vcat(
Doc.english("Cannot check"),
Doc.par(1, expr.toDoc(options)),
Doc.english("against the Pi type"),
Doc.par(1, type.toDoc(options)),
Doc.english("because explicitness do not match"));
return Doc.sep(Doc.english("Unexpected implicit argument"),
Doc.code(expr.toDoc(options)));
}
}

/*record UnexpectedImplicitArg(@Override @NotNull Expr.NamedArg expr) implements LicitError {
record BadNamedArg(@Override @NotNull Expr.NamedArg expr) implements LicitError {
@Override public @NotNull SourcePos sourcePos() {
return expr.sourcePos();
}

@Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
return Doc.sep(Doc.english("Unexpected implicit argument"),
Doc.code(expr.toDoc(options)));
return Doc.vcat(
Doc.sep(Doc.english("Named argument unwanted here:"),
Doc.code(expr.toDoc(options))),
Doc.english("Named applications are only allowed in direct application to definitions."));
}
}*/
}
}
25 changes: 16 additions & 9 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 @@ -3,6 +3,7 @@
package org.aya.tyck.tycker;

import kala.collection.immutable.ImmutableSeq;
import kala.function.CheckedBiFunction;
import org.aya.syntax.concrete.stmt.decl.Decl;
import org.aya.syntax.concrete.stmt.decl.TeleDecl;
import org.aya.syntax.core.def.*;
Expand All @@ -14,31 +15,37 @@
import org.aya.tyck.Result;
import org.jetbrains.annotations.NotNull;

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

public final class AppTycker {
@FunctionalInterface
public interface Factory<Ex extends Throwable> extends
CheckedBiFunction<ImmutableSeq<Param>, Function<ImmutableSeq<Term>, Result>, Result, Ex> {
}

private AppTycker() {}

@SuppressWarnings("unchecked")
public static @NotNull Result checkDefApplication(
public static <Ex extends Throwable> @NotNull Result checkDefApplication(
@NotNull DefVar<? extends Def, ? extends Decl> defVar,
Function<ImmutableSeq<Param>, ImmutableSeq<Term>> makeArgs
) {
Factory<Ex> makeArgs
) throws Ex {
var core = defVar.core;
var concrete = defVar.concrete;

if (core instanceof FnDef || concrete instanceof TeleDecl.FnDecl) {
var fnVar = (DefVar<FnDef, TeleDecl.FnDecl>) defVar;
new Result.Default(
new FnCall(fnVar, 0, makeArgs.apply(TeleDef.defTele(fnVar))),
return makeArgs.apply(TeleDef.defTele(fnVar), args -> new Result.Default(
new FnCall(fnVar, 0, args),
TeleDef.defType(fnVar)
);
));
} else if (core instanceof DataDef || concrete instanceof TeleDecl.DataDecl) {
var dataVar = (DefVar<DataDef, TeleDecl.DataDecl>) defVar;
new Result.Default(
new DataCall(dataVar, 0, ImmutableSeq.empty()),
return makeArgs.apply(TeleDef.defTele(dataVar), args -> new Result.Default(
new DataCall(dataVar, 0, args),
TeleDef.defType(dataVar)
);
));
} else if (core instanceof CtorDef || concrete instanceof TeleDecl.DataCtor) {
var ctorVar = (DefVar<CtorDef, TeleDecl.DataCtor>) defVar;
// TODO: original code looks terrible
Expand Down
4 changes: 2 additions & 2 deletions base/src/main/java/org/aya/tyck/tycker/Problematic.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ public interface Problematic {
return fail(expr, ErrorTerm.typeOf(expr), prob);
}

default @NotNull Result fail(@NotNull AyaDocile expr, @NotNull Term term, @NotNull Problem prob) {
default @NotNull Result fail(@NotNull AyaDocile expr, @NotNull Term type, @NotNull Problem prob) {
reporter().report(prob);
return new Result.Default(new ErrorTerm(expr), term);
return new Result.Default(new ErrorTerm(expr), type);
}
}
8 changes: 7 additions & 1 deletion syntax/src/main/java/org/aya/syntax/concrete/Expr.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ record NamedArg(
@Override boolean explicit,
@Nullable String name,
@NotNull WithPos<Expr> arg
) implements SourceNode, BinOpElem<Expr> {
) implements SourceNode, BinOpElem<Expr>, AyaDocile {
@Override
public @NotNull Expr term() {
return arg.data();
Expand All @@ -162,6 +162,12 @@ record NamedArg(
return expr == arg ? this : new NamedArg(sourcePos, explicit, name, expr);
}

@Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
var doc = name == null ? arg.data().toDoc(options) :
Doc.braced(Doc.sep(Doc.plain(name), Doc.symbol("=>"), arg.data().toDoc(options)));
return Doc.bracedUnless(doc, explicit);
}

public @NotNull NamedArg descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(arg.descent(f));
}
Expand Down

0 comments on commit 145e98e

Please sign in to comment.