merge: #873

873: Happy new year! r=ice1000 a=ice1000

update something and clean ups...

Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2021-2022 Tesla (Yinsen) Zhang
+Copyright (c) 2021-2023 Tesla (Yinsen) Zhang
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

base/src/main/java/org/aya/concrete/Expr.java

@@ -1,4 +1,4 @@
-// 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.concrete;
 
@@ -11,12 +11,12 @@
 import kala.value.MutableValue;
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.core.def.PrimDef;
-import org.aya.prettier.BasePrettier;
-import org.aya.prettier.ConcretePrettier;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.ParamLike;
 import org.aya.generic.SortKind;
 import org.aya.guest0x0.cubical.Restr;
+import org.aya.prettier.BasePrettier;
+import org.aya.prettier.ConcretePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.AnyVar;
 import org.aya.ref.DefVar;
@@ -27,15 +27,14 @@
 import org.aya.tyck.Result;
 import org.aya.util.ForLSP;
 import org.aya.util.binop.BinOpParser;
-import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
+import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.function.Consumer;
 import java.util.function.Function;
 import java.util.function.UnaryOperator;
 
@@ -280,14 +279,6 @@ record Lambda(
     }
   }
 
-  static @NotNull Expr unlam(@NotNull Expr expr, int max, @NotNull Consumer<Param> params) {
-    while (expr instanceof Lambda lambda && max-- > 0) {
-      params.accept(lambda.param);
-      expr = lambda.body;
-    }
-    return expr;
-  }
-
   /**
    * @author re-xyr
    */

base/src/main/java/org/aya/concrete/visitor/EndoPattern.java

@@ -1,12 +1,10 @@
-// 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.concrete.visitor;
 
 import org.aya.concrete.Pattern;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.function.UnaryOperator;
