From 815f566077208cbfc508edeb4ca0f0d35b6249b3 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 5 Jan 2025 06:28:15 -0500 Subject: [PATCH 1/6] parser: comma sep `elim`s --- .../org/aya/parser/AyaPsiElementTypes.java | 2 +- .../main/gen/org/aya/parser/AyaPsiParser.java | 21 +++---------------- parser/src/main/grammar/AyaPsiParser.bnf | 4 ++-- .../java/org/aya/producer/AyaProducer.java | 6 ++++-- 4 files changed, 10 insertions(+), 23 deletions(-) diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java index 25c730970..18866abe4 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. diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java index b28c1d23d..30e885269 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,7 +882,7 @@ private static boolean elimDataBody_1(PsiBuilder b, int l) { } /* ********************************************************** */ - // KW_ELIM weakId+ + // KW_ELIM <> static boolean elims(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "elims")) return false; if (!nextTokenIs(b, KW_ELIM)) return false; @@ -890,26 +890,11 @@ static boolean elims(PsiBuilder b, int l) { Marker m = enter_section_(b, l, _NONE_); 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 b40be7b3e..9d50711b5 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 } +private 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 b70ad0f48..fc94bccd6 100644 --- a/producer/src/main/java/org/aya/producer/AyaProducer.java +++ b/producer/src/main/java/org/aya/producer/AyaProducer.java @@ -345,7 +345,8 @@ 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) + var elims = node.child(COMMA_SEP) + .childrenOfType(WEAK_ID) .map(this::weakId) .toImmutableSeq(); return new FnBody.BlockBody(body, elims); @@ -381,7 +382,8 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl } public @NotNull MatchBody elimDataBody(@NotNull GenericNode node) { - var elims = node.childrenOfType(WEAK_ID) + var elims = node.child(COMMA_SEP) + .childrenOfType(WEAK_ID) .map(this::weakId) .toImmutableSeq(); var bodies = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq(); From d8e821a940b4d84fee63abeba2884bbad2aedeb3 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 5 Jan 2025 06:33:16 -0500 Subject: [PATCH 2/6] parser: fix comma sep `elim`s, close #1269 --- base/src/test/java/org/aya/tyck/TyckTest.java | 5 +---- .../gen/org/aya/parser/AyaPsiElementTypes.java | 1 + .../main/gen/org/aya/parser/AyaPsiParser.java | 4 ++-- parser/src/main/grammar/AyaPsiParser.bnf | 2 +- .../main/java/org/aya/producer/AyaProducer.java | 16 +++++++++------- 5 files changed, 14 insertions(+), 14 deletions(-) diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index 84a042630..5a5a90374 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/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java index 18866abe4..53a9265f2 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java @@ -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 30e885269..7cf515595 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java @@ -883,11 +883,11 @@ private static boolean elimDataBody_1(PsiBuilder b, int l) { /* ********************************************************** */ // KW_ELIM <> - static boolean elims(PsiBuilder b, int l) { + 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 && commaSep(b, l + 1, AyaPsiParser::weakId); diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf index 9d50711b5..c70ba53d5 100644 --- a/parser/src/main/grammar/AyaPsiParser.bnf +++ b/parser/src/main/grammar/AyaPsiParser.bnf @@ -205,7 +205,7 @@ private simpleBody ::= IMPLIES expr { pin=1 } fnBody ::= simpleBody | elims? barredClause* -private elims ::= KW_ELIM <> { 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 fc94bccd6..6a3cfa73c 100644 --- a/producer/src/main/java/org/aya/producer/AyaProducer.java +++ b/producer/src/main/java/org/aya/producer/AyaProducer.java @@ -345,10 +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.child(COMMA_SEP) - .childrenOfType(WEAK_ID) - .map(this::weakId) - .toImmutableSeq(); + var elims = elims(node.peekChild(ELIMS)); return new FnBody.BlockBody(body, elims); } @@ -382,12 +379,17 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl } public @NotNull MatchBody elimDataBody(@NotNull GenericNode node) { - var elims = node.child(COMMA_SEP) + 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(); - var bodies = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq(); - return new MatchBody<>(bodies, elims); } public @Nullable DataCon dataBody(@NotNull GenericNode node) { From 8779dd3d881a59377d0d3a67837d9ea0458c6e63 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 5 Jan 2025 06:36:38 -0500 Subject: [PATCH 3/6] test: use comma sep `elim`s --- .../src/test/resources/shared/src/arith/nat/base.aya | 4 ++-- .../resources/shared/src/relation/binary/nat_cmp.aya | 12 ++++++------ cli-impl/src/test/resources/success/src/Pattern.aya | 2 +- cli-impl/src/test/resources/success/src/STLC.aya | 2 +- 4 files changed, 10 insertions(+), 10 deletions(-) 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 7337f65d1..6880d2793 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 2f04d2910..e9619a4fe 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)) @@ -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/Pattern.aya b/cli-impl/src/test/resources/success/src/Pattern.aya index a8fba6abf..5d4c7a986 100644 --- a/cli-impl/src/test/resources/success/src/Pattern.aya +++ b/cli-impl/src/test/resources/success/src/Pattern.aya @@ -51,6 +51,6 @@ 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 + 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 c5fa2cf7c..8f572a4af 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) From 27db965aeccec589ca83956843e4950ce6e71c0b Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 5 Jan 2025 06:41:11 -0500 Subject: [PATCH 4/6] test: suppress warnings --- .../test/resources/shared/src/relation/binary/nat_cmp.aya | 4 ++-- cli-impl/src/test/resources/success/src/PLFA.aya | 1 + cli-impl/src/test/resources/success/src/Pattern.aya | 5 +++-- cli-impl/src/test/resources/success/src/STLC.aya | 2 +- 4 files changed, 7 insertions(+), 5 deletions(-) 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 e9619a4fe..94df5755b 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 @@ -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 diff --git a/cli-impl/src/test/resources/success/src/PLFA.aya b/cli-impl/src/test/resources/success/src/PLFA.aya index e0ec1a73c..f258bc434 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 5d4c7a986..206d42f34 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 + @suppress(Shadowing) 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 8f572a4af..60c3f4456 100644 --- a/cli-impl/src/test/resources/success/src/STLC.aya +++ b/cli-impl/src/test/resources/success/src/STLC.aya @@ -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 From cfce2e29595e74f19b839bfbce53d0c7f9cc813c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 5 Jan 2025 07:21:20 -0500 Subject: [PATCH 5/6] doc: changelog for v0.37, prepare for release --- .../test/resources/success/src/Pattern.aya | 2 +- gradle/libs.versions.toml | 2 +- .../morphism/source/SourceClassBuilder.java | 14 ++-- note/early-changelog.md | 66 +++++++++++++++++++ .../org/aya/syntax/compile/CompiledAya.java | 8 +-- 5 files changed, 80 insertions(+), 12 deletions(-) diff --git a/cli-impl/src/test/resources/success/src/Pattern.aya b/cli-impl/src/test/resources/success/src/Pattern.aya index 206d42f34..35a0beb24 100644 --- a/cli-impl/src/test/resources/success/src/Pattern.aya +++ b/cli-impl/src/test/resources/success/src/Pattern.aya @@ -51,7 +51,7 @@ module PullRequest1268 { // telescope: A a B b C // unpi: D d0 -> d1 - @suppress(Shadowing) + @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/gradle/libs.versions.toml b/gradle/libs.versions.toml index 1eb7a00f9..3a5e3eee6 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.37.0" # https://openjdk.org/ java = "22" 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 4e92d21d8..8bde692de 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 dcdb7e14f..460e4b265 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/syntax/src/main/java/org/aya/syntax/compile/CompiledAya.java b/syntax/src/main/java/org/aya/syntax/compile/CompiledAya.java index f77dd2931..34196b23d 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 { }; } From 6a522b8d33d98968331eb30b5fcf77c593d4b873 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 5 Jan 2025 07:29:29 -0500 Subject: [PATCH 6/6] version: bump to 0.38 --- gradle/libs.versions.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 3a5e3eee6..81ccb9c4d 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" +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" }