refactor: move files

Co-authored-by: HoshinoTented <hoshinotented@qq.com>

base/build.gradle.kts

@@ -1,24 +1,16 @@
-// 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.
 import org.aya.gradle.GenerateVersionTask
 
-//CommonTasks.nativeImageConfig(project)
-
 dependencies {
-  api(project(":tools-kala"))
+  api(project(":syntax"))
   api(project(":tools-md"))
-  api(project(":pretty"))
   implementation(libs.aya.commonmark)
-  implementation(libs.aya.ij.core)
   testImplementation(libs.junit.params)
   testImplementation(libs.junit.jupiter)
   testImplementation(libs.hamcrest)
 }
 
-plugins {
-  id("org.graalvm.buildtools.native")
-}
-
 val genDir = file("src/main/gen")
 val generateVersion = tasks.register<GenerateVersionTask>("generateVersion") {
   basePackage = "org.aya"

base/src/main/java/module-info.java

@@ -1,27 +1,13 @@
 module aya.base {
   requires transitive aya.md;
-  requires transitive aya.pretty;
-  requires transitive aya.util;
-  requires transitive aya.util.more;
-  requires transitive kala.base;
-  requires transitive kala.collection;
+  requires transitive aya.syntax;
 
   requires static org.jetbrains.annotations;
 
-  requires aya.ij.parsing.core;
   requires org.commonmark;
 
-  exports org.aya.generic;
   exports org.aya.prelude;
   exports org.aya.resolve.context;
-  exports org.aya.syntax.concrete.stmt.decl;
-  exports org.aya.syntax.concrete.stmt;
-  exports org.aya.syntax.concrete;
-  exports org.aya.syntax.core.def;
-  exports org.aya.syntax.core.pat;
-  exports org.aya.syntax.core.term.call;
-  exports org.aya.syntax.core.term;
-  exports org.aya.syntax.ref;
   exports org.aya.tyck.tycker;
   exports org.aya.tyck;
 }

base/src/main/java/org/aya/tyck/TyckState.java

@@ -2,10 +2,13 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
+import kala.collection.mutable.MutableList;
+import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.LocalCtx;
 import org.jetbrains.annotations.NotNull;
 
 public record TyckState(
-  @NotNull LocalCtx ctx
-) {
+  @NotNull LocalCtx ctx,
+  @NotNull MutableList<Term> dCtx
+  ) {
 }

settings.gradle.kts

@@ -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.
 
 rootProject.name = "aya-prover"
@@ -15,6 +15,7 @@ include(
   "tools-kala",
   "tools-md",
   "tools-repl",
+  "syntax",
   "base",
   "pretty",
   "parser",

syntax/build.gradle.kts

@@ -0,0 +1,17 @@
+// 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.
+
+//CommonTasks.nativeImageConfig(project)
+
+dependencies {
+  api(project(":tools-kala"))
+  api(project(":pretty"))
+  api(libs.aya.ij.core)
+  testImplementation(libs.junit.params)
+  testImplementation(libs.junit.jupiter)
+  testImplementation(libs.hamcrest)
+}
+
+plugins {
+  id("org.graalvm.buildtools.native")
+}

syntax/src/main/java/module-info.java

@@ -0,0 +1,20 @@
+module aya.syntax {
+  requires transitive aya.pretty;
+  requires transitive aya.util;
+  requires transitive aya.util.more;
+  requires transitive kala.base;
+  requires transitive kala.collection;
+  requires transitive aya.ij.parsing.core;
+
+  requires static org.jetbrains.annotations;
+
+  exports org.aya.generic;
+  exports org.aya.syntax.concrete.stmt.decl;
+  exports org.aya.syntax.concrete.stmt;
+  exports org.aya.syntax.concrete;
+  exports org.aya.syntax.core.def;
+  exports org.aya.syntax.core.pat;
+  exports org.aya.syntax.core.term.call;
+  exports org.aya.syntax.core.term;
+  exports org.aya.syntax.ref;
+}

base/src/main/java/org/aya/generic/Modifier.java → syntax/src/main/java/org/aya/generic/Modifier.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.generic;
 

base/src/main/java/org/aya/generic/SortKind.java → syntax/src/main/java/org/aya/generic/SortKind.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.generic;
 

base/src/main/java/org/aya/resolve/context/ModuleName.java → syntax/src/main/java/org/aya/syntax/concrete/stmt/ModuleName.java

@@ -1,9 +1,8 @@
-// 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.resolve.context;
+package org.aya.syntax.concrete.stmt;
 
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.syntax.concrete.stmt.QualifiedID;
 import org.aya.util.error.InternalException;
 import org.jetbrains.annotations.NotNull;
 

base/src/main/java/org/aya/syntax/concrete/stmt/QualifiedID.java → syntax/src/main/java/org/aya/syntax/concrete/stmt/QualifiedID.java

@@ -5,7 +5,6 @@
 import kala.collection.Seq;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.generic.Constants;
-import org.aya.resolve.context.ModuleName;
 import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;

base/src/main/java/org/aya/syntax/concrete/stmt/decl/Decl.java → syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/Decl.java

@@ -2,14 +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.syntax.concrete.stmt.decl;
 
-import org.aya.resolve.context.Context;
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.ref.DefVar;
 import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 /**
  * TODO: update document
@@ -57,7 +55,5 @@ public sealed interface Decl extends SourceNode, Stmt permits TeleDecl {
    */
   sealed interface TopLevel permits TeleDecl.TopLevel {
     @NotNull DeclInfo.Personality personality();
-    @Nullable Context getCtx();
-    void setCtx(@NotNull Context ctx);
   }
 }

base/src/main/java/org/aya/syntax/concrete/stmt/decl/TeleDecl.java → syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/TeleDecl.java

@@ -5,17 +5,16 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import org.aya.generic.Modifier;
-import org.aya.resolve.context.Context;
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.core.Signature;
 import org.aya.syntax.core.def.CtorDef;
 import org.aya.syntax.core.def.DataDef;
 import org.aya.syntax.core.def.FnDef;
 import org.aya.syntax.core.def.TeleDef;
-import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.core.term.SortTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.ref.DefVar;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
@@ -60,7 +59,6 @@ public void modifyTelescope(@NotNull UnaryOperator<ImmutableSeq<Expr.Param>> f)
 
   public sealed abstract static class TopLevel<RetTy extends Term> extends TeleDecl<RetTy> implements Decl.TopLevel {
     private final @NotNull DeclInfo.Personality personality;
-    public @Nullable Context ctx = null;
 
     protected TopLevel(
       @NotNull DeclInfo info, @NotNull ImmutableSeq<Expr.Param> telescope,
@@ -73,14 +71,6 @@ protected TopLevel(
     @Override public @NotNull DeclInfo.Personality personality() {
       return personality;
     }
-
-    @Override public @Nullable Context getCtx() {
-      return ctx;
-    }
-
-    @Override public void setCtx(@NotNull Context ctx) {
-      this.ctx = ctx;
-    }
   }
 
   /**

base/src/main/java/org/aya/syntax/core/def/Def.java → syntax/src/main/java/org/aya/syntax/core/def/Def.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.syntax.core.def;
 

base/src/main/java/org/aya/syntax/core/def/TeleDef.java → syntax/src/main/java/org/aya/syntax/core/def/TeleDef.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.syntax.core.def;
 

base/src/main/java/org/aya/syntax/core/def/UserDef.java → syntax/src/main/java/org/aya/syntax/core/def/UserDef.java

@@ -5,7 +5,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
-import org.aya.tyck.ExprTycker;
 import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -19,8 +18,6 @@ public sealed abstract class UserDef<Ret extends Term>
   extends TopLevelDef<Ret> permits FnDef, DataDef {
   /**
    * In case of counterexamples, this field will be assigned.
-   *
-   * @see org.aya.tyck.StmtTycker#tyck(Decl, ExprTycker)
    */
   public @Nullable ImmutableSeq<Problem> problems;
 

base/src/main/java/org/aya/syntax/core/term/AppTerm.java → syntax/src/main/java/org/aya/syntax/core/term/AppTerm.java

@@ -1,3 +1,5 @@
+// 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.syntax.core.term;
 
 import kala.function.IndexedFunction;

base/src/main/java/org/aya/syntax/core/term/Formation.java → syntax/src/main/java/org/aya/syntax/core/term/Formation.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.syntax.core.term;
 

base/src/main/java/org/aya/syntax/core/term/LamTerm.java → syntax/src/main/java/org/aya/syntax/core/term/LamTerm.java

@@ -1,3 +1,5 @@
+// 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.syntax.core.term;
 
 import kala.collection.SeqLike;

base/src/main/java/org/aya/syntax/core/term/SortTerm.java → syntax/src/main/java/org/aya/syntax/core/term/SortTerm.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.syntax.core.term;
 

base/src/main/java/org/aya/syntax/core/term/StableWHNF.java → syntax/src/main/java/org/aya/syntax/core/term/StableWHNF.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.syntax.core.term;
 

base/src/main/java/org/aya/syntax/core/term/Term.java → syntax/src/main/java/org/aya/syntax/core/term/Term.java

@@ -1,7 +1,5 @@
 // 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.
-// 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.syntax.core.term;
 
 import kala.collection.SeqView;

base/src/main/java/org/aya/syntax/core/term/TupTerm.java → syntax/src/main/java/org/aya/syntax/core/term/TupTerm.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 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.syntax.core.term;
 

base/src/main/java/org/aya/syntax/core/term/call/ConCall.java → syntax/src/main/java/org/aya/syntax/core/term/call/ConCall.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.syntax.core.term.call;
 

base/src/main/java/org/aya/syntax/core/term/call/ConCallLike.java → syntax/src/main/java/org/aya/syntax/core/term/call/ConCallLike.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.syntax.core.term.call;
 

base/src/main/java/org/aya/syntax/core/term/call/FnCall.java → syntax/src/main/java/org/aya/syntax/core/term/call/FnCall.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.syntax.core.term.call;
 

base/src/main/java/org/aya/syntax/ref/AnyVar.java → syntax/src/main/java/org/aya/syntax/ref/AnyVar.java

@@ -1,3 +1,5 @@
+// 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.syntax.ref;
 
 import org.jetbrains.annotations.Debug;

base/src/main/java/org/aya/syntax/ref/DefVar.java → syntax/src/main/java/org/aya/syntax/ref/DefVar.java

@@ -1,3 +1,5 @@
+// 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.syntax.ref;
 
 import kala.collection.immutable.ImmutableSeq;
@@ -17,8 +19,8 @@ public final class DefVar<Core extends Def, Concrete extends Decl> implements An
   /** Initialized in type checking or core deserialization, so it might be null for unchecked user definitions. */
   public @UnknownNullability Core core;
   /** Initialized in the resolver or core deserialization */
-  public @Nullable ImmutableSeq<String> module;
-  public @Nullable ImmutableSeq<String> fileModule; // TODO: unify `module` and `fileModule`
+  public @Nullable ModulePath module;
+  public @Nullable ModulePath fileModule; // TODO: unify `module` and `fileModule`
   /** Initialized in the resolver or core deserialization */
   public @Nullable OpDecl opDecl;
 
@@ -54,14 +56,11 @@ private DefVar(Concrete concrete, Core core, @NotNull String name) {
     return this == o;
   }
 
-  public boolean isInModule(@NotNull ImmutableSeq<String> moduleName) {
-    var maybeSubmodule = module;
-    if (maybeSubmodule == null) return false;
-    if (maybeSubmodule.sizeLessThan(moduleName.size())) return false;
-    return maybeSubmodule.sliceView(0, moduleName.size()).sameElements(moduleName);
+  public boolean isInModule(@NotNull ModulePath moduleName) {
+    return module != null && module.isInModule(moduleName);
   }
 
   public @NotNull ImmutableSeq<String> qualifiedName() {
-    return module == null ? ImmutableSeq.of(name) : module.appended(name);
+    return module == null ? ImmutableSeq.of(name) : module.module().appended(name);
   }
 }

base/src/main/java/org/aya/syntax/ref/LocalCtx.java → syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java

@@ -8,10 +8,7 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-public record LocalCtx(
-  @NotNull MutableMap<LocalVar, Term> binds,
-  @Nullable LocalCtx parent
-) {
+public record LocalCtx(@NotNull MutableMap<LocalVar, Term> binds, @Nullable LocalCtx parent) {
   @Contract("-> new")
   public @NotNull LocalCtx derive() {
     return new LocalCtx(MutableMap.create(), this);

base/src/main/java/org/aya/syntax/ref/LocalVar.java → syntax/src/main/java/org/aya/syntax/ref/LocalVar.java

@@ -1,3 +1,5 @@
+// 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.syntax.ref;
 
 import org.aya.util.error.SourcePos;

syntax/src/main/java/org/aya/syntax/ref/ModulePath.java

@@ -0,0 +1,14 @@
+// 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.syntax.ref;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.jetbrains.annotations.NotNull;
+
+public record ModulePath(@NotNull ImmutableSeq<String> module) {
+  public boolean isInModule(@NotNull ModulePath other) {
+    var moduleName = other.module;
+    if (module.sizeLessThan(moduleName.size())) return false;
+    return module.sliceView(0, moduleName.size()).sameElements(moduleName);
+  }
+}