Remove unused strict field from ParseInModule (#3807)

This PR removes the `strict` field in `ParseInModule`.

The field is safe to remove because, after eliminating some dead code,
- The only use of `strict` in `ParseInModule` is in `parseStringTerm`
- `strict` is (almost) always set to `true`
- The only place where `strict` is set to `false` is through a few calls
to `RuleGrammarGenerator.getCombinedGrammar` in `KPrint`. However, these
usages only ever call `getParsingModule` and `getExtensionModule` on the
constructed `ParseInModule` object, neither of which invokes
`parseStringTerm`, so the value of `strict` here is actually irrelevant.

Note that no actual functionality is lost either - the only live usage
of `strict` in `parseStringTerm` is now fully controlled by the
`inferSortChecks` argument rather than `strict && inferSortChecks`.

Co-authored-by: rv-jenkins <[email protected]>

kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java

@@ -249,8 +249,7 @@ public Module resolve(Module m) {
     if (m.name().equals(def.mainModule().name())) {
       if (!m.definedKLabels().contains(KLabels.GENERATED_TOP_CELL)) {
         RuleGrammarGenerator gen = new RuleGrammarGenerator(def);
-        ParseInModule mod =
-            RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), true, files);
+        ParseInModule mod = RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), files);
         ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(m);
         Sort topCellSort;
         try {
@@ -283,8 +282,7 @@ public Module resolve(Module m) {
     }
     if (m.localKLabels().contains(KLabels.GENERATED_TOP_CELL)) {
       RuleGrammarGenerator gen = new RuleGrammarGenerator(def);
-      ParseInModule mod =
-          RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), true, files);
+      ParseInModule mod = RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), files);
       Set<Sentence> newSentences =
           GenerateSentencesFromConfigDecl.gen(
               freshCell, BooleanUtils.TRUE, Att.empty(), mod.getExtensionModule());

kernel/src/main/java/org/kframework/kast/KastFrontEnd.java

