merge: Improve build, make it possible to write code with lsp (#1045)

.github/README.md

@@ -17,7 +17,7 @@ Aya is under active development, so please expect bugs, usability or performance
 ## What to expect?
 
 + Dependent types, including pi-types, sigma types, indexed families, etc.
-  You could write a [type-safe interpreter][gadt].
+  You could write a [sized-vector type][gadt].
 + Set-level cubical type theory (XTT).
   + Demonstration of [higher-inductive-inductive-recursive types][hiir].
 + Pattern matching with first-match semantics.
@@ -67,17 +67,17 @@ of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
 [codecov]: https://img.shields.io/codecov/c/github/aya-prover/aya-dev?logo=codecov&logoColor=white
 [gitter]: https://img.shields.io/gitter/room/aya-prover/community?color=cyan&logo=gitter
 [maven]: https://img.shields.io/maven-central/v/org.aya-prover/base?logo=gradle
-[oop]: ../base/src/test/resources/success/common/src/Arith/Nat/Core.aya
-[gadt]: ../base/src/test/resources/success/src/TypeSafeNorm.aya
-[regularity]: ../base/src/test/resources/success/common/src/Paths.aya
-[funExt]: ../base/src/test/resources/success/common/src/Paths.aya
-[rbtree]: ../base/src/test/resources/success/common/src/Data/Tree/RedBlack/Direct.aya
-[hiir]: ../base/src/test/resources/success/common/src/TypeTheory/Thorsten.aya
+[oop]: ../cli-impl/src/test/resources/shared/src/Arith/Nat.aya
+[gadt]: ../cli-impl/src/test/resources/shared/src/Data/Vec.aya
+[regularity]: ../cli-impl/src/test/resources/shared/src/Paths.aya
+[funExt]: ../cli-impl/src/test/resources/shared/src/Paths.aya
+[rbtree]: ../cli-impl/src/test/resources/shared/src/Data/Tree/RedBlack/Direct.aya
+[hiir]: ../cli-impl/src/test/resources/shared/src/TypeTheory/Thorsten.aya
 [assoc]: ../base/src/test/resources/success/src/Assoc.aya
 [foetus]: ../base/src/test/resources/success/src/FoetusLimitation.aya
 [mutual]: ../base/src/test/resources/success/src/Order.aya
 [maven-repo]: https://repo1.maven.org/maven2/org/aya-prover
-[stdlib-style]: ../base/src/test/resources/success/common
+[stdlib-style]: ../cli-impl/src/test/resources/shared
 
 ## Use as a library
 

cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java

@@ -76,7 +76,7 @@ def test (a : Type) : Type
     """;
 
   @Language("Aya") String testNoPattern = """
-    open import Paths
+    open import Paths hiding (funExt)
     
     variable A B : Type
     def funExt (f g : A -> B) (p : forall a -> f a = g a) : f = g

cli-impl/src/test/resources/shared/aya.json

@@ -1,5 +1,5 @@
 {
-  "ayaVersion": "0.23",
+  "ayaVersion": "0.31",
   "group": "org.aya-prover",
   "name": "tests",
   "version": "0.1.0",
@@ -20,10 +20,5 @@
         "styleFamily": "Default"
       }
     }
-  },
-
-  "dependency": {
-    "common": { "file": "common" },
-    "nonsense": { "file": "nonsense" }
   }
 }

cli-impl/src/test/resources/shared/src/Arith/Nat.aya

@@ -1,7 +1,24 @@
+open import Paths
+
 open data Nat | zero | suc Nat
 
 overlap def infix + Nat Nat : Nat
 | 0, b => b
 | a, 0 => a
 | suc a, b => suc (a + b)
 | a, suc b => suc (a + b)
+tighter =
+
+overlap def +-comm (a b : Nat) : a + b = b + a
+| 0, _ => refl
+| suc _, _ => pmap suc (+-comm _ _)
+| _, 0 => refl
+| _, suc _ => pmap suc (+-comm _ _)
+
+overlap def +-assoc (a b c : Nat) : a + (b + c) = (a + b) + c
+| 0, _, _ => refl
+| suc _, _, _ => pmap suc (+-assoc _ _ _)
+| _, 0, _ => refl
+| _, suc _, _ => pmap suc (+-assoc _ _ _)
+| _, _, 0 => refl
+| _, _, suc _ => pmap suc (+-assoc _ _ _)

