From 5a5f2a53cd9322c20d4cf3dc66f0334647cfe3c5 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 26 Mar 2022 18:12:42 -0400 Subject: [PATCH 1/2] CORE: add `ulift` to `CallTerm.Hole` --- base/src/main/java/org/aya/core/Meta.java | 6 +++--- base/src/main/java/org/aya/core/term/CallTerm.java | 10 +++------- .../main/java/org/aya/core/visitor/TermConsumer.java | 10 ++++++++++ .../main/java/org/aya/core/visitor/TermFixpoint.java | 5 +++-- base/src/main/java/org/aya/tyck/env/LocalCtx.java | 2 +- 5 files changed, 20 insertions(+), 13 deletions(-) diff --git a/base/src/main/java/org/aya/core/Meta.java b/base/src/main/java/org/aya/core/Meta.java index cffd050c21..02b059d1ae 100644 --- a/base/src/main/java/org/aya/core/Meta.java +++ b/base/src/main/java/org/aya/core/Meta.java @@ -67,13 +67,13 @@ private Meta( public @NotNull FormTerm.Pi asPi( @NotNull String domName, @NotNull String codName, boolean explicit, - @NotNull ImmutableSeq> contextArgs + int ulift, @NotNull ImmutableSeq> contextArgs ) { assert telescope.isEmpty(); var domVar = Meta.from(contextTele, domName, result, sourcePos); var codVar = Meta.from(contextTele, codName, result, sourcePos); - var dom = new CallTerm.Hole(domVar, contextArgs, ImmutableSeq.empty()); - var cod = new CallTerm.Hole(codVar, contextArgs, ImmutableSeq.empty()); + var dom = new CallTerm.Hole(domVar, ulift, contextArgs, ImmutableSeq.empty()); + var cod = new CallTerm.Hole(codVar, ulift, contextArgs, ImmutableSeq.empty()); var domParam = new Term.Param(Constants.randomlyNamed(sourcePos), dom, explicit); return new FormTerm.Pi(domParam, cod); } diff --git a/base/src/main/java/org/aya/core/term/CallTerm.java b/base/src/main/java/org/aya/core/term/CallTerm.java index 2f60e71343..33cd39a00b 100644 --- a/base/src/main/java/org/aya/core/term/CallTerm.java +++ b/base/src/main/java/org/aya/core/term/CallTerm.java @@ -36,7 +36,7 @@ interface Factory { make(@NotNull Term f, @NotNull Arg arg) { if (f instanceof Hole hole) { if (hole.args.sizeLessThan(hole.ref.telescope)) - return new Hole(hole.ref, hole.contextArgs, hole.args.appended(arg)); + return new Hole(hole.ref, hole.ulift, hole.contextArgs, hole.args.appended(arg)); } if (!(f instanceof IntroTerm.Lambda lam)) return new ElimTerm.App(f, 0, arg); return make(lam, arg); @@ -149,11 +149,12 @@ public Con( */ record Hole( @NotNull Meta ref, + int ulift, @NotNull ImmutableSeq<@NotNull Arg<@NotNull Term>> contextArgs, @NotNull ImmutableSeq<@NotNull Arg<@NotNull Term>> args ) implements CallTerm { public @NotNull FormTerm.Pi asPi(boolean explicit) { - return ref.asPi(ref.name() + "dom", ref.name() + "cod", explicit, contextArgs); + return ref.asPi(ref.name() + "dom", ref.name() + "cod", explicit, ulift, contextArgs); } public @NotNull SeqView<@NotNull Arg> fullArgs() { @@ -163,11 +164,6 @@ record Hole( @Override public R doAccept(@NotNull Visitor visitor, P p) { return visitor.visitHole(this, p); } - - @Override public int ulift() { - // TODO[lift-meta]: we should be able to lift a meta - return 0; - } } /** diff --git a/base/src/main/java/org/aya/core/visitor/TermConsumer.java b/base/src/main/java/org/aya/core/visitor/TermConsumer.java index 856c5e4c0c..f9aa96ac7c 100644 --- a/base/src/main/java/org/aya/core/visitor/TermConsumer.java +++ b/base/src/main/java/org/aya/core/visitor/TermConsumer.java @@ -9,9 +9,13 @@ import org.jetbrains.annotations.NotNull; public interface TermConsumer

extends Term.Visitor { + default void visitCall(@NotNull CallTerm call, P p) { + } + @Override default Unit visitHole(@NotNull CallTerm.Hole term, P p) { visitArgs(p, term.args()); visitArgs(p, term.contextArgs()); + visitCall(term, p); // TODO[ice]: is it fine? Maybe we want to visit the solutions as well? // var body = term.ref().body; // if (body != null) body.accept(this, p); @@ -56,28 +60,33 @@ default void visitArg(@NotNull Arg arg, P p) { @Override default Unit visitFnCall(@NotNull CallTerm.Fn fnCall, P p) { visitArgs(p, fnCall.args()); + visitCall(fnCall, p); return Unit.unit(); } @Override default Unit visitPrimCall(CallTerm.@NotNull Prim prim, P p) { visitArgs(p, prim.args()); + visitCall(prim, p); return Unit.unit(); } @Override default Unit visitDataCall(@NotNull CallTerm.Data dataCall, P p) { visitArgs(p, dataCall.args()); + visitCall(dataCall, p); return Unit.unit(); } @Override default Unit visitConCall(@NotNull CallTerm.Con conCall, P p) { visitArgs(p, conCall.head().dataArgs()); visitArgs(p, conCall.conArgs()); + visitCall(conCall, p); return Unit.unit(); } @Override default Unit visitStructCall(@NotNull CallTerm.Struct structCall, P p) { visitArgs(p, structCall.args()); + visitCall(structCall, p); return Unit.unit(); } @@ -110,6 +119,7 @@ default void visitArgs(P p, SeqLike> args) { @Override default Unit visitAccess(@NotNull CallTerm.Access term, P p) { visitArgs(p, term.fieldArgs()); + visitCall(term, p); return term.of().accept(this, p); } } diff --git a/base/src/main/java/org/aya/core/visitor/TermFixpoint.java b/base/src/main/java/org/aya/core/visitor/TermFixpoint.java index de1263f7de..bc60d2b2a4 100644 --- a/base/src/main/java/org/aya/core/visitor/TermFixpoint.java +++ b/base/src/main/java/org/aya/core/visitor/TermFixpoint.java @@ -17,9 +17,10 @@ public interface TermFixpoint

extends Term.Visitor { @Override default @NotNull Term visitHole(@NotNull CallTerm.Hole term, P p) { var contextArgs = term.contextArgs().map(arg -> visitArg(arg, p)); var args = term.args().map(arg -> visitArg(arg, p)); - if (term.contextArgs().sameElements(contextArgs, true) + if (ulift() == 0 + && term.contextArgs().sameElements(contextArgs, true) && term.args().sameElements(args, true)) return term; - return new CallTerm.Hole(term.ref(), contextArgs, args); + return new CallTerm.Hole(term.ref(), ulift() + term.ulift(), contextArgs, args); } @Override default @NotNull Term visitFieldRef(@NotNull RefTerm.Field term, P p) { diff --git a/base/src/main/java/org/aya/tyck/env/LocalCtx.java b/base/src/main/java/org/aya/tyck/env/LocalCtx.java index d4df5c554b..aabafaf993 100644 --- a/base/src/main/java/org/aya/tyck/env/LocalCtx.java +++ b/base/src/main/java/org/aya/tyck/env/LocalCtx.java @@ -33,7 +33,7 @@ public sealed interface LocalCtx permits MapLocalCtx, SeqLocalCtx { freshHole(@Nullable Term type, @NotNull String name, @NotNull SourcePos sourcePos) { var ctxTele = extract(); var meta = Meta.from(ctxTele, name, type, sourcePos); - var hole = new CallTerm.Hole(meta, ctxTele.map(Term.Param::toArg), meta.telescope.map(Term.Param::toArg)); + var hole = new CallTerm.Hole(meta, 0, ctxTele.map(Term.Param::toArg), meta.telescope.map(Term.Param::toArg)); return Tuple2.of(hole, IntroTerm.Lambda.make(meta.telescope, hole)); } default T with(@NotNull Term.Param param, @NotNull Supplier action) { From 9f488e9655b4f4bc968183551417d37282aff89a Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 26 Mar 2022 18:18:34 -0400 Subject: [PATCH 2/2] UNIFY: unlift --- .../main/java/org/aya/tyck/unify/DefEq.java | 136 +++++++++--------- 1 file changed, 72 insertions(+), 64 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/DefEq.java b/base/src/main/java/org/aya/tyck/unify/DefEq.java index 0eb9088fc6..39afc625ec 100644 --- a/base/src/main/java/org/aya/tyck/unify/DefEq.java +++ b/base/src/main/java/org/aya/tyck/unify/DefEq.java @@ -380,75 +380,83 @@ yield checkParam(lhs.param(), rhs.param(), null, lr, rl, () -> null, () -> { if (lhs.ref() != rhs.ref()) yield null; yield Def.defResult(lhs.ref()); } - case CallTerm.Hole lhs -> { - var meta = lhs.ref(); - if (preRhs instanceof CallTerm.Hole rcall && lhs.ref() == rcall.ref()) { - // If we do not know the type, then we do not perform the comparison - if (meta.result == null) yield null; - var holeTy = FormTerm.Pi.make(meta.telescope, meta.result); - for (var arg : lhs.args().view().zip(rcall.args())) { - if (!(holeTy instanceof FormTerm.Pi holePi)) - throw new IllegalStateException("meta arg size larger than param size. this should not happen"); - if (!compare(arg._1.term(), arg._2.term(), lr, rl, holePi.param().type())) yield null; - holeTy = holePi.substBody(arg._1.term()); - } - yield holeTy; - } - // Long time ago I wrote this to generate more unification equations, - // which solves more universe levels. However, with latest version Aya (0.13), - // removing this does not break anything. - // Update: this is still needed, see #327 last task (`coe'`) - var resultTy = preRhs.computeType(state, ctx); - if (meta.result != null) compareUntyped(resultTy, meta.result, rl, lr); - var argSubst = extract(lhs, preRhs, meta); - if (argSubst == null) { - reporter.report(new HoleProblem.BadSpineError(lhs, pos)); - yield null; - } - var subst = Unfolder.buildSubst(meta.contextTele, lhs.contextArgs()); - // In this case, the solution may not be unique (see #608), - // so we may delay its resolution to the end of the tycking when we disallow vague unification. - if (!allowVague && subst.overlap(argSubst).anyMatch(var -> preRhs.findUsages(var) > 0)) { - state.addEqn(createEqn(lhs, preRhs, lr, rl)); - // Skip the unification and scope check - yield meta.result; - } - subst.add(argSubst); - // TODO - // TODO: what's the TODO above? I don't know what's TODO? ???? - rl.map.forEach(subst::add); - assert !state.metas().containsKey(meta); - var solved = preRhs.freezeHoles(state).subst(subst); - var allowedVars = meta.fullTelescope().map(Term.Param::ref).toImmutableSeq(); - var scopeCheck = solved.scopeCheck(allowedVars); - if (scopeCheck.invalid.isNotEmpty()) { - // Normalization may remove the usages of certain variables - solved = solved.normalize(state, NormalizeMode.NF); - scopeCheck = solved.scopeCheck(allowedVars); - } - if (scopeCheck.invalid.isNotEmpty()) { - reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.invalid, pos)); - yield new ErrorTerm(solved); - } - if (scopeCheck.confused.isNotEmpty()) { - if (allowConfused) state.addEqn(createEqn(lhs, solved, lr, rl)); - else { - reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.confused, pos)); - yield new ErrorTerm(solved); - } - } - if (!meta.solve(state, solved)) { - reporter.report(new HoleProblem.RecursionError(lhs, solved, pos)); - yield new ErrorTerm(solved); - } - tracing(builder -> builder.append(new Trace.LabelT(pos, "Hole solved!"))); - yield resultTy; - } + case CallTerm.Hole lhs -> solveMeta(preRhs, lr, rl, lhs); }; traceExit(); return ret; } + private @Nullable Term solveMeta(@NotNull Term preRhs, Sub lr, Sub rl, CallTerm.Hole lhs) { + var meta = lhs.ref(); + if (preRhs instanceof CallTerm.Hole rcall && lhs.ref() == rcall.ref()) { + // If we do not know the type, then we do not perform the comparison + if (meta.result == null) return null; + // Is this going to produce a readable error message? + compareLevel(lhs.ulift(), rcall.ulift()); + var holeTy = FormTerm.Pi.make(meta.telescope, meta.result); + for (var arg : lhs.args().view().zip(rcall.args())) { + if (!(holeTy instanceof FormTerm.Pi holePi)) + throw new IllegalStateException("meta arg size larger than param size. this should not happen"); + if (!compare(arg._1.term(), arg._2.term(), lr, rl, holePi.param().type())) return null; + holeTy = holePi.substBody(arg._1.term()); + } + return holeTy.subst(Substituter.TermSubst.EMPTY, lhs.ulift()); + } + // Long time ago I wrote this to generate more unification equations, + // which solves more universe levels. However, with latest version Aya (0.13), + // removing this does not break anything. + // Update: this is still needed, see #327 last task (`coe'`) + var resultTy = preRhs.computeType(state, ctx); + if (meta.result != null) { + var liftedType = meta.result.subst(Substituter.TermSubst.EMPTY, lhs.ulift()); + compareUntyped(resultTy, liftedType, rl, lr); + } + var argSubst = extract(lhs, preRhs, meta); + if (argSubst == null) { + reporter.report(new HoleProblem.BadSpineError(lhs, pos)); + return null; + } + var subst = Unfolder.buildSubst(meta.contextTele, lhs.contextArgs()); + // In this case, the solution may not be unique (see #608), + // so we may delay its resolution to the end of the tycking when we disallow vague unification. + if (!allowVague && subst.overlap(argSubst).anyMatch(var -> preRhs.findUsages(var) > 0)) { + state.addEqn(createEqn(lhs, preRhs, lr, rl)); + // Skip the unification and scope check + return resultTy; + } + subst.add(argSubst); + // TODO + // TODO: what's the TODO above? I don't know what's TODO? ???? + rl.map.forEach(subst::add); + assert !state.metas().containsKey(meta); + // TODO: report error if unlifting makes < 0 levels + var solved = preRhs.freezeHoles(state).subst(subst, -lhs.ulift()); + var allowedVars = meta.fullTelescope().map(Term.Param::ref).toImmutableSeq(); + var scopeCheck = solved.scopeCheck(allowedVars); + if (scopeCheck.invalid.isNotEmpty()) { + // Normalization may remove the usages of certain variables + solved = solved.normalize(state, NormalizeMode.NF); + scopeCheck = solved.scopeCheck(allowedVars); + } + if (scopeCheck.invalid.isNotEmpty()) { + reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.invalid, pos)); + return new ErrorTerm(solved); + } + if (scopeCheck.confused.isNotEmpty()) { + if (allowConfused) state.addEqn(createEqn(lhs, solved, lr, rl)); + else { + reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.confused, pos)); + return new ErrorTerm(solved); + } + } + if (!meta.solve(state, solved)) { + reporter.report(new HoleProblem.RecursionError(lhs, solved, pos)); + return new ErrorTerm(solved); + } + tracing(builder -> builder.append(new Trace.LabelT(pos, "Hole solved!"))); + return resultTy; + } + private boolean compareLevel(int l, int r) { switch (cmp) { case Eq: