Tester

ARCHITECTURE.md

@@ -57,6 +57,7 @@ Arend is split into several subprojects:
 |`api`|open API for writing Arend extensions.|
 |`base`|the Arend typechecker.<br/>It depends on `api`, `proto`.|
 |`cli`|the CLI frontend of Arend with the ANTLR parser.<br/>It depends on `base`, `parser`, `api`, `proto`.|
+|`tester`|Helper for writing unit tests with JUnit4.<br/>It depends on `base`, `parser`, `api`, `cli`.|
 
 The purpose of `parser` is to avoid introducing the dependency of the ANTLR
 generator to other subprojects which only requires

README.md

@@ -41,6 +41,8 @@ dependencies {
     implementation "com.github.JetBrains.Arend:proto:$arendVersion"
     // The main compiler
     implementation "com.github.JetBrains.Arend:base:$arendVersion"
+    // The unit test helpers
+    testImplementation "com.github.JetBrains.Arend:tester:$arendVersion"
 }
 ```
 
@@ -58,5 +60,6 @@ dependencies {
     implementation("com.github.JetBrains.Arend:parser:$arendVersion")
     implementation("com.github.JetBrains.Arend:proto:$arendVersion")
     implementation("com.github.JetBrains.Arend:base:$arendVersion")
+    testImplementation("com.github.JetBrains.Arend:tester:$arendVersion")
 }
 ```

build.gradle.kts

@@ -88,6 +88,7 @@ dependencies {
     testImplementation(project(":base"))
     testImplementation(project(":parser"))
     testImplementation(project(":cli"))
+    testImplementation(project(":tester"))
 
     testImplementation("junit:junit:4.12")
     testImplementation("org.hamcrest:hamcrest-library:1.3")

settings.gradle.kts

@@ -7,5 +7,6 @@ include(
     "base",
     "cli",
     "proto",
+    "tester",
     "parser"
 )

tester/build.gradle.kts

@@ -0,0 +1,18 @@
+plugins {
+    java
+}
+
+dependencies {
+    val annotationsVersion: String by rootProject.ext
+    val antlrVersion: String by rootProject.ext
+    implementation("org.jetbrains:annotations:$annotationsVersion")
+    implementation("org.antlr:antlr4-runtime:$antlrVersion")
+
+    implementation(project(":api"))
+    implementation(project(":base"))
+    implementation(project(":parser"))
+    implementation(project(":cli"))
+
+    implementation("junit:junit:4.12")
+    implementation("org.hamcrest:hamcrest-library:1.3")
+}

src/test/java/org/arend/naming/NameResolverTestCase.java → tester/src/main/java/org/arend/naming/NameResolverTestCase.java

@@ -1,5 +1,6 @@
 package org.arend.naming;
 
+import org.arend.ArendTestCase;
 import org.arend.core.context.binding.Binding;
 import org.arend.frontend.ConcreteReferableProvider;
 import org.arend.frontend.reference.ConcreteLocatedReferable;
@@ -60,7 +61,7 @@ ChildGroup resolveNamesDefGroup(String text, int errors) {
     ChildGroup group = parseDef(text);
     Scope parentScope = new MergeScope(new SingletonScope(group.getReferable()), PreludeLibrary.getPreludeScope());
     new DefinitionResolveNameVisitor(ConcreteReferableProvider.INSTANCE, errorReporter).resolveGroupWithTypes(group, null, CachingScope.make(LexicalScope.insideOf(group, parentScope)));
-    assertThat(errorList, containsErrors(errors));
+    assertThat(errorList, ArendTestCase.containsErrors(errors));
     return group;
   }
 
@@ -81,7 +82,7 @@ private void resolveNamesModule(ChildGroup group, int errors) {
     Scope scope = CachingScope.make(ScopeFactory.forGroup(group, moduleScopeProvider));
     new DefinitionResolveNameVisitor(ConcreteReferableProvider.INSTANCE, errorReporter).resolveGroupWithTypes(group, null, scope);
     libraryManager.getInstanceProviderSet().collectInstances(group, CachingScope.make(ScopeFactory.parentScopeForGroup(group, moduleScopeProvider, true)), ConcreteReferableProvider.INSTANCE, null);
-    assertThat(errorList, containsErrors(errors));
+    assertThat(errorList, ArendTestCase.containsErrors(errors));
   }
 
   protected ChildGroup resolveNamesModule(String text, int errors) {