cli-impl/src/test/resources/shared/src/Data/Vec.aya

@@ -3,3 +3,16 @@ open import Arith::Nat
 open data Vec Nat Type
 | 0, A => []
 | suc n, A => infixr :> A (Vec n A)
+
+variable A B : Type
+variable n m o : Nat
+
+def vmap (f : A -> B) (xs : Vec n A) : Vec n B elim xs
+| [] => []
+| x :> xs' => f x :> vmap f xs'
+
+def head (Vec (suc n) A) : A
+| x :> _ => x
+
+def tail (Vec (suc n) A) : Vec n A
+| _ :> xs => xs

cli-impl/src/test/resources/shared/src/Paths.aya

@@ -7,3 +7,26 @@ def infix = (a b : A) : Type => Path (\i => A) a b
 def refl {a : A} : a = a => \i => a
 def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \i => f (p i)
 def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
+
+def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
+
+def hcomp2d
+  {a b c d : A}
+  (p : a = b)
+  (q : b = d)
+  (r : a = c) : c = d
+  => coe 0 1 (\ k => r k = q k) p
+
+def infixr <=> {a b c : A} (p : a = b) (q : b = c) : a = c =>
+  \k => hcomp2d p q refl k
+
+/// Carlo Angiuli's PhD thesis, Section 3.2
+module Angiuli {
+  def transport {a b : A} (B : A -> Type) (p : a = b) (x : B a) : B b
+    => coe 0 1 (\y => B (p y)) x
+}
+public open Angiuli using (transport)
+
+// TODO: make the following work
+// def infixr <=>' {a b c : A} (p : a = b) (q : b = c) : a = c =>
+  // \k => hcomp2d (\i => p i) q refl k

cli-impl/src/test/resources/shared/src/TypeTheory/Thorsten.aya

@@ -0,0 +1,54 @@
+open import Paths
+
+open data Con : Type
+| •
+| infix ▷ (Γ : Con) (Ty Γ)
+
+// The ↑ operator in the paper
+def ext {Γ Δ : Con} (δ : Γ << Δ) (A : Ty Δ) : Γ ▷ Subst A δ << Δ ▷ A =>
+  δ ∘ π₁ (id refl) ∷ transport (Tm _) SubAss (π₂ (id refl))
+
+// Incomplete
+open data Ty (Γ : Con) : Type
+| U
+| Π (A : Ty Γ) (B : Ty (Γ ▷ A))
+| El (A : Tm Γ U)
+| Subst {Δ : Con} (Ty Δ) (s : Γ << Δ)
+| SubId {A : Ty Γ} : Subst A (id refl) = A
+| SubAss {Δ Θ : Con} {A : Ty Θ} {θ : Γ << Δ} {δ : Δ << Θ}
+    : Subst (Subst A δ) θ = Subst A (δ ∘ θ)
+| SubU {Δ : Con} (δ : Γ << Δ) : Subst U δ = U
+| SubEl {Δ : Con} {δ : Γ << Δ} {a : Tm Δ U}
+    : Subst (El a) δ = El (transport (Tm _) (SubU δ) (sub a))
+| SubΠ {Δ : Con} (σ : Γ << Δ) {A : Ty Δ} {B : Ty (Δ ▷ A)}
+    : Subst (Π A B) σ = Π (Subst A σ) (Subst B (ext σ A))
+
+// Tms
+open data infix << (Γ : Con) (Δ : Con) : Type
+   tighter = looser ▷
+| _, • => ε
+| _, Δ ▷ A => infixr ∷ (δ : Γ << Δ) (Tm Γ (Subst A δ)) tighter =
+| infix ∘ {Θ : Con} (Θ << Δ) (Γ << Θ) tighter = ∷
+| π₁ {A : Ty Δ} (Γ << Δ ▷ A)
+| id (Γ = Δ)
+| idl• {s : Γ << Δ} : id refl ∘ s = s
+| idr• {s : Γ << Δ} : s ∘ id refl = s
+| ass {Θ Ξ : Con} {ν : Γ << Ξ} {δ : Ξ << Θ} {σ : Θ << Δ}
+    : (σ ∘ δ) ∘ ν = σ ∘ (δ ∘ ν)
+| π₁β {δ : Γ << Δ} {A : Ty Δ} (t : Tm Γ (Subst A δ)) : π₁ (δ ∷ t) = δ
+| Γ, Δ ▷ A => πη {δ : Γ << Δ ▷ A} : (π₁ δ ∷ π₂ δ) = δ
+| Γ, Δ ▷ A => ∷∘ {Θ : Con} {σ : Θ << Δ} {δ : Γ << Θ} {t : Tm Θ (Subst A σ)}
+    : (σ ∷ t) ∘ δ = (σ ∘ δ) ∷ transport (Tm _) SubAss (sub t)
+| Γ, • => εη {δ : Γ << •} : δ = ε
+
+// Incomplete
+open data Tm (Γ : Con) (A : Ty Γ) : Type
+| _, Π A B => λ (Tm (Γ ▷ A) B)
+| Γ' ▷ A, B => app (Tm Γ' (Π A B))
+| _, Subst A δ => sub (Tm _ A)
+| _, Subst A (π₁ δ) => π₂ (Γ << _ ▷ A)
+| _, Subst B δ => π₂β {Δ : Con} (t : Tm Γ A)
+    : transport (Tm _) (pmap (Subst B) (π₁β t)) (π₂ (δ ∷ t)) = t
+| _ ▷ _, A => Πβ (f : Tm Γ A) : app (λ f) = f
+| _, Π _ _ => Πη (f : Tm Γ A) : λ (app f) = f
+// Subλ is omitted for its overwhleming complexity

