Enable new TI in kprove (#3855)

Move the option to enable new type inference to InnerParsingOptions so
it's available in kprove as well.

k-distribution/include/kframework/ktest.mak

@@ -53,7 +53,7 @@ ifeq ($(UNAME), Darwin)
 endif
 
 KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode checked
-KPROVE_FLAGS+=--no-exc-wrap
+KPROVE_FLAGS+=--no-exc-wrap --type-inference-mode checked
 KRUN_FLAGS+=--no-exc-wrap
 
 KRUN_OR_LEGACY=$(KRUN)

kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java

@@ -445,7 +445,7 @@ private Definition resolveConfigBubbles(Definition def) {
                       profileRules,
                       files,
                       options.debugTypeInference,
-                      options.typeInferenceMode)) {
+                      innerParsingOptions.typeInferenceMode)) {
                 // each parser gets its own scanner because config labels can conflict with user
                 // tokens
                 parser.getScanner(globalOptions);
@@ -514,7 +514,7 @@ private Definition resolveConfigBubbles(Definition def) {
                           profileRules,
                           files,
                           options.debugTypeInference,
-                          options.typeInferenceMode)
+                          innerParsingOptions.typeInferenceMode)
                       .getExtensionModule();
               Set<Sentence> configDeclProductions =
                   stream(module.localSentences())
@@ -561,7 +561,7 @@ private Definition resolveNonConfigBubbles(
             true,
             files,
             options.debugTypeInference,
-            options.typeInferenceMode,
+            innerParsingOptions.typeInferenceMode,
             false)) {
       Scanner scanner;
       if (deserializeScanner) {
@@ -598,15 +598,15 @@ private Module resolveNonConfigBubbles(Module module, Scanner scanner, RuleGramm
                 profileRules,
                 files,
                 options.debugTypeInference,
-                options.typeInferenceMode)
+                innerParsingOptions.typeInferenceMode)
             : RuleGrammarGenerator.getCombinedGrammar(
                 cache.module(),
                 scanner,
                 profileRules,
                 false,
                 files,
                 options.debugTypeInference,
-                options.typeInferenceMode,
+                innerParsingOptions.typeInferenceMode,
                 false)) {
       if (needNewScanner) parser.getScanner(globalOptions);
       parser.initialize();
@@ -806,7 +806,7 @@ public Rule parseRule(CompiledDefinition compiledDef, String contents, Source so
             true,
             files,
             options.debugTypeInference,
-            options.typeInferenceMode,
+            innerParsingOptions.typeInferenceMode,
             false)) {
       parser.setScanner(new Scanner(parser, globalOptions, files.resolveKompiled("scanner")));
       java.util.Set<K> res =

kernel/src/main/java/org/kframework/kompile/KompileOptions.java

@@ -244,22 +244,4 @@ public String syntaxModule(FileUtil files) {
       description = "Enable generation of legacy antileft priority predicates.",
       hidden = true)
   public boolean enableKoreAntileft;
-
-  public enum TypeInferenceMode {
-    Z3,
-    SIMPLESUB,
-    CHECKED,
-    // We use an explicit DEFAULT option here so that ParseInModule can set a default which
-    // applies even for those codepaths that don't rely on KompileOptions
-    DEFAULT,
-  }
-
-  @Parameter(
-      names = "--type-inference-mode",
-      description =
-          "Choose between the Z3-based and SimpleSub-based type inference algorithms, or run both"
-              + " and check that their results are equal. Must be one of "
-              + "[z3|simplesub|checked|default].",
-      hidden = true)
-  public TypeInferenceMode typeInferenceMode = TypeInferenceMode.DEFAULT;
 }

kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java

@@ -15,7 +15,6 @@
 import org.kframework.definition.Module;
 import org.kframework.definition.Terminal;
 import org.kframework.definition.TerminalLike;
-import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.K;
 import org.kframework.kore.Sort;
 import org.kframework.main.GlobalOptions;
@@ -29,6 +28,7 @@
 import org.kframework.utils.StringUtil;
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.file.FileUtil;
+import org.kframework.utils.options.InnerParsingOptions;
 import scala.Tuple2;
 import scala.Tuple3;
 import scala.util.Either;
