Skip to content

Commit

Permalink
MERGE: #354
Browse files Browse the repository at this point in the history 
354: Lift a meta and unlift the solution r=ice1000 a=ice1000

Related to #352
bors r+

Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>
  • Loading branch information
@bors @ice1000
bors[bot] and ice1000 committed Mar 26, 2022
2 parents 03c684e + 9f488e9 commit c67474d
Show file tree
Hide file tree
Showing 6 changed files with 92 additions and 77 deletions.
6 changes: 3 additions & 3 deletions base/src/main/java/org/aya/core/Meta.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,13 +67,13 @@ private Meta(

public @NotNull FormTerm.Pi asPi(
@NotNull String domName, @NotNull String codName, boolean explicit,
@NotNull ImmutableSeq<Arg<Term>> contextArgs
int ulift, @NotNull ImmutableSeq<Arg<Term>> 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);
}
Expand Down
10 changes: 3 additions & 7 deletions base/src/main/java/org/aya/core/term/CallTerm.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ interface Factory<D extends Def, S extends Signatured> {
make(@NotNull Term f, @NotNull Arg<Term> 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);
Expand Down Expand Up @@ -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<Term>> fullArgs() {
Expand All @@ -163,11 +164,6 @@ record Hole(
@Override public <P, R> R doAccept(@NotNull Visitor<P, R> 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;
}
}

/**
Expand Down
10 changes: 10 additions & 0 deletions base/src/main/java/org/aya/core/visitor/TermConsumer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,13 @@
import org.jetbrains.annotations.NotNull;

public interface TermConsumer<P> extends Term.Visitor<P, Unit> {
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);
Expand Down Expand Up @@ -56,28 +60,33 @@ default void visitArg(@NotNull Arg<? extends Term> 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();
}

Expand Down Expand Up @@ -110,6 +119,7 @@ default void visitArgs(P p, SeqLike<Arg<@NotNull Term>> args) {

@Override default Unit visitAccess(@NotNull CallTerm.Access term, P p) {
visitArgs(p, term.fieldArgs());
visitCall(term, p);
return term.of().accept(this, p);
}
}
5 changes: 3 additions & 2 deletions base/src/main/java/org/aya/core/visitor/TermFixpoint.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,10 @@ public interface TermFixpoint<P> extends Term.Visitor<P, @NotNull Term> {
@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) {
Expand Down
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/tyck/env/LocalCtx.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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> T with(@NotNull Term.Param param, @NotNull Supplier<T> action) {
Expand Down
136 changes: 72 additions & 64 deletions base/src/main/java/org/aya/tyck/unify/DefEq.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down

0 comments on commit c67474d

Please sign in to comment.