merge: Properly initialize DiskLibraryOwner (#1262)

It should have `srcPath` in `modulePath`

cli-impl/src/main/java/org/aya/cli/library/source/DiskLibraryOwner.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 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.cli.library.source;
 
@@ -22,9 +22,9 @@
  */
 public record DiskLibraryOwner(
   @NotNull SourceFileLocator locator,
-  @NotNull MutableList<Path> modulePathMut,
-  @NotNull MutableList<LibraryOwner> libraryDepsMut,
-  @NotNull MutableList<LibrarySource> librarySourcesMut,
+  @Override @NotNull MutableList<Path> modulePathMut,
+  @Override @NotNull MutableList<LibraryOwner> libraryDepsMut,
+  @Override @NotNull MutableList<LibrarySource> librarySourcesMut,
   @NotNull LibraryConfig underlyingLibrary
 ) implements MutableLibraryOwner {
   private static @Nullable LibraryConfig depConfig(@NotNull LibraryConfig config, @NotNull LibraryDependency dep) throws IOException {
@@ -45,7 +45,7 @@ public record DiskLibraryOwner(
   public static @NotNull DiskLibraryOwner from(@NotNull LibraryConfig config) throws IOException {
     var srcRoot = config.librarySrcRoot();
     var locator = new SourceFileLocator.Module(SeqView.of(srcRoot));
-    var owner = new DiskLibraryOwner(locator, MutableList.create(),
+    var owner = new DiskLibraryOwner(locator, MutableList.of(srcRoot),
       MutableList.create(), MutableList.create(), config);
     owner.librarySourcesMut.appendAll(AyaFiles.collectAyaSourceFiles(srcRoot)
       .map(p -> LibrarySource.create(owner, p)));

cli-impl/src/test/resources/shared/src/data/list/properties.aya

@@ -116,7 +116,7 @@ def insert<=length
         (fn a => a + length (take i xs) = length xs) (pinv (drop<=length _ _))
         (transport
           (fn a => (subTrunc (length xs) i + a = length xs)) (pinv (take<=length _ _ p))
-          (a-b+b=a _ _ p))
+          (a-b+b=a p))
     | BanGDream : length (take i xs) + length (drop i xs) = length xs := transport (fn lhs => lhs = length xs) +-comm myGoal!
     | haruhikage : suc (length (take i xs) + length (drop i xs)) = suc (length xs) := pmap suc BanGDream
     | nande : length (take i xs ++ (x :< drop i xs)) = suc (length (take i xs) + length (drop i xs)) := length-++ _ _

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

@@ -41,22 +41,24 @@ def <=-trans {a b c : Nat} (p : a <= b) (q : b <= c) : a <= c elim a b c
 | 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
-| 0, 0, _, _ => refl
-| 0, suc b, _, _ => exfalso (np p)
-| suc a, 0, p, _ => exfalso (z≠s (pinv p))
-| suc a, suc b, _, _ => pmap suc (some-lemma a b p np)
+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))
+| suc a, suc b => pmap suc (some-lemma p np)
 
+@suppress(Shadowing)
 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_false np => inr (some-lemma p np)
   }
 
+@suppress(Shadowing)
 def ¬<→>= {a b : Nat} (np : neg (a < b)) : a >= b
 | {_}, {0}, np => refl
 | {0}, {suc b}, np => exfalso (np refl)
-| {suc a}, {suc b}, np => s<=s (¬<→>= {a} {b} (fn p => np p))
+| {suc a}, {suc b}, np => s<=s (¬<→>= np)
 
 def <=-with-≠ {a b : Nat} (p : a <= b) (q : neg (a = b)) : a < b => match <=-case p {
 | inl proof => proof
@@ -67,10 +69,10 @@ 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
-| 0, _, _ => n<=z p
-| suc a', 0, _ => refl
-| suc a', suc b', _ => pmap suc (a-b+b=a a' b' (s<=s p))
+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
 | _, zero => refl

cli-impl/src/test/resources/shared/src/relation/nullary/decidable.aya

@@ -14,8 +14,8 @@ def yes {P : Type} (p : P) : Decidable P => true because (reflect_true p)
 def no {P : Type} (np : neg P) : Decidable P => false because (reflect_false np)
 
 def map {P Q : Type} (f : P -> Q) (g : Q -> P) (d : Decidable P) : Decidable Q elim d
-| true because (reflect_true p) => yes (f p)
-| false because (reflect_false np) => no (fn q => np (g q))
+| _ because (reflect_true p) => yes (f p)
+| _ because (reflect_false np) => no (fn q => np (g q))
 
 def if-then-else {A P : Type} (d : Decidable P) (then else : A) : A elim d
 | true because _ => then

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

@@ -73,7 +73,7 @@ public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar ref, @NotNull WithP
 
   /// @param filling  the inner expr of goal
   /// @param explicit whether the hole is a type-directed programming goal or
-  ///                                                 a to-be-solved by tycking hole.
+  ///                 a to-be-solved by tycking hole.
   record Hole(
     boolean explicit,
     @Nullable WithPos<Expr> filling,
@@ -422,7 +422,7 @@ public void forEach(@NotNull Consumer<Expr> f) {
     /// @param generator `x * y` part above
     /// @param binds     `x <- [1, 2, 3], y <- [4, 5, 6]` part above
     /// @param names     the bind (`>>=`) function, it is [#monadBind] in default,
-    ///                                                                     the pure (`return`) function, it is [#functorPure] in default
+    ///                  the pure (`return`) function, it is [#functorPure] in default
     /// @apiNote a ArrayCompBlock will be desugar to a do-block. For the example above,
     /// it will be desugared to `do x <- [1, 2, 3], y <- [4, 5, 6], return x * y`
     public record CompBlock(
@@ -570,9 +570,11 @@ record Match(
         returns != null ? returns.descent(f) : null);
     }
 
+    /// Patterns will be visited externally, so we don't need to visit them here.
+    ///
+    /// @see StmtVisitor#visitExpr
     @Override public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
       discriminant.forEach(f::accept);
-      // TODO: what about the patterns
       clauses.forEach(clause -> clause.forEach(f, (_, _) -> { }));
       if (returns != null) f.accept(returns);
     }