Merge pull request #6 from lorchrob/type-decl-flag

Support lus_main_type flag
kind2-mc · Jun 19, 2024 · 34829b1 · 34829b1
2 parents bce641a + 0f31b07
commit 34829b1
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 8 deletions.
diff --git a/build.gradle b/build.gradle
@@ -8,7 +8,7 @@ repositories {
 }
 
 dependencies {
-  implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.9'
+  implementation 'edu.uiowa.cs.clc:kind2-java-api:0.4.1'
   implementation 'org.eclipse.lsp4j:org.eclipse.lsp4j:0.13.0'
   testImplementation 'org.junit.jupiter:junit-jupiter-api:5.7.2'
   testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.7.2'

diff --git a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java
@@ -260,7 +260,7 @@ public CompletableFuture<List<String>> getComponents(String uri) {
       if (parseResults.containsKey(uri)) {
         try {
           for (AstInfo info : parseResults.get(uri).getAstInfos()) {
-            if (info instanceof NodeInfo || info instanceof FunctionInfo) {
+            if (info instanceof NodeInfo || info instanceof FunctionInfo || info instanceof TypeDeclInfo) {
               components.add(replacePathWithUri(info.getJson(), uri,
                   info.getFile() == null ? new URI(uri).getPath()
                       : info.getFile()));
@@ -297,7 +297,7 @@ public void done() {
         if (workingDirectory == null) {
           workingDirectory = client.workspaceFolders().get().get(0).getUri();
         }
-        Kind2Api api = getCheckKind2Api(name);
+        Kind2Api api = getCheckKind2Api(name, false);
         api.includeDir(Paths.get(new URI(uri)).getParent().toString());
         String filepath = computeRelativeFilepath(workingDirectory, uri);
         api.setFakeFilepath(filepath);
@@ -363,7 +363,7 @@ public void done() {
   }
 
   @JsonRequest(value = "kind2/realizability", useSegment = false)
-  public CompletableFuture<List<String>> realizability(String uri, String name) {
+  public CompletableFuture<List<String>> realizability(String uri, String name, boolean typeDecl) {
     return CompletableFutures.computeAsync(cancelToken -> {
       client.logMessage(new MessageParams(MessageType.Info,
           "Checking realizability of component " + name + " in " + uri + "..."));
@@ -384,7 +384,7 @@ public void done() {
         if (workingDirectory == null) {
           workingDirectory = client.workspaceFolders().get().get(0).getUri();
         }
-        Kind2Api api = getCheckKind2Api(name);
+        Kind2Api api = getCheckKind2Api(name, typeDecl);
         api.includeDir(Paths.get(new URI(uri)).getParent().toString());
         String filepath = computeRelativeFilepath(workingDirectory, uri);
         api.setFakeFilepath(filepath);
@@ -679,7 +679,7 @@ public Kind2Api getPresetKind2Api()
     return api;
   }
 
-  public Kind2Api getCheckKind2Api(String name)
+  public Kind2Api getCheckKind2Api(String name, boolean typeDecl)
       throws InterruptedException, ExecutionException {
     ConfigurationItem kind2Options = new ConfigurationItem();
     kind2Options.setSection("kind2");
@@ -737,7 +737,11 @@ public Kind2Api getCheckKind2Api(String name)
       otherOptions.add(option.getAsString());
     }
     api.setOtherOptions(otherOptions);
-    api.setLusMain(name);
+    if (typeDecl) {
+      api.setLusMainType(name);
+    } else {
+      api.setLusMain(name);
+    }
     return api;
   }
 
@@ -763,7 +767,7 @@ public CompletableFuture<String> interpret(String uri, String main,
   public CompletableFuture<List<String>> getKind2Cmd(String uri, String main) {
     return CompletableFuture.supplyAsync(() -> {
       try {
-        Kind2Api api = getCheckKind2Api(main);
+        Kind2Api api = getCheckKind2Api(main, false);
         List<String> cmd = api.getOptions();
         cmd.set(0, Kind2Api.KIND2);
         cmd.add(new URI(uri).getPath());