merge: Kala 0.82 (#1324)

Nice
aya-prover · Feb 14, 2025 · ec865dd · ec865dd
2 parents 4ba4c80 + 47944fe
commit ec865dd
Show file tree

Hide file tree

Showing 79 changed files with 169 additions and 194 deletions.
diff --git a/base/src/main/java/org/aya/normalize/Finalizer.java b/base/src/main/java/org/aya/normalize/Finalizer.java
@@ -74,7 +74,7 @@ case MetaCall(var ref, _) when !ref.isUser() && !alreadyReported.contains(ref) -
           fail(new UnsolvedMeta(stack.view()
             .drop(1)
             .map(this::freezeHoles)
-            .toImmutableSeq(), ref.pos(), ref.name()));
+            .toSeq(), ref.pos(), ref.name()));
         }
         case MetaLitTerm mlt -> fail(new UnsolvedLit(mlt));
         default -> {

diff --git a/base/src/main/java/org/aya/primitive/ShapeFactory.java b/base/src/main/java/org/aya/primitive/ShapeFactory.java
@@ -22,7 +22,7 @@ public class ShapeFactory {
     return discovered.view()
       .map(AyaShape.FindImpl::new)
       .filter(t -> t.recog().shape() == shape)
-      .toImmutableSeq();
+      .toSeq();
   }
 
   public @NotNull Option<ShapeRecognition> find(@Nullable AnyDef def) {

diff --git a/base/src/main/java/org/aya/resolve/context/ModuleExport.java b/base/src/main/java/org/aya/resolve/context/ModuleExport.java
@@ -78,7 +78,7 @@ public ModuleExport(@NotNull ModuleExport that) {
 
     return new ExportResult(
       badNames.isNotEmpty() ? this : newModule,
-      badNames.toImmutableSeq(),
+      badNames.toSeq(),
       ImmutableSeq.empty());
   }
 
@@ -115,8 +115,8 @@ public ModuleExport(@NotNull ModuleExport that) {
 
     return new ExportResult(
       hasError ? this : newExport,
-      badNames.toImmutableSeq(),
-      shadowNames.toImmutableSeq()
+      badNames.toSeq(),
+      shadowNames.toSeq()
     );
   }
 

diff --git a/base/src/main/java/org/aya/resolve/error/NameProblem.java b/base/src/main/java/org/aya/resolve/error/NameProblem.java
@@ -47,7 +47,7 @@ record AmbiguousNameError(
     }
 
     public @NotNull ImmutableSeq<String> didYouMean() {
-      return disambiguation.view().map(mod -> mod.resolve(name).toString()).toImmutableSeq();
+      return disambiguation.view().map(mod -> mod.resolve(name).toString()).toSeq();
     }
   }
 
@@ -210,7 +210,7 @@ record UnqualifiedNameNotFoundError(
           possible.append(modName.resolve(name).toString());
         }
       });
-      return possible.toImmutableSeq();
+      return possible.toSeq();
     }
   }
 

diff --git a/base/src/main/java/org/aya/resolve/error/OperatorError.java b/base/src/main/java/org/aya/resolve/error/OperatorError.java
@@ -83,8 +83,8 @@ record Circular(@NotNull ImmutableSeq<BinOpSet.BinOP> items) implements Operator
     @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.sep(
         Doc.english("Circular precedence found between"),
-        Doc.commaList(items.view().map(BinOpSet.BinOP::name).toImmutableSeq()
-          .sorted().view().map(Doc::plain))
+        Doc.commaList(items.view().map(BinOpSet.BinOP::name)
+          .sorted().map(Doc::plain))
       );
     }
   }

diff --git a/base/src/main/java/org/aya/resolve/module/ModuleLoader.java b/base/src/main/java/org/aya/resolve/module/ModuleLoader.java
@@ -42,7 +42,7 @@ public interface ModuleLoader extends Problematic {
       SCCs.forEach(sccTycker::tyckSCC);
     } finally {
       if (onTycked != null) onTycked.onModuleTycked(
-        resolveInfo, sccTycker.sccTycker().wellTyped().toImmutableSeq());
+        resolveInfo, sccTycker.sccTycker().wellTyped().toSeq());
     }
     return resolveInfo;
   }

diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -65,7 +65,7 @@ public static LiterateResolved resolveLax(@NotNull ModuleContext context, @NotNu
     var resolver = new ExprResolver(context, true);
     resolver.enter(Where.FnBody);
     var inner = expr.descent(resolver);
-    var view = resolver.allowedGeneralizes().valuesView().toImmutableSeq();
+    var view = resolver.allowedGeneralizes().valuesView().toSeq();
     return new LiterateResolved(view, inner);
   }
 
