merge: Release v0.37 (#1279)

Also fix #1269

base/src/test/java/org/aya/tyck/TyckTest.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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;
 
@@ -88,9 +88,6 @@ prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
       | zro : pos 0 = neg 0
       example def testZro0 : zro 0 = pos 0 => refl
       example def testZro1 : zro 1 = neg 0 => refl
-      def funExt (A B : Type) (f g : A -> B) (p : Fn (a : A) -> f a = g a) : f = g =>
-        \\ i => \\ a => p a i
-      def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\\i => p i = a) refl
       """).defs;
     assertTrue(result.isNotEmpty());
   }

cli-impl/src/test/resources/shared/src/arith/nat/base.aya

@@ -17,13 +17,13 @@ overlap def subTrunc (x y : Nat) : Nat
 | n, 0 => n
 | suc n, suc m => subTrunc n m
 
-overlap def +-comm : a + b = b + a elim a b
+overlap def +-comm : a + b = b + a elim a, b
 | 0, _ => refl
 | suc _, _ => pmap suc +-comm
 | _, 0 => refl
 | _, suc _ => pmap suc +-comm
 
-overlap def +-assoc : a + (b + c) = (a + b) + c elim a b c
+overlap def +-assoc : a + (b + c) = (a + b) + c elim a, b, c
 | 0, _, _ => refl
 | _, 0, _ => refl
 | _, _, 0 => refl

cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya

@@ -23,7 +23,7 @@ def n<=n (n : Nat) : n <= n
 | 0 => refl
 | suc n => n<=n n
 
-def n<=s {a b : Nat} (p : a <= b) : a <= suc b elim a b
+def n<=s {a b : Nat} (p : a <= b) : a <= suc b elim a, b
 | zero, _ => refl
 | suc a, zero => exfalso (sn<=z p)
 | suc a, suc b => n<=s p
@@ -35,13 +35,13 @@ def infix <? (a b : Nat) : Decidable (a < b) => (suc a) <=? b
 def n<=z {n : Nat} (p : n <= 0) : n = 0 => p
 def sn<=z {n : Nat} (p : suc n <= 0) : ⊥ => z≠s (pinv (n<=z p))
 
-def <=-trans {a b c : Nat} (p : a <= b) (q : b <= c) : a <= c elim a b c
+def <=-trans {a b c : Nat} (p : a <= b) (q : b <= c) : a <= c elim a, b, c
 | zero, _, _ => refl
 | suc a, zero, _ => exfalso (sn<=z p)
 | suc a, suc b, zero => exfalso (sn<=z q)
 | suc a, suc b, suc c => <=-trans (s<=s p) (s<=s q)
 
-private def some-lemma {a b : Nat} (p : subTrunc a b = 0) (np : neg (subTrunc (suc a) b = 0)) : a = b elim a b
+private def some-lemma {a b : Nat} (p : subTrunc a b = 0) (np : neg (subTrunc (suc a) b = 0)) : a = b elim a, b
 | 0, 0 => refl
 | 0, suc b => exfalso (np p)
 | suc a, 0 => exfalso (z≠s (pinv p))
@@ -50,8 +50,8 @@ private def some-lemma {a b : Nat} (p : subTrunc a b = 0) (np : neg (subTrunc (s
 
 def <=-case {a b : Nat} (p : a <= b) : Sum (a < b) (a = b) =>
   match a <? b {
-  | _ because reflect_true p => inl p
-  | _ because reflect_false np => inr (some-lemma p np)
+  | _ because reflect_true q => inl q
+  | _ because reflect_false nq => inr (some-lemma p nq)
   }
 
 def ¬<→>= {a b : Nat} (np : neg (a < b)) : a >= b
@@ -64,16 +64,16 @@ def <=-with-≠ {a b : Nat} (p : a <= b) (q : neg (a = b)) : a < b => match <=-c
 | inr eq => exfalso (q eq)
 }
 
-def <→s {a b : Nat} (p : a < b) : Sig (n : Nat) ** b = suc n elim a b
+def <→s {a b : Nat} (p : a < b) : Sig (n : Nat) ** b = suc n elim a, b
 | _, 0 => exfalso (n<z→⊥ p)
 | _, suc b => (b, refl)
 
-def a-b+b=a {a b : Nat} (p : b <= a) : subTrunc a b + b = a elim a b
+def a-b+b=a {a b : Nat} (p : b <= a) : subTrunc a b + b = a elim a, b
 | 0, _ => n<=z p
 | suc a', 0 => refl
 | suc a', suc b' => pmap suc (a-b+b=a (s<=s p))
 
-def suc-sub {a b : Nat} (p : b < (suc a)) : subTrunc (suc a) b = suc (subTrunc a b) elim a b
+def suc-sub {a b : Nat} (p : b < (suc a)) : subTrunc (suc a) b = suc (subTrunc a b) elim a, b
 | _, zero => refl
 | zero, suc b => exfalso (n<z→⊥ (s<s {b} {0} p))
 | suc a, suc b => suc-sub p

cli-impl/src/test/resources/success/src/PLFA.aya

@@ -43,6 +43,7 @@ def peirce-law=>double-neg-elim (pl : peirce-law) : double-neg-elim =>
   fn tyA ¬¬A =>
     pl tyA Empty (fn ¬A => exfalso (¬¬A ¬A))
 
+@suppress(MostGeneralSolution)
 def double-neg-elim=>LEM (dne : double-neg-elim) : LEM =>
   fn tyA => dne _ (fn ¬A+nA =>
     ¬A+nA (inr (fn A => ¬A+nA (inl A))))

cli-impl/src/test/resources/success/src/Pattern.aya

@@ -6,9 +6,9 @@ module Test1 {
   def unwrap (A : Type) (v : Vec 1 A) : A elim v
   | x :> [] => x
 
-  def length (A : Type) (n : Nat) (v : Vec n A) : Nat elim v
+  def vec-length (A : Type) (n : Nat) (v : Vec n A) : Nat elim v
   | [] => 0
-  | _ :> xs => suc (length _ _ xs)
+  | _ :> xs => suc (vec-length _ _ xs)
 
   def threeTimesAhThreeTimes (A : Type) (a : A) : Vec 3 A =>
     a :> a :> a :> []
@@ -51,6 +51,7 @@ module PullRequest1268 {
 
   // telescope: A a B b C
   // unpi: D d0 -> d1
-  def elims {A : Type} (a : A) (B : Type) (b : B) {C : Type} : Fn (D : Type) D -> D elim a b
+  @suppress(LocalShadow)
+  def elims {A : Type} (a : A) (B : Type) (b : B) {C : Type} : Fn (D : Type) D -> D elim a, b
   | a => fn b D => id D
 }

cli-impl/src/test/resources/success/src/STLC.aya

@@ -46,7 +46,7 @@ open inductive not_refer_to (tm : Tm) (i : Nat)
 | False, _ => False_nrt
 
 // shift all index since [gap] back, this operation requires term [tm] has no reference to [gap].
-def shiftBack (t : Tm) (gap : Nat) (nrt : not_refer_to t gap) : Tm elim t nrt
+def shiftBack (t : Tm) (gap : Nat) (nrt : not_refer_to t gap) : Tm elim t, nrt
 | Lam l, Lam_nrt p => Lam (shiftBack l (suc gap) p)
 | App f a, App_nrt pf pa => App (shiftBack f gap pf) (shiftBack a gap pa)
 | Idx idx, Var_nrt plt => ifd (gap <? idx) (fn p => Idx ((<→s p).1)) (fn np => t)
@@ -146,7 +146,7 @@ def inst_preservation
   | _ because reflect_true p =>
     let
     | A=B : A = B := just-inj (pinv eqV <=> (transport (fn j => G !! j = just B) p eqG))
-    in coe 0 1 (fn i => hasType G v (pinv A=B i)) vhT
+    in coe 0 1 (fn j => hasType G v (pinv A=B j)) vhT
   | _ because reflect_false np => Var_hasType eqV
   }
 | True_hasType, _, _, _ => True_hasType

gradle/libs.versions.toml

@@ -2,7 +2,7 @@
 # The Version of this project, aka, The Aya Theorem Prover.
 # Remove "-SNAPSHOT" suffix and run gradle publish to release a new version.
 # After that, increase the version number and add "-SNAPSHOT" suffix back for next cycle.
-project = "0.37.0-SNAPSHOT"
+project = "0.38.0-SNAPSHOT"
 
 # https://openjdk.org/
 java = "22"
@@ -26,7 +26,7 @@ jlink = "3.1.1"
 # https://github.com/jacoco/jacoco
 jacoco = "0.8.12"
 # https://github.com/manifold-systems/manifold/tree/master/manifold-deps-parent/manifold-delegation
-manifold = "2024.1.42"
+manifold = "2024.1.43"
 
 [plugins]
 jlink = { id = "org.beryx.jlink", version.ref = "jlink" }

jit-compiler/src/main/java/org/aya/compiler/free/morphism/source/SourceClassBuilder.java

@@ -1,12 +1,12 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.compiler.free.morphism.source;
 
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.compiler.SourceBuilder;
 import org.aya.compiler.free.*;
-import org.aya.compiler.free.data.MethodRef;
 import org.aya.compiler.free.data.FieldRef;
+import org.aya.compiler.free.data.MethodRef;
 import org.aya.compiler.serializers.ExprializeUtil;
 import org.aya.syntax.compile.CompiledAya;
 import org.aya.syntax.core.repr.CodeShape;
@@ -37,9 +37,11 @@ public void buildMetadata(@NotNull CompiledAya compiledAya) {
       ), true);
       buildMetadataRecord("fileModuleSize", Integer.toString(compiledAya.fileModuleSize()), false);
       buildMetadataRecord("name", ExprializeUtil.makeString(compiledAya.name()), false);
-      buildMetadataRecord("assoc", Integer.toString(compiledAya.assoc()), false);
-      buildMetadataRecord("shape", Integer.toString(compiledAya.shape()), false);
-      buildMetadataRecord("recognition", SourceCodeBuilder.mkHalfArray(
+      if (compiledAya.assoc() != -1)
+        buildMetadataRecord("assoc", Integer.toString(compiledAya.assoc()), false);
+      if (compiledAya.shape() != -1)
+        buildMetadataRecord("shape", Integer.toString(compiledAya.shape()), false);
+      if (compiledAya.recognition().length != 0) buildMetadataRecord("recognition", SourceCodeBuilder.mkHalfArray(
         ImmutableSeq.from(compiledAya.recognition()).map(x ->
           SourceCodeBuilder.makeRefEnum(FreeUtil.fromClass(CodeShape.GlobalId.class), x.name())
         )
@@ -104,7 +106,7 @@ private void buildMethod(
     @NotNull Function<FreeExprBuilder, FreeJavaExpr> initializer
   ) {
     sourceBuilder.append("public static final " + toClassRef(returnType) + " " + name + " = ");
-    var codeBuilder = new SourceCodeBuilder(this, sourceBuilder); 
+    var codeBuilder = new SourceCodeBuilder(this, sourceBuilder);
     var initValue = initializer.apply(codeBuilder);
     codeBuilder.appendExpr(initValue);
     sourceBuilder.append(";");

note/early-changelog.md

@@ -1,5 +1,71 @@
 # Early changelog
 
+## v0.37
+
+Breaking changes:
+
+- The multi-variable version of `elim` now needs comma-separated names,
+  like `elim a b c` needs to be `elim a, b, c`.
+
+The JIT compiler now _optimizes_ the generated code, by first generating a Java AST,
+optimizes it, and then translate this Java AST into Java source.
+There are the following optimizations:
+
+1. For empty `telescope` and trivial `isAvailable`, they are no longer generated, and the default
+   implementation of these methods will be used. This should only make the code (much) smaller,
+   and generally more hot-code JIT friendly.
+2. `CompiledAya` metadata now has default values, and the code generator will use them.
+3. For `break` statements at the end of `do while` blocks, they are removed. This should make the
+   code faster, but turns out javac already optimizes this, so it only makes the code smaller.
+   But this is helpful for our own bytecode generator in the future.
+4. For `switch` statements with a `Panic.unreachable` default case, it merges with the last case,
+   because the unreachable-ness is guaranteed and very unlikely there's a bug that reaches it.
+   This should both make the code smaller and faster.
+5. After 3, `switch` with only one case is inlined, and `switch` with only two cases is turned into
+   an `if` statement. This should make the code much smaller, but not faster.
+
+In June, the compiled bytecode of the stdlib is 1.12MB, and after all these and some added definitions
+during this time, it's even smaller at 806KB. This is amazing.
+
+Other major new features:
+
+- Identifiers can begin with `-` now. This means `-` (minus) and `-->` (long arrow)
+  are now valid identifiers.
+- No-arg constructor pattern matching, when the constructor is out-of-scope,
+  will be understood as variable patterns. This is even more harmful in constructor patterns.
+  There will be a warning for this now.
+- SIT supports `elim`.
+
+Minor new features:
+
+- The library now has more stuff: `maybe`, more list functions, etc.
+- You can now use `--datetime-front-matter` and `--datetime-front-matter-key` to insert date time
+  info in the front matter of markdown output. If there is no front matter, Aya will make one,
+  and if there is, Aya will insert into it.
+- Patterns shadowing telescope will no longer trigger warnings.
+- The pattern type checker now handles more cases, see `Pattern.aya` in
+  `cli-impl/src/test/resources/success/src`.
+- The highlighter now handles `import` and `open` statements more robustly and smartly.
+  For `import a::b::c`, the `a::b` part will be considered a reference, and `c` is considered a definition,
+  because it introduces a module that can be used locally. If you do `import a::b::c as d` instead,
+  then the entire `a::b::c` part will be considered a reference, and `d` is considered a definition.
+
+Bugs fixed:
+
+- `JitCon.selfTele` was wrong.
+- `match` type checking.
+- `EqTerm` type checking now correctly handles `ErrorTerm`.
+- Subtyping from path to pi is now correctly implemented.
+- If con patterns have an error, Aya will no longer raise NPE.
+- Using implicit pattern with `elim` will no longer crash (but report error instead).
+
+Internal changes:
+
+- Use Markdown doc comments in a few places. Now `gradle javadoc` should no longer throw those warnings.
+- Move some code from `pretty` to `tools`. Now code coverage test will check `tools` too, and some unused classes are removed now.
+- `registerLibrary` returns registered libraries. This is so the IDE can watch file changes correctly, and changing non-project files will not cause a reload.
+- Negative tests are now checked using `git diff` rather than `assertEquals`. This generates much more readable error message.
+
 ## v0.36
 
 Major new features:

parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 
 // This is a generated file. Not intended for manual editing.
@@ -41,6 +41,7 @@ public interface AyaPsiElementTypes {
   IElementType DO_BINDING = new AyaPsiElementType("DO_BINDING");
   IElementType DO_BLOCK_CONTENT = new AyaPsiElementType("DO_BLOCK_CONTENT");
   IElementType DO_EXPR = new AyaPsiElementType("DO_EXPR");
+  IElementType ELIMS = new AyaPsiElementType("ELIMS");
   IElementType ELIM_DATA_BODY = new AyaPsiElementType("ELIM_DATA_BODY");
   IElementType EXPR = new AyaPsiElementType("EXPR");
   IElementType FN_BODY = new AyaPsiElementType("FN_BODY");

parser/src/main/gen/org/aya/parser/AyaPsiParser.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 
 // This is a generated file. Not intended for manual editing.
@@ -882,34 +882,19 @@ private static boolean elimDataBody_1(PsiBuilder b, int l) {
   }
 
   /* ********************************************************** */
-  // KW_ELIM weakId+
-  static boolean elims(PsiBuilder b, int l) {
+  // KW_ELIM <<commaSep weakId>>
+  public static boolean elims(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "elims")) return false;
     if (!nextTokenIs(b, KW_ELIM)) return false;
     boolean r, p;
-    Marker m = enter_section_(b, l, _NONE_);
+    Marker m = enter_section_(b, l, _NONE_, ELIMS, null);
     r = consumeToken(b, KW_ELIM);
     p = r; // pin = 1
-    r = r && elims_1(b, l + 1);
+    r = r && commaSep(b, l + 1, AyaPsiParser::weakId);
     exit_section_(b, l, m, r, p, null);
     return r || p;
   }
 
-  // weakId+
-  private static boolean elims_1(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "elims_1")) return false;
-    boolean r;
-    Marker m = enter_section_(b);
-    r = weakId(b, l + 1);
-    while (r) {
-      int c = current_position_(b);
-      if (!weakId(b, l + 1)) break;
-      if (!empty_element_parsed_guard_(b, "elims_1", c)) break;
-    }
-    exit_section_(b, m, null, r);
-    return r;
-  }
-
   /* ********************************************************** */
   // <<commaSep expr>>
   static boolean exprList(PsiBuilder b, int l) {

parser/src/main/grammar/AyaPsiParser.bnf

@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+ * Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
  * Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
  */
 
@@ -205,7 +205,7 @@ private simpleBody ::= IMPLIES expr { pin=1 }
 fnBody ::= simpleBody
          | elims? barredClause*
 
-private elims ::= KW_ELIM weakId+ { pin=1 }
+elims ::= KW_ELIM <<commaSep weakId>> { pin=1 }
 
 // primName should not be mixed-in with NamedWeakId -- the primDecl already is a named element.
 // This rule is used for convenience in semantic highlight.

producer/src/main/java/org/aya/producer/AyaProducer.java

@@ -345,9 +345,7 @@ private void pragma(GenericNode<?> node, Decl decl) {
     if (expr != null) return new FnBody.ExprBody(expr(expr));
     var body = node.childrenOfType(BARRED_CLAUSE)
       .map(this::bareOrBarredClause).toImmutableSeq();
-    var elims = node.childrenOfType(WEAK_ID)
-      .map(this::weakId)
-      .toImmutableSeq();
+    var elims = elims(node.peekChild(ELIMS));
     return new FnBody.BlockBody(body, elims);
   }
 
@@ -381,13 +379,19 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl
   }
 
   public @NotNull MatchBody<DataCon> elimDataBody(@NotNull GenericNode<?> node) {
-    var elims = node.childrenOfType(WEAK_ID)
-      .map(this::weakId)
-      .toImmutableSeq();
+    var elims = elims(node.peekChild(ELIMS));
     var bodies = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq();
     return new MatchBody<>(bodies, elims);
   }
 
+  private @NotNull ImmutableSeq<WithPos<String>> elims(@Nullable GenericNode<?> node) {
+    if (node == null) return ImmutableSeq.empty();
+    return node.child(COMMA_SEP)
+      .childrenOfType(WEAK_ID)
+      .map(this::weakId)
+      .toImmutableSeq();
+  }
+
   public @Nullable DataCon dataBody(@NotNull GenericNode<?> node) {
     var dataConClause = node.peekChild(DATA_CON_CLAUSE);
     if (dataConClause != null) return dataCon(

syntax/src/main/java/org/aya/syntax/compile/CompiledAya.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.compile;
 
@@ -14,8 +14,8 @@
   int fileModuleSize();
   @NotNull String name();
   /** @return the index in the Assoc enum, -1 if null */
-  int assoc();
+  int assoc() default -1;
   /** @return the index in the AyaShape enum, -1 if null */
-  int shape();
-  @NotNull CodeShape.GlobalId[] recognition();
+  int shape() default -1;
+  @NotNull CodeShape.GlobalId[] recognition() default { };
 }