Initial implementation of constraint collection and compactification …

…for new sort inference.
runtimeverification · Sep 27, 2023 · 8a3f629 · 8a3f629
1 parent 6bda50e
commit 8a3f629
Show file tree

Hide file tree

Showing 3 changed files with 517 additions and 0 deletions.
diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
@@ -24,9 +24,13 @@
 import scala.util.Left;
 import scala.util.Right;
 
+import java.io.BufferedWriter;
 import java.io.File;
+import java.io.FileWriter;
 import java.io.IOException;
+import java.io.PrintWriter;
 import java.io.Serializable;
+import java.io.Writer;
 import java.nio.charset.StandardCharsets;
 import java.util.Collections;
 import java.util.Queue;
@@ -267,6 +271,24 @@ public void setScanner(Scanner s) {
                 }
             }
 
+
+
+            PrintWriter debug = null;
+            try {
+                File debugFile = files.resolveWorkingDirectory("inference/" + disambModule.name() + ".log");
+                debugFile.getParentFile().mkdirs();
+                debug = new PrintWriter(new BufferedWriter(new FileWriter(debugFile, true)));
+                new SortInferencer(disambModule, debug, strict && inferSortChecks, true).
+                        apply(rez3, startSymbol, isAnywhere);
+            } catch (java.io.IOException e) {
+                throw KEMException.criticalError(e.getMessage());
+            } finally {
+                if (debug != null) {
+                    debug.close();
+                }
+            }
+
+
             rez = new TypeInferenceVisitor(currentInferencer, startSymbol, strict && inferSortChecks, true, isAnywhere).apply(rez3);
             if (rez.isLeft())
                 return new Tuple2<>(rez, warn);