diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index 84a0426303..5a5a903744 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/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()); } diff --git a/cli-impl/src/test/resources/shared/src/arith/nat/base.aya b/cli-impl/src/test/resources/shared/src/arith/nat/base.aya index 7337f65d1b..6880d27936 100644 --- a/cli-impl/src/test/resources/shared/src/arith/nat/base.aya +++ b/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 diff --git a/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya b/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya index 2f04d2910f..94df5755b7 100644 --- a/cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya +++ b/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 (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 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 (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 suc-sub p diff --git a/cli-impl/src/test/resources/success/src/PLFA.aya b/cli-impl/src/test/resources/success/src/PLFA.aya index e0ec1a73c9..f258bc4341 100644 --- a/cli-impl/src/test/resources/success/src/PLFA.aya +++ b/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)))) diff --git a/cli-impl/src/test/resources/success/src/Pattern.aya b/cli-impl/src/test/resources/success/src/Pattern.aya index a8fba6abfb..35a0beb245 100644 --- a/cli-impl/src/test/resources/success/src/Pattern.aya +++ b/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 } diff --git a/cli-impl/src/test/resources/success/src/STLC.aya b/cli-impl/src/test/resources/success/src/STLC.aya index c5fa2cf7cd..60c3f44569 100644 --- a/cli-impl/src/test/resources/success/src/STLC.aya +++ b/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 ((<→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 diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 1eb7a00f9a..81ccb9c4de 100644 --- a/gradle/libs.versions.toml +++ b/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" } diff --git a/jit-compiler/src/main/java/org/aya/compiler/free/morphism/source/SourceClassBuilder.java b/jit-compiler/src/main/java/org/aya/compiler/free/morphism/source/SourceClassBuilder.java index 4e92d21d8f..8bde692dee 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/free/morphism/source/SourceClassBuilder.java +++ b/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 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(";"); diff --git a/note/early-changelog.md b/note/early-changelog.md index dcdb7e14ff..460e4b2656 100644 --- a/note/early-changelog.md +++ b/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: diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java index 25c730970b..53a9265f2e 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java +++ b/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"); diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java index b28c1d23d2..7cf5155955 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java +++ b/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 <> + 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; - } - /* ********************************************************** */ // <> static boolean exprList(PsiBuilder b, int l) { diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf index b40be7b3e5..c70ba53d5f 100644 --- a/parser/src/main/grammar/AyaPsiParser.bnf +++ b/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 <> { 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. diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java index b70ad0f484..6a3cfa73c4 100644 --- a/producer/src/main/java/org/aya/producer/AyaProducer.java +++ b/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 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> 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( diff --git a/syntax/src/main/java/org/aya/syntax/compile/CompiledAya.java b/syntax/src/main/java/org/aya/syntax/compile/CompiledAya.java index f77dd29319..34196b23d3 100644 --- a/syntax/src/main/java/org/aya/syntax/compile/CompiledAya.java +++ b/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 { }; }