Skip to content

Commit

Permalink
merge: #1011, remove isProp
Browse files Browse the repository at this point in the history 
This PR:
+ [x] Remove the uses of `isProp` in `TermComparator`
  • Loading branch information
@ice1000
ice1000 committed Nov 11, 2023
2 parents dd44ae8 + 40e1859 commit 8f7acdf
Show file tree
Hide file tree
Showing 30 changed files with 57 additions and 274 deletions.
62 changes: 26 additions & 36 deletions base/src/main/java/org/aya/concrete/Expr.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ default Expr resolveLax(@NotNull ModuleContext context) {
resolver.enterBody();
var inner = resolver.apply(this);
var view = resolver.allowedGeneralizes().valuesView().toImmutableSeq().view();
return Expr.buildLam(sourcePos(), view, inner);
return buildLam(sourcePos(), view, inner);
}

@Override default @NotNull Doc toDoc(@NotNull PrettierOptions options) {
Expand All @@ -85,7 +85,7 @@ public Unresolved(@NotNull SourcePos sourcePos, @NotNull String name) {
this(sourcePos, new QualifiedID(sourcePos, name));
}

@Override public @NotNull Expr.Unresolved descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Unresolved descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}
Expand Down Expand Up @@ -115,11 +115,11 @@ public Hole(@NotNull SourcePos sourcePos, boolean explicit, @Nullable Expr filli
this(sourcePos, explicit, filling, MutableValue.create());
}

public @NotNull Expr.Hole update(@Nullable Expr filling) {
public @NotNull Hole update(@Nullable Expr filling) {
return filling == filling() ? this : new Hole(sourcePos, explicit, filling);
}

@Override public @NotNull Expr.Hole descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Hole descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(filling == null ? null : f.apply(filling));
}
}
Expand All @@ -132,11 +132,11 @@ record App(
@NotNull Expr function,
@NotNull NamedArg argument
) implements Expr {
public @NotNull Expr.App update(@NotNull Expr function, @NotNull NamedArg argument) {
public @NotNull App update(@NotNull Expr function, @NotNull NamedArg argument) {
return function == function() && argument == argument() ? this : new App(sourcePos, function, argument);
}

@Override public @NotNull Expr.App descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull App descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(f.apply(function), argument.descent(f));
}
}
Expand Down Expand Up @@ -197,11 +197,11 @@ record Pi(
return last;
}

public @NotNull Expr.Pi update(@NotNull Param param, @NotNull Expr last) {
public @NotNull Pi update(@NotNull Param param, @NotNull Expr last) {
return param == param() && last == last() ? this : new Pi(sourcePos, param, last);
}

@Override public @NotNull Expr.Pi descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Pi descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(param.descent(f), f.apply(last));
}
}
Expand Down Expand Up @@ -280,11 +280,11 @@ record Lambda(
@NotNull Param param,
@NotNull Expr body
) implements Expr, Nested<Param, Expr, Lambda> {
public @NotNull Expr.Lambda update(@NotNull Param param, @NotNull Expr body) {
public @NotNull Lambda update(@NotNull Param param, @NotNull Expr body) {
return param == param() && body == body() ? this : new Lambda(sourcePos, param, body);
}

@Override public @NotNull Expr.Lambda descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Lambda descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(param.descent(f), f.apply(body));
}
}
Expand All @@ -296,11 +296,11 @@ record Sigma(
@NotNull SourcePos sourcePos,
@NotNull ImmutableSeq<@NotNull Param> params
) implements Expr {
public @NotNull Expr.Sigma update(@NotNull ImmutableSeq<@NotNull Param> params) {
public @NotNull Sigma update(@NotNull ImmutableSeq<@NotNull Param> params) {
return params.sameElements(params(), true) ? this : new Sigma(sourcePos, params);
}

@Override public @NotNull Expr.Sigma descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Sigma descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(params.map(param -> param.descent(f)));
}
}
Expand All @@ -322,17 +322,17 @@ public Ref(@NotNull SourcePos sourcePos, @NotNull AnyVar resolvedVar) {
this(sourcePos, resolvedVar, MutableValue.create());
}

@Override public @NotNull Expr.Ref descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Ref descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}