@@ -65,7 +65,7 @@ public class ParseInModule implements Serializable, AutoCloseable {
   private final boolean forGlobalScanner;
   private final FileUtil files;
   private final String typeInferenceDebug;
-  private final KompileOptions.TypeInferenceMode typeInferenceMode;
+  private final InnerParsingOptions.TypeInferenceMode typeInferenceMode;
   private final boolean partialParseDebug;
 
   ParseInModule(
@@ -75,7 +75,7 @@ public class ParseInModule implements Serializable, AutoCloseable {
       boolean forGlobalScanner,
       FileUtil files,
       String typeInferenceDebug,
-      KompileOptions.TypeInferenceMode typeInferenceMode,
+      InnerParsingOptions.TypeInferenceMode typeInferenceMode,
       boolean partialParseDebug) {
     this(
         seedModule,
@@ -100,7 +100,7 @@ public class ParseInModule implements Serializable, AutoCloseable {
       boolean forGlobalScanner,
       FileUtil files,
       String typeInferenceDebug,
-      KompileOptions.TypeInferenceMode typeInferenceMode,
+      InnerParsingOptions.TypeInferenceMode typeInferenceMode,
       boolean partialParseDebug) {
     this(
         seedModule,
@@ -128,7 +128,7 @@ private ParseInModule(
       boolean forGlobalScanner,
       FileUtil files,
       String typeInferenceDebug,
-      KompileOptions.TypeInferenceMode typeInferenceMode,
+      InnerParsingOptions.TypeInferenceMode typeInferenceMode,
       boolean partialParseDebug) {
     this.seedModule = seedModule;
     this.extensionModule = extensionModule;
@@ -141,8 +141,8 @@ private ParseInModule(
     this.files = files;
     this.typeInferenceDebug = typeInferenceDebug;
     this.typeInferenceMode =
-        typeInferenceMode == KompileOptions.TypeInferenceMode.DEFAULT
-            ? KompileOptions.TypeInferenceMode.Z3
+        typeInferenceMode == InnerParsingOptions.TypeInferenceMode.DEFAULT
+            ? InnerParsingOptions.TypeInferenceMode.Z3
             : typeInferenceMode;
     this.partialParseDebug = partialParseDebug;
   }
@@ -414,17 +414,17 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
       rez3 = new PushTopAmbiguityUp().apply(rez3);
       startTypeInf = profileRules ? System.currentTimeMillis() : 0;
 
-      KompileOptions.TypeInferenceMode infModeForTerm =
+      InnerParsingOptions.TypeInferenceMode infModeForTerm =
           SortInferencer.isSupported(rez3)
               ? typeInferenceMode
-              : KompileOptions.TypeInferenceMode.Z3;
+              : InnerParsingOptions.TypeInferenceMode.Z3;
 
-      if (infModeForTerm == KompileOptions.TypeInferenceMode.SIMPLESUB
-          || infModeForTerm == KompileOptions.TypeInferenceMode.CHECKED) {
+      if (infModeForTerm == InnerParsingOptions.TypeInferenceMode.SIMPLESUB
+          || infModeForTerm == InnerParsingOptions.TypeInferenceMode.CHECKED) {
         rez = new SortInferencer(disambModule).apply(rez3, startSymbol, isAnywhere);
       }
-      if (infModeForTerm == KompileOptions.TypeInferenceMode.Z3
-          || infModeForTerm == KompileOptions.TypeInferenceMode.CHECKED) {
+      if (infModeForTerm == InnerParsingOptions.TypeInferenceMode.Z3
+          || infModeForTerm == InnerParsingOptions.TypeInferenceMode.CHECKED) {
 
         TypeInferencer currentInferencer;
         if (isDebug(source, startLine)) {
@@ -440,7 +440,7 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
         }
         Either<Set<KEMException>, Term> z3Rez =
             new TypeInferenceVisitor(currentInferencer, startSymbol, isAnywhere).apply(rez3);
-        if (infModeForTerm == KompileOptions.TypeInferenceMode.CHECKED) {
+        if (infModeForTerm == InnerParsingOptions.TypeInferenceMode.CHECKED) {
           boolean bothLeft = rez.isLeft() && z3Rez.isLeft();
           boolean equalRight =
               rez.isRight() && z3Rez.isRight() && rez.right().get().equals(z3Rez.right().get());

kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java

@@ -33,12 +33,12 @@
 import org.kframework.definition.Terminal;
 import org.kframework.definition.UidProvider;
 import org.kframework.definition.UserList;
-import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.Sort;
 import org.kframework.kore.SortHead;
 import org.kframework.parser.inner.kernel.Scanner;
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.file.FileUtil;
+import org.kframework.utils.options.InnerParsingOptions;
 import scala.Option;
 import scala.Tuple3;
 import scala.collection.Seq;
@@ -203,7 +203,14 @@ public static boolean isParserSort(Sort s) {
   /* use this overload if you don't need to profile rule parse times. */
   public static ParseInModule getCombinedGrammar(Module mod, FileUtil files) {
     return getCombinedGrammar(
-        mod, false, false, false, files, null, KompileOptions.TypeInferenceMode.DEFAULT, false);
+        mod,
+        false,
+        false,
+        false,
+        files,
+        null,
+        InnerParsingOptions.TypeInferenceMode.DEFAULT,
+        false);
   }
 
   public static ParseInModule getCombinedGrammar(
@@ -215,29 +222,43 @@ public static ParseInModule getCombinedGrammar(
         false,
         files,
         null,
-        KompileOptions.TypeInferenceMode.DEFAULT,
+        InnerParsingOptions.TypeInferenceMode.DEFAULT,
         partialParseDebug);
   }
 
   public static ParseInModule getCombinedGrammar(Module mod, boolean timing, FileUtil files) {
     return getCombinedGrammar(
-        mod, timing, false, false, files, null, KompileOptions.TypeInferenceMode.DEFAULT, false);
+        mod,
+        timing,
+        false,
+        false,
+        files,
+        null,
+        InnerParsingOptions.TypeInferenceMode.DEFAULT,
+        false);
   }
 
   public static ParseInModule getCombinedGrammar(
       Module mod,
       boolean timing,
       FileUtil files,
       String debugTypeInference,
-      KompileOptions.TypeInferenceMode typeInferenceMode) {
+      InnerParsingOptions.TypeInferenceMode typeInferenceMode) {
     return getCombinedGrammar(
         mod, timing, false, false, files, debugTypeInference, typeInferenceMode, false);
   }
 
   public static ParseInModule getCombinedGrammar(
       Module mod, boolean timing, boolean isBison, FileUtil files) {
     return getCombinedGrammar(
-        mod, timing, isBison, false, files, null, KompileOptions.TypeInferenceMode.DEFAULT, false);
+        mod,
+        timing,
+        isBison,
+        false,
+        files,
+        null,
+        InnerParsingOptions.TypeInferenceMode.DEFAULT,
+        false);
   }
 
   public static ParseInModule getCombinedGrammar(
@@ -249,7 +270,7 @@ public static ParseInModule getCombinedGrammar(
         forGlobalScanner,
         files,
         null,
-        KompileOptions.TypeInferenceMode.DEFAULT,
+        InnerParsingOptions.TypeInferenceMode.DEFAULT,
         false);
   }
 
@@ -262,7 +283,7 @@ public static ParseInModule getCombinedGrammar(
         isBison,
         files,
         null,
-        KompileOptions.TypeInferenceMode.DEFAULT,
+        InnerParsingOptions.TypeInferenceMode.DEFAULT,
         false);
   }
 
@@ -291,7 +312,7 @@ public static ParseInModule getCombinedGrammar(
       boolean forGlobalScanner,
       FileUtil files,
       String debugTypeInference,
-      KompileOptions.TypeInferenceMode typeInferenceMode,
+      InnerParsingOptions.TypeInferenceMode typeInferenceMode,
       boolean partialParseDebug) {
     return new ParseInModule(
         mod,
@@ -311,7 +332,7 @@ public static ParseInModule getCombinedGrammar(
       boolean isBison,
       FileUtil files,
       String debugTypeInference,
-      KompileOptions.TypeInferenceMode typeInferenceMode,
+      InnerParsingOptions.TypeInferenceMode typeInferenceMode,
       boolean partialParseDebug) {
     return new ParseInModule(
         mod,

kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java

@@ -23,4 +23,22 @@ public InnerParsingOptions(Void v) {}
       descriptionKey = "file",
       hidden = true)
   public String profileRules;
+
+  public enum TypeInferenceMode {
+    Z3,
+    SIMPLESUB,
+    CHECKED,
+    // We use an explicit DEFAULT option here so that ParseInModule can set a default which
+    // applies even for those codepaths that don't rely on KompileOptions
+    DEFAULT,
+  }
+
+  @Parameter(
+      names = "--type-inference-mode",
+      description =
+          "Choose between the Z3-based and SimpleSub-based type inference algorithms, or run both"
+              + " and check that their results are equal. Must be one of "
+              + "[z3|simplesub|checked|default].",
+      hidden = true)
+  public TypeInferenceMode typeInferenceMode = TypeInferenceMode.DEFAULT;
 }