import: fix source pos

Co-authored-by: Hoshino Tented <[email protected]>
aya-prover · Jan 4, 2025 · df382d5 · df382d5
1 parent e160945
commit df382d5
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 13 deletions.
diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.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.resolve.visitor;
 
@@ -64,7 +64,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
           context.reportAndThrow(new NameProblem.ModNotFoundError(modulePath, cmd.sourcePos()));
         var mod = success.thisModule();
         var as = cmd.asName();
-        var importedName = as != null ? ModuleName.This.resolve(as) : modulePath.asName();
+        var importedName = as != null ? ModuleName.This.resolve(as.data()) : modulePath.asName();
         context.importModuleContext(importedName, mod, cmd.accessibility(), cmd.sourcePos());
         var importInfo = new ResolveInfo.ImportInfo(success, cmd.accessibility() == Stmt.Accessibility.Public);
         resolveInfo.imports().put(importedName, importInfo);

diff --git a/note/clause-tyck.md b/note/clause-tyck.md
@@ -10,7 +10,7 @@
 `PatternTycker` 负责找到用户给定的 pattern 所对应的 parameter，并且在遇到问题时报错，
 如过多隐式 pattern 或过少的 pattern。
 
-尽管我们一开始就对函数签名进行 pusheen，对于 PatternTycker 来说，它需要知道哪些 parameter 是必须有 pattern 而哪些不必须。因此，在 pattern 
+尽管我们一开始就对函数签名进行 pusheen，但对于 PatternTycker 来说，它需要知道哪些 parameter 是必须有 pattern 而哪些不必须。因此，在 pattern 
 
 ## After Pattern Typecheck (checkLhs)
 

diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.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.producer;
 
@@ -120,7 +120,7 @@ public record AyaProducer(
     return new Command.Import(
       sourcePosOf(importMod),
       modulePath(importMod),
-      asId == null ? null : weakId(asId).data(),
+      asId == null ? null : weakId(asId),
       acc == null ? Stmt.Accessibility.Private : Stmt.Accessibility.Public
     );
   }

diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.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.prettier;
 
@@ -294,7 +294,7 @@ private Doc visitAccess(@NotNull Accessibility acc, @Nullable Accessibility theD
         var prelude = MutableList.of(KW_IMPORT, Doc.symbol(cmd.path().toString()));
         if (cmd.asName() != null) {
           prelude.append(KW_AS);
-          prelude.append(Doc.plain(cmd.asName()));
+          prelude.append(Doc.plain(cmd.asName().data()));
         }
         yield Doc.sep(prelude);
       }

diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/Command.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/Command.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.concrete.stmt;
 
@@ -8,6 +8,7 @@
 import org.aya.syntax.ref.ModulePath;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.SourcePos;
+import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -17,7 +18,7 @@ public sealed interface Command extends Stmt {
   record Import(
     @Override @NotNull SourcePos sourcePos,
     @NotNull ModulePath path,
-    @Nullable String asName,
+    @Nullable WithPos<String> asName,
     @Override @NotNull Accessibility accessibility
   ) implements Command { }
 

diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.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.concrete.stmt;
 
@@ -77,10 +77,9 @@ private void visitVars(@NotNull Stmt stmt) {
       case Generalize g -> g.variables.forEach(v -> visitVarDecl(v.sourcePos, v, noType));
       case Command.Module m -> visitModuleDecl(m.sourcePos(), ModuleName.of(m.name()));
       case Command.Import i -> {
-        var isAlsoDef = i.asName() == null;
         visitModuleRef(i.sourcePos(), i.path());
-        if (!isAlsoDef) {
-          visitModuleDecl(i.sourcePos(), ModuleName.of(i.asName()));
+        if (i.asName() instanceof WithPos(var pos, var asName)) {
+          visitModuleDecl(pos, ModuleName.of(asName));
         } else {
           // TODO: visitModuleDecl on the last element of i.path
         }