record Lift(@NotNull SourcePos sourcePos, @NotNull Expr expr, int lift) implements Expr {
public @NotNull Expr.Lift update(@NotNull Expr expr) {
public @NotNull Lift update(@NotNull Expr expr) {
return expr == expr() ? this : new Lift(sourcePos, expr, lift);
}

@Override public @NotNull Expr.Lift descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Lift descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(f.apply(expr));
}
}
Expand All @@ -341,7 +341,7 @@ record Lift(@NotNull SourcePos sourcePos, @NotNull Expr expr, int lift) implemen
* @author tsao-chi
*/
record RawSort(@NotNull SourcePos sourcePos, @NotNull SortKind kind) implements Expr {
@Override public @NotNull Expr.RawSort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull RawSort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}
Expand All @@ -351,7 +351,7 @@ sealed interface Sort extends Expr {

SortKind kind();

@Override default @NotNull Expr.Sort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override default @NotNull Sort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}
Expand All @@ -368,16 +368,6 @@ record Set(@NotNull SourcePos sourcePos, @Override int lift) implements Sort {
}
}

record Prop(@NotNull SourcePos sourcePos) implements Sort {
@Override public int lift() {
return 0;
}

@Override public SortKind kind() {
return SortKind.Prop;
}
}

record ISet(@NotNull SourcePos sourcePos) implements Sort {
@Override public int lift() {
return 0;
Expand Down Expand Up @@ -487,13 +477,13 @@ record Match(
* @author kiva
*/
record LitInt(@NotNull SourcePos sourcePos, int integer) implements Expr {
@Override public @NotNull Expr.LitInt descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull LitInt descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}

record LitString(@NotNull SourcePos sourcePos, @NotNull String string) implements Expr {
@Override public @NotNull Expr.LitString descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull LitString descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}
Expand Down Expand Up @@ -695,15 +685,15 @@ public static Expr.Array newGenerator(
*/
record Let(
@NotNull SourcePos sourcePos,
@NotNull Expr.LetBind bind,
@NotNull LetBind bind,
@NotNull Expr body
) implements Expr, Nested<LetBind, Expr, Let> {
@Override
public @NotNull LetBind param() {
return bind;
}

public @NotNull Let update(@NotNull Expr.LetBind bind, @NotNull Expr body) {
public @NotNull Let update(@NotNull LetBind bind, @NotNull Expr body) {
return bind() == bind && body() == body
? this
: new Let(sourcePos(), bind, body);
Expand All @@ -722,13 +712,13 @@ record LetBind(
@NotNull Expr result,
@NotNull Expr definedAs
) implements SourceNode {
public @NotNull Expr.LetBind update(@NotNull ImmutableSeq<Expr.Param> telescope, @NotNull Expr result, @NotNull Expr definedAs) {
public @NotNull LetBind update(@NotNull ImmutableSeq<Expr.Param> telescope, @NotNull Expr result, @NotNull Expr definedAs) {
return telescope().sameElements(telescope, true) && result() == result && definedAs() == definedAs
? this
: new LetBind(sourcePos, bindName, telescope, result, definedAs);
}

public @NotNull Expr.LetBind descent(@NotNull UnaryOperator<@NotNull Expr> f) {
public @NotNull LetBind descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(telescope().map(x -> x.descent(f)), f.apply(result()), f.apply(definedAs()));
}
}
Expand Down Expand Up @@ -764,15 +754,15 @@ record LetOpen(
}

static @NotNull Expr buildPi(@NotNull SourcePos sourcePos, @NotNull SeqView<Param> params, @NotNull Expr body) {
return buildNested(sourcePos, params, body, Expr.Pi::new);
return buildNested(sourcePos, params, body, Pi::new);
}

static @NotNull Expr buildLam(@NotNull SourcePos sourcePos, @NotNull SeqView<Param> params, @NotNull Expr body) {
return buildNested(sourcePos, params, body, Expr.Lambda::new);
return buildNested(sourcePos, params, body, Lambda::new);
}

static @NotNull Expr buildLet(@NotNull SourcePos sourcePos, @NotNull SeqView<LetBind> binds, @NotNull Expr body) {
return buildNested(sourcePos, binds, body, Expr.Let::new);
return buildNested(sourcePos, binds, body, Let::new);
}

/** convert flattened terms into nested right-associate terms */
Expand Down
1 change: 0 additions & 1 deletion base/src/main/java/org/aya/concrete/desugar/Desugarer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,6 @@ public static class DesugarInterruption extends Exception {}
case Expr.RawSort(var pos, var kind) -> switch (kind) {
case Type -> new Expr.Type(pos, 0);
case Set -> new Expr.Set(pos, 0);
case Prop -> new Expr.Prop(pos);
case ISet -> new Expr.ISet(pos);
};
case Expr.BinOpSeq(var pos, var seq) -> {
Expand Down
11 changes: 0 additions & 11 deletions base/src/main/java/org/aya/core/def/CtorDef.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,12 @@
import kala.collection.immutable.ImmutableSeq;
import org.aya.concrete.stmt.decl.TeleDecl;
import org.aya.core.pat.Pat;
import org.aya.core.term.SortTerm;
import org.aya.core.term.Term;
import org.aya.guest0x0.cubical.Partial;
import org.aya.ref.DefVar;
import org.aya.util.Arg;
import org.jetbrains.annotations.NotNull;

import java.util.Objects;
import java.util.function.Consumer;

/**
Expand Down Expand Up @@ -59,13 +57,4 @@ public void descentConsume(@NotNull Consumer<Term> f, @NotNull Consumer<Pat> g)
@Override public @NotNull ImmutableSeq<Term.Param> telescope() {
return fullTelescope().toImmutableSeq();
}

private @NotNull SortTerm dataResult() {
return dataRef.concrete == null ? dataRef.core.result
: Objects.requireNonNull(dataRef.concrete.signature).result();
}

public boolean inProp() {
return dataResult().isProp();
}
}
9 changes: 2 additions & 7 deletions base/src/main/java/org/aya/core/term/PiTerm.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,19 +69,14 @@ case PiTerm(var param, var body) when param.explicit() -> {
case Type -> switch (codomain.kind()) {
case Type, Set -> new SortTerm(SortKind.Type, Math.max(alift, blift));
case ISet -> new SortTerm(SortKind.Set, alift);
case Prop -> codomain;
};
case ISet -> switch (codomain.kind()) {
case ISet, Prop -> SortTerm.Set0;
case ISet -> SortTerm.Set0;
case Set, Type -> codomain;
};
case Set -> switch (codomain.kind()) {
case Set, Type -> new SortTerm(SortKind.Set, Math.max(alift, blift));
case ISet, Prop -> new SortTerm(SortKind.Set, alift);
};
case Prop -> switch (codomain.kind()) {
case Prop, Type -> codomain;
default -> new SortTerm(SortKind.Set, blift);
case ISet -> new SortTerm(SortKind.Set, alift);
};
};
}
Expand Down
4 changes: 1 addition & 3 deletions base/src/main/java/org/aya/core/term/SigmaTerm.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,7 @@ public record SigmaTerm(@NotNull ImmutableSeq<@NotNull Param> params) implements

public static @NotNull SortTerm lub(@NotNull SortTerm x, @NotNull SortTerm y) {
int lift = Math.max(x.lift(), y.lift());
if (x.kind() == SortKind.Prop || y.kind() == SortKind.Prop) {
return SortTerm.Prop;
} else if (x.kind() == SortKind.Set || y.kind() == SortKind.Set) {
if (x.kind() == SortKind.Set || y.kind() == SortKind.Set) {
return new SortTerm(SortKind.Set, lift);
} else if (x.kind() == SortKind.Type || y.kind() == SortKind.Type) {
return new SortTerm(SortKind.Type, lift);
Expand Down
6 changes: 0 additions & 6 deletions base/src/main/java/org/aya/core/term/SortTerm.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,15 +26,13 @@ public SortTerm(@NotNull SortKind kind, int lift) {
public static final @NotNull SortTerm Set0 = new SortTerm(SortKind.Set, 0);
public static final @NotNull SortTerm Set1 = new SortTerm(SortKind.Set, 1);
public static final @NotNull SortTerm ISet = new SortTerm(SortKind.ISet, 0);
public static final @NotNull SortTerm Prop = new SortTerm(SortKind.Prop, 0);

/**
* <a href="https://github.com/agda/agda/blob/6a92d584c70a615fdc3f364975814d75a0e31bf7/src/full/Agda/TypeChecking/Substitute.hs#L1541-L1558">Agda</a>
*/
public @NotNull SortTerm succ() {
return switch (kind) {
case Type, Set -> new SortTerm(kind, lift + 1);
case Prop -> Type0;
case ISet -> Set1;
};
}
Expand All @@ -43,8 +41,4 @@ public SortTerm(@NotNull SortKind kind, int lift) {
if (kind.hasLevel()) return new SortTerm(kind, this.lift + lift);
else return this;
}

public boolean isProp() {
return kind == SortKind.Prop;
}
}
4 changes: 2 additions & 2 deletions base/src/main/java/org/aya/generic/SortKind.java
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
package org.aya.generic;

public enum SortKind {
Type, Set, Prop, ISet;
Type, Set, ISet;

public boolean hasLevel() {
return this == Type || this == Set;
Expand Down
8 changes: 3 additions & 5 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
import org.aya.core.visitor.Subst;
import org.aya.core.visitor.Zonker;
import org.aya.generic.Constants;
import org.aya.tyck.tycker.UnifiedTycker;
import org.aya.util.error.InternalException;
import org.aya.guest0x0.cubical.CofThy;
import org.aya.guest0x0.cubical.Partial;
Expand All @@ -30,7 +31,6 @@
import org.aya.tyck.error.*;
import org.aya.tyck.pat.ClauseTycker;
import org.aya.tyck.trace.Trace;
import org.aya.tyck.tycker.PropTycker;
import org.aya.tyck.tycker.TyckState;
import org.aya.util.Arg;
import org.aya.util.reporter.Reporter;
Expand All @@ -45,7 +45,7 @@
* Do <em>not</em> use multiple instances in the tycking of one {@link Decl.TopLevel}
* and do <em>not</em> reuse instances of this class in the tycking of multiple {@link Decl.TopLevel}s.
*/
public final class ExprTycker extends PropTycker {
public final class ExprTycker extends UnifiedTycker {
public final @NotNull AyaShape.Factory shapeFactory;

private @NotNull Result doSynthesize(@NotNull Expr expr) {
Expand Down Expand Up @@ -126,8 +126,6 @@ public final class ExprTycker extends PropTycker {
var type = telescope.get(index).type();
var subst = ProjTerm.projSubst(projecteeWHNF, index, telescope, new Subst());
var resultTy = type.subst(subst).freezeHoles(state);
if (inProp(pseudoSigma) && !inProp(resultTy))
return fail(proj, resultTy, new IrrElimProblem.Proj(proj, projecteeWHNF, pseudoSigma, resultTy, state));
return new Result.Default(ProjTerm.proj(projecteeWHNF, ix), resultTy);
}, sp -> {
var fieldName = sp.name();
Expand Down Expand Up @@ -528,6 +526,6 @@ private static boolean needImplicitParamIns(@NotNull Expr expr) {
}

public @NotNull Result check(@NotNull Expr expr, @NotNull Term type) {
return withInProp(inProp(type), () -> inherit(expr, type));
return inherit(expr, type);
}
}
4 changes: 2 additions & 2 deletions base/src/main/java/org/aya/tyck/StmtTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,7 @@ private void checkCtor(@NotNull ExprTycker tycker, TeleDecl.DataCtor ctor) {
if (ctor.patterns.isNotEmpty()) {
var sig = new Def.Signature<>(dataSig.param(), predataCall);
var lhs = ClauseTycker.checkLhs(tycker,
new Pattern.Clause(ctor.sourcePos(), ctor.patterns, Option.none()), sig, false, false);
new Pattern.Clause(ctor.sourcePos(), ctor.patterns, Option.none()), sig, false);
pat = lhs.preclause().patterns();
// Revert to the "after patterns" state
tycker.ctx = lhs.gamma();
Expand All @@ -252,7 +252,7 @@ private void checkCtor(@NotNull ExprTycker tycker, TeleDecl.DataCtor ctor) {
// Because we need to use in a lambda expression later
var dataCall = predataCall;
var ulift = dataConcrete.signature.result();
var tele = tele(tycker, ctor.telescope, ulift.isProp() ? null : ulift);
var tele = tele(tycker, ctor.telescope, ulift);

var elabClauses = tycker.zonk(tycker.elaboratePartial(ctor.clauses, dataCall));

Expand Down
Loading

0 comments on commit 8f7acdf

Please sign in to comment.