Skip to content

Commit

Permalink
merge: Use Java 21 features (#1023)
Browse files Browse the repository at this point in the history 
Yeeassss
  • Loading branch information
@ice1000
ice1000 authored Dec 13, 2023
2 parents 808d4ef + 4dd8428 commit c54bc3d
Show file tree
Hide file tree
Showing 22 changed files with 93 additions and 109 deletions.
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/core/pat/PatUnify.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ private void visitAs(@NotNull LocalVar as, Pat rhs) {

private void reportError(@NotNull Pat lhs, @NotNull Pat pat) {
var doc = Doc.sep(lhs.toDoc(AyaPrettierOptions.debug()), Doc.plain("and"), pat.toDoc(AyaPrettierOptions.debug()));
throw new InternalException(doc.debugRender() + " are patterns of different types!");
throw new InternalException(STR."\{doc.debugRender()} are patterns of different types!");
}

private static void unifyPat(Pat lhs, Pat rhs, Subst lhsSubst, Subst rhsSubst, LocalCtx ctx) {
Expand Down
10 changes: 1 addition & 9 deletions base/src/main/java/org/aya/core/term/Term.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
import org.aya.pretty.doc.Doc;
import org.aya.ref.AnyVar;
import org.aya.ref.LocalVar;
import org.aya.tyck.env.LocalCtx;
import org.aya.tyck.tycker.TyckState;
import org.aya.tyck.unify.Synthesizer;
import org.aya.util.Arg;
Expand Down Expand Up @@ -50,7 +49,7 @@ public sealed interface Term extends AyaDocile, Restr.TermLike<Term>
permits Callable, CoeTerm, Elimination, Formation, FormulaTerm, HCompTerm, InTerm, MatchTerm, MetaLitTerm, MetaPatTerm, PartialTerm, RefTerm, RefTerm.Field, StableWHNF {
/**
* Descending an operation to the term AST. NOTE: Currently we require the operation `f` to preserve:
* {@link StructCall}, {@link DataCall}, {@link SortTerm}, {@link org.aya.generic.Shaped.Applicable}.
* {@link ClassCall}, {@link DataCall}, {@link SortTerm}, {@link org.aya.generic.Shaped.Applicable}.
*/
@NotNull Term descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g);

Expand Down Expand Up @@ -114,13 +113,6 @@ default VarConsumer.ScopeChecker scopeCheck(@NotNull ImmutableSeq<LocalVar> allo
default @NotNull Term lift(int ulift) {
return new EndoTerm.Elevator(ulift).apply(this);
}
/**
* @return WHNF
* @throws NullPointerException if the term is an introduction rule
*/
default @NotNull Term computeType(@NotNull TyckState state, @NotNull LocalCtx ctx) {
return new Synthesizer(state, ctx).press(this);
}

/**
* @author re-xyr
Expand Down
8 changes: 4 additions & 4 deletions base/src/main/java/org/aya/core/visitor/BetaExpander.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,24 +56,24 @@ yield switch (partial(partial)) {
case PartialTerm(var partial, var rhsTy) -> new PartialTerm(partial(partial), rhsTy);
// TODO[coe]: temporary hack
case CoeTerm(
var ty,
_,
FormulaTerm(Formula.Lit(var r)),
FormulaTerm(Formula.Lit(var s))
) when r == s -> identity("x");
case CoeTerm(var ty, RefTerm(var r), RefTerm(var s)) when r == s -> identity("x");
case CoeTerm(_, RefTerm(var r), RefTerm(var s)) when r == s -> identity("x");
case CoeTerm coe -> {
var varI = new LamTerm.Param(new LocalVar("i"), true);
var codom = apply(AppTerm.make(coe.type(), varI.toArg()));

yield switch (codom) {
case PathTerm path -> term;
case PathTerm _ -> term;
case PiTerm pi -> pi.coe(coe, varI);
case SigmaTerm sigma -> sigma.coe(coe, varI);
case DataCall data when data.args().isEmpty() -> identity(String.valueOf(data.ref()
.name().chars()
.filter(Character::isAlphabetic)
.findFirst()).toLowerCase(Locale.ROOT));
case SortTerm type -> identity("A");
case SortTerm _ -> identity("A");
default -> term;
};
}
Expand Down
8 changes: 4 additions & 4 deletions base/src/main/java/org/aya/prettier/Codifier.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,17 +101,17 @@ case FormulaTerm(var mula) -> {
formula(mula);
builder.append(")");
}
case ErrorTerm error -> throw new UnsupportedOperationException("Cannot generate error");
case Callable call -> throw new UnsupportedOperationException("Cannot generate calls");
case IntervalTerm interval -> builder.append("IntervalTerm.INSTANCE");
case ErrorTerm _ -> throw new UnsupportedOperationException("Cannot generate error");
case Callable _ -> throw new UnsupportedOperationException("Cannot generate calls");
case IntervalTerm _ -> builder.append("IntervalTerm.INSTANCE");
case SortTerm sort -> {
builder.append("new SortTerm(SortKind.");
builder.append(sort.kind().name());
builder.append(", ");
builder.append(sort.lift());
builder.append(")");
}
default -> throw new UnsupportedOperationException("TODO: " + term.getClass().getCanonicalName());
default -> throw new UnsupportedOperationException(STR."TODO: \{term.getClass().getCanonicalName()}");
}
}

Expand Down
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ private void addReference(@NotNull DefVar<?, ?> defVar) {
addReference(maybe);
yield new Pattern.Ctor(bind, maybe);
}
ctx.set(ctx.get().bind(bind.bind(), var -> false));
ctx.set(ctx.get().bind(bind.bind(), _ -> false));
yield bind;
}
case Pattern.QualifiedRef qref -> {
Expand Down
13 changes: 6 additions & 7 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ yield switch (whnf(term)) {
return new Result.Default(new RefTerm(loc), ty);
});
case DefVar<?, ?> defVar -> inferRef(defVar);
default -> throw new InternalException("Unknown var: " + ref.resolvedVar().getClass());
default -> throw new InternalException(STR."Unknown var: \{ref.resolvedVar().getClass()}");
};
case Expr.Pi pi -> {
var corePi = ty(pi);
Expand Down Expand Up @@ -253,7 +253,7 @@ yield switch (whnf(term)) {
yield new Result.Default(TupTerm.explicits(items.map(Result::wellTyped)),
new SigmaTerm(items.map(item -> new Term.Param(LocalVar.IGNORED, item.type(), true))));
}
case Expr.App(var sourcePos, var appF, var argument) -> {
case Expr.App(_, var appF, var argument) -> {
var f = synthesize(appF);
var app = f.wellTyped();
if (app instanceof ErrorTerm || f.type() instanceof ErrorTerm) yield f;
Expand Down Expand Up @@ -324,7 +324,7 @@ yield switch (whnf(term)) {
var defs = shapeFactory.findImpl(AyaShape.NAT_SHAPE);
if (defs.isEmpty()) yield fail(expr, new NoRuleError(expr, null));
if (defs.sizeGreaterThan(1)) {
var type = ctx.freshTyHole("_ty" + lit.integer() + "'", lit.sourcePos());
var type = ctx.freshTyHole(STR."_ty\{lit.integer()}'", lit.sourcePos());
yield new Result.Default(new MetaLitTerm(lit.sourcePos(), lit.integer(), defs, type.component1()), type.component1());
}
var match = defs.getFirst();
Expand Down Expand Up @@ -558,7 +558,7 @@ private static class ClauseTyckState {
var field = (DefVar<MemberDef, TeleDecl.ClassMember>) var;
return new Result.Default(new RefTerm.Field(field), Def.defType(field));
} else {
final var msg = "Def var `" + var.name() + "` has core `" + var.core + "` which we don't know.";
final var msg = STR."Def var `\{var.name()}` has core `\{var.core}` which we don't know.";
throw new InternalException(msg);
}
}
Expand All @@ -584,14 +584,13 @@ private static boolean needImplicitParamIns(@NotNull Expr expr) {
return expr instanceof Expr.Lambda ex && ex.param().explicit() || !(expr instanceof Expr.Lambda);
}

@SuppressWarnings("unchecked")
private @Nullable Result inferShapedFn(@NotNull DefVar<FnDef, TeleDecl.FnDecl> var) {
var recog = shapeFactory.find(var.core);

if (recog.isDefined()) {
var head = ShapeFactory.ofFn(var, recog.get());
assert head != null : "bad ShapeFactory";
return defCall(var, (defVar, ulift, args) -> new RuleReducer.Fn(head, ulift, args));
return defCall(var, (_, ulift, args) -> new RuleReducer.Fn(head, ulift, args));
}

return null;
Expand All @@ -604,7 +603,7 @@ private static boolean needImplicitParamIns(@NotNull Expr expr) {
if (recog.shape() == AyaShape.NAT_SHAPE) {
var head = ShapeFactory.ofCtor(var, recog, new DataCall(dataVar, 0, ImmutableSeq.empty()));
assert head != null : "bad ShapeFactory";
return defCall(var, (mVar, ulift, args) -> new RuleReducer.Con(head, ulift, ImmutableSeq.empty(), args));
return defCall(var, (_, ulift, args) -> new RuleReducer.Con(head, ulift, ImmutableSeq.empty(), args));
}

return null;
Expand Down
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/tyck/StmtTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ record Tmp(ImmutableSeq<TeleResult> okTele, Term preresult, Term prebody) {}
}

public void tyckHeader(@NotNull Decl decl, @NotNull ExprTycker tycker) {
tracing(builder -> builder.shift(new Trace.LabelT(decl.sourcePos(), "telescope of " + decl.ref().name())));
tracing(builder -> builder.shift(new Trace.LabelT(decl.sourcePos(), STR."telescope of \{decl.ref().name()}")));
switch (decl) {
case ClassDecl clazz -> {
var body = clazz.members.map(field -> (MemberDef) tyck(field, tycker));
Expand Down
48 changes: 23 additions & 25 deletions base/src/main/java/org/aya/tyck/unify/TermComparator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,6 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
else return null;
}

@SuppressWarnings("unused")
private boolean doCompareTyped(@NotNull Term type, @NotNull Term lhs, @NotNull Term rhs, Sub lr, Sub rl) {
// Skip tracing, because too easy.
// Note that it looks tempting to apply some unification here, but it is not correct:
Expand Down Expand Up @@ -298,23 +297,22 @@ case SigmaTerm(var paramsSeq) -> {
// https://stackoverflow.com/q/75971020/7083401
case PiTerm pi -> ctx.with(pi.param(), () -> {
var pair = new Pair<>(lhs, rhs);
if (pair instanceof Pair(LamTerm(var lp, var lb), LamTerm(var rp, var rb))) {
var ref = pi.param().ref();
if (ref == LocalVar.IGNORED) ref = new LocalVar(lp.ref().name() + rp.ref().name());
lr.map.put(ref, rp.toTerm());
rl.map.put(ref, lp.toTerm());
var piParam = new RefTerm(ref);
var res = compare(lb.subst(lp.ref(), piParam), rb.subst(rp.ref(), piParam), lr, rl, pi.body());
lr.map.remove(ref);
rl.map.remove(ref);
return res;
} else if (pair instanceof Pair(var $, LamTerm rambda)) {
return compareLambdaBody(rambda, lhs, rl, lr, pi);
} else if (pair instanceof Pair(LamTerm lambda, var $)) {
return compareLambdaBody(lambda, rhs, lr, rl, pi);
} else {
return compare(lhs, rhs, lr, rl, null);
}
return switch (pair) {
case Pair(LamTerm(var lp, var lb), LamTerm(var rp, var rb)) -> {
var ref = pi.param().ref();
if (ref == LocalVar.IGNORED) ref = new LocalVar(lp.ref().name() + rp.ref().name());
lr.map.put(ref, rp.toTerm());
rl.map.put(ref, lp.toTerm());
var piParam = new RefTerm(ref);
var res = compare(lb.subst(lp.ref(), piParam), rb.subst(rp.ref(), piParam), lr, rl, pi.body());
lr.map.remove(ref);
rl.map.remove(ref);
yield res;
}
case Pair(_, LamTerm rambda) -> compareLambdaBody(rambda, lhs, rl, lr, pi);
case Pair(LamTerm lambda, _) -> compareLambdaBody(lambda, rhs, lr, rl, pi);
default -> compare(lhs, rhs, lr, rl, null);
};
});
// In this case, both sides have the same type (I hope)
case PathTerm cube -> ctx.withIntervals(cube.params().view(), () -> {
Expand Down Expand Up @@ -376,7 +374,7 @@ private boolean comparePartial(
) {
return switch (new Pair<>(lhs.partial(), rhs.partial())) {
case Pair(Partial.Const(var ll), Partial.Const(var rr)) -> compare(ll, rr, lr, rl, type.type());
case Pair(Partial.Split<?> ll, Partial.Split<?> rr) -> CofThy.conv(type.restr(), new Subst(),
case Pair(Partial.Split<?> _, Partial.Split<?> _) -> CofThy.conv(type.restr(), new Subst(),
subst -> compare(lhs.subst(subst), rhs.subst(subst), lr, rl, type.subst(subst)));
default -> false;
};
Expand Down Expand Up @@ -414,12 +412,12 @@ case Pair(PiTerm(var lParam, var lBody), PiTerm(var rParam, var rBody)) ->
checkParam(lParam, rParam, new Subst(), new Subst(), lr, rl, () -> false,
(lsub, rsub) -> compare(lBody.subst(lsub), rBody.subst(rsub), lr, rl, null));
case Pair(SigmaTerm(var lParams), SigmaTerm(var rParams)) -> checkParams(lParams.view(), rParams.view(),
new Subst(), new Subst(), lr, rl, () -> false, (lsub, rsub) -> true);
new Subst(), new Subst(), lr, rl, () -> false, (_, _) -> true);
case Pair(SortTerm lhs, SortTerm rhs) -> compareSort(lhs, rhs);
case Pair(PartialTyTerm(var lTy, var lR), PartialTyTerm(var rTy, var rR)) ->
compare(lTy, rTy, lr, rl, null) && compareRestr(lR, rR);
case Pair(PathTerm lCube, PathTerm rCube) -> compareCube(lCube, rCube, lr, rl);
case Pair(IntervalTerm lhs, IntervalTerm rhs) -> true;
case Pair(IntervalTerm _, IntervalTerm _) -> true;
default -> throw noRules(preLhs);
};
}
Expand Down Expand Up @@ -474,7 +472,7 @@ case AppTerm(var lOf, var lArg) -> {
else yield null;
}
// See compareApprox for why we don't compare these
case FnCall lhs -> null;
case FnCall _ -> null;
case CoeTerm coe -> {
if (!(preRhs instanceof CoeTerm(var rType, var rR, var rS))) yield null;
if (!compare(coe.r(), rR, lr, rl, IntervalTerm.INSTANCE)) yield null;
Expand All @@ -501,7 +499,7 @@ yield compare(coe.type(), rType, lr, rl, PrimDef.intervalToType()) ?
default -> null;
};
// end ConCallLike
case PrimCall lhs -> null;
case PrimCall _ -> null;
case FieldTerm lhs -> {
if (!(preRhs instanceof FieldTerm rhs)) yield null;
var preStructType = compareUntyped(lhs.of(), rhs.of(), lr, rl);
Expand All @@ -510,8 +508,8 @@ yield compare(coe.type(), rType, lr, rl, PrimDef.intervalToType()) ?
yield Def.defResult(lhs.ref());
}
// We expect to only compare the elimination "outS" here
case OutTerm(var lPhi, var pal, var lU) -> {
if (!(preRhs instanceof OutTerm(var rPhi, var par, var rU))) yield null;
case OutTerm(var lPhi, _, var lU) -> {
if (!(preRhs instanceof OutTerm(var rPhi, _, var rU))) yield null;
if (!compare(lPhi, rPhi, lr, rl, IntervalTerm.INSTANCE)) yield null;
var innerTy = compareUntyped(lU, rU, lr, rl);
if (innerTy == null) yield null;
Expand Down
2 changes: 1 addition & 1 deletion base/src/test/java/org/aya/literate/AyaMdParserTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ public void testExtract(String caseName) throws IOException {
var expPath = oneCase.expectedAyaFile();

if (!expPath.toFile().exists()) {
System.err.println("Test Data " + expPath + " doesn't exist, skip.");
System.err.println(STR."Test Data \{expPath} doesn't exist, skip.");
} else {
var expAyaFile = file(expPath);

Expand Down
12 changes: 6 additions & 6 deletions base/src/test/java/org/aya/literate/HighlighterTester.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
var expectedText = expected.expected.display();
var actualText = sourceCode.substring(sourcePos.tokenStartIndex(), sourcePos.tokenEndIndex() + 1);

assertEquals(expectedText, actualText, "at " + sourcePos);
assertEquals(expectedText, actualText, STR."at \{sourcePos}");

switch (actual) {
case HighlightInfo.Lit(_, var ty)
Expand All @@ -141,7 +141,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
case HighlightInfo.Err _ -> throw new UnsupportedOperationException("TODO"); // TODO

default ->
fail("expected: " + expected.getClass().getSimpleName() + ", but actual: " + actual.getClass().getSimpleName());
fail(STR."expected: \{expected.getClass().getSimpleName()}, but actual: \{actual.getClass().getSimpleName()}");
}
});
assertEquals(expecteds.size(), actuals.size(), "size mismatch");
Expand All @@ -152,7 +152,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
*/
public void checkDef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Def def) {
var existDef = defSet.containsKey(def.target());
assertFalse(existDef, "Duplicated def: " + def.target() + " at " + sourcePos);
assertFalse(existDef, STR."Duplicated def: \{def.target()} at \{sourcePos}");

defSet.put(def.target(), Option.ofNullable(def.kind()));
}
Expand All @@ -166,7 +166,7 @@ public void assertDef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Def a

if (name != null) {
var existName = defMap.getOption(name);
assertFalse(existName.isDefined(), "Duplicated name: " + expectedDef.name());
assertFalse(existName.isDefined(), STR."Duplicated name: \{expectedDef.name()}");

defMap.put(name, Tuple.of(actualDef.target(), Option.ofNullable(actualDef.kind())));
}
Expand All @@ -178,7 +178,7 @@ public void assertDef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Def a
public void checkRef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Ref ref) {
var defData = defSet.getOrNull(ref.target());

assertNotNull(defData, "Expected def: " + ref.target() + " at " + sourcePos);
assertNotNull(defData, STR."Expected def: \{ref.target()} at \{sourcePos}");
assertEquals(defData.getOrNull(), ref.kind());
}

Expand All @@ -189,7 +189,7 @@ public void assertRef(@NotNull SourcePos sourcePos, @NotNull HighlightInfo.Ref a

if (name != null) {
var existName = defMap.getOption(name);
assertTrue(existName.isDefined(), "Undefined name: " + expectedRef.name());
assertTrue(existName.isDefined(), STR."Undefined name: \{expectedRef.name()}");

var defData = existName.get();
assertEquals(defData.component2().getOrNull(), actualRef.kind());
Expand Down
Loading

0 comments on commit c54bc3d

Please sign in to comment.