test: scope error

aya-prover · Jun 9, 2024 · 03e85b4 · 03e85b4
1 parent 873fc1a
commit 03e85b4
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 0 deletions.
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java b/cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java
@@ -46,6 +46,7 @@ open A hiding (bar)
     | zero
     """;
   @Language("Aya") String testRedefPrim = "prim I prim I";
+  @Language("Aya") String testPrimDeps = "prim Path";
   @Language("Aya") String testUnknownPrim = "prim senpaiSuki";
   @Language("Aya") String testUnknownVar = """
     open inductive Nat : Type | zero
@@ -70,4 +71,8 @@ def p (a : Bool) : Bool elim b
     def test Type : Type
     | _ => A
     """;
+  @Language("Aya") String testDuplicateModName = """
+    module A {}
+    module A {}
+    """;
 }
diff --git a/cli-impl/src/test/resources/negative/ScopeError.txt b/cli-impl/src/test/resources/negative/ScopeError.txt
@@ -139,6 +139,18 @@ Resolving interrupted due to:
 1 error(s), 0 warning(s).
 What are you doing?
 
+PrimDeps:
+In file $FILE:1:5 ->
+
+  1 │   prim Path
+    │        ╰──╯
+
+Error: The primitive `Path` depends on undeclared primitive(s): `I`
+
+Resolving interrupted due to:
+1 error(s), 0 warning(s).
+What are you doing?
+
 UnknownPrim:
 In file $FILE:1:5 ->
 
@@ -195,3 +207,16 @@ Resolving interrupted due to:
 1 error(s), 0 warning(s).
 What are you doing?
 
+DuplicateModName:
+In file $FILE:2:7 ->
+
+  1 │   module A {}
+  2 │   module A {}
+    │          ╰╯
+
+Error: The module name `A` is already defined elsewhere
+
+Resolving interrupted due to:
+1 error(s), 0 warning(s).
+What are you doing?
+