-
 public interface EndoPattern {
   default @NotNull Pattern pre(@NotNull Pattern pattern) {
     return pattern;

base/src/main/java/org/aya/core/Meta.java

@@ -1,16 +1,18 @@
-// 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.core;
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.tuple.Tuple2;
-import org.aya.core.term.*;
+import org.aya.core.term.MetaTerm;
+import org.aya.core.term.PiTerm;
+import org.aya.core.term.Term;
 import org.aya.core.visitor.Subst;
-import org.aya.util.Arg;
 import org.aya.generic.Constants;
 import org.aya.ref.AnyVar;
+import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -74,8 +76,8 @@ private Meta(
     @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 domVar = new Meta(contextTele, ImmutableSeq.empty(), domName, result, isType, sourcePos);
+    var codVar = new Meta(contextTele, ImmutableSeq.empty(), codName, result, isType, sourcePos);
     var dom = new MetaTerm(domVar, contextArgs, ImmutableSeq.empty());
     var cod = new MetaTerm(codVar, contextArgs, ImmutableSeq.empty());
     var domParam = new Term.Param(Constants.randomlyNamed(sourcePos), dom, explicit);

base/src/main/java/org/aya/core/def/Def.java

@@ -1,17 +1,15 @@
-// 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.core.def;
 
 import kala.collection.Seq;
-import kala.collection.SeqLike;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.concrete.stmt.Decl;
 import org.aya.concrete.stmt.TeleDecl;
 import org.aya.core.term.PiTerm;
 import org.aya.core.term.Term;
-import org.aya.core.visitor.Subst;
-import org.aya.prettier.CorePrettier;
 import org.aya.generic.AyaDocile;
+import org.aya.prettier.CorePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.DefVar;
 import org.aya.util.prettier.PrettierOptions;
@@ -42,10 +40,6 @@ public sealed interface Def extends AyaDocile, GenericDef permits SubLevelDef, T
       // guaranteed as this is already a core term
     else return Objects.requireNonNull(defVar.concrete.signature()).result;
   }
-  static @NotNull ImmutableSeq<Term.Param>
-  substParams(@NotNull SeqLike<Term.@NotNull Param> param, @NotNull Subst subst) {
-    return param.view().drop(1).map(p -> p.subst(subst)).toImmutableSeq();
-  }
 
   @Override @NotNull DefVar<? extends Def, ? extends Decl> ref();
   @NotNull ImmutableSeq<Term.Param> telescope();

base/src/main/java/org/aya/core/pat/PatMatcher.java

@@ -1,8 +1,7 @@
-// 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.core.pat;
 
-import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableHashMap;
 import kala.control.Result;

base/src/main/java/org/aya/core/pat/PatToTerm.java

@@ -1,4 +1,4 @@
-// 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.core.pat;
 
@@ -31,8 +31,7 @@ public Term visit(@NotNull Pat pat) {
 
   protected @NotNull Term visitCtor(Pat.@NotNull Ctor ctor) {
     var data = (DataCall) ctor.type();
-    var args = Arg.mapSeq(ctor.params(), this::visit)
-      .toImmutableSeq();
+    var args = Arg.mapSeq(ctor.params(), this::visit);
     return new ConCall(data.ref(), ctor.ref(),
       data.args().map(Arg::implicitify),
       data.ulift(), args);

base/src/main/java/org/aya/core/term/PartialTerm.java

@@ -1,4 +1,4 @@
-// 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.core.term;
 
@@ -7,7 +7,6 @@
 import kala.collection.mutable.MutableArrayList;
 import org.aya.core.visitor.AyaRestrSimplifier;
 import org.aya.core.visitor.Subst;
-import org.aya.generic.util.NormalizeMode;
 import org.aya.guest0x0.cubical.CofThy;
 import org.aya.guest0x0.cubical.Partial;
 import org.aya.guest0x0.cubical.Partial.Const;

base/src/main/java/org/aya/core/term/Term.java

@@ -1,13 +1,11 @@
-// 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.core.term;
 
 import kala.collection.Map;
-import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableMap;
-import kala.tuple.Tuple;
 import kala.tuple.Tuple3;
 import org.aya.core.UntypedParam;
 import org.aya.core.pat.Pat;

base/src/main/java/org/aya/resolve/error/NameProblem.java

@@ -1,20 +1,20 @@
-// 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.resolve.error;
 
 import kala.collection.Seq;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import org.aya.concrete.stmt.QualifiedID;
-import org.aya.prettier.BasePrettier;
 import org.aya.generic.Constants;
+import org.aya.prettier.BasePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.AnyVar;
 import org.aya.resolve.context.BindContext;
 import org.aya.resolve.context.Context;
 import org.aya.resolve.context.ModuleContext;
-import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.NotNull;
 
@@ -42,7 +42,7 @@ record AmbiguousNameError(
           Doc.code(Doc.plain(name)),
           Doc.english("is ambiguous")),
         Doc.english("Did you mean:"),
-        Doc.nest(2, Doc.vcat(didYouMean().map(n -> Doc.code(n)))));
+        Doc.nest(2, Doc.vcat(didYouMean().map(Doc::code))));
     }
 
     public @NotNull ImmutableSeq<String> didYouMean() {
@@ -185,7 +185,7 @@ record UnqualifiedNameNotFoundError(
       var tail = possible.sizeEquals(1)
         ? Doc.sep(Doc.english("Did you mean:"), Doc.code(possible.first()))
         : Doc.vcat(Doc.english("Did you mean:"),
-          Doc.nest(2, Doc.vcat(possible.view().map(n -> Doc.code(n)))));
+          Doc.nest(2, Doc.vcat(possible.view().map(Doc::code))));
       return Doc.vcat(head, tail);
     }
 

base/src/main/java/org/aya/terck/CallResolver.java

@@ -1,11 +1,10 @@
-// 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.terck;
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableSet;
 import kala.tuple.Tuple;
-import kala.tuple.Tuple2;
 import kala.value.MutableValue;
 import org.aya.core.def.Def;
 import org.aya.core.def.FnDef;

base/src/main/java/org/aya/tyck/Synthesizer.java

@@ -1,4 +1,4 @@
-// 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.tyck;
 
@@ -71,7 +71,7 @@ public record Synthesizer(@NotNull TyckState state, @NotNull LocalCtx ctx) {
       }
       case PiTerm pi -> {
         var paramTyRaw = press(pi.param().type());
-        var t = new Synthesizer(state, ctx.deriveMap());
+        var t = new Synthesizer(state, ctx.deriveSeq());
         yield t.ctx.with(pi.param(), () -> {
           if (paramTyRaw instanceof SortTerm paramTy && t.press(pi.body()) instanceof SortTerm retTy) {
             return PiTerm.max(paramTy, retTy);

base/src/main/java/org/aya/tyck/env/LocalCtx.java

@@ -1,4 +1,4 @@
-// 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.tyck.env;
 
@@ -145,9 +145,17 @@ default boolean isEmpty() {
     return false;
   }
   boolean isMeEmpty();
+  /**
+   * Whether to choose map or seq is completely random in Aya.
+   *
+   * @see #deriveSeq()
+   */
   @Contract(" -> new") default @NotNull MapLocalCtx deriveMap() {
     return new MapLocalCtx(MutableLinkedHashMap.of(), this);
   }
+  /**
+   * @see #deriveMap()
+   */
   @Contract(" -> new") default @NotNull SeqLocalCtx deriveSeq() {
     return new SeqLocalCtx(MutableList.create(), this);
   }

base/src/main/java/org/aya/tyck/error/FieldError.java

@@ -1,4 +1,4 @@
-// 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.tyck.error;
 
@@ -7,8 +7,8 @@
 import org.aya.prettier.BasePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.AnyVar;
-import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface FieldError extends TyckError {
@@ -19,7 +19,7 @@ record MissingField(
     @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.sep(Doc.english("Missing field(s):"), Doc.commaList(missing.view()
         .map(BasePrettier::varDoc)
-        .map(m -> Doc.code(m))));
+        .map(Doc::code)));
     }
   }
   record NoSuchField(

base/src/main/java/org/aya/tyck/order/AyaSccTycker.java

@@ -1,4 +1,4 @@
-// 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.tyck.order;
 
@@ -17,9 +17,8 @@
 import org.aya.core.term.Term;
 import org.aya.generic.util.InterruptException;
 import org.aya.resolve.ResolveInfo;
-import org.aya.util.terck.CallGraph;
-import org.aya.terck.CallResolver;
 import org.aya.terck.BadRecursion;
+import org.aya.terck.CallResolver;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.StmtTycker;
 import org.aya.tyck.error.CounterexampleError;
@@ -29,6 +28,7 @@
 import org.aya.util.reporter.CollectingReporter;
 import org.aya.util.reporter.CountingReporter;
 import org.aya.util.reporter.Reporter;
+import org.aya.util.terck.CallGraph;
 import org.aya.util.terck.MutableGraph;
 import org.aya.util.tyck.SCCTycker;
 import org.jetbrains.annotations.NotNull;

base/src/main/java/org/aya/tyck/pat/ClauseTycker.java

@@ -1,4 +1,4 @@
-// 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.tyck.pat;
 
@@ -10,7 +10,9 @@
 import org.aya.concrete.visitor.PatternConsumer;
 import org.aya.core.def.Def;
 import org.aya.core.pat.Pat;
-import org.aya.core.term.*;
+import org.aya.core.term.ErrorTerm;
+import org.aya.core.term.MetaPatTerm;
+import org.aya.core.term.Term;
 import org.aya.core.visitor.EndoTerm;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.env.LocalCtx;
@@ -140,7 +142,7 @@ public record LhsResult(
 
       match.hasError |= patTycker.hasError();
 
-      var patterns = step0.wellTyped().map(p -> p.descent(x -> x.inline(exprTycker.localCtx))).toImmutableSeq();
+      var patterns = step0.wellTyped().map(p -> p.descent(x -> x.inline(exprTycker.localCtx)));
       // inline after inline patterns
       inlineTypedSubst(patTycker.bodySubst);
       var type = inlineTerm(step0.codomain());

base/src/main/java/org/aya/tyck/pat/PatternTycker.java

@@ -1,4 +1,4 @@
-// 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.tyck.pat;
 
@@ -88,8 +88,7 @@ public PatternTycker(@NotNull ExprTycker exprTycker,
           new ErrorTerm(Doc.plain("Rua"), false));
         yield new Pat.Tuple(
           tyckInner(sig, tuple.patterns().view(), tuple, resultIsProp)
-            .wellTyped()
-            .toImmutableSeq());
+            .wellTyped());
       }
       case Pattern.Ctor ctor -> {
         var var = ctor.resolved().data();
@@ -103,7 +102,7 @@ public PatternTycker(@NotNull ExprTycker exprTycker,
         final var dataCall = realCtor.component1();
         var sig = new Def.Signature<>(Term.Param.subst(ctorCore.selfTele, realCtor.component2(), 0), dataCall);
         // It is possible that `ctor.params()` is empty.
-        var patterns = tyckInner(sig, ctor.params().view(), ctor, resultIsProp).wellTyped.toImmutableSeq();
+        var patterns = tyckInner(sig, ctor.params().view(), ctor, resultIsProp).wellTyped;
         yield new Pat.Ctor(realCtor.component3().ref(), patterns, dataCall);
       }
       case Pattern.Bind(var pos, var bind, var tyExpr, var tyRef) -> {