@@ -101,7 +101,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
       case Expr.Hole(var expl, var fill, var core, var local) -> {
         assert local.isEmpty();
         yield new Expr.Hole(expl, fill, core,
-          ctx.collect(MutableList.create()).toImmutableSeq());
+          ctx.collect(MutableList.create()).toSeq());
       }
       default -> expr;
     };

diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
@@ -64,7 +64,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
             resolveElim(resolver, body.inner());
             var clausesResolver = resolver.deriveRestrictive();
             clausesResolver.reference().append(new TyckOrder.Head(decl));
-            decl.body = body.map(x -> clausesResolver.clause(decl.teleVars().toImmutableSeq(), x));
+            decl.body = body.map(x -> clausesResolver.clause(decl.teleVars().toSeq(), x));
             addReferences(info, new TyckOrder.Body(decl), clausesResolver);
           }
           case FnBody.ExprBody(var expr) -> {
@@ -86,7 +86,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
           bodyResolver.enter(Where.ConPattern);
           con.patterns = con.patterns.map(pat ->
             pat.descent(pattern ->
-              bodyResolver.resolvePattern(pattern, data.teleVars().toImmutableSeq(), mCtx)));
+              bodyResolver.resolvePattern(pattern, data.teleVars().toSeq(), mCtx)));
           bodyResolver.exit();
           resolveMemberSignature(con, bodyResolver, mCtx);
           addReferences(info, new TyckOrder.Head(con), bodyResolver);

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -206,7 +206,7 @@ && whnf(type) instanceof DataCall dataCall
     var lifted = new Matchy(type.bindTele(wellArgs.size(), captures.view()),
       new QName(QPath.fileLevel(fileModule), "match-" + exprPos.lineColumnString()),
       wellClauses.map(clause -> clause.update(clause.body().bindTele(clause.bindCount(), captures.view())))
-        .toImmutableSeq());
+        .toSeq());
 
     var wellTerms = wellArgs.map(Jdg::wellTyped);
     return new MatchCall(lifted, wellTerms, captures.map(FreeTerm::new));

diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -291,7 +291,7 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
       freeDataCall = new DataCall(dataDef, 0, lhsResult.freePats().map(PatToTerm::visit));
 
       var allTypedBinds = Pat.collectBindings(wellPats.view());
-      ownerBinds = patWithTypeBound.component1().toImmutableSeq();
+      ownerBinds = patWithTypeBound.component1().toSeq();
       TeleTycker.bindTele(ownerBinds, allTypedBinds);
       ownerTelePos = ownerBinds.map(LocalVar::definition);
       ownerTele = allTypedBinds.map(Param::implicitize);