@@ -139,8 +139,7 @@ public int run() {
         String stringToParse = FileUtil.read(options.stringToParse());
         Source source = options.source();
 
-        try (ParseInModule parseInModule =
-            RuleGrammarGenerator.getCombinedGrammar(mod, true, null)) {
+        try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(mod, null)) {
           if (options.debugTokens)
             System.out.println(parseInModule.tokenizeString(stringToParse, source));
           else {
@@ -155,7 +154,7 @@ public int run() {
             // syntax
             // like casts, projections and others
             Module unparsingMod = parseInModule.getExtensionModule();
-            K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get());
+            K parsed = new TreeNodesToKORE(Outer::parseSort).down(res._1().right().get());
 
             if (options.expandMacros) {
               parsed =

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

@@ -233,27 +233,26 @@ public K parseSingleTerm(
       Source source,
       boolean partialParseDebug) {
     try (ParseInModule parseInModule =
-        RuleGrammarGenerator.getCombinedGrammar(module, true, files, partialParseDebug)) {
+        RuleGrammarGenerator.getCombinedGrammar(module, files, partialParseDebug)) {
       Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> res =
           parseInModule.parseString(s, programStartSymbol, startSymbolLocation, source);
       kem.addAllKException(
           res._2().stream().map(e -> e.getKException()).collect(Collectors.toSet()));
       if (res._1().isLeft()) {
         throw res._1().left().get().iterator().next();
       }
-      return new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get());
+      return new TreeNodesToKORE(Outer::parseSort).down(res._1().right().get());
     }
   }
 
   public String showTokens(Module module, FileUtil files, String s, Source source) {
-    try (ParseInModule parseInModule =
-        RuleGrammarGenerator.getCombinedGrammar(module, true, files)) {
+    try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(module, files)) {
       return parseInModule.tokenizeString(s, source);
     }
   }
 
   public Module getExtensionModule(Module module, FileUtil files) {
-    return RuleGrammarGenerator.getCombinedGrammar(module, true, files).getExtensionModule();
+    return RuleGrammarGenerator.getCombinedGrammar(module, files).getExtensionModule();
   }
 
   public Rule compilePatternIfAbsent(

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

@@ -441,7 +441,7 @@ private Definition resolveConfigBubbles(Definition def) {
               ParseCache cache = loadCache(configParserModule);
               try (ParseInModule parser =
                   RuleGrammarGenerator.getCombinedGrammar(
-                      cache.module(), true, profileRules, files, options.debugTypeInference)) {
+                      cache.module(), profileRules, files, options.debugTypeInference)) {
                 // each parser gets its own scanner because config labels can conflict with user
                 // tokens
                 parser.getScanner(globalOptions);
@@ -507,7 +507,6 @@ private Definition resolveConfigBubbles(Definition def) {
               Module extMod =
                   RuleGrammarGenerator.getCombinedGrammar(
                           gen.getConfigGrammar(module),
-                          true,
                           profileRules,
                           files,
                           options.debugTypeInference)
@@ -551,14 +550,7 @@ private Definition resolveNonConfigBubbles(
     ParseCache cache = loadCache(ruleParserModule);
     try (ParseInModule parser =
         RuleGrammarGenerator.getCombinedGrammar(
-            cache.module(),
-            true,
-            profileRules,
-            false,
-            true,
-            files,
-            options.debugTypeInference,
-            false)) {
+            cache.module(), profileRules, false, true, files, options.debugTypeInference, false)) {
       Scanner scanner;
       if (deserializeScanner) {
         scanner = new Scanner(parser, globalOptions, files.resolveKompiled("scanner"));
@@ -590,11 +582,10 @@ private Module resolveNonConfigBubbles(Module module, Scanner scanner, RuleGramm
     try (ParseInModule parser =
         needNewScanner
             ? RuleGrammarGenerator.getCombinedGrammar(
-                cache.module(), true, profileRules, files, options.debugTypeInference)
+                cache.module(), profileRules, files, options.debugTypeInference)
             : RuleGrammarGenerator.getCombinedGrammar(
                 cache.module(),
                 scanner,
-                true,
                 profileRules,
                 false,
                 files,
@@ -682,8 +673,7 @@ private Definition resolveCachedBubbles(Definition def, boolean isRule) {
                               registerWarnings(parse.warnings());
                               KApply k =
                                   (KApply)
-                                      new TreeNodesToKORE(Outer::parseSort, true)
-                                          .down(parse.parse());
+                                      new TreeNodesToKORE(Outer::parseSort).down(parse.parse());
                               return Stream.of(Pair.of(b, upSentence(k, b.sentenceType())));
                             }
                             return Stream.of();
@@ -794,7 +784,6 @@ public Rule parseRule(CompiledDefinition compiledDef, String contents, Source so
     try (ParseInModule parser =
         RuleGrammarGenerator.getCombinedGrammar(
             gen.getRuleGrammar(compiledDef.getParsedDefinition().mainModule()),
-            true,
             profileRules,
             false,
             true,
@@ -961,7 +950,7 @@ private Stream<? extends K> parseBubble(
           b.contents(),
           new ParsedSentence(
               k, new HashSet<>(result._2()), new HashSet<>(), startLine, startColumn, source));
-      k = (KApply) new TreeNodesToKORE(Outer::parseSort, true).down(k);
+      k = (KApply) new TreeNodesToKORE(Outer::parseSort).down(k);
       return Stream.of(k);
     } else {
       cache.put(

kernel/src/main/java/org/kframework/parser/KRead.java

@@ -79,7 +79,7 @@ public void createBisonParser(
       boolean library) {
     Stopwatch sw = new Stopwatch(globalOptions);
     try (ParseInModule parseInModule =
-        RuleGrammarGenerator.getCombinedGrammar(mod, true, false, true, false, files)) {
+        RuleGrammarGenerator.getCombinedGrammar(mod, false, true, false, files)) {
       try (Scanner scanner = parseInModule.getScanner(kem.options)) {
         File scannerFile = files.resolveTemp("scanner.l");
         File scanHdr = files.resolveTemp("scanner.h");

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

@@ -58,7 +58,6 @@ public class ParseInModule implements Serializable, AutoCloseable {
   private volatile Module parsingModule;
 
   private volatile EarleyParser parser = null;
-  private final boolean strict;
   private final boolean profileRules;
   private final boolean isBison;
   private final boolean forGlobalScanner;
@@ -68,7 +67,6 @@ public class ParseInModule implements Serializable, AutoCloseable {
 
   ParseInModule(
       Module seedModule,
-      boolean strict,
       boolean profileRules,
       boolean isBison,
       boolean forGlobalScanner,
@@ -81,7 +79,6 @@ public class ParseInModule implements Serializable, AutoCloseable {
         null,
         null,
         null,
-        strict,
         profileRules,
         isBison,
         forGlobalScanner,
@@ -93,7 +90,6 @@ public class ParseInModule implements Serializable, AutoCloseable {
   ParseInModule(
       Module seedModule,
       Scanner scanner,
-      boolean strict,
       boolean profileRules,
       boolean isBison,
       boolean forGlobalScanner,
@@ -106,7 +102,6 @@ public class ParseInModule implements Serializable, AutoCloseable {
         null,
         null,
         scanner,
-        strict,
         profileRules,
         isBison,
         forGlobalScanner,
@@ -121,7 +116,6 @@ private ParseInModule(
       Module disambModule,
       Module parsingModule,
       Scanner scanner,
-      boolean strict,
       boolean profileRules,
       boolean isBison,
       boolean forGlobalScanner,
@@ -133,7 +127,6 @@ private ParseInModule(
     this.disambModule = disambModule;
     this.parsingModule = parsingModule;
     this.scanner = scanner;
-    this.strict = strict;
     this.profileRules = profileRules;
     this.isBison = isBison;
     this.forGlobalScanner = forGlobalScanner;
@@ -350,9 +343,7 @@ public Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> parseString(
       parseInfo = Left.apply(result._1().left().get());
     } else {
       parseInfo =
-          Right.apply(
-              new TreeNodesToKORE(Outer::parseSort, inferSortChecks && strict)
-                  .apply(result._1().right().get()));
+          Right.apply(new TreeNodesToKORE(Outer::parseSort).apply(result._1().right().get()));
     }
     return new Tuple2<>(parseInfo, result._2());
   }
@@ -430,7 +421,7 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
 
       rez =
           new TypeInferenceVisitor(
-                  currentInferencer, startSymbol, strict && inferSortChecks, true, isAnywhere)
+                  currentInferencer, startSymbol, inferSortChecks, true, isAnywhere)
               .apply(rez3);
       if (rez.isLeft()) return new Tuple2<>(rez, warn);
       endTypeInf = profileRules ? System.currentTimeMillis() : 0;
@@ -439,7 +430,7 @@ private Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> parseStringTe
       if (rez.isLeft()) return new Tuple2<>(rez, warn);
       rez3 =
           new PushAmbiguitiesDownAndPreferAvoid(disambModule.overloads()).apply(rez.right().get());
-      rez = new AmbFilterError(strict && inferSortChecks).apply(rez3);
+      rez = new AmbFilterError().apply(rez3);
       if (rez.isLeft()) return new Tuple2<>(rez, warn);
       Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> rez2 =
           new AddEmptyLists(disambModule, startSymbol).apply(rez.right().get());
@@ -500,11 +491,11 @@ public static Term disambiguateForUnparse(Module mod, Term ambiguity) {
       rez = new TypeInferenceVisitor(inferencer, Sorts.K(), false, false, false).apply(rez3);
     }
     if (rez.isLeft()) {
-      rez2 = new AmbFilter(false).apply(rez3);
+      rez2 = new AmbFilter().apply(rez3);
       return rez2._1().right().get();
     }
     rez3 = new PushAmbiguitiesDownAndPreferAvoid(mod.overloads()).apply(rez.right().get());
-    rez2 = new AmbFilter(false).apply(rez3);
+    rez2 = new AmbFilter().apply(rez3);
     return rez2._1().right().get();
   }
 }

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

@@ -200,48 +200,37 @@ 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, boolean strict, FileUtil files) {
-    return getCombinedGrammar(mod, strict, false, false, false, files, null, false);
+  public static ParseInModule getCombinedGrammar(Module mod, FileUtil files) {
+    return getCombinedGrammar(mod, false, false, false, files, null, false);
   }
 
   public static ParseInModule getCombinedGrammar(
-      Module mod, boolean strict, FileUtil files, boolean partialParseDebug) {
-    return getCombinedGrammar(mod, strict, false, false, false, files, null, partialParseDebug);
+      Module mod, FileUtil files, boolean partialParseDebug) {
+    return getCombinedGrammar(mod, false, false, false, files, null, partialParseDebug);
   }
 
-  public static ParseInModule getCombinedGrammar(
-      Module mod, boolean strict, boolean timing, FileUtil files) {
-    return getCombinedGrammar(mod, strict, timing, false, false, files, null, false);
+  public static ParseInModule getCombinedGrammar(Module mod, boolean timing, FileUtil files) {
+    return getCombinedGrammar(mod, timing, false, false, files, null, false);
   }
 
   public static ParseInModule getCombinedGrammar(
-      Module mod, boolean strict, boolean timing, FileUtil files, String debugTypeInference) {
-    return getCombinedGrammar(mod, strict, timing, false, false, files, debugTypeInference, false);
+      Module mod, boolean timing, FileUtil files, String debugTypeInference) {
+    return getCombinedGrammar(mod, timing, false, false, files, debugTypeInference, false);
   }
 
   public static ParseInModule getCombinedGrammar(
-      Module mod, boolean strict, boolean timing, boolean isBison, FileUtil files) {
-    return getCombinedGrammar(mod, strict, timing, isBison, false, files, null, false);
+      Module mod, boolean timing, boolean isBison, FileUtil files) {
+    return getCombinedGrammar(mod, timing, isBison, false, files, null, false);
   }
 
   public static ParseInModule getCombinedGrammar(
-      Module mod,
-      boolean strict,
-      boolean timing,
-      boolean isBison,
-      boolean forGlobalScanner,
-      FileUtil files) {
-    return getCombinedGrammar(mod, strict, timing, isBison, forGlobalScanner, files, null, false);
+      Module mod, boolean timing, boolean isBison, boolean forGlobalScanner, FileUtil files) {
+    return getCombinedGrammar(mod, timing, isBison, forGlobalScanner, files, null, false);
   }
 
   public static ParseInModule getCombinedGrammar(
-      Module mod,
-      Scanner scanner,
-      boolean strict,
-      boolean timing,
-      boolean isBison,
-      FileUtil files) {
-    return getCombinedGrammar(mod, scanner, strict, timing, isBison, files, null, false);
+      Module mod, Scanner scanner, boolean timing, boolean isBison, FileUtil files) {
+    return getCombinedGrammar(mod, scanner, timing, isBison, files, null, false);
   }
 
   // the forGlobalScanner flag tells the ParseInModule class not to exclude
@@ -264,35 +253,26 @@ public static ParseInModule getCombinedGrammar(
    */
   public static ParseInModule getCombinedGrammar(
       Module mod,
-      boolean strict,
       boolean timing,
       boolean isBison,
       boolean forGlobalScanner,
       FileUtil files,
       String debugTypeInference,
       boolean partialParseDebug) {
     return new ParseInModule(
-        mod,
-        strict,
-        timing,
-        isBison,
-        forGlobalScanner,
-        files,
-        debugTypeInference,
-        partialParseDebug);
+        mod, timing, isBison, forGlobalScanner, files, debugTypeInference, partialParseDebug);
   }
 
   public static ParseInModule getCombinedGrammar(
       Module mod,
       Scanner scanner,
-      boolean strict,
       boolean timing,
       boolean isBison,
       FileUtil files,
       String debugTypeInference,
       boolean partialParseDebug) {
     return new ParseInModule(
-        mod, scanner, strict, timing, isBison, false, files, debugTypeInference, partialParseDebug);
+        mod, scanner, timing, isBison, false, files, debugTypeInference, partialParseDebug);
   }
 
   public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(

kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java

@@ -17,11 +17,7 @@
 /** Eliminate remaining ambiguities by choosing one of them. */
 public class AmbFilter extends SetsGeneralTransformer<KEMException, KEMException> {
 
-  private final boolean strict;
-
-  public AmbFilter(boolean strict) {
-    this.strict = strict;
-  }
+  public AmbFilter() {}
 
   @Override
   public Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> apply(Ambiguity amb) {
@@ -31,7 +27,7 @@ public Tuple2<Either<Set<KEMException>, Term>, Set<KEMException>> apply(Ambiguit
     for (Term t : amb.items()) {
       candidate = this.apply(t);
       K next =
-          new TreeNodesToKORE(Outer::parseSort, strict)
+          new TreeNodesToKORE(Outer::parseSort)
               .apply(new RemoveBracketVisitor().apply(candidate._1().right().get()));
       if (last != null) {
         if (!last.equals(next)) {

kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java

@@ -17,11 +17,7 @@
 /** Report remaining ambiguities as errors. */
 public class AmbFilterError extends SetsTransformerWithErrors<KEMException> {
 
-  private final boolean strict;
-
-  public AmbFilterError(boolean strict) {
-    this.strict = strict;
-  }
+  public AmbFilterError() {}
 
   @Override
   public Either<Set<KEMException>, Term> apply(Ambiguity amb) {
@@ -34,7 +30,7 @@ public Either<Set<KEMException>, Term> apply(Ambiguity amb) {
         return candidate;
       }
       K next =
-          new TreeNodesToKORE(Outer::parseSort, strict)
+          new TreeNodesToKORE(Outer::parseSort)
               .apply(new RemoveBracketVisitor().apply(candidate.right().get()));
       if (last != null) {
         if (!last.equals(next)) {