diff --git a/k-distribution/include/kframework/ktest.mak b/k-distribution/include/kframework/ktest.mak index d76f3f03a9f..39b371b6ca3 100644 --- a/k-distribution/include/kframework/ktest.mak +++ b/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) diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java index ba8136a20e6..5b227b566dc 100644 --- a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java +++ b/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 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,7 +598,7 @@ private Module resolveNonConfigBubbles(Module module, Scanner scanner, RuleGramm profileRules, files, options.debugTypeInference, - options.typeInferenceMode) + innerParsingOptions.typeInferenceMode) : RuleGrammarGenerator.getCombinedGrammar( cache.module(), scanner, @@ -606,7 +606,7 @@ private Module resolveNonConfigBubbles(Module module, Scanner scanner, RuleGramm 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 res = diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index 23aaf4be5e3..3f865669673 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/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; } diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java index cab42970e4b..f1dea8b64de 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/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, Term>, Set> 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, Term>, Set> parseStringTe } Either, 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()); diff --git a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java index 35f20d563f7..51a5c14eb45 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java +++ b/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,13 +222,20 @@ 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( @@ -229,7 +243,7 @@ public static ParseInModule getCombinedGrammar( boolean timing, FileUtil files, String debugTypeInference, - KompileOptions.TypeInferenceMode typeInferenceMode) { + InnerParsingOptions.TypeInferenceMode typeInferenceMode) { return getCombinedGrammar( mod, timing, false, false, files, debugTypeInference, typeInferenceMode, false); } @@ -237,7 +251,14 @@ public static ParseInModule getCombinedGrammar( 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, diff --git a/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java b/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java index 19dda052663..82cb5634f3b 100644 --- a/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java +++ b/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; }