ide-lsp/build.gradle.kts

@@ -1,5 +1,6 @@
 // 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.
+import org.apache.tools.ant.taskdefs.condition.Os
 import org.aya.gradle.CommonTasks
 import org.aya.gradle.JdkUrls
 import java.nio.file.Files
@@ -84,7 +85,7 @@ supportedPlatforms.forEach { platform ->
     from(file("src/main/shell")) {
       // https://ss64.com/bash/chmod.html
       filePermissions { unix("755") }
-      if (platform.contains("windows")) {
+      if (platform.contains("windows") || platform == "current" && Os.isFamily(Os.FAMILY_WINDOWS)) {
         include("*.bat")
       } else {
         include("*.sh")
@@ -101,7 +102,7 @@ supportedPlatforms.forEach { platform ->
   }
 
   val copyAyaLibrary = tasks.register<Copy>("copyAyaLibrary_$platform") {
-    from(rootProject.file("base/src/test/resources/success/common"))
+    from(rootProject.file("cli-impl/src/test/resources/shared"))
     into(installDir.resolve("std"))
   }
 

ide-lsp/src/main/java/org/aya/lsp/LspMain.java

@@ -2,8 +2,12 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp;
 
+import org.aya.cli.library.incremental.CompilerAdvisor;
+import org.aya.lsp.server.AyaLanguageClient;
+import org.aya.lsp.server.AyaLanguageServer;
 import org.aya.lsp.utils.Log;
 import org.aya.lsp.utils.LspArgs;
+import org.javacs.lsp.LSP;
 import org.jetbrains.annotations.NotNull;
 import picocli.CommandLine;
 
@@ -28,14 +32,13 @@ public static void main(String[] args) {
       case debug -> runDebug();
     };
 
-    throw new UnsupportedOperationException("TODO");
-    // LSP.connect(
-    //   AyaLanguageClient.class,
-    //   client -> new AyaLanguageServer(CompilerAdvisor.inMemory(), client),
-    //   startup.in,
-    //   startup.out
-    // );
-    // return 0;
+    LSP.connect(
+      AyaLanguageClient.class,
+      client -> new AyaLanguageServer(CompilerAdvisor.inMemory(), client),
+      startup.in,
+      startup.out
+    );
+    return 0;
   }
 
   private static @NotNull Startup runDebug() {