diff --git a/base/src/main/java/org/aya/tyck/TyckState.java b/base/src/main/java/org/aya/tyck/TyckState.java
@@ -99,7 +99,7 @@ public void solveMetas(@NotNull Reporter reporter) {
     while (eqns.isNotEmpty()) {
       //noinspection StatementWithEmptyBody
       while (simplify(reporter)) ;
-      var frozenEqns = eqns.toImmutableSeq();
+      var frozenEqns = eqns.toSeq();
       if (postSimplificationSize == frozenEqns.size()) {
         // TODO: report error, cannot solve eqns
         reporter.report(new MetaVarError.CannotSolveEquations(frozenEqns));

diff --git a/base/src/main/java/org/aya/tyck/error/Goal.java b/base/src/main/java/org/aya/tyck/error/Goal.java
@@ -38,7 +38,7 @@ public record Goal(
       Doc.vcat(hole.args().map(arg -> renderScopeVar(options, arg)))
       // ,meta.conditions.isNotEmpty() ? Doc.vcat(
       //   ImmutableSeq.of(Doc.plain("To ensure confluence:"))
-      //     .concat(meta.conditions.toImmutableSeq().map(tup -> Doc.par(1, Doc.cat(
+      //     .concat(meta.conditions.toSeq().map(tup -> Doc.par(1, Doc.cat(
       //       Doc.plain("Given "),
       //       Doc.parened(tup.component1().toDoc(options)),
       //       Doc.plain(", we should have: "),

diff --git a/base/src/main/java/org/aya/tyck/error/TyckOrderError.java b/base/src/main/java/org/aya/tyck/error/TyckOrderError.java
@@ -30,7 +30,7 @@ record CircularSignature(@NotNull ImmutableSeq<TyckUnit> cycles) implements Tyck
     @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.sep(
         Doc.english("Circular signature dependency found between"),
-        Doc.commaList(cycles.view().map(this::nameOf).toImmutableSeq()
+        Doc.commaList(cycles.view().map(this::nameOf).toSeq()
           .sorted().view().map(Doc::plain))
       );
     }

diff --git a/base/src/main/java/org/aya/tyck/order/AyaSccTycker.java b/base/src/main/java/org/aya/tyck/order/AyaSccTycker.java
@@ -75,7 +75,7 @@ private void checkMutual(@NotNull ImmutableSeq<TyckOrder> scc) {
     var unit = scc.view().map(TyckOrder::unit)
       .distinct()
       .sorted(Comparator.comparing(SourceNode::sourcePos))
-      .toImmutableSeq();
+      .toSeq();
     if (unit.sizeEquals(1)) checkUnit(new TyckOrder.Body(unit.getFirst()));
     else {
       unit.forEach(u -> check(new TyckOrder.Head(u)));
@@ -108,14 +108,14 @@ private void terck(@NotNull ImmutableSeq<TyckOrder.Body> units) {
     var recDefs = units.view()
       .filter(u -> selfReferencing(resolveInfo.depGraph(), u))
       .map(TyckOrder::unit)
-      .toImmutableSeq();
+      .toSeq();
     if (recDefs.isEmpty()) return;
     // TODO: positivity check for data/record definitions
     var fn = recDefs.view()
       .filterIsInstance(FnDecl.class)
       .filterNot(f -> f.modifiers.contains(Modifier.NonTerminating))
       .map(f -> f.ref.core)
-      .toImmutableSeq();
+      .toSeq();
     terckRecursiveFn(fn);
   }
 

diff --git a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
@@ -74,7 +74,7 @@ public record PatClassifier(
     var classifier = new PatClassifier(tycker, pos);
     var cl = classifier.classifyN(ImmutableSeq.empty(), telescope, freePats
       .mapIndexed((i, clause) -> new Indexed<>(clause.view(), i))
-      .toImmutableSeq(), 4);
+      .toSeq(), 4);
     var p = cl.partition(c -> c.cls().isEmpty());
     var missing = p.component1();
     if (missing.isNotEmpty()) tycker.fail(
@@ -170,7 +170,7 @@ case DepTypeTerm(var kind, var lT, var rT) when kind == DTKind.Sigma -> {
         if (missedCon >= body.size()) {
           return ImmutableSeq.of(simple(param.toFreshPat(), ImmutableIntSeq.empty()));
         }
-        return buffer.toImmutableSeq();
+        return buffer.toSeq();
       }
       default -> { }
     }

diff --git a/base/src/main/java/org/aya/tyck/pat/PatUnify.java b/base/src/main/java/org/aya/tyck/pat/PatUnify.java
@@ -108,6 +108,6 @@ public record Result(PatUnify unify, @NotNull Seq<Term> args) { }
   ) {
     assert rpats.sizeEquals(lpats);
     var args = lpats.zip(rpats, (lp, rp) -> unifyPat(lp, rp, ctx, lhsSubst, rhsSubst));
-    return new Result(new PatUnify(lhsSubst, rhsSubst, ctx), args.toImmutableSeq());
+    return new Result(new PatUnify(lhsSubst, rhsSubst, ctx), args.toSeq());
   }
 }
diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
@@ -239,7 +239,7 @@ public enum Kind {
           foundError(new PatternProblem.TooManyImplicitPattern(pattern, currentParam));
         }
 
-        return new FindNextParam(generatedPats.toImmutableSeq(), FindNextParam.Kind.TooManyImplicit);
+        return new FindNextParam(generatedPats.toSeq(), FindNextParam.Kind.TooManyImplicit);
       } else {
         // current param is implicit, generate pattern for it
         generatedPats.append(generatePattern());
@@ -253,10 +253,10 @@ public enum Kind {
 
     // no more param
     if (currentParam == null) {
-      return new FindNextParam(generatedPats.toImmutableSeq(), FindNextParam.Kind.TooManyPattern);
+      return new FindNextParam(generatedPats.toSeq(), FindNextParam.Kind.TooManyPattern);
     }
 
-    return new FindNextParam(generatedPats.toImmutableSeq(), FindNextParam.Kind.Success);
+    return new FindNextParam(generatedPats.toSeq(), FindNextParam.Kind.Success);
   }
 
   public @NotNull TyckResult tyck(
@@ -416,7 +416,7 @@ private void addAsSubst(@NotNull LocalVar as, @NotNull Pat pattern, @NotNull Ter
   }
 
   private @NotNull TyckResult done(@NotNull MutableList<Pat> wellTyped) {
-    return new TyckResult(wellTyped.toImmutableSeq(), paramSubst.toImmutableSeq(), asSubst, hasError);
+    return new TyckResult(wellTyped.toSeq(), paramSubst.toSeq(), asSubst, hasError);
   }
 
   private record Selection(

diff --git a/base/src/main/java/org/aya/tyck/pat/iter/PiPusheen.java b/base/src/main/java/org/aya/tyck/pat/iter/PiPusheen.java
@@ -26,7 +26,7 @@ public PiPusheen(@NotNull DepTypeTerm.Unpi unpi) {
   }
 
   public @NotNull DepTypeTerm.Unpi unpiBody() {
-    return new DepTypeTerm.Unpi(unpi.sliceView(pusheenIdx, unpi.size()).toImmutableSeq(), result);
+    return new DepTypeTerm.Unpi(unpi.sliceView(pusheenIdx, unpi.size()).toSeq(), result);
   }
 
   @Override public boolean hasNext() { return pusheenIdx < unpi.size(); }

diff --git a/base/src/main/java/org/aya/tyck/pat/iter/SignatureIterator.java b/base/src/main/java/org/aya/tyck/pat/iter/SignatureIterator.java
@@ -84,7 +84,7 @@ public SignatureIterator(Iterator<Param> iter, @NotNull Pusheenable<Param, Term>
   }
 
   public @NotNull AbstractTele.Locns signature() {
-    return new AbstractTele.Locns(consumed.toImmutableSeq(), body().body());
+    return new AbstractTele.Locns(consumed.toSeq(), body().body());
   }
 
   @Override

diff --git a/base/src/main/java/org/aya/tyck/tycker/Contextful.java b/base/src/main/java/org/aya/tyck/tycker/Contextful.java
@@ -49,7 +49,7 @@ public interface Contextful {
    * @see LocalCtx#extract()
    */
   default @NotNull MetaCall freshMeta(String name, @NotNull SourcePos pos, MetaVar.Requirement req, boolean isUser) {
-    var vars = localCtx().extract().toImmutableSeq();
+    var vars = localCtx().extract().toSeq();
     var args = vars.<Term>map(FreeTerm::new);
     return new MetaCall(new MetaVar(name, pos, args.size(), req.bind(vars.view()), isUser), args);
   }

diff --git a/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java b/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java
@@ -42,7 +42,7 @@ public sealed interface TeleTycker extends Contextful {
     @NotNull ImmutableSeq<Expr.Param> cTele,
     @NotNull WithPos<Expr> result
   ) {
-    var locals = cTele.view().map(Expr.Param::ref).toImmutableSeq();
+    var locals = cTele.view().map(Expr.Param::ref).toSeq();
     var checkedParam = checkTele(cTele);
     var checkedResult = checkType(result, true).bindTele(locals.view());
     return new Signature(new AbstractTele.Locns(checkedParam, checkedResult), cTele.map(Expr.Param::sourcePos));
@@ -53,9 +53,9 @@ public sealed interface TeleTycker extends Contextful {
    */
   default @NotNull ImmutableSeq<Param> checkTele(@NotNull ImmutableSeq<Expr.Param> cTele) {
     var tele = checkTeleFree(cTele);
-    var locals = cTele.view().map(Expr.Param::ref).toImmutableSeq();
+    var locals = cTele.view().map(Expr.Param::ref).toSeq();
     bindTele(locals, tele);
-    return tele.toImmutableSeq();
+    return tele.toSeq();
   }
 
   /**

diff --git a/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java b/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java
@@ -91,7 +91,7 @@ public int run(@NotNull MainArgs.PlctAction args) throws Exception {
     var seq = parse(client.send(req, HttpResponse.BodyHandlers.ofInputStream()).body())
       .view()
       .filter(i -> i.updatedAt.isAfter(since))
-      .toImmutableSeq();
+      .toSeq();
     if (seq.isEmpty()) return Doc.empty();
     return Doc.vcat(seq.view()
       .map(this::pullRequest)

diff --git a/cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java b/cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java
@@ -146,7 +146,7 @@ public record ModuleTrie(@NotNull ImmutableMap<String, ModuleTrie> children, boo
       hint.addAll(mod.symbols().keysView());
     }
 
-    return hint.toImmutableSeq();
+    return hint.toSeq();
   }
 
   public @NotNull ImmutableMap<String, ModuleTrie> moduleTree() {
@@ -155,7 +155,7 @@ public record ModuleTrie(@NotNull ImmutableMap<String, ModuleTrie> children, boo
       return this.moduleTree;
     }
 
-    var moduleNames = this.modules.keysView().toImmutableSeq()
+    var moduleNames = this.modules.keysView().toSeq()
       .map(x -> x.ids().view());
 
     this.moduleTree = buildModuleTree(moduleNames);
@@ -192,7 +192,7 @@ public record ModuleTrie(@NotNull ImmutableMap<String, ModuleTrie> children, boo
       }
     }
 
-    return indexed.toImmutableSeq()
+    return indexed.toSeq()
       .collect(ImmutableMap.collector(Tuple2::component1, x -> {
         var children = buildModuleTree(x.component2());
         var isInhabited = inhabited.contains(x.component1());

diff --git a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java
@@ -251,7 +251,7 @@ private boolean make(@NotNull ImmutableSeq<LibrarySource> modified) throws IOExc
     var depGraph = resolveImports();
     var affected = collectAffected(modified, depGraph);
     var SCCs = affected.topologicalOrder().view()
-      .reversed().toImmutableSeq();
+      .reversed().toSeq();
     // ^ top order generated from usage graph should be reversed.
     // Only here we generate top order from usage graph just for efficiency
     // (transposing a graph is slower than reversing a list).
@@ -321,7 +321,7 @@ private static void collectAffected(
 
   /** collect source files that are directly modified by user */
   private @NotNull ImmutableSeq<LibrarySource> collectModified() {
-    return owner.librarySources().filter(advisor::isSourceModified).toImmutableSeq();
+    return owner.librarySources().filter(advisor::isSourceModified).toSeq();
   }
 
   private void clearPrimitives(@Nullable ImmutableSeq<Stmt> stmts) {

diff --git a/cli-impl/src/main/java/org/aya/cli/library/json/LibraryConfigData.java b/cli-impl/src/main/java/org/aya/cli/library/json/LibraryConfigData.java
@@ -85,7 +85,7 @@ public void checkDeserialization() {
       literateConfig,
       ImmutableSeq.from(dependency.entrySet()).view()
         .map(e -> e.getValue().as(libraryRoot, e.getKey()))
-        .toImmutableSeq()
+        .toSeq()
     );
   }
 

diff --git a/cli-impl/src/main/java/org/aya/cli/library/source/LibrarySource.java b/cli-impl/src/main/java/org/aya/cli/library/source/LibrarySource.java
@@ -68,7 +68,7 @@ public record LibrarySource(
     var displayNoExt = display.resolveSibling(AyaFiles.stripAyaSourcePostfix(display.getFileName().toString()));
     return new ModulePath(IntRange.closedOpen(0, displayNoExt.getNameCount())
       .mapToObjTo(MutableList.create(), i -> displayNoExt.getName(i).toString())
-      .toImmutableSeq());
+      .toSeq());
   }
 
   public @NotNull Path displayPath() {

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/FaithfulPrettier.java b/cli-impl/src/main/java/org/aya/cli/literate/FaithfulPrettier.java
@@ -37,7 +37,7 @@ static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlights) {
       .filterNot(h -> h.sourcePos().isEmpty())
       .filter(x -> codeRange.containsIndex(x.sourcePos()))
       .sorted().distinct()
-      .toImmutableSeq();
+      .toSeq();
     checkHighlights(highlightInRange);
     return highlightInRange;
   }

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/FlclFaithfulPrettier.java b/cli-impl/src/main/java/org/aya/cli/literate/FlclFaithfulPrettier.java
@@ -32,7 +32,7 @@ public record FlclFaithfulPrettier(@Override @NotNull PrettierOptions options)
     return new HighlightInfo.Ref(range, EMPTY_LINK, kind, null);
   }
   public @NotNull Doc highlight(@NotNull FlclToken.File file) {
-    var highlights = file.tokens().view().map(FlclFaithfulPrettier::toInfo).sorted().toImmutableSeq();
+    var highlights = file.tokens().view().map(FlclFaithfulPrettier::toInfo).sorted().toSeq();
     FaithfulPrettier.checkHighlights(highlights);
     return doHighlight(file.sourceCode(), file.startIndex(), highlights);
   }

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/LiterateFaithfulPrettier.java b/cli-impl/src/main/java/org/aya/cli/literate/LiterateFaithfulPrettier.java
@@ -64,7 +64,7 @@ public record LiterateFaithfulPrettier(
       .filter(p -> codeRange.containsIndex(p.sourcePos()))
       .flatMap(p -> InlineHintProblem.withInlineHints(p, options))
       .distinct()
-      .toImmutableSeq();
+      .toSeq();
 
     return problemsInRange.foldLeft(FaithfulPrettier.highlightsInRange(codeRange, highlights), (acc, p) -> {
       var partition = acc.partition(