diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java index db0edf996c9..f8a347e878d 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java @@ -44,7 +44,7 @@ public HaskellBackend( @Override public void accept(Backend.Holder h) { Stopwatch sw = new Stopwatch(globalOptions); - String kore = getKompiledString(h.def, true); + String kore = getKompiledString(h.def); h.def = null; files.saveToKompiled("definition.kore", kore); sw.printIntermediate(" Print definition.kore"); diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java index 7eda4dc7a61..885faba3523 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java @@ -48,18 +48,6 @@ public List, Boolean>> kompileOptions() { return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true)); } - @Override - public List getKRunModules() { - return Collections.singletonList( - new AbstractModule() { - @Override - protected void configure() { - binder().requireAtInjectOnConstructors(); - installHaskellRewriter(binder()); - } - }); - } - private void installHaskellRewriter(Binder binder) { bindOptions(HaskellBackendKModule.this::krunOptions, binder); diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java index 7cbca201265..de397c0f36d 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java @@ -39,7 +39,6 @@ import org.kframework.parser.KoreParser; import org.kframework.parser.kore.parser.ParseError; import org.kframework.rewriter.Rewriter; -import org.kframework.rewriter.SearchType; import org.kframework.unparser.KPrint; import org.kframework.unparser.OutputModes; import org.kframework.utils.RunProcess; @@ -50,7 +49,6 @@ import org.kframework.utils.inject.RequestScoped; import org.kframework.utils.options.BackendOptions; import org.kframework.utils.options.SMTOptions; -import scala.Tuple2; @RequestScoped public record HaskellRewriter( @@ -136,22 +134,12 @@ public RewriterResult execute(K k, Optional depth) { @Override public K match(K k, Rule rule) { - return search(k, Optional.of(0), Optional.empty(), rule, SearchType.STAR); - } - - @Override - public Tuple2 executeAndMatch(K k, Optional depth, Rule rule) { - RewriterResult res = execute(k, depth); - return Tuple2.apply(res, match(res.k(), rule)); + return search(k, Optional.of(0), Optional.empty(), rule); } @Override public K search( - K initialConfiguration, - Optional depth, - Optional bound, - Rule pattern, - SearchType searchType) { + K initialConfiguration, Optional depth, Optional bound, Rule pattern) { Module mod = getExecutionModule(module); String koreOutput = getKoreString( @@ -216,8 +204,7 @@ public K search( pgmPath, "--output", koreOutputFile.getAbsolutePath(), - "--searchType", - searchType.toString(), + "--searchType STAR", "--search", patternPath)); if (depth.isPresent()) { @@ -378,7 +365,7 @@ private RewriterResult executeKoreCommands( @Override public RewriterResult prove(Module rules, Boolean reuseDef) { - Module kompiledModule = KoreBackend.getKompiledModule(module, true); + Module kompiledModule = KoreBackend.getKompiledModule(module); ModuleToKORE converter = new ModuleToKORE( kompiledModule, @@ -424,12 +411,6 @@ public RewriterResult prove(Module rules, Boolean reuseDef) { return executeKoreCommands(rules, koreCommand, koreDirectory, koreOutputFile); } - - @Override - public boolean equivalence( - Rewriter firstDef, Rewriter secondDef, Module firstSpec, Module secondSpec) { - throw new UnsupportedOperationException(); - } }; } diff --git a/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java b/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java index f873cd0580d..3f712149226 100644 --- a/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java +++ b/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java @@ -99,7 +99,6 @@ protected DefinitionWithContext parseUsingOuter(File definitionFile) { } def.setItems(Outer.parse(Source.apply(definitionFile.getPath()), definitionText, null)); def.setMainModule("TEST"); - def.setMainSyntaxModule("TEST"); ProcessGroupAttributes.apply(def); Context context = new Context(); diff --git a/k-distribution/src/test/java/org/kframework/kore/convertors/TstKILtoKOREIT.java b/k-distribution/src/test/java/org/kframework/kore/convertors/TstKILtoKOREIT.java index 50ed558136e..1e8444c6f7d 100644 --- a/k-distribution/src/test/java/org/kframework/kore/convertors/TstKILtoKOREIT.java +++ b/k-distribution/src/test/java/org/kframework/kore/convertors/TstKILtoKOREIT.java @@ -60,7 +60,7 @@ public void syntaxWithOR() throws IOException { } protected String convert(DefinitionWithContext defWithContext) { - KILtoKORE kilToKore = new KILtoKORE(defWithContext.context, false, false); + KILtoKORE kilToKore = new KILtoKORE(defWithContext.context, false); org.kframework.definition.Definition koreDef = kilToKore.apply(defWithContext.definition); String koreDefString = koreDef.toString(); return koreDefString; diff --git a/kernel/src/main/java/org/kframework/backend/Backends.java b/kernel/src/main/java/org/kframework/backend/Backends.java index d05b6224b61..5535d3711d6 100644 --- a/kernel/src/main/java/org/kframework/backend/Backends.java +++ b/kernel/src/main/java/org/kframework/backend/Backends.java @@ -2,9 +2,6 @@ package org.kframework.backend; public class Backends { - - public static final String PDF = "pdf"; - public static final String HTML = "html"; public static final String HASKELL = "haskell"; public static final String LLVM = "llvm"; } diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java index 1e1e1ec6418..15b89c6bb6f 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java +++ b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java @@ -27,7 +27,7 @@ import org.kframework.utils.file.FileUtil; import scala.Function1; -public class KoreBackend extends AbstractBackend { +public class KoreBackend implements Backend { private final KompileOptions kompileOptions; protected final FileUtil files; @@ -57,20 +57,16 @@ public KoreBackend( @Override public void accept(Backend.Holder h) { CompiledDefinition def = h.def; - String kore = getKompiledString(def, true); + String kore = getKompiledString(def); File defFile = kompileOptions.outerParsing.mainDefinitionFile(files); String name = defFile.getName(); String basename = FilenameUtils.removeExtension(name); files.saveToDefinitionDirectory(basename + ".kore", kore); } - /** - * Convert a CompiledDefinition to a String of a KORE definition. - * - * @param hasAnd whether the backend in question supports and-patterns during pattern matching. - */ - protected String getKompiledString(CompiledDefinition def, boolean hasAnd) { - Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule(), hasAnd); + /** Convert a CompiledDefinition to a String of a KORE definition. */ + protected String getKompiledString(CompiledDefinition def) { + Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule()); ModuleToKORE converter = new ModuleToKORE(mainModule, def.topCellInitializer, def.kompileOptions); return getKompiledString(converter, files, heatCoolEquations, tool); @@ -98,7 +94,7 @@ public static String getKompiledStringAndWriteSyntaxMacros( return semantics.toString(); } - public static Module getKompiledModule(Module mainModule, boolean hasAnd) { + public static Module getKompiledModule(Module mainModule) { mainModule = ModuleTransformer.fromSentenceTransformer( new AddSortInjections(mainModule)::addInjections, "Add sort injections") @@ -106,12 +102,10 @@ public static Module getKompiledModule(Module mainModule, boolean hasAnd) { mainModule = ModuleTransformer.from(new RemoveUnit()::apply, "Remove unit applications for collections") .apply(mainModule); - if (hasAnd) { - mainModule = - ModuleTransformer.fromSentenceTransformer( - new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction") - .apply(mainModule); - } + mainModule = + ModuleTransformer.fromSentenceTransformer( + new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction") + .apply(mainModule); return mainModule; } @@ -123,8 +117,7 @@ public Function steps() { Function1 resolveStrict = d -> DefinitionTransformer.from( - new ResolveStrict(kompileOptions, d)::resolve, - "resolving strict and seqstrict attributes") + new ResolveStrict(d)::resolve, "resolving strict and seqstrict attributes") .apply(d); DefinitionTransformer resolveHeatCoolAttribute = DefinitionTransformer.fromSentenceTransformer( @@ -240,7 +233,7 @@ public Function steps() { .andThen(resolveFunctionWithConfig) .andThen(resolveStrict) .andThen(resolveAnonVars) - .andThen(d -> new ResolveContexts(kompileOptions).resolve(d)) + .andThen(d -> new ResolveContexts().resolve(d)) .andThen(numberSentences) .andThen(resolveHeatCoolAttribute) .andThen(resolveSemanticCasts) diff --git a/kernel/src/main/java/org/kframework/compile/AbstractBackend.java b/kernel/src/main/java/org/kframework/compile/AbstractBackend.java deleted file mode 100644 index 30e4b2b9ff4..00000000000 --- a/kernel/src/main/java/org/kframework/compile/AbstractBackend.java +++ /dev/null @@ -1,22 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.compile; - -import java.util.List; -import java.util.function.Function; -import javax.annotation.Nullable; -import org.kframework.definition.Definition; -import scala.Function1; - -/** - * @author Denis Bogdanas Created on 09-Jan-20. - */ -public abstract class AbstractBackend implements Backend { - - @Override - public Function proofDefinitionNonCachedSteps( - @Nullable List extraConcreteRuleLabels) { - Function1 markExtraConcrete = - def -> MarkExtraConcreteRules.mark(def, extraConcreteRuleLabels); - return markExtraConcrete::apply; - } -} diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java index 12e80a7e3f3..dd91256e4da 100644 --- a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java +++ b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java @@ -27,15 +27,6 @@ public static Definition transformDefinition(Definition input) { .apply(input); } - public static Module transformModule(Module mod) { - ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod); - LabelInfo labelInfo = new LabelInfoFromModule(mod); - return ModuleTransformer.fromSentenceTransformer( - new AddImplicitComputationCell(configInfo, labelInfo)::apply, - "concretizing configuration") - .apply(mod); - } - public Sentence apply(Module m, Sentence s) { if (skipSentence(s)) { return s; diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java index db24d9d9a95..e6e89cbb50c 100644 --- a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java +++ b/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java @@ -7,7 +7,6 @@ import java.util.*; import org.kframework.builtin.KLabels; import org.kframework.definition.Claim; -import org.kframework.definition.Module; import org.kframework.definition.Sentence; import org.kframework.kore.*; @@ -19,7 +18,7 @@ public class AddImplicitCounterCell { public AddImplicitCounterCell() {} - public Sentence apply(Module m, Sentence s) { + public Sentence apply(Sentence s) { if (s instanceof Claim claim) { Set freshVars = new HashSet<>(); VisitK visitor = @@ -36,8 +35,7 @@ public void apply(KVariable var) { if (!ConcretizeCells.hasCells(claim.body()) && freshVars.isEmpty()) { return s; } - return claim.newInstance( - apply(claim.body(), m), claim.requires(), claim.ensures(), claim.att()); + return claim.newInstance(apply(claim.body()), claim.requires(), claim.ensures(), claim.att()); } return s; } @@ -50,7 +48,7 @@ private boolean alreadyHasGeneratedCounter(List items) { .anyMatch(cell -> ((KApply) cell).klabel().equals(KLabels.GENERATED_COUNTER_CELL)); } - private K apply(K term, Module m) { + private K apply(K term) { List items = IncompleteCellUtils.flattenCells(term); if (alreadyHasGeneratedCounter(items)) { return term; diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java index e081913e216..c3a07a6db18 100644 --- a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java +++ b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java @@ -15,12 +15,10 @@ import java.util.Set; import java.util.function.BiFunction; import java.util.stream.Collectors; -import java.util.stream.IntStream; import org.kframework.Collections; import org.kframework.attributes.Att; import org.kframework.attributes.HasLocation; import org.kframework.builtin.Sorts; -import org.kframework.definition.Context; import org.kframework.definition.Module; import org.kframework.definition.NonTerminal; import org.kframework.definition.Production; @@ -40,7 +38,6 @@ import org.kframework.parser.outer.Outer; import org.kframework.utils.errorsystem.KEMException; import scala.Option; -import scala.Tuple2; public class AddSortInjections { @@ -174,7 +171,6 @@ private K internalAddSortInjections(K term, Sort expectedSort) { adjustedExpectedSort = k.att().get(Sort.class); } Production prod = production(k); - List children = new ArrayList<>(); Production substituted = substituteProd( prod, @@ -206,13 +202,6 @@ private K internalAddSortInjections(K term, Sort expectedSort) { } } - private Context addInjections(Context context) { - return new Context( - internalAddSortInjections(context.body(), Sorts.K()), - internalAddSortInjections(context.requires(), Sorts.Bool()), - context.att()); - } - private void initSortParams() { freshSortParamCounter = 0; sortParams.clear(); @@ -355,14 +344,6 @@ private void match( } } - private Set getPositions(Sort param, Production prod) { - return IntStream.range(0, prod.nonterminals().size()) - .mapToObj(i -> Tuple2.apply(prod.nonterminals().apply(i), i)) - .filter(t -> t._1().sort().equals(param)) - .map(t -> t._2()) - .collect(Collectors.toSet()); - } - /** * Compute the sort of a term in a context where there is no expected sort, i.e., at the top of a * rule body. diff --git a/kernel/src/main/java/org/kframework/compile/Backend.java b/kernel/src/main/java/org/kframework/compile/Backend.java index a5a3db6ebef..2995883b5f6 100644 --- a/kernel/src/main/java/org/kframework/compile/Backend.java +++ b/kernel/src/main/java/org/kframework/compile/Backend.java @@ -1,10 +1,8 @@ // Copyright (c) Runtime Verification, Inc. All Rights Reserved. package org.kframework.compile; -import java.util.List; import java.util.Set; import java.util.function.Function; -import javax.annotation.Nullable; import org.kframework.attributes.Att; import org.kframework.definition.Definition; import org.kframework.definition.Module; @@ -26,9 +24,6 @@ public Holder(CompiledDefinition def) { Function steps(); - Function proofDefinitionNonCachedSteps( - @Nullable List extraConcreteRuleLabels); - Function specificationSteps(Definition def); Set excludedModuleTags(); diff --git a/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java b/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java index 146eb04b30f..d68a322205b 100644 --- a/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java +++ b/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java @@ -6,7 +6,6 @@ import edu.uci.ics.jung.graph.DirectedGraph; import edu.uci.ics.jung.graph.DirectedSparseGraph; import java.util.Collection; -import java.util.Collections; import java.util.HashSet; import java.util.LinkedHashSet; import java.util.LinkedList; @@ -99,10 +98,6 @@ private static Set ancestors( return visited; } - public Set ancestors(KLabel label) { - return ancestors(Collections.singleton(label), dependencies); - } - public Set ancestors(Set labels) { return ancestors(labels, dependencies); } diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java b/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java index 7c035db1873..506f55378e8 100644 --- a/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java +++ b/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java @@ -25,10 +25,6 @@ public Sort getCellSort(K k) { } } - public ConfigurationInfo.Multiplicity getMultiplicity(KLabel label) { - return cfg.getMultiplicity(labels.getCodomain(label)); - } - public ConfigurationInfo.Multiplicity getMultiplicity(Sort sort) { return cfg.getMultiplicity(sort); } @@ -72,11 +68,6 @@ public K getCellAbsentTerm(Sort cellSort) { return l == null ? null : KApply(l); } - public boolean isCellCollection(KLabel klabel) { - Sort s = labels.getCodomain(klabel); - return cfg.isCellCollection(s); - } - public boolean isCell(KLabel klabel) { Sort s = labels.getCodomain(klabel); return cfg.isCell(s) && cfg.getCellLabel(s).equals(klabel); diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java b/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java index 26a68011f69..a43dc47f01d 100644 --- a/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java +++ b/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java @@ -41,16 +41,6 @@ public static Definition transformDefinition(Definition input) { .apply(input); } - public static Module transformModule(Module mod) { - ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod); - LabelInfo labelInfo = new LabelInfoFromModule(mod); - SortInfo sortInfo = SortInfo.fromModule(mod); - return ModuleTransformer.fromSentenceTransformer( - new ConcretizeCells(configInfo, labelInfo, sortInfo, mod)::concretize, - "concretizing configuration") - .apply(mod); - } - public ConcretizeCells( ConfigurationInfo configurationInfo, LabelInfo labelInfo, SortInfo sortInfo, Module module) { this.configurationInfo = configurationInfo; diff --git a/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java b/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java index d0a40a55a5b..b1bb9387f58 100644 --- a/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java +++ b/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java @@ -5,39 +5,13 @@ import static org.kframework.definition.Constructors.*; import static org.kframework.kore.KORE.*; -import com.google.common.collect.HashMultiset; -import com.google.common.collect.Lists; -import com.google.common.collect.Multiset; -import java.util.ArrayList; -import java.util.Collections; import java.util.HashSet; -import java.util.LinkedHashMap; -import java.util.LinkedHashSet; -import java.util.List; import java.util.Map; -import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; -import java.util.stream.Stream; -import org.kframework.TopologicalSort; import org.kframework.attributes.Att; -import org.kframework.builtin.BooleanUtils; -import org.kframework.builtin.KLabels; -import org.kframework.builtin.Sorts; -import org.kframework.definition.Context; import org.kframework.definition.Module; -import org.kframework.definition.Rule; -import org.kframework.definition.Sentence; -import org.kframework.kore.Assoc; -import org.kframework.kore.FoldK; -import org.kframework.kore.K; -import org.kframework.kore.KApply; import org.kframework.kore.KLabel; -import org.kframework.kore.KRewrite; -import org.kframework.kore.KVariable; -import org.kframework.kore.TransformK; -import org.kframework.kore.VisitK; -import org.kframework.utils.errorsystem.KEMException; import scala.Tuple2; /** @@ -66,32 +40,6 @@ * ordinary map. */ public class ConvertDataStructureToLookup { - - private final Set state = new HashSet<>(); - private final Multiset vars = HashMultiset.create(); - - void reset() { - state.clear(); - vars.clear(); - counter = 0; - } - - private final Module m; - private final Map collectionFor; - private final boolean matchOnConsList; - - public ConvertDataStructureToLookup(Module m, boolean matchOnConsList) { - this.m = m; - collectionFor = collectionFor(m); - this.matchOnConsList = matchOnConsList; - } - - public ConvertDataStructureToLookup(ConvertDataStructureToLookup copy) { - this.m = copy.m; - this.collectionFor = copy.collectionFor; - this.matchOnConsList = copy.matchOnConsList; - } - public static Map collectionFor(Module m) { return stream(m.productions()) .filter(p -> p.att().contains(Att.ASSOC()) && p.att().contains(Att.ELEMENT())) @@ -116,588 +64,4 @@ public static Map collectionFor(Module m) { .distinct() .collect(Collectors.toMap(Tuple2::_1, Tuple2::_2)); } - - public static Set filteredMapConstructors(Module m) { - return stream(m.productions()) - .filter(p -> p.att().contains(Att.ASSOC()) && p.att().contains(Att.FILTER_ELEMENT())) - .map(p -> p.klabel().get()) - .collect(Collectors.toSet()); - } - - private Rule convert(Rule rule) { - reset(); - gatherVars(rule.body(), vars); - gatherVars(rule.requires(), vars); - gatherVars(rule.ensures(), vars); - K body = transform(rule.body()); - return Rule(body, addSideCondition(rule.requires()), rule.ensures(), rule.att()); - } - - private Context convert(Context context) { - reset(); - gatherVars(context.body(), vars); - gatherVars(context.requires(), vars); - K body = transform(context.body()); - return new Context(body, addSideCondition(context.requires()), context.att()); - } - - /** Collects all the variables in {@code term} into {@code vars}. */ - void gatherVars(K term, Multiset vars) { - new VisitK() { - @Override - public void apply(KVariable v) { - vars.add(v); - super.apply(v); - } - }.apply(term); - } - - /** - * Adds lookups to the side condition in sorted order in which they must be performed. Lookups are - * sorted based on dependencies between each other, but non-lookup operations appear in no - * particular order with respect to the lookups. - * - * @param requires Previous side condition, if any. - * @return Side condition generated by this compiler pass + previous side condition. - */ - K addSideCondition(K requires) { - Optional sideCondition = getSortedLookups().reduce(BooleanUtils::and); - if (sideCondition.isEmpty()) { - return requires; - } else if (requires.equals(BooleanUtils.TRUE) && sideCondition.isPresent()) { - return sideCondition.get(); - } else { - // we order lookups before the requires clause so that the fresh constant - // matching side condition remains last. This is necessary in order to - // ensure that fresh constants in rule RHSs are consecutive - return BooleanUtils.and(sideCondition.get(), requires); - } - } - - /** - * Sorts lookups based on their dependencies with each other. Non-lookups (i.e. everything except - * #match, #setChoice, and #mapChoice) are in no particular order in this ordering, since they can - * always be inferred later to occur at the final step after all other variables are bound. - * - * @return - */ - private Stream getSortedLookups() { - List> edges = new ArrayList<>(); - for (KApply k1 : state) { - Multiset rhsVars = HashMultiset.create(); - if (k1.klabel().name().equals("Set:in")) { - continue; - } - gatherVars(k1.klist().items().get(1), rhsVars); - for (KApply k2 : state) { - Multiset lhsVars = HashMultiset.create(); - if (k2.klabel().name().equals("Set:in")) { - continue; - } - gatherVars(k2.klist().items().get(0), lhsVars); - for (KVariable var : rhsVars) { - if (lhsVars.contains(var)) { - if (k1 != k2) { - edges.add(Tuple2.apply(k2, k1)); - break; - } - } - } - } - } - List topologicalSorted = mutable(TopologicalSort.tsort(immutable(edges)).toList()); - return state.stream() - .sorted((k1, k2) -> (topologicalSorted.indexOf(k1) - topologicalSorted.indexOf(k2))); - } - - private int counter = 0; - - KVariable newDotVariable() { - KVariable newLabel; - do { - newLabel = KVariable("_Gen" + (counter++)); - } while (vars.contains(newLabel)); - vars.add(newLabel); - return newLabel; - } - - /** - * For the cell bag sorts with multiplicity *, add the single-element wrapper around individual - * cells. - */ - private K infer(K term) { - return new TransformK() { - @Override - public K apply(KApply k) { - for (KLabel collectionLabel : collectionFor.keySet()) { - Optional wrapElement = - m.attributesFor().apply(collectionLabel).getOptional(Att.WRAP_ELEMENT()); - if (wrapElement.isPresent()) { - KLabel wrappedLabel = KLabel(wrapElement.get()); - KLabel elementLabel = - KLabel(m.attributesFor().apply(collectionLabel).get(Att.ELEMENT())); - if (k.klabel().equals(elementLabel)) { - return k; - } - if (k.klabel().equals(wrappedLabel)) { - if (collectionIsMap(collectionLabel)) { - // Map - return KApply(elementLabel, super.apply(k.klist().items().get(0)), super.apply(k)); - } else { - return KApply(elementLabel, super.apply(k)); - } - } - } - } - return super.apply(k); - } - }.apply(term); - } - - public boolean collectionIsMap(KLabel collectionLabel) { - return m.attributesFor().apply(collectionLabel).contains(Att.COMM()) - && !m.attributesFor().apply(collectionLabel).contains(Att.IDEM()) - && !m.attributesFor().apply(collectionLabel).contains(Att.BAG()); - } - - private boolean isThread = false; - - private K transform(K body) { - if (body instanceof KRewrite - && ((KRewrite) body).left() instanceof KApply - && collectionFor.containsKey(((KApply) ((KRewrite) body).left()).klabel())) { - // this is a rule intended to implement one of the collection operations; do not transform it. - return body; - } - // maintain the list of variables in the term so that we can deduce that a particular variable - // is unconstrained - Multiset varConstraints = HashMultiset.create(); - gatherVars(RewriteToTop.toLeft(body), varConstraints); - return new TransformK() { - public K apply(KApply k) { - if (KLabels.KSEQ.equals(k.klabel())) return super.apply(k); - if (k.klabel().name().equals("#Thread")) { - K global = apply(k.klist().items().get(0)); - K id = apply(k.klist().items().get(1)); - isThread = true; - K thread = apply(k.klist().items().get(2)); - isThread = false; - K otherThreads = apply(k.klist().items().get(3)); - return KApply(k.klabel(), global, id, thread, otherThreads); - } - - if (collectionFor.containsKey(k.klabel())) { - if (isThread) { - isThread = false; - K res = super.apply(k); - isThread = true; - return res; - } else { - KLabel collectionLabel = collectionFor.get(k.klabel()); - Att att = m.attributesFor().apply(collectionLabel); - // assumed assoc - KApply left = (KApply) RewriteToTop.toLeft(k); - List components = Assoc.flatten(collectionLabel, Collections.singletonList(left), m); - if (att.contains(Att.COMM())) { - if (att.contains(Att.IDEM())) { - // Set - return convertSet(k, collectionLabel, components); - } else { - if (att.contains(Att.BAG())) - // Bag - // TODO(dwightguth): handle bags - return super.apply(k); - else - // Map - return convertMap(k, collectionLabel, components, varConstraints); - } - } else { - // List - return convertList(k, collectionLabel, components); - } - } - } else { - return super.apply(k); - } - } - - /** - * Convert a list pattern, requiring that there is at most one list variable component. - * Individual items may appear before and after the frame variable, which can be translated - * into efficient operatations at the beginning and end of the list. - */ - private K convertList(KApply k, KLabel collectionLabel, List components) { - if (rhsOf == null) { - // left hand side - KVariable frame = null; - List elementsLeft = new ArrayList(); - List elementsRight = new ArrayList(); - KLabel elementLabel = KLabel(m.attributesFor().apply(collectionLabel).get(Att.ELEMENT())); - boolean isRight = false; // true for components later than the frame variable. - // build the components of the list from the flattened KApply. - for (K component : components) { - if (component instanceof KVariable) { - if (frame != null) { - throw KEMException.internalError( - "Unsupported associative matching on List. Found variables " - + component - + " and " - + frame, - k); - } - frame = (KVariable) component; - isRight = true; - } else if (component instanceof KApply kapp) { - boolean needsWrapper = false; - if (kapp.klabel().equals(elementLabel) - || (needsWrapper = kapp.klabel().equals(getWrapElement(collectionLabel)))) { - if (kapp.klist().size() != 1 && !needsWrapper) { - throw KEMException.internalError( - "Unexpected arity of list element: " + kapp.klist().size(), kapp); - } - K stack = lhsOf; - // setting lhsOf prevents inner lists from being translated to rewrites, - lhsOf = kapp; - - // overloading means the following two apply functions are actually different - // methods - (isRight ? elementsRight : elementsLeft) - .add( - needsWrapper - ? super.apply(kapp) - : super.apply(kapp.klist().items().get(0))); - - lhsOf = stack; - } else { - throw KEMException.internalError( - "Unexpected term in list, not a list element.", kapp); - } - } - } - K list; - if (elementsRight.size() == 0 && matchOnConsList) { - K tail; - if (frame == null) { - tail = KApply(KLabel(m.attributesFor().apply(collectionLabel).get(Att.UNIT()))); - } else { - tail = frame; - } - list = - Lists.reverse(elementsLeft).stream() - .map(e -> (K) KApply(elementLabel, e)) - .reduce(tail, (res, el) -> KApply(collectionLabel, el, res)); - } else { - list = newDotVariable(); - // Ctx[ListItem(5) Frame ListItem(X) ListItem(foo(Y))] => Ctx [L] - // requires Frame := range(L, 1, 2) - // andBool 5 := L[0] - // andBool X := L[-2] - // andBool foo(Y) := L[-1] - if (frame != null) { - state.add( - KApply( - KLabel("#match"), - frame, - KApply( - KLabel("List:range"), - list, - KToken(Integer.toString(elementsLeft.size()), Sorts.Int()), - KToken(Integer.toString(elementsRight.size()), Sorts.Int())))); - } else { - KLabel unit = KLabel(m.attributesFor().apply(collectionLabel).get(Att.UNIT())); - // Ctx[.List] => Ctx[L] requires L ==K range(L, 0, 0) - state.add( - KApply( - KLabel("_==K_"), - KApply(unit), - KApply( - KLabel("List:range"), - list, - KToken(Integer.toString(elementsLeft.size()), Sorts.Int()), - KToken(Integer.toString(elementsRight.size()), Sorts.Int())))); - } - for (int i = 0; i < elementsLeft.size(); i++) { - K element = elementsLeft.get(i); - state.add( - KApply( - KLabel("#match"), - element, - KApply(KLabel("List:get"), list, KToken(Integer.toString(i), Sorts.Int())))); - } - for (int i = 0; i < elementsRight.size(); i++) { - K element = elementsRight.get(i); - state.add( - KApply( - KLabel("#match"), - element, - KApply( - KLabel("List:get"), - list, - KToken(Integer.toString(i - elementsRight.size()), Sorts.Int())))); - } - } - if (lhsOf == null) { - if (!hasRewrite(k)) { - return list; - } - // An outermost list may contain nested rewrites, so the term - // is translated into a rewrite from compiled match into the original right-hand side. - return KRewrite(list, infer(RewriteToTop.toRight(k))); - } else { - return list; - } - } else { - return infer(super.apply(k)); - } - } - - /** - * Convert a map pattern, requiring that there is at most one map variable component. Map keys - * must either be a variable, or bound elsewhere in the rule. Map value patterns become - * additional matching constraints on lookups in the map. - */ - private K convertMap( - KApply k, - KLabel collectionLabel, - List components, - Multiset varConstraints) { - if (rhsOf == null) { - // left hand side - KVariable frame = null; - Map elements = new LinkedHashMap<>(); - // build the components of the map from the flattened KApply. - for (K component : components) { - if (component instanceof KVariable) { - if (frame != null) { - throw KEMException.internalError( - "Unsupported associative matching on Map. Found variables " - + component - + " and " - + frame, - k); - } - frame = (KVariable) component; - } else if (component instanceof KApply kapp) { - - boolean needsWrapper = false; - if (kapp.klabel() - .equals(KLabel(m.attributesFor().apply(collectionLabel).get(Att.ELEMENT()))) - || (needsWrapper = kapp.klabel().equals(getWrapElement(collectionLabel)))) { - if (kapp.klist().size() != 2 && !needsWrapper) { - throw KEMException.internalError( - "Unexpected arity of map element: " + kapp.klist().size(), kapp); - } - K stack = lhsOf; - // setting lhsOf prevents inner lists from being translated to rewrites, - lhsOf = kapp; - - elements.put( - super.apply(kapp.klist().items().get(0)), - needsWrapper ? super.apply(kapp) : super.apply(kapp.klist().items().get(1))); - - lhsOf = stack; - } else { - throw KEMException.internalError( - "Unexpected term in map, not a map element.", kapp); - } - } - } - KVariable map = newDotVariable(); - // K1,Ctx[K1 |-> K2 K3] => K1,Ctx[M] requires K3 := M[K1<-undef] andBool K1 := choice(M) - // andBool K2 := M[K1] - KLabel remove = - KLabel( - m.attributesFor() - .apply(collectionLabel) - .getOptional(Att.REMOVE()) - .orElse("_[_<-undef]")); - if (frame != null) { - state.add( - KApply( - KLabel("#match"), - frame, - elements.keySet().stream().reduce(map, (a1, a2) -> KApply(remove, a1, a2)))); - } else { - KLabel unit = KLabel(m.attributesFor().apply(collectionLabel).get(Att.UNIT())); - state.add( - KApply( - KLabel("_==K_"), - KApply(unit), - elements.keySet().stream().reduce(map, (a1, a2) -> KApply(remove, a1, a2)))); - } - for (Map.Entry element : elements.entrySet()) { - // TODO(dwightguth): choose better between lookup and choice. - if (element.getKey() instanceof KVariable - && varConstraints.count(element.getKey()) == 1) { - state.add(KApply(KLabel("#mapChoice"), element.getKey(), map)); - } - state.add( - KApply( - KLabel("#match"), - element.getValue(), - KApply(KLabel("Map:lookup"), map, element.getKey()))); - } - if (lhsOf == null) { - if (!hasRewrite(k)) { - return map; - } - // An outermost map may contain nested rewrites, so the term - // is translated into a rewrite from compiled match into the original right-hand side. - return KRewrite(map, infer(RewriteToTop.toRight(k))); - } else { - return map; - } - } else { - return infer(super.apply(k)); - } - } - - private KLabel getWrapElement(KLabel collectionLabel) { - return KLabel(m.attributesFor().apply(collectionLabel).get(Att.WRAP_ELEMENT())); - } - - /** - * Convert a set pattern, requiring that there is at most one set variable component. Set - * elements without variables become membership checks in the map, whereas Set elements with - * variables trigger iteration over the set with matching on each element. - */ - private K convertSet(KApply k, KLabel collectionLabel, List components) { - if (rhsOf == null) { - // left hand side - KVariable frame = null; - Set elements = new LinkedHashSet<>(); - KLabel elementLabel = KLabel(m.attributesFor().apply(collectionLabel).get(Att.ELEMENT())); - // build the components of the set from the flattened KApply. - for (K component : components) { - if (component instanceof KVariable) { - if (frame != null) { - throw KEMException.internalError( - "Unsupported associative matching on Set. Found variables " - + component - + " and " - + frame, - k); - } - frame = (KVariable) component; - } else if (component instanceof KApply kapp) { - - boolean needsWrapper = false; - if (kapp.klabel().equals(elementLabel) - || (needsWrapper = kapp.klabel().equals(getWrapElement(collectionLabel)))) { - if (kapp.klist().size() != 1 && !needsWrapper) { - throw KEMException.internalError( - "Unexpected arity of set element: " + kapp.klist().size(), kapp); - } - K stack = lhsOf; - // setting lhsOf prevents inner lists from being translated to rewrites, - lhsOf = kapp; - - // overloading means the following two apply functions are actually different - // methods - elements.add( - needsWrapper ? super.apply(kapp) : super.apply(kapp.klist().items().get(0))); - - lhsOf = stack; - } else { - throw KEMException.internalError( - "Unexpected term in set, not a set element.", kapp); - } - } - } - KVariable set = newDotVariable(); - K accum = set; - // Ctx[SetItem(K1) K2] => Ctx[S] requires K1 := choice(S) andBool K2 := S -Set SetItem(K1) - // Ctx[SetItem(5) SetItem(6) K] => Ctx[S] requires 5 in S andBool 6 in S andBool K := S - // -Set SetItem(5) SetItem(6) - for (K element : elements) { - // TODO(dwightguth): choose better between lookup and choice. - Multiset vars = HashMultiset.create(); - gatherVars(element, vars); - if (vars.isEmpty()) { - state.add(KApply(KLabel("Set:in"), element, accum)); - } else { - // set choice - state.add(KApply(KLabel("#setChoice"), element, accum)); - } - accum = KApply(KLabel("Set:difference"), accum, KApply(elementLabel, element)); - } - KLabel unit = KLabel(m.attributesFor().apply(collectionLabel).get(Att.UNIT())); - if (frame != null) { - state.add(KApply(KLabel("#match"), frame, accum)); - } else { - state.add(KApply(KLabel("_==K_"), KApply(unit), accum)); - } - if (lhsOf == null) { - if (!hasRewrite(k)) { - return set; - } - // An outermost set may contain nested rewrites, so the term - // is translated into a rewrite from compiled match into the original right-hand side. - return KRewrite(set, infer(RewriteToTop.toRight(k))); - } else { - return set; - } - } else { - return infer(super.apply(k)); - } - } - - private K lhsOf; - private K rhsOf; - - @Override - public K apply(KRewrite k) { - lhsOf = k; - K l = apply(k.left()); - lhsOf = null; - rhsOf = k; - K r = apply(k.right()); - rhsOf = null; - if (l != k.left() || r != k.right()) { - return KRewrite(l, r, k.att()); - } else { - return k; - } - } - }.apply(body); - } - - private Boolean hasRewrite(KApply k) { - return new FoldK() { - public Boolean unit() { - return false; - } - - public Boolean merge(Boolean a, Boolean b) { - return a || b; - } - - public Boolean apply(KRewrite rew) { - return true; - } - }.apply(k); - } - - public Sentence convert(Sentence s) { - if (s.att().contains(Att.SMT_LEMMA()) || s.att().contains(Att.PATTERN_FOLDING())) { - return s; - } else if (s instanceof Rule) { - return convert((Rule) s); - } else if (s instanceof Context) { - return convert((Context) s); - } else { - return s; - } - } - - public static boolean isLookupKLabel(KLabel k) { - return k.name().equals("#match") - || k.name().equals("#mapChoice") - || k.name().equals("#filterMapChoice") - || k.name().equals("#setChoice"); - } - - public static boolean isLookupKLabel(KApply k) { - return isLookupKLabel(k.klabel()); - } } diff --git a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java index 02c0441d7bd..f9747fa232b 100644 --- a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java +++ b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java @@ -67,18 +67,8 @@ public class ExpandMacros { private final FileChannel channel; private final boolean reverse; private final ResolveFunctionWithConfig transformer; - private final KompileOptions kompileOptions; private final KExceptionManager kem; - public static ExpandMacros fromMainModule( - Module mod, - FileUtil files, - KExceptionManager kem, - KompileOptions kompileOptions, - boolean reverse) { - return new ExpandMacros(mod, files, kem, kompileOptions, reverse, true); - } - public static ExpandMacros forNonSentences( Module mod, FileUtil files, KompileOptions kompileOptions, boolean reverse) { return new ExpandMacros(mod, files, null, kompileOptions, reverse, false); @@ -110,7 +100,6 @@ public ExpandMacros( this.mod = mod; this.reverse = reverse; this.cover = kompileOptions.coverage; - this.kompileOptions = kompileOptions; this.kem = kem; files.resolveKompiled(".").mkdirs(); List allMacros = @@ -459,7 +448,7 @@ public Sentence expand(Sentence s) { } else if (s instanceof Claim) { return transformer.resolve(expand((Claim) s), mod); } else if (s instanceof Context) { - return transformer.resolve(expand((Context) s), mod); + return transformer.resolve(expand((Context) s)); } else { return s; } diff --git a/kernel/src/main/java/org/kframework/compile/GatherVarsVisitor.java b/kernel/src/main/java/org/kframework/compile/GatherVarsVisitor.java index 59cc2fc2032..6b868ec18d5 100644 --- a/kernel/src/main/java/org/kframework/compile/GatherVarsVisitor.java +++ b/kernel/src/main/java/org/kframework/compile/GatherVarsVisitor.java @@ -17,7 +17,7 @@ public class GatherVarsVisitor extends RewriteAwareVisitor { public GatherVarsVisitor( boolean isBody, Set errors, Set vars, boolean errorExistential) { - super(isBody, errors); + super(isBody); this.errors = errors; this.vars = vars; this.errorExistential = errorExistential; diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java index 258c690bcbd..6014fc5e07f 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java @@ -98,8 +98,7 @@ private static Tuple4, List, K, Boolean> genInternal( if (startLabel instanceof KToken label) { if (label.sort().equals(Sort("#CellName"))) { String cellName = label.s(); - Att cellProperties = - getCellPropertiesAsAtt(kapp.klist().items().get(1), cellName, ensures); + Att cellProperties = getCellPropertiesAsAtt(kapp.klist().items().get(1), cellName); Multiplicity multiplicity = convertStringMultiplicity(cellProperties.getOption(Att.MULTIPLICITY()), term); boolean isStream = cellProperties.getOption(Att.STREAM()).isDefined(); @@ -203,13 +202,13 @@ private static Tuple4, List, K, Boolean> genInternal( // particular sort. // A leaf cell initializes to the value specified in the configuration declaration. Sort sort = kapp.att().get(Production.class).sort(); - Tuple2> res = getLeafInitializer(term, m); + Tuple2> res = getLeafInitializer(term); return Tuple4.apply(res._2(), Lists.newArrayList(sort), res._1(), true); } else if (term instanceof KToken ktoken) { // child of a leaf cell. Generate no productions, but inform parent that it has a child of a // particular sort. // A leaf cell initializes to the value specified in the configuration declaration. - Tuple2> res = getLeafInitializer(term, m); + Tuple2> res = getLeafInitializer(term); return Tuple4.apply(res._2(), Lists.newArrayList(ktoken.sort()), res._1(), true); } else if (term instanceof KSequence || term instanceof KVariable @@ -217,7 +216,7 @@ private static Tuple4, List, K, Boolean> genInternal( // child of a leaf cell. Generate no productions, but inform parent that it has a child of a // particular sort. // A leaf cell initializes to the value specified in the configuration declaration. - Tuple2> res = getLeafInitializer(term, m); + Tuple2> res = getLeafInitializer(term); return Tuple4.apply(res._2(), Lists.newArrayList(Sorts.K()), res._1(), true); } else { throw KEMException.compilerError( @@ -300,7 +299,7 @@ public void apply(KVariable k) { * @param leafContents * @return */ - private static Tuple2> getLeafInitializer(K leafContents, Module m) { + private static Tuple2> getLeafInitializer(K leafContents) { class Holder { Set sentences = Set(); } @@ -322,11 +321,11 @@ public K apply(KToken k) { if (k.sort().equals(Sorts.KConfigVar())) { if (sort == null || sort.equals(Sorts.K())) { return KApply( - GenerateSortProjections.getProjectLbl(Sorts.KItem(), m), + GenerateSortProjections.getProjectLbl(Sorts.KItem()), KApply(KLabel("Map:lookup"), INIT, k)); } else { return KApply( - GenerateSortProjections.getProjectLbl(sort, m), + GenerateSortProjections.getProjectLbl(sort), KApply(KLabel("Map:lookup"), INIT, k)); } } @@ -758,7 +757,7 @@ private static KApply optionalCellInitializer( } } - private static Att getCellPropertiesAsAtt(K k, String cellName, K ensures) { + private static Att getCellPropertiesAsAtt(K k, String cellName) { Att att = Att(); if (cellName.equals("k")) { att = att.add(Att.MAINCELL()); diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java b/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java index 047c802339e..f73b6eebd19 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java @@ -54,7 +54,7 @@ public Module gen(Module mod) { mod.att()); } - public static KLabel getProjectLbl(Sort sort, Module m) { + public static KLabel getProjectLbl(Sort sort) { KLabel lbl; lbl = KLabel("project:" + sort.toString()); return lbl; @@ -70,7 +70,7 @@ public Stream gen(Sort sort) { && !sort.equals(Sorts.K())) { return Stream.empty(); } - KLabel lbl = getProjectLbl(sort, mod); + KLabel lbl = getProjectLbl(sort); KVariable var = KVariable("K", Att.empty().add(Sort.class, sort)); Rule r = Rule( diff --git a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java b/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java index 585d6594a01..99a7e63362a 100644 --- a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java +++ b/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java @@ -42,12 +42,6 @@ private Context resolve(Module m, Context context) { transform(context.body(), m), transform(context.requires(), m), context.att()); } - public K resolveK(Module m, K k) { - resetVars(); - gatherVars(k); - return transform(k, m); - } - public synchronized Sentence resolve(Module m, Sentence s) { if (s instanceof Rule) { return resolve(m, (Rule) s); diff --git a/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java b/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java index 11abc01936d..36bd23b850f 100644 --- a/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java +++ b/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java @@ -92,7 +92,7 @@ public void apply(KVariable v) { } void gatherTerms(K term, boolean body) { - new RewriteAwareVisitor(body, new HashSet<>()) { + new RewriteAwareVisitor(body) { @Override public void apply(K k) { if (isLHS() @@ -145,7 +145,7 @@ public void apply(KApply k) { } void filterTerms(K term, boolean body) { - new RewriteAwareVisitor(body, new HashSet<>()) { + new RewriteAwareVisitor(body) { @Override public void apply(K k) { if (isRHS() && !isLHS() && cache.containsKey(k)) { diff --git a/kernel/src/main/java/org/kframework/compile/NormalizeVariables.java b/kernel/src/main/java/org/kframework/compile/NormalizeVariables.java index 49ac9f9efc9..cec92ccce8b 100644 --- a/kernel/src/main/java/org/kframework/compile/NormalizeVariables.java +++ b/kernel/src/main/java/org/kframework/compile/NormalizeVariables.java @@ -32,31 +32,6 @@ private KVariable normalize(KVariable var) { return KVariable(vars.get(var), var.att().add(Att.DENORMAL(), var.name())); } - /** - * Applies the normalization existing in a particular set of normalized terms to a denormal term - * - * @param denormal The term to be normalized. Only variables which exist in the specified {@code - * normals} are normalized. - * @param normals A list of terms that have previously been normalized using this class, or which - * have been constructed manually with all variables given the "denormal" attribute specifying - * their denormal name. The term to be normalized will be normalized according to the same - * normalization as these terms. - * @return The normalized version of {@code denormal}, in which each variable present in the - * denormal version of the specified {@code normals} is replaced with its normalized name. - */ - public K applyNormalization(K denormal, K... normals) { - Map normalization = inferNormalizationFromTerm(normals); - return new TransformK() { - @Override - public K apply(KVariable k) { - if (normalization.containsKey(k)) { - return KVariable(normalization.get(k), k.att().add(Att.DENORMAL(), k.name())); - } - return super.apply(k); - } - }.apply(denormal); - } - private Map inferNormalizationFromTerm(K[] normals) { Map normalization = new HashMap<>(); for (K normal : normals) { @@ -72,14 +47,6 @@ public void apply(KVariable k) { return normalization; } - public Rule applyNormalization(Rule denormal, K... normals) { - return Rule( - applyNormalization(denormal.body(), normals), - applyNormalization(denormal.requires(), normals), - applyNormalization(denormal.ensures(), normals), - denormal.att()); - } - public K normalize(K term, K... normals) { resetVars(Stream.concat(Stream.of(term), Arrays.stream(normals)).toArray(K[]::new)); return transform(term); diff --git a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java b/kernel/src/main/java/org/kframework/compile/ResolveContexts.java index 99c117ab245..e42e7f30ba1 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveContexts.java @@ -24,7 +24,6 @@ import org.kframework.definition.Production; import org.kframework.definition.ProductionItem; import org.kframework.definition.Sentence; -import org.kframework.kompile.KompileOptions; import org.kframework.kore.FindK; import org.kframework.kore.FoldK; import org.kframework.kore.K; @@ -38,11 +37,7 @@ public class ResolveContexts { - private final KompileOptions kompileOptions; - - public ResolveContexts(KompileOptions kompileOptions) { - this.kompileOptions = kompileOptions; - } + public ResolveContexts() {} public Definition resolve(Definition d) { klabels = new HashSet<>(); diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java b/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java index 5d9616d91a5..6a53667fe75 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java @@ -58,7 +58,7 @@ public ResolveFunctionWithConfig(Module mod) { .anyMatch(r -> ruleNeedsConfig(r))) .collect(Collectors.toSet())); withConfigFunctions.addAll(deps.ancestors(withConfigFunctions)); - ConfigurationInfoFromModule info = new ConfigurationInfoFromModule(mod); + new ConfigurationInfoFromModule(mod); topCell = Sorts.GeneratedTopCell(); topCellLabel = KLabels.GENERATED_TOP_CELL; CONFIG_VAR = KVariable("#Configuration", Att().add(Sort.class, topCell).add(Att.WITH_CONFIG())); @@ -92,25 +92,24 @@ public Boolean apply(KVariable k) { public RuleOrClaim resolve(RuleOrClaim rule, Module m) { return rule.newInstance( - transform(resolve(rule.body(), m), m), - transform(rule.requires(), m), - transform(rule.ensures(), m), + transform(resolve(rule.body(), m)), + transform(rule.requires()), + transform(rule.ensures()), rule.att()); } - public Context resolve(Context context, Module m) { - return new Context( - transform(context.body(), m), transform(context.requires(), m), context.att()); + public Context resolve(Context context) { + return new Context(transform(context.body()), transform(context.requires()), context.att()); } - public ContextAlias resolve(ContextAlias context, Module m) { + public ContextAlias resolve(ContextAlias context) { return new ContextAlias( - transform(context.body(), m), transform(context.requires(), m), context.att()); + transform(context.body()), transform(context.requires()), context.att()); } public final KVariable CONFIG_VAR; - private K transform(K term, Module module) { + private K transform(K term) { return new TransformK() { @Override public K apply(KApply kapp) { @@ -247,9 +246,9 @@ public Module moduleResolve(Module m) { if (s instanceof RuleOrClaim) { newSentences.add(resolve((RuleOrClaim) s, m)); } else if (s instanceof Context) { - newSentences.add(resolve((Context) s, m)); + newSentences.add(resolve((Context) s)); } else if (s instanceof ContextAlias) { - newSentences.add(resolve((ContextAlias) s, m)); + newSentences.add(resolve((ContextAlias) s)); } else if (s instanceof Production) { Production prd = resolve((Production) s); newSentences.add(prd); diff --git a/kernel/src/main/java/org/kframework/compile/ResolveStrict.java b/kernel/src/main/java/org/kframework/compile/ResolveStrict.java index c6c97e6d5c7..0eb3cf4b1c3 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveStrict.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveStrict.java @@ -19,7 +19,6 @@ import org.kframework.builtin.Hooks; import org.kframework.definition.*; import org.kframework.definition.Module; -import org.kframework.kompile.KompileOptions; import org.kframework.kore.K; import org.kframework.kore.KApply; import org.kframework.kore.KLabel; @@ -33,13 +32,11 @@ public class ResolveStrict { - private final KompileOptions kompileOptions; private final Definition d; private Module currentModule; - public ResolveStrict(KompileOptions kompileOptions, Definition d) { - this.kompileOptions = kompileOptions; + public ResolveStrict(Definition d) { this.d = d; } diff --git a/kernel/src/main/java/org/kframework/compile/RewriteAwareVisitor.java b/kernel/src/main/java/org/kframework/compile/RewriteAwareVisitor.java index f2a70e679f5..629c196eea1 100644 --- a/kernel/src/main/java/org/kframework/compile/RewriteAwareVisitor.java +++ b/kernel/src/main/java/org/kframework/compile/RewriteAwareVisitor.java @@ -1,12 +1,10 @@ // Copyright (c) Runtime Verification, Inc. All Rights Reserved. package org.kframework.compile; -import java.util.Set; import org.kframework.kore.KApply; import org.kframework.kore.KRewrite; import org.kframework.kore.KVariable; import org.kframework.kore.VisitK; -import org.kframework.utils.errorsystem.KEMException; /** * A visitor designed to track whether we are currently in the left hand side or right hand side of @@ -18,10 +16,7 @@ */ public class RewriteAwareVisitor extends VisitK { - private final Set errors; - - public RewriteAwareVisitor(boolean isBody, Set errors) { - this.errors = errors; + public RewriteAwareVisitor(boolean isBody) { if (isBody) { isRHS = true; isLHS = true; diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java index 0a39154dde3..33563cbb697 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java @@ -12,7 +12,6 @@ import org.kframework.compile.ResolveAnonVar; import org.kframework.definition.Context; import org.kframework.definition.ContextAlias; -import org.kframework.definition.Module; import org.kframework.definition.RuleOrClaim; import org.kframework.definition.Sentence; import org.kframework.kore.InjectedKLabel; @@ -28,12 +27,10 @@ public class CheckAnonymous { private final Set errors; private final KExceptionManager kem; - private final Module module; - public CheckAnonymous(Set errors, Module module, KExceptionManager kem) { + public CheckAnonymous(Set errors, KExceptionManager kem) { this.errors = errors; this.kem = kem; - this.module = module; } private final Multiset vars = HashMultiset.create(); @@ -98,8 +95,9 @@ public void check(Sentence s) { && entry.getElement().equals("HOLE")) { continue; } - if (loc.get(entry.getElement()).location().isPresent()) // ignore generated variables - kem.registerCompilerWarning( + if (loc.get(entry.getElement()).location().isPresent()) { + // ignore generated variables + kem.registerCompilerWarning( ExceptionType.UNUSED_VAR, errors, "Variable '" @@ -107,6 +105,7 @@ public void check(Sentence s) { + "' defined but not used. Prefix variable name with underscore if this is" + " intentional.", loc.get(entry.getElement())); + } } } else if (entry.getCount() > 1) { if ((entry.getElement().startsWith("_") diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java index 94f7aa07c9f..323d290fa61 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java @@ -32,7 +32,7 @@ public void check(Sentence sentence) { } public void check(K body) { - new RewriteAwareVisitor(true, errors) { + new RewriteAwareVisitor(true) { boolean atTop = true; @Override @@ -85,7 +85,7 @@ && isLHS() } public void checkFuncAtt(Rule r) { - new RewriteAwareVisitor(true, errors) { + new RewriteAwareVisitor(true) { @Override public void apply(KApply k) { if (k.klabel().name().equals("#withConfig")) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java b/kernel/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java index 5632e41069a..24e66a5d950 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java +++ b/kernel/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java @@ -29,7 +29,7 @@ public ComputeUnboundVariables( Set errors, Set vars, Consumer reporter) { - super(isBody, errors); + super(isBody); this.lambda = lambda; this.vars = vars; this.reporter = reporter; diff --git a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java index 1b2ee81a217..cabf998da94 100644 --- a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java +++ b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java @@ -219,7 +219,7 @@ public int run() { unparsingMod = maybeUnparsingMod.get(); } - Option maybeMod = def.programParsingModuleFor(options.module, kem); + Option maybeMod = def.programParsingModuleFor(options.module); if (maybeMod.isEmpty()) { throw KEMException.innerParserError( "Module " + options.module + " not found. Specify a module with -m."); diff --git a/kernel/src/main/java/org/kframework/kil/Definition.java b/kernel/src/main/java/org/kframework/kil/Definition.java index 1b6a260543a..7933613717a 100644 --- a/kernel/src/main/java/org/kframework/kil/Definition.java +++ b/kernel/src/main/java/org/kframework/kil/Definition.java @@ -2,7 +2,6 @@ package org.kframework.kil; import com.google.inject.Inject; -import java.io.File; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -11,12 +10,8 @@ public class Definition extends ASTNode { private List items; - private File mainFile; private String mainModule; - /** An index of all modules in {@link #items} by name */ - private String mainSyntaxModule; - public Map locations = new HashMap<>(); public Definition() { @@ -49,8 +44,4 @@ public void setMainModule(String mainModule) { public String getMainModule() { return mainModule; } - - public void setMainSyntaxModule(String mainSyntaxModule) { - this.mainSyntaxModule = mainSyntaxModule; - } } diff --git a/kernel/src/main/java/org/kframework/kil/DefinitionItem.java b/kernel/src/main/java/org/kframework/kil/DefinitionItem.java index dd8f570379c..7afcb2325a1 100644 --- a/kernel/src/main/java/org/kframework/kil/DefinitionItem.java +++ b/kernel/src/main/java/org/kframework/kil/DefinitionItem.java @@ -2,19 +2,7 @@ package org.kframework.kil; public abstract class DefinitionItem extends ASTNode { - - /** set iff the item was read from a file in the standard libraries */ - private boolean predefined; - public DefinitionItem() { super(); } - - public void setPredefined(boolean predefined) { - this.predefined = predefined; - } - - public boolean isPredefined() { - return predefined; - } } diff --git a/kernel/src/main/java/org/kframework/kil/Lexical.java b/kernel/src/main/java/org/kframework/kil/Lexical.java index 43132247920..4b9cfda2bc3 100644 --- a/kernel/src/main/java/org/kframework/kil/Lexical.java +++ b/kernel/src/main/java/org/kframework/kil/Lexical.java @@ -35,14 +35,6 @@ public int hashCode() { return this.lexicalRule.hashCode(); } - public void setFollow(String follow) { - this.follow = follow; - } - - public String getFollow() { - return follow; - } - public String getLexicalRule() { return lexicalRule; } diff --git a/kernel/src/main/java/org/kframework/kil/Module.java b/kernel/src/main/java/org/kframework/kil/Module.java index 5d7c6b3b66a..f12b3050931 100644 --- a/kernel/src/main/java/org/kframework/kil/Module.java +++ b/kernel/src/main/java/org/kframework/kil/Module.java @@ -6,17 +6,12 @@ import java.util.ArrayList; import java.util.Base64; import java.util.List; -import java.util.Set; -import org.kframework.kore.Sort; /** A module. */ public class Module extends DefinitionItem { private String name; private List items = new ArrayList<>(); - // lazily computed set of sorts. - private Set sorts; - public Module() { super(); } @@ -28,7 +23,6 @@ public Module(String name) { public void appendModuleItem(ModuleItem item) { this.items.add(item); - this.sorts = null; } public void setName(String name) { @@ -41,7 +35,6 @@ public String getName() { public void setItems(List items) { this.items = items; - this.sorts = null; } public List getItems() { diff --git a/kernel/src/main/java/org/kframework/kil/ModuleItem.java b/kernel/src/main/java/org/kframework/kil/ModuleItem.java index 7160635d20a..edd08f3ad9d 100644 --- a/kernel/src/main/java/org/kframework/kil/ModuleItem.java +++ b/kernel/src/main/java/org/kframework/kil/ModuleItem.java @@ -12,12 +12,4 @@ public ModuleItem() { public ModuleItem(Location loc, Source source) { super(loc, source); } - - public java.util.List getLabels() { - return null; - } - - public java.util.List getKLabels() { - return null; - } } diff --git a/kernel/src/main/java/org/kframework/kil/PriorityBlock.java b/kernel/src/main/java/org/kframework/kil/PriorityBlock.java index 2096be50c53..ba37fbf823f 100644 --- a/kernel/src/main/java/org/kframework/kil/PriorityBlock.java +++ b/kernel/src/main/java/org/kframework/kil/PriorityBlock.java @@ -31,10 +31,6 @@ public String getAssoc() { return assoc; } - public void setAssoc(String assoc) { - this.assoc = assoc; - } - public PriorityBlock() { super(); this.assoc = ""; diff --git a/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java b/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java index 3b78d096afd..a7cee5bd5cc 100644 --- a/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java +++ b/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java @@ -17,10 +17,6 @@ public java.util.List getProductions() { return productions; } - public void setProductions(java.util.List productions) { - this.productions = productions; - } - public PriorityBlockExtended(java.util.List productions) { super(); this.productions.addAll(productions); diff --git a/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java b/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java index ca950c880d2..e3c0455846f 100644 --- a/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java +++ b/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java @@ -4,7 +4,7 @@ import org.kframework.definition.Tag; /** - * An associativity declaration, one of {@code syntax left}, {@code syntax right}, or {@ code syntax + * An associativity declaration, one of {@code syntax left}, {@code syntax right}, or {@code syntax * non-assoc}. */ public class PriorityExtendedAssoc extends ModuleItem { @@ -18,18 +18,10 @@ public String getAssoc() { return assoc; } - public void setAssoc(String assoc) { - this.assoc = assoc; - } - public java.util.List getTags() { return tags; } - public void setTags(java.util.List tags) { - this.tags = tags; - } - public PriorityExtendedAssoc(String assoc, java.util.List tags) { super(); this.tags = tags; diff --git a/kernel/src/main/java/org/kframework/kil/Production.java b/kernel/src/main/java/org/kframework/kil/Production.java index 672e7345179..8b525db2dff 100644 --- a/kernel/src/main/java/org/kframework/kil/Production.java +++ b/kernel/src/main/java/org/kframework/kil/Production.java @@ -1,7 +1,6 @@ // Copyright (c) Runtime Verification, Inc. All Rights Reserved. package org.kframework.kil; -import com.google.common.collect.Multimap; import java.util.ArrayList; import java.util.List; import org.kframework.attributes.Att; @@ -22,7 +21,6 @@ public class Production extends ASTNode { protected Sort sort; protected List params; protected String ownerModuleName; - private Multimap binderMap; public boolean isListDecl() { return items.size() == 1 && items.get(0) instanceof UserList; @@ -194,24 +192,6 @@ public void setParams(List params) { this.params = params; } - public ASTNode getChildNode(int idx) { - int arity = -1; - if (items.get(0) instanceof UserList) { - if (idx == 0) { - return items.get(0); - } else { - return this; - } - } - for (ProductionItem i : items) { - if (!(i instanceof Terminal)) arity++; - if (arity == idx) { - return i; - } - } - return null; - } - @Override public boolean equals(Object obj) { if (this == obj) return true; @@ -227,9 +207,7 @@ public boolean equals(Object obj) { if (sort == null) { if (other.sort != null) return false; } else if (!sort.equals(other.sort)) return false; - if (binderMap == null) { - return other.binderMap == null; - } else return binderMap.equals(other.binderMap); + return true; } @Override @@ -241,7 +219,6 @@ public int hashCode() { prime * result + ((getAttribute(Att.KLABEL()) == null) ? 0 : getAttribute(Att.KLABEL()).hashCode()); result = prime * result + ((sort == null) ? 0 : sort.hashCode()); - result = prime * result + ((binderMap == null) ? 0 : binderMap.hashCode()); return result; } diff --git a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java index 362acc9b326..b068d49d431 100644 --- a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java +++ b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java @@ -2,8 +2,6 @@ package org.kframework.kompile; import static org.kframework.Collections.*; -import static org.kframework.definition.Constructors.*; -import static org.kframework.kore.KORE.*; import java.io.Serializable; import java.util.HashMap; @@ -15,10 +13,8 @@ import org.kframework.Collections; import org.kframework.attributes.Att; import org.kframework.attributes.Source; -import org.kframework.builtin.BooleanUtils; import org.kframework.builtin.KLabels; import org.kframework.builtin.Sorts; -import org.kframework.compile.IncompleteCellUtils; import org.kframework.definition.Definition; import org.kframework.definition.Module; import org.kframework.definition.Production; @@ -70,7 +66,6 @@ public CompiledDefinition( Definition parsedDefinition, Definition kompiledDefinition, FileUtil files, - KExceptionManager kem, KLabel topCellInitializer) { this.kompileOptions = kompileOptions; this.outerParsingOptions = outerParsingOptions; @@ -84,31 +79,6 @@ public CompiledDefinition( this.languageParsingModule = kompiledDefinition.getModule("LANGUAGE-PARSING").get(); } - private Rule getExitCodeRule(Definition parsedDefinition) { - Module mainMod = parsedDefinition.mainModule(); - Set exitProds = - stream(mainMod.productions()) - .filter(p -> p.att().contains(Att.EXIT())) - .collect(Collectors.toSet()); - if (exitProds.size() == 0) { - return null; - } else if (exitProds.size() > 1) { - throw KEMException.compilerError( - "Found more than one or zero productions with 'exit' attribute. Exactly one production, a" - + " cell, must have this attribute, designating the exit code of krun. Found:\n" - + exitProds); - } - Production exitProd = exitProds.iterator().next(); - return Rule( - IncompleteCellUtils.make( - exitProd.klabel().get(), - false, - KApply(KLabel("#SemanticCastToInt"), KVariable("_")), - false), - BooleanUtils.TRUE, - BooleanUtils.TRUE); - } - private void initializeConfigurationVariableDefaultSorts(FileUtil files) { StringBuilder sb = new StringBuilder(); sb.append("#!/usr/bin/env bash\n\n"); @@ -189,7 +159,7 @@ public String mainSyntaxModuleName() { * module postfixed with {@link RuleGrammarGenerator#POSTFIX}. In latter case, it uses the * user-defined module. */ - public Option programParsingModuleFor(String moduleName, KExceptionManager kem) { + public Option programParsingModuleFor(String moduleName) { RuleGrammarGenerator gen = new RuleGrammarGenerator(parsedDefinition); Option userProgramParsingModule = @@ -251,10 +221,6 @@ public String showTokens(Module module, FileUtil files, String s, Source source) } } - public Module getExtensionModule(Module module, FileUtil files) { - return RuleGrammarGenerator.getCombinedGrammar(module, files).getExtensionModule(); - } - public Rule compilePatternIfAbsent( FileUtil files, KExceptionManager kem, String pattern, Source source) { return cachedcompiledPatterns.computeIfAbsent( diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 9431e32d302..135578582ae 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -13,7 +13,6 @@ import java.nio.file.Files; import java.util.ArrayList; import java.util.Arrays; -import java.util.Collections; import java.util.HashMap; import java.util.HashSet; import java.util.List; @@ -53,7 +52,6 @@ import org.kframework.definition.Production; import org.kframework.definition.Rule; import org.kframework.definition.Sentence; -import org.kframework.kore.KLabel; import org.kframework.kore.Sort; import org.kframework.main.GlobalOptions; import org.kframework.parser.InputModes; @@ -67,8 +65,6 @@ import org.kframework.utils.Stopwatch; import org.kframework.utils.StringUtil; import org.kframework.utils.errorsystem.KEMException; -import org.kframework.utils.errorsystem.KException; -import org.kframework.utils.errorsystem.KException.ExceptionType; import org.kframework.utils.errorsystem.KExceptionManager; import org.kframework.utils.file.FileUtil; import org.kframework.utils.file.JarInfo; @@ -253,7 +249,6 @@ public CompiledDefinition run( parsedDef, kompiledDefinition, files, - kem, configInfo.getDefaultCell(rootCell).klabel()); if (kompileOptions.genBisonParser || kompileOptions.genGlrBisonParser) { @@ -264,7 +259,7 @@ public CompiledDefinition run( File linkFile = files.resolveKompiled("parser_PGM"); new KRead(kem, files, InputModes.PROGRAM, globalOptions) .createBisonParser( - def.programParsingModuleFor(def.mainSyntaxModuleName(), kem).get(), + def.programParsingModuleFor(def.mainSyntaxModuleName()).get(), def.programStartSymbol, outputFile, kompileOptions.genGlrBisonParser, @@ -290,7 +285,7 @@ public CompiledDefinition run( } String name = part[0]; String module = part[1]; - Option mod = def.programParsingModuleFor(module, kem); + Option mod = def.programParsingModuleFor(module); if (!mod.isDefined()) { throw KEMException.compilerError( "Could not find module referenced by parser attribute: " + module, prod); @@ -455,16 +450,6 @@ public static Function1 excludeModulesByTag( return excludeModules.andThen(walkModules); } - public static Sentence removePolyKLabels(Sentence s) { - if (s instanceof Production p) { - if (!p.isSyntacticSubsort() && p.params().nonEmpty()) { - p = p.substitute(immutable(Collections.nCopies(p.params().size(), Sorts.K()))); - return Production(p.klabel().map(KLabel::head), Seq(), p.sort(), p.items(), p.att()); - } - } - return s; - } - public static Module subsortKItem(Module module) { java.util.Set prods = new HashSet<>(); for (Sort srt : iterable(module.allSorts())) { @@ -521,43 +506,6 @@ public void definitionChecks(Set modules) { })); } - // Extra checks just for the prover specification. - public Module proverChecks(Module specModule, Module mainDefModule) { - // check rogue syntax in spec module - Set toCheck = mutable(specModule.sentences().$minus$minus(mainDefModule.sentences())); - for (Sentence s : toCheck) - if (s.isSyntax() && !s.att().contains(Att.TOKEN())) - kem.registerCompilerWarning( - ExceptionType.FUTURE_ERROR, - errors, - "Found syntax declaration in proof module. This will not be visible from the main" - + " module.", - s); - - // TODO: remove once transition to claim rules is done - // transform rules into claims if - // - they are in the spec modules but not in the definition modules - // - they don't contain the `simplification` attribute - ModuleTransformer mt = - ModuleTransformer.fromSentenceTransformer( - (m, s) -> { - if (m.name().equals(mainDefModule.name()) - || mainDefModule.importedModuleNames().contains(m.name())) return s; - if (s instanceof Rule && !s.att().contains(Att.SIMPLIFICATION())) { - kem.registerCompilerWarning( - KException.ExceptionType.FUTURE_ERROR, - errors, - "Deprecated: use claim instead of rule to specify proof objectives.", - s); - return new Claim( - ((Rule) s).body(), ((Rule) s).requires(), ((Rule) s).ensures(), s.att()); - } - return s; - }, - "rules to claim"); - return mt.apply(specModule); - } - // Extra checks just for the prover specification. public void proverChecksX(Module specModule, Module mainDefModule) { // check rogue syntax in spec module @@ -628,8 +576,7 @@ public void structuralChecks( .forEach(m -> stream(m.localSentences()).forEach(new CheckFunctions(errors, m)::check)); stream(modules) - .forEach( - m -> stream(m.localSentences()).forEach(new CheckAnonymous(errors, m, kem)::check)); + .forEach(m -> stream(m.localSentences()).forEach(new CheckAnonymous(errors, kem)::check)); stream(modules) .forEach( diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index 4befd3d94ac..43acadc467f 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -136,13 +136,6 @@ public String syntaxModule(FileUtil files) { hidden = true) public boolean bisonLists; - @Parameter( - names = "--read-only-kompiled-directory", - description = - "Files in the generated kompiled directory should be read-only to other frontend tools.", - hidden = true) - public boolean readOnlyKompiledDirectory = false; - @Parameter( names = "--concrete-rules", description = @@ -199,8 +192,6 @@ public String syntaxModule(FileUtil files) { hidden = true) public boolean genBisonParserLibrary; - public static final String DEFAULT_TRANSITION = "transition"; - @Parameter( names = "--top-cell", description = diff --git a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java index 2ae9cc1b975..d6fa9802c4f 100644 --- a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java +++ b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java @@ -36,14 +36,11 @@ public class KILtoKORE extends KILTransformation { private final org.kframework.kil.loader.Context context; - private final boolean syntactic; private String moduleName; private final boolean bisonLists; - public KILtoKORE( - org.kframework.kil.loader.Context context, boolean syntactic, boolean bisonLists) { + public KILtoKORE(org.kframework.kil.loader.Context context, boolean bisonLists) { this.context = context; - this.syntactic = syntactic; this.bisonLists = bisonLists; } @@ -355,7 +352,6 @@ public void applyUserList( org.kframework.attributes.Att attrs = convertAttributes(p).add(Att.USER_LIST(), userList.getListType()); - String kilProductionId = "" + System.identityHashCode(p); org.kframework.definition.Production prod1, prod3; if (bisonLists) { diff --git a/kernel/src/main/java/org/kframework/kprove/KProve.java b/kernel/src/main/java/org/kframework/kprove/KProve.java index bd59419503b..e331cd33a8f 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProve.java +++ b/kernel/src/main/java/org/kframework/kprove/KProve.java @@ -44,10 +44,7 @@ public int run() { } Tuple2 compiled = - proofDefinitionBuilder.build( - kproveOptions.specFile(files), - kproveOptions.specModule, - compiledDefinition.kompileOptions.readOnlyKompiledDirectory); + proofDefinitionBuilder.build(kproveOptions.specFile(files), kproveOptions.specModule); Rewriter rewriter = rewriterGenerator.apply(compiled._1()); Module specModule = compiled._2(); diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java index f5bf36c6d48..e6f6d8f8696 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java +++ b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java @@ -36,8 +36,6 @@ public GlobalOptions getGlobalOptions_useOnlyInGuiceProvider() { @ParametersDelegate public InnerParsingOptions innerParsing = new InnerParsingOptions(); - private File specFile; - public synchronized File specFile(FileUtil files) { return outerParsing.mainDefinitionFile(files); } diff --git a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java b/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java index 52ec3c4732f..504bf7f06c3 100644 --- a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java +++ b/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java @@ -39,8 +39,7 @@ public record ProofDefinitionBuilder( * @param specFile File containing specification rules to prove. Not part of definition. * @param specModuleName Module containing specifications to prove */ - public Tuple2 build( - File specFile, String specModuleName, boolean readOnlyCache) { + public Tuple2 build(File specFile, String specModuleName) { String defModuleNameUpdated = compiledDefinition.kompiledDefinition.mainModule().name(); String specModuleNameUpdated = specModuleName == null diff --git a/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java b/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java index 8fba5763fe2..31f2c50e996 100644 --- a/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java +++ b/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java @@ -53,7 +53,6 @@ public KServerFrontEnd( } private static KServerFrontEnd instance; - private static Thread threadInstance; private static final ImmutableList tools = ImmutableList.of( "-kompile", "-kast", "-kdep", "-kprove", "-kserver", "-k-compile-search-pattern"); @@ -100,7 +99,6 @@ protected int run() { } Thread t = new Thread(server); instance = this; - threadInstance = t; t.start(); if (isLocal()) { diff --git a/kernel/src/main/java/org/kframework/lsp/KPos.java b/kernel/src/main/java/org/kframework/lsp/KPos.java index 942414f8bf6..e3ece1dd8a1 100644 --- a/kernel/src/main/java/org/kframework/lsp/KPos.java +++ b/kernel/src/main/java/org/kframework/lsp/KPos.java @@ -16,11 +16,6 @@ public class KPos { /** Character offset on a line in a document (one-based). */ private int character; - public KPos() { - line = 0; - character = 0; - } - public KPos(int line, int character) { this.line = line; this.character = character; @@ -31,10 +26,6 @@ public KPos(Position pos) { this.character = pos.getCharacter() + 1; } - public Position toPosition() { - return new Position(line - 1, character - 1); - } - public int getLine() { return line; } diff --git a/kernel/src/main/java/org/kframework/lsp/KTextDocumentService.java b/kernel/src/main/java/org/kframework/lsp/KTextDocumentService.java index dca4abad70d..58c9c31131a 100644 --- a/kernel/src/main/java/org/kframework/lsp/KTextDocumentService.java +++ b/kernel/src/main/java/org/kframework/lsp/KTextDocumentService.java @@ -16,7 +16,6 @@ /** TextDocumentService implementation for K. */ public class KTextDocumentService implements TextDocumentService { - private final KLanguageServer languageServer; private final LSClientLogger clientLogger; public final TextDocumentSyncHandler memo; @@ -41,7 +40,6 @@ public class KTextDocumentService implements TextDocumentService { } public KTextDocumentService(KLanguageServer languageServer) throws URISyntaxException { - this.languageServer = languageServer; this.clientLogger = LSClientLogger.getInstance(); memo = new TextDocumentSyncHandler(clientLogger, languageServer); memo.add(domains.toString()); diff --git a/kernel/src/main/java/org/kframework/main/AbstractKModule.java b/kernel/src/main/java/org/kframework/main/AbstractKModule.java index e12bb8bc1e5..2f08d053a28 100644 --- a/kernel/src/main/java/org/kframework/main/AbstractKModule.java +++ b/kernel/src/main/java/org/kframework/main/AbstractKModule.java @@ -52,36 +52,6 @@ public List getKastModules() { return Lists.newArrayList(); } - @Override - public List getKRunModules() { - return Lists.newArrayList( - new AbstractModule() { - - @Override - protected void configure() { - bindOptions(AbstractKModule.this::krunOptions, binder()); - } - }); - } - - @Override - public List getKEqModules(List definitionSpecificModules) { - return Lists.newArrayList(); - } - - @Override - public List getDefinitionSpecificKEqModules() { - return Lists.newArrayList( - new AbstractModule() { - - @Override - protected void configure() { - binder().requireAtInjectOnConstructors(); - // bind backend implementations of tools to their interfaces - } - }); - } - @Override public List getKProveModules() { return Lists.newArrayList( diff --git a/kernel/src/main/java/org/kframework/main/FrontEnd.java b/kernel/src/main/java/org/kframework/main/FrontEnd.java index e904143199d..78a77c8d7e7 100644 --- a/kernel/src/main/java/org/kframework/main/FrontEnd.java +++ b/kernel/src/main/java/org/kframework/main/FrontEnd.java @@ -6,9 +6,7 @@ import com.google.inject.Provider; import org.kframework.utils.ExitOnTimeoutThread; import org.kframework.utils.InterrupterRunnable; -import org.kframework.utils.StringUtil; import org.kframework.utils.errorsystem.KEMException; -import org.kframework.utils.errorsystem.KException; import org.kframework.utils.errorsystem.KExceptionManager; import org.kframework.utils.file.FileUtil; import org.kframework.utils.file.JarInfo; @@ -79,8 +77,4 @@ public int main() { } return retval; } - - public static void printBootError(String message) { - System.err.println(StringUtil.splitLines(KException.criticalError(message).toString())); - } } diff --git a/kernel/src/main/java/org/kframework/main/KModule.java b/kernel/src/main/java/org/kframework/main/KModule.java index ab6dab9a399..3ceab9ea139 100644 --- a/kernel/src/main/java/org/kframework/main/KModule.java +++ b/kernel/src/main/java/org/kframework/main/KModule.java @@ -10,11 +10,5 @@ public interface KModule { List getKastModules(); - List getKRunModules(); - - List getKEqModules(List definitionSpecificModules); - - List getDefinitionSpecificKEqModules(); - List getKProveModules(); } diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java index aa84d4e048b..5f944c7f32b 100644 --- a/kernel/src/main/java/org/kframework/parser/KRead.java +++ b/kernel/src/main/java/org/kframework/parser/KRead.java @@ -1,16 +1,11 @@ // Copyright (c) Runtime Verification, Inc. All Rights Reserved. package org.kframework.parser; -import java.io.ByteArrayInputStream; import java.io.File; import java.io.IOException; -import java.io.InputStream; import java.util.ArrayList; import java.util.Arrays; import java.util.List; -import javax.json.Json; -import javax.json.JsonObject; -import javax.json.JsonReader; import org.kframework.attributes.Source; import org.kframework.definition.Module; import org.kframework.kompile.CompiledDefinition; @@ -181,29 +176,4 @@ public static K deserialize(String stringToParse, InputModes inputMode, Source s "Unsupported input mode for deserialization: " + inputMode); }; } - - public static K autoDeserialize(byte[] kast, Source source) { - if (BinaryParser.isBinaryKast(kast)) return BinaryParser.parse(kast); - - InputStream input = new ByteArrayInputStream(kast); - int c; - try { - while (Character.isWhitespace(c = input.read())) - ; - } catch (IOException e) { - throw KEMException.criticalError("Could not read output from parser: ", e); - } - - if (c == '{') { - JsonReader reader = Json.createReader(new ByteArrayInputStream(kast)); - JsonObject data = reader.readObject(); - return JsonParser.parseJson(data); - } - - try { - return KastParser.parse(new String(kast), source); - } catch (KEMException e) { - throw KEMException.criticalError("Could not read input: " + source.source()); - } - } } diff --git a/kernel/src/main/java/org/kframework/parser/ParserUtils.java b/kernel/src/main/java/org/kframework/parser/ParserUtils.java index 1c4beae44fb..9b2e0a8dd5e 100644 --- a/kernel/src/main/java/org/kframework/parser/ParserUtils.java +++ b/kernel/src/main/java/org/kframework/parser/ParserUtils.java @@ -81,13 +81,12 @@ public static Module parseMainModuleOuterSyntax( Definition def = new Definition(); def.setItems(Outer.parse(source, definitionText, null)); def.setMainModule(mainModule); - def.setMainSyntaxModule(mainModule); ProcessGroupAttributes.apply(def); Context context = new Context(); new CollectProductionsVisitor(context).visit(def); - KILtoKORE kilToKore = new KILtoKORE(context, false, false); + KILtoKORE kilToKore = new KILtoKORE(context, false); return kilToKore.apply(def).getModule(mainModule).get(); } @@ -296,7 +295,7 @@ public Set loadModules( System.out.println(def); } - KILtoKORE kilToKore = new KILtoKORE(context, false, leftAssoc); + KILtoKORE kilToKore = new KILtoKORE(context, leftAssoc); // Order modules by name to stabilize the error message for circular imports java.util.List flatModules = kilModules.stream() diff --git a/kernel/src/main/java/org/kframework/parser/binary/BinaryParser.java b/kernel/src/main/java/org/kframework/parser/binary/BinaryParser.java index 6bfd375472f..0b1df72b59e 100644 --- a/kernel/src/main/java/org/kframework/parser/binary/BinaryParser.java +++ b/kernel/src/main/java/org/kframework/parser/binary/BinaryParser.java @@ -66,15 +66,14 @@ public class BinaryParser { public static final byte[] MAGIC = {0x7f, 'K', 'A', 'S', 'T'}; - public static final int BEGIN = 0, - KTOKEN = 1, - KAPPLY = 2, - KSEQUENCE = 3, - KVARIABLE = 4, - KREWRITE = 5, - INJECTEDKLABEL = 6, - END = 7, - BACK_REFERENCE = 8; + public static final int KTOKEN = 1; + public static final int KAPPLY = 2; + public static final int KSEQUENCE = 3; + public static final int KVARIABLE = 4; + public static final int KREWRITE = 5; + public static final int INJECTEDKLABEL = 6; + public static final int END = 7; + public static final int BACK_REFERENCE = 8; private final ByteBuffer data; private final List interns = new ArrayList<>(); 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 fe41de2e74f..4f7c069bd54 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java @@ -278,7 +278,6 @@ public String tokenizeString(String input, Source source) { "|-%s|--%s|-%s|\n", "-".repeat(maxTokenLen), "-".repeat(maxLocLen), "-".repeat(maxTerminalLen))); for (int i = 0; i < words.size(); i++) { - Scanner.Token word = words.get(i); sb.append( String.format( "|%-" + maxTokenLen + "s | %-" + maxLocLen + "s | %-" + maxTerminalLen + "s|\n", @@ -359,7 +358,7 @@ public Tuple2, K>, Set> parseString( /** * Parse the given input. This function is private because the final disambiguation in {@link - * AmbFilter} eliminates ambiguities that will be equivalent only after calling {@link + * AmbFilterError} eliminates ambiguities that will be equivalent only after calling {@link * TreeNodesToKORE#apply(Term)}, but returns a result that is somewhat arbitrary as an actual * parser {@link Term}. Fortunately all callers want the result as a K, and can use the public * version of this method. 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 1b03e867c43..882369bf92b 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java +++ b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java @@ -65,19 +65,12 @@ public record RuleGrammarGenerator(Definition baseK) { kSorts.add(Sorts.KString()); } - private static Set kSorts() { - return java.util.Collections.unmodifiableSet(kSorts); - } - /// modules that have a meaning: public static final String DEFAULT_LAYOUT = "DEFAULT-LAYOUT"; public static final String RULE_CELLS = "RULE-CELLS"; public static final String CONFIG_CELLS = "CONFIG-CELLS"; public static final String K = "K"; public static final String AUTO_CASTS = "AUTO-CASTS"; - public static final String KSEQ_SYMBOLIC = "KSEQ-SYMBOLIC"; - public static final String K_TOP_SORT = "K-TOP-SORT"; - public static final String K_BOTTOM_SORT = "K-BOTTOM-SORT"; public static final String AUTO_FOLLOW = "AUTO-FOLLOW"; public static final String PROGRAM_LISTS = "PROGRAM-LISTS"; public static final String RULE_LISTS = "RULE-LISTS"; @@ -86,7 +79,6 @@ private static Set kSorts() { public static final String POSTFIX = "-PROGRAM-PARSING"; - public static final String NOT_INJECTION = "notInjection"; public static final String ID = "ID"; private static final String ID_SYNTAX = "ID-SYNTAX"; public static final String ID_PROGRAM_PARSING = ID_SYNTAX + POSTFIX; @@ -99,11 +91,6 @@ private static Set kSorts() { */ public RuleGrammarGenerator {} - private Set renameKItem2Bottom(Set def) { - // TODO: do renaming of KItem and K in the LHS to KBott? - return def; - } - /** * Creates the seed module that can be used to parse rules. Imports module markers RULE-CELLS and * K found in /include/kast.k. @@ -372,19 +359,18 @@ public static Tuple3 getCombinedGrammarImpl( } if (mod.importedModuleNames().contains(AUTO_CASTS)) { // create the diamond - Set temp; for (Sort srt : iterable(mod.allSorts())) { if (!isParserSort(srt) || mod.subsorts().directlyLessThan(Sorts.KVariable(), srt)) { // K ::= K "::Sort" | K ":Sort" | K "<:Sort" | K ":>Sort" - prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), srt, srt)); + prods.addAll(makeCasts(Sorts.K(), srt, srt)); } } - prods.addAll(makeCasts(Sorts.KLabel(), Sorts.KLabel(), Sorts.KLabel(), Sorts.KLabel())); - prods.addAll(makeCasts(Sorts.KList(), Sorts.KList(), Sorts.KList(), Sorts.KList())); - prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), Sorts.KItem(), Sorts.KItem())); - prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), Sorts.K(), Sorts.K())); + prods.addAll(makeCasts(Sorts.KLabel(), Sorts.KLabel(), Sorts.KLabel())); + prods.addAll(makeCasts(Sorts.KList(), Sorts.KList(), Sorts.KList())); + prods.addAll(makeCasts(Sorts.K(), Sorts.KItem(), Sorts.KItem())); + prods.addAll(makeCasts(Sorts.K(), Sorts.K(), Sorts.K())); for (SortSynonym syn : iterable(mod.sortSynonyms())) { - prods.addAll(makeCasts(Sorts.KBott(), Sorts.K(), syn.newSort(), syn.oldSort())); + prods.addAll(makeCasts(Sorts.K(), syn.newSort(), syn.oldSort())); } } @@ -501,7 +487,7 @@ public static Tuple3 getCombinedGrammarImpl( // syntax {P} Int ::= P "+" Int // syntax Int ::= K "+" Int List instantiationMask = new ArrayList<>(); - for (Sort param : mutable(p.params())) instantiationMask.add(Sorts.K()); + for (Sort ignored : mutable(p.params())) instantiationMask.add(Sorts.K()); Production subst = p.substitute(immutable(instantiationMask)); Production p1 = Production( @@ -794,8 +780,7 @@ private static void addCellNameProd(Set prods, Sentence prod) { } } - private static Set makeCasts( - Sort outerSort, Sort innerSort, Sort castSort, Sort labelSort) { + private static Set makeCasts(Sort innerSort, Sort castSort, Sort labelSort) { Set prods = new HashSet<>(); Att attrs1 = Att().add(Sort.class, castSort); prods.add( diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java index 04d9bf47243..2a6b0224627 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java @@ -2,7 +2,6 @@ package org.kframework.parser.inner.disambiguation; import static org.kframework.Collections.*; -import static org.kframework.kore.KORE.*; import com.google.common.collect.Sets; import java.util.ArrayList; @@ -13,7 +12,6 @@ import java.util.LinkedList; import java.util.List; import java.util.Map; -import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; import org.kframework.POSet; @@ -25,9 +23,7 @@ import org.kframework.definition.Production; import org.kframework.definition.ProductionItem; import org.kframework.definition.UserList; -import org.kframework.kore.KLabel; import org.kframework.kore.Sort; -import org.kframework.parser.Constant; import org.kframework.parser.ProductionReference; import org.kframework.parser.SetsGeneralTransformer; import org.kframework.parser.Term; @@ -214,93 +210,4 @@ private Sort getSort(ProductionReference child, Sort expectedSort) { child) .sort(); } - - /** - * Returns an element of sorts which is related to and no greater than every other element of - * sorts, if any exists. - */ - private Optional least(Iterable sorts) { - Iterator iter = sorts.iterator(); - if (!iter.hasNext()) { - return Optional.empty(); - } - Sort min = iter.next(); - while (iter.hasNext()) { - Sort next = iter.next(); - if (!subsorts.lessThanEq(min, next)) { - // if min is unrelated to next, it can't be the least sort so - // we also might as well switch - min = next; - } - } - for (Sort s : sorts) { - if (!subsorts.lessThanEq(min, s)) { - return Optional.empty(); - } - } - return Optional.of(min); - } - - /** - * Returns an element of sorts which is related to and no less than every other element of sorts, - * if any exists. - */ - private Optional greatest(Iterable sorts) { - Iterator iter = sorts.iterator(); - if (!iter.hasNext()) { - return Optional.empty(); - } - Sort max = iter.next(); - while (iter.hasNext()) { - Sort next = iter.next(); - if (!subsorts.greaterThanEq(max, next)) { - // if min is unrelated to next, it can't be the least sort so - // we also might as well switch - max = next; - } - } - for (Sort s : sorts) { - if (!subsorts.greaterThanEq(max, s)) { - return Optional.empty(); - } - } - return Optional.of(max); - } - - private Optional klabelFromTerm(Term labelTerm) { - if (labelTerm instanceof Constant labelCon) { - if (labelCon.production().sort().equals(Sorts.KLabel())) { - String labelVal = labelCon.value(); - if (labelVal.charAt(0) == '`') { - return Optional.of(KLabel(labelVal.substring(1, labelVal.length() - 1))); - } else { - return Optional.of(KLabel(labelVal)); - } - } - } - return Optional.empty(); - } - - private List lowerKList(Term listTerm) { - List items = new ArrayList<>(); - lowerKListAcc(listTerm, items); - return items; - } - - private void lowerKListAcc(Term term, List items) { - if (term instanceof TermCons cons) { - if (cons.production().klabel().isDefined()) { - String labelName = cons.production().klabel().get().name(); - if (labelName.equals("#KList")) { - assert cons.items().size() == 2; - lowerKListAcc(cons.get(0), items); - lowerKListAcc(cons.get(1), items); - return; - } else if (labelName.equals("#EmptyKList")) { - return; - } - } - } - items.add(term); - } } diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java deleted file mode 100644 index 3b715dc6f94..00000000000 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java +++ /dev/null @@ -1,63 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.parser.inner.disambiguation; - -import java.util.Set; -import org.kframework.kore.K; -import org.kframework.parser.Ambiguity; -import org.kframework.parser.ProductionReference; -import org.kframework.parser.SetsGeneralTransformer; -import org.kframework.parser.Term; -import org.kframework.parser.TreeNodesToKORE; -import org.kframework.parser.outer.Outer; -import org.kframework.utils.errorsystem.KEMException; -import scala.Tuple2; -import scala.util.Either; -import scala.util.Right; - -/** Eliminate remaining ambiguities by choosing one of them. */ -public class AmbFilter extends SetsGeneralTransformer { - - public AmbFilter() {} - - @Override - public Tuple2, Term>, Set> apply(Ambiguity amb) { - K last = null; - boolean equal = true; - Tuple2, Term>, Set> candidate = null; - for (Term t : amb.items()) { - candidate = this.apply(t); - K next = - new TreeNodesToKORE(Outer::parseSort) - .apply(new RemoveBracketVisitor().apply(candidate._1().right().get())); - if (last != null) { - if (!last.equals(next)) { - equal = false; - break; - } - } - last = next; - } - if (equal) { - // all ambiguities have the same abstract syntax, so just pick one - return candidate; - } - - String msg = "Parsing ambiguity. Arbitrarily choosing the first."; - - for (int i = 0; i < amb.items().size(); i++) { - msg += "\n" + (i + 1) + ": "; - Term elem = (Term) amb.items().toArray()[i]; - if (elem instanceof ProductionReference tc) { - msg += tc.production().toString(); - } - // TODO: use the unparser - // Unparser unparser = new Unparser(context); - // msg += "\n " + unparser.print(elem).replace("\n", "\n "); - msg += "\n " + new RemoveBracketVisitor().apply(elem); - } - // TODO: add location information - Tuple2, Term>, Set> rez = - this.apply(amb.items().iterator().next()); - return new Tuple2<>(Right.apply(rez._1().right().get()), rez._2()); - } -} diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java index bc509f64576..ca99277fa09 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java @@ -66,13 +66,8 @@ public TypeInferenceVisitor(TypeInferencer inferencer, Sort topSort, boolean isA @Override public Either, Term> apply(Term t) { - Term loc = t; - if (loc instanceof Ambiguity) { - loc = ((Ambiguity) loc).items().iterator().next(); - } // add constraints to inferencer inferencer.push(t, topSort, isAnywhere); - Either, Term> typed; try { if (inferencer.hasNoVariables()) { // skip the rest as there is nothing to infer diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java index 2c37e6cf55b..32964acc506 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java @@ -567,7 +567,7 @@ public String apply(Term t) { return apply(amb.items().iterator().next()); } // compute name of expected sort for use in cache. - String expected = printSort(expectedSort, expectedParams, false).replace("|", ""); + String expected = printSort(expectedSort, expectedParams).replace("|", ""); Map contexts = ambCache.computeIfAbsent(amb, amb2 -> new HashMap<>()); int id = contexts.computeIfAbsent(expected, expected2 -> ambId); boolean cached = id != ambId; @@ -656,7 +656,7 @@ public String apply(Term t) { expectedParams = oldExpectedParams; } // compute name of expected sort for use in cache. - String expected = printSort(expectedSort, expectedParams, false).replace("|", ""); + String expected = printSort(expectedSort, expectedParams).replace("|", ""); boolean cached = !cacheById.get(id).add(expected); if (!isIncremental && (!shared || !cached)) { // if we are in non-incremental mode and this is the first time reaching this term under @@ -736,12 +736,12 @@ private void pushConstraint(Sort actualSort, Optional actua } else { sb.append("(<=Sort "); } - sb.append(printSort(actualSort, actualParams, isIncremental)); + sb.append(printSort(actualSort, actualParams)); sb.append(" "); if (mod.subsorts().lessThan(Sorts.K(), expectedSort)) { expectedSort = Sorts.K(); } - sb.append(printSort(expectedSort, expectedParams, isIncremental)); + sb.append(printSort(expectedSort, expectedParams)); sb.append(") "); } if (isIncremental) { @@ -765,7 +765,7 @@ private void pushConstraint(String name, Constant loc) { if (mod.subsorts().lessThan(Sorts.K(), expectedSort)) { expectedSort = Sorts.K(); } - sb.append(printSort(expectedSort, expectedParams, isIncremental)); + sb.append(printSort(expectedSort, expectedParams)); sb.append(") "); if (isIncremental) { saveConstraint(name, loc); @@ -796,7 +796,7 @@ private boolean isBadNatSort(Sort actualSort) { return stream(actualSort.params()).anyMatch(this::isBadNatSort); } - private String printSort(Sort s, Optional t, boolean isIncremental) { + private String printSort(Sort s, Optional t) { Map params = new HashMap<>(); if (t.isPresent()) { if (t.get().production().params().nonEmpty()) { @@ -809,10 +809,10 @@ private String printSort(Sort s, Optional t, boolean isIncr } } } - return printSort(s, params, isIncremental); + return printSort(s, params); } - private String printSort(Sort s, Map params, boolean isIncremental) { + private String printSort(Sort s, Map params) { StringBuilder sb = new StringBuilder(); if (params.containsKey(s)) { sb.append("|").append(params.get(s)).append("|"); @@ -825,7 +825,7 @@ private String printSort(Sort s, Map params, boolean isIncremental sb.append("(|Sort").append(s.name()).append("|"); for (Sort param : iterable(s.params())) { sb.append(" "); - sb.append(printSort(param, params, isIncremental)); + sb.append(printSort(param, params)); } sb.append(")"); return sb.toString(); @@ -964,7 +964,7 @@ private Sort getValue(String name) { private Sort eval(Sort s, Optional params) { if (isBadNatSort(s)) return s; print("(eval "); - print(printSort(s, params, true)); + print(printSort(s, params)); println(")"); return readSort(false); } diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 2e75458cdf4..ede6d80c190 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -52,34 +52,33 @@ /** Parses a Json term into the KORE data structures. */ public class JsonParser { - public static final String INJECTEDKLABEL = "InjectedKLabel", - KAPPLY = "KApply", - KAS = "KAs", - KATT = "KAtt", - KBUBBLE = "KBubble", - KCONFIGURATION = "KConfiguration", - KCONTEXT = "KContext", - KDEFINITION = "KDefinition", - KNONTERMINAL = "KNonTerminal", - KMODULE = "KModule", - KFLATMODULE = "KFlatModule", - KFLATMODULELIST = "KFlatModuleList", - KIMPORT = "KImport", - KPRODUCTION = "KProduction", - KREGEXTERMINAL = "KRegexTerminal", - KREWRITE = "KRewrite", - KRULE = "KRule", - KCLAIM = "KClaim", - KSEQUENCE = "KSequence", - KSORT = "KSort", - KSORTSYNONYM = "KSortSynonym", - KSYNTAXLEXICAL = "KSyntaxLexical", - KSYNTAXASSOCIATIVITY = "KSyntaxAssociativity", - KSYNTAXPRIORITY = "KSyntaxPriority", - KSYNTAXSORT = "KSyntaxSort", - KTERMINAL = "KTerminal", - KTOKEN = "KToken", - KVARIABLE = "KVariable"; + public static final String INJECTEDKLABEL = "InjectedKLabel"; + public static final String KAPPLY = "KApply"; + public static final String KAS = "KAs"; + public static final String KATT = "KAtt"; + public static final String KBUBBLE = "KBubble"; + public static final String KCONFIGURATION = "KConfiguration"; + public static final String KCONTEXT = "KContext"; + public static final String KDEFINITION = "KDefinition"; + public static final String KNONTERMINAL = "KNonTerminal"; + public static final String KFLATMODULE = "KFlatModule"; + public static final String KFLATMODULELIST = "KFlatModuleList"; + public static final String KIMPORT = "KImport"; + public static final String KPRODUCTION = "KProduction"; + public static final String KREGEXTERMINAL = "KRegexTerminal"; + public static final String KREWRITE = "KRewrite"; + public static final String KRULE = "KRule"; + public static final String KCLAIM = "KClaim"; + public static final String KSEQUENCE = "KSequence"; + public static final String KSORT = "KSort"; + public static final String KSORTSYNONYM = "KSortSynonym"; + public static final String KSYNTAXLEXICAL = "KSyntaxLexical"; + public static final String KSYNTAXASSOCIATIVITY = "KSyntaxAssociativity"; + public static final String KSYNTAXPRIORITY = "KSyntaxPriority"; + public static final String KSYNTAXSORT = "KSyntaxSort"; + public static final String KTERMINAL = "KTerminal"; + public static final String KTOKEN = "KToken"; + public static final String KVARIABLE = "KVariable"; ///////////////////////////// // Parsing Definition Json // @@ -150,7 +149,7 @@ public static Definition toDefinition(JsonObject data) throws IOException { // Parsing Module Json // ///////////////////////// - public static FlatModule toFlatModule(JsonObject data) throws IOException { + public static FlatModule toFlatModule(JsonObject data) { if (!data.getString("node").equals(KFLATMODULE)) throw KEMException.criticalError( "Unexpected node found in KAST Json term: " + data.getString("node")); diff --git a/kernel/src/main/java/org/kframework/unparser/AddBrackets.java b/kernel/src/main/java/org/kframework/unparser/AddBrackets.java index 3e6be4e702a..7335082df70 100644 --- a/kernel/src/main/java/org/kframework/unparser/AddBrackets.java +++ b/kernel/src/main/java/org/kframework/unparser/AddBrackets.java @@ -213,7 +213,6 @@ boolean hasTerminalAtIdx(Production p, int position) { } private int getPosition(ProductionReference inner, ProductionReference outer) { - EnumSet set = EnumSet.noneOf(Fixity.class); assert outer instanceof TermCons; TermCons tc = (TermCons) outer; Production p = tc.production(); diff --git a/kernel/src/main/java/org/kframework/unparser/Formatter.java b/kernel/src/main/java/org/kframework/unparser/Formatter.java index 2cceb72a535..b231bac1251 100644 --- a/kernel/src/main/java/org/kframework/unparser/Formatter.java +++ b/kernel/src/main/java/org/kframework/unparser/Formatter.java @@ -2,7 +2,6 @@ package org.kframework.unparser; -import static org.fusesource.jansi.Ansi.*; import static org.kframework.Collections.*; import org.kframework.attributes.Att; diff --git a/kernel/src/main/java/org/kframework/unparser/KPrint.java b/kernel/src/main/java/org/kframework/unparser/KPrint.java index 1087eaa0a41..e7071e94c59 100644 --- a/kernel/src/main/java/org/kframework/unparser/KPrint.java +++ b/kernel/src/main/java/org/kframework/unparser/KPrint.java @@ -131,16 +131,6 @@ public void prettyPrint(Definition def, Module module, Consumer print, K def, module, result, s, options.color(tty.stdout(), files.getEnv()), options.output)); } - public byte[] prettyPrint(Definition def, Module module, K result) { - return prettyPrint( - def, - module, - result, - Sorts.GeneratedTopCell(), - options.color(tty.stdout(), files.getEnv()), - options.output); - } - public byte[] prettyPrint( Definition def, Module module, @@ -210,7 +200,7 @@ public String unparseTerm(K input, Module test, ColorSetting colorize) { return unparseInternal(test, input, colorize); } - private Term disambiguateForUnparse(Module mod, Term t) { + private Term disambiguateForUnparse(Term t) { return t; } @@ -221,7 +211,6 @@ private String unparseInternal(Module mod, K input, ColorSetting colorize) { .addBrackets( (ProductionReference) disambiguateForUnparse( - mod, KOREToTreeNodes.apply( KOREToTreeNodes.up(mod, expandMacros.expand(input)), mod))), colorize); diff --git a/kernel/src/main/java/org/kframework/unparser/OutputModes.java b/kernel/src/main/java/org/kframework/unparser/OutputModes.java index 8fc9b4fa5fb..5c402a25bbf 100644 --- a/kernel/src/main/java/org/kframework/unparser/OutputModes.java +++ b/kernel/src/main/java/org/kframework/unparser/OutputModes.java @@ -15,21 +15,4 @@ public enum OutputModes { LATEX, KORE, NONE; - - private String extension; - - static { - PRETTY.extension = "kpretty"; - PROGRAM.extension = "pgm"; - KAST.extension = "kast"; - BINARY.extension = "kbin"; - JSON.extension = "json"; - LATEX.extension = "tex"; - KORE.extension = "kore"; - NONE.extension = ""; - } - - public String ext() { - return extension; - } } diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java index 5d676add297..c5efb409bae 100644 --- a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java +++ b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java @@ -12,10 +12,6 @@ public class PrintOptions { public PrintOptions() {} - public PrintOptions(ColorSetting color) { - this.color = color; - } - public PrintOptions(OutputModes output) { this.output = output; } diff --git a/kernel/src/main/java/org/kframework/utils/ColorUtil.java b/kernel/src/main/java/org/kframework/utils/ColorUtil.java index 86bc38122f0..d0344a8eba5 100644 --- a/kernel/src/main/java/org/kframework/utils/ColorUtil.java +++ b/kernel/src/main/java/org/kframework/utils/ColorUtil.java @@ -3,7 +3,6 @@ import java.awt.Color; import java.awt.color.ColorSpace; -import java.lang.reflect.Field; import java.util.Collections; import java.util.HashMap; import java.util.Map; @@ -506,14 +505,4 @@ private static double getColorError(Color color1, Color color2) { double i = l * l + c * c + h * h; return i < 0 ? 0 : Math.sqrt(i); } - - public static Color getColorByName(String colorName) { - try { - // Find the field and value of colorName - Field field = Class.forName("java.awt.Color").getField(colorName); - return (Color) field.get(null); - } catch (ClassNotFoundException | NoSuchFieldException | IllegalAccessException e) { - return null; - } - } } diff --git a/kernel/src/main/java/org/kframework/utils/IndentingFormatter.java b/kernel/src/main/java/org/kframework/utils/IndentingFormatter.java deleted file mode 100644 index 002c6a8f49c..00000000000 --- a/kernel/src/main/java/org/kframework/utils/IndentingFormatter.java +++ /dev/null @@ -1,47 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.utils; - -import java.util.Formatter; -import javax.annotation.Nonnull; - -/** - * An extension of {@code java.util.Formatter} that indents every new line with specified prefix. - * - * @author Denis Bogdanas Created on 14-Apr-19. - */ -public class IndentingFormatter { - - public static final String ENDL = "\n"; - private final Formatter formatter; - private final String endlReplacement; - - public IndentingFormatter(@Nonnull Formatter formatter, @Nonnull String indent) { - this.formatter = formatter; - this.endlReplacement = indent.isEmpty() ? ENDL : ENDL + indent; - } - - public Formatter format(String format, Object... args) { - if (endlReplacement.equals(ENDL)) { - return formatter.format(format, args); - } else { - String newFormat = buildNewFormat(format); - Object[] newArgs = buildNewArgs(args); - return formatter.format(newFormat, newArgs); - } - } - - public String buildNewFormat(String format) { - return format.replaceAll("\\R", endlReplacement); - } - - public Object[] buildNewArgs(Object[] args) { - Object[] newArgs = new Object[args.length]; - for (int i = 0; i < args.length; i++) { - newArgs[i] = - args[i] instanceof String - ? ((String) args[i]).replaceAll("\\R", endlReplacement) - : args[i]; - } - return newArgs; - } -} diff --git a/kernel/src/main/java/org/kframework/utils/Stopwatch.java b/kernel/src/main/java/org/kframework/utils/Stopwatch.java index 980e56cecdb..50220d82a9d 100644 --- a/kernel/src/main/java/org/kframework/utils/Stopwatch.java +++ b/kernel/src/main/java/org/kframework/utils/Stopwatch.java @@ -45,11 +45,4 @@ private static String milisecondsToTime(long miliseconds) { if (m > 0) return String.format("%02dm %02ds", m, (long) s); return String.format("%6.3fs", s); } - - public long getIntermediateMilliseconds() { - long endd = System.currentTimeMillis(); - long rez = lastIntermediate - endd; - lastIntermediate = endd; - return rez; - } } diff --git a/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java b/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java index 9bd827168ac..94bf158bf68 100644 --- a/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java +++ b/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java @@ -91,30 +91,6 @@ public void registerCriticalWarning(ExceptionType type, String message, Throwabl register(type, KExceptionGroup.CRITICAL, message, e, null, null); } - public void registerCriticalWarning(ExceptionType type, String message, HasLocation node) { - register( - type, - KExceptionGroup.CRITICAL, - message, - null, - node.location().orElse(null), - node.source().orElse(null)); - } - - public void registerInternalWarning(ExceptionType type, String message) { - register(type, KExceptionGroup.INTERNAL, message, null, null, null); - } - - public void registerInternalWarning(ExceptionType type, String message, HasLocation node) { - register( - type, - KExceptionGroup.INTERNAL, - message, - null, - node.location().orElse(null), - node.source().orElse(null)); - } - public void registerInternalWarning(ExceptionType type, String message, Throwable e) { register(type, KExceptionGroup.INTERNAL, message, e, null, null); } @@ -174,22 +150,18 @@ private void registerInternal(KException exception, boolean _throw) { } public void print() { - Collections.sort( - exceptions, + exceptions.sort( Comparator.comparing(KException::getSource, Comparator.nullsLast(Comparator.naturalOrder())) .thenComparing(KException::getLocation, Comparator.nullsLast(Comparator.naturalOrder())) - .thenComparing(e -> e.toString(options.verbose))); + .thenComparing(KException::toString)); KException last = null; synchronized (exceptions) { for (KException e : exceptions) { - if (last != null && last.toString(options.verbose).equals(e.toString(options.verbose))) { + if (last != null && last.toString().equals(e.toString())) { continue; } printStackTrace(e); - String msg = - options.noExcWrap - ? e.toString(options.verbose) - : StringUtil.splitLines(e.toString(options.verbose)); + String msg = options.noExcWrap ? e.toString() : StringUtil.splitLines(e.toString()); System.err.println(msg); last = e; } diff --git a/kernel/src/main/java/org/kframework/utils/file/FileUtil.java b/kernel/src/main/java/org/kframework/utils/file/FileUtil.java index 25f60089b22..61deb271aa7 100644 --- a/kernel/src/main/java/org/kframework/utils/file/FileUtil.java +++ b/kernel/src/main/java/org/kframework/utils/file/FileUtil.java @@ -2,33 +2,20 @@ package org.kframework.utils.file; import com.google.inject.Inject; -import java.io.BufferedReader; import java.io.File; -import java.io.FileInputStream; import java.io.FileNotFoundException; import java.io.FileReader; import java.io.IOException; -import java.io.InputStream; -import java.io.InputStreamReader; -import java.io.PipedInputStream; -import java.io.PipedOutputStream; import java.io.Reader; import java.text.DateFormat; import java.text.SimpleDateFormat; import java.util.Calendar; import java.util.Date; import java.util.Map; -import java.util.Properties; import java.util.UUID; -import java.util.stream.Collectors; -import java.util.stream.Stream; import javax.annotation.Nullable; import org.apache.commons.io.FileUtils; -import org.apache.commons.io.FilenameUtils; import org.apache.commons.io.IOUtils; -import org.apache.commons.io.input.BoundedInputStream; -import org.apache.commons.lang3.tuple.Pair; -import org.kframework.attributes.Location; import org.kframework.main.GlobalOptions; import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.errorsystem.KException.ExceptionType; @@ -85,11 +72,6 @@ public void deleteTempDir(KExceptionManager kem) { } } - /** Get language name in uppercase (main module name) given the filename of definition. */ - public static String getMainModule(String filename) { - return FilenameUtils.getBaseName(filename).toUpperCase(); - } - // generate an unique name for a folder with the name dirName public static String generateUniqueFolderName(String dirName) { DateFormat df = new SimpleDateFormat("-yyyy-MM-dd-HH-mm-ss-SSS-"); @@ -98,17 +80,6 @@ public static String generateUniqueFolderName(String dirName) { return dirName + reportDate + UUID.randomUUID(); } - /** Loads the properties from the given file into the given Properties object. */ - public static void loadProperties(Properties properties, Class cls, String resourcePath) - throws IOException { - try (InputStream inStream = cls.getResourceAsStream(resourcePath)) { - if (inStream == null) { - throw new IOException("Could not find resource " + resourcePath); - } - properties.load(inStream); - } - } - public void saveToDefinitionDirectory(String file, String content) { save(resolveDefinitionDirectory(file), content); } @@ -117,38 +88,18 @@ public String loadFromWorkingDirectory(String file) { return load(resolveWorkingDirectory(file)); } - public void saveToWorkingDirectory(String file, String content) { - save(resolveWorkingDirectory(file), content); - } - public void saveToWorkingDirectory(String file, byte[] content) { save(resolveWorkingDirectory(file), content); } - public String loadFromKompiled(String file) { - return load(resolveKompiled(file)); - } - public void saveToKompiled(String file, String content) { save(resolveKompiled(file), content); } - public String loadFromTemp(String file) { - return load(resolveTemp(file)); - } - - public byte[] loadBytesFromTemp(String file) { - return loadBytes(resolveTemp(file)); - } - public void saveToTemp(String file, String content) { save(resolveTemp(file), content); } - public void saveToTemp(String file, byte[] content) { - save(resolveTemp(file), content); - } - public String loadFromKIncludeDir(String file) { return load(resolveKInclude(file)); } @@ -181,39 +132,6 @@ public File resolveKInclude(String file) { return new File(JarInfo.getKIncludeDir().toFile(), file); } - // don't use this if you want a file in the include directory. Use resolveKInclude. - public File resolveKBase(String file) { - return new File(JarInfo.getKBase(), file); - } - - public void copyTempFileToDefinitionDirectory(String fromPath) { - copyFileToDirectory(resolveTemp(fromPath), resolveDefinitionDirectory(".")); - } - - public void copyTempFileToKompiledDirectory(String fromPath) { - copyFileToDirectory(resolveTemp(fromPath), resolveKompiled(".")); - } - - public void copyTempFileToKompiledFile(String fromPath, String toPath) { - copyFile(resolveTemp(fromPath), resolveKompiled(toPath)); - } - - private void copyFile(File from, File to) { - try { - FileUtils.copyFile(from, to); - } catch (IOException e) { - throw KEMException.criticalError("Could not copy " + from + " to " + to, e); - } - } - - public void copyFileToDirectory(File from, File toDir) { - try { - FileUtils.copyFileToDirectory(from, toDir); - } catch (IOException e) { - throw KEMException.criticalError("Could not copy " + from + " to directory " + toDir, e); - } - } - public static void save(File file, String content) { try { File dir = file.getAbsoluteFile().getParentFile(); @@ -246,32 +164,6 @@ public static String load(File file) { } } - /** - * Loads the given fragment of a file to String. - * - *

Source: https://stackoverflow.com/a/4305478/4182868 - */ - public static String loadFragment(File file, int pos, int len) { - try (FileInputStream stream = new FileInputStream(file)) { - stream.skip(pos); - return IOUtils.toString(new BoundedInputStream(stream, len)); - } catch (IOException e) { - throw KEMException.criticalError("Could not read from file " + file.getAbsolutePath(), e); - } - } - - public static String loadFragment(File file, Location location) { - try (Stream lines = - new BufferedReader(new InputStreamReader(new FileInputStream(file))) - .lines() - .skip(location.startLine() - 1) - .limit(location.endLine() - location.startLine() + 1)) { - return lines.collect(Collectors.joining("\n")); - } catch (IOException e) { - throw KEMException.criticalError("Could not read from file " + file.getAbsolutePath(), e); - } - } - public static byte[] loadBytes(File file) { try { return FileUtils.readFileToByteArray(file); @@ -280,26 +172,6 @@ public static byte[] loadBytes(File file) { } } - public static Pair pipeOutputToInput() { - try { - PipedOutputStream out = new PipedOutputStream(); - PipedInputStream in = new PipedInputStream(out); - return Pair.of(in, out); - } catch (IOException e) { - throw KEMException.internalError("Error creating input/output pipe", e); - } - } - - public static Pair pipeInputToOutput() { - try { - PipedInputStream in = new PipedInputStream(); - PipedOutputStream out = new PipedOutputStream(in); - return Pair.of(out, in); - } catch (IOException e) { - throw KEMException.internalError("Error creating input/output pipe", e); - } - } - public static String read(Reader reader) { try { return IOUtils.toString(reader); diff --git a/kernel/src/main/java/org/kframework/utils/inject/Annotations.java b/kernel/src/main/java/org/kframework/utils/inject/Annotations.java index 94b004e3722..da4b49b4692 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/Annotations.java +++ b/kernel/src/main/java/org/kframework/utils/inject/Annotations.java @@ -31,58 +31,4 @@ public boolean equals(Object o) { } }; } - - public static Spec1 spec1(Class annotation) { - return new Spec1() { - - @Override - public Class annotationType() { - return Spec1.class; - } - - @Override - public Class value() { - return annotation; - } - - public int hashCode() { - // This is specified in java.lang.Annotation. - return (127 * "value".hashCode()) ^ annotation.hashCode(); - } - - public boolean equals(Object o) { - if (!(o instanceof Spec1 other)) { - return false; - } - return annotation.equals(other.value()); - } - }; - } - - public static Spec2 spec2(Class annotation) { - return new Spec2() { - - @Override - public Class annotationType() { - return Spec2.class; - } - - @Override - public Class value() { - return annotation; - } - - public int hashCode() { - // This is specified in java.lang.Annotation. - return (127 * "value".hashCode()) ^ annotation.hashCode(); - } - - public boolean equals(Object o) { - if (!(o instanceof Spec2 other)) { - return false; - } - return annotation.equals(other.value()); - } - }; - } } diff --git a/kernel/src/main/java/org/kframework/utils/inject/GraphInjector.java b/kernel/src/main/java/org/kframework/utils/inject/GraphInjector.java deleted file mode 100644 index 70de2579c1f..00000000000 --- a/kernel/src/main/java/org/kframework/utils/inject/GraphInjector.java +++ /dev/null @@ -1,32 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.utils.inject; - -import com.google.inject.Guice; -import com.google.inject.Injector; -import com.google.inject.grapher.graphviz.GraphvizGrapher; -import com.google.inject.grapher.graphviz.GraphvizModule; -import java.io.File; -import java.io.IOException; -import java.io.PrintWriter; -import java.nio.charset.StandardCharsets; -import java.util.Arrays; -import org.kframework.main.Main; - -public class GraphInjector { - - public static void main(String[] args) throws IOException { - String[] args2 = Arrays.copyOfRange(args, 1, args.length); - Injector injector = Main.getInjector(args[0]); - graph("injector.dot", injector); - } - - private static void graph(String filename, Injector demoInjector) throws IOException { - PrintWriter out = new PrintWriter(new File(filename), StandardCharsets.UTF_8); - - Injector injector = Guice.createInjector(new GraphvizModule()); - GraphvizGrapher grapher = injector.getInstance(GraphvizGrapher.class); - grapher.setOut(out); - grapher.setRankdir("TB"); - grapher.graph(demoInjector); - } -} diff --git a/kernel/src/main/java/org/kframework/utils/options/EnumSetConverter.java b/kernel/src/main/java/org/kframework/utils/options/EnumSetConverter.java deleted file mode 100644 index 248028c08f7..00000000000 --- a/kernel/src/main/java/org/kframework/utils/options/EnumSetConverter.java +++ /dev/null @@ -1,30 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.utils.options; - -import com.beust.jcommander.converters.BaseConverter; -import java.util.EnumSet; -import java.util.List; -import java.util.Set; - -public abstract class EnumSetConverter, C extends BaseEnumConverter> - extends BaseConverter> { - - public EnumSetConverter(String optionName) { - super(optionName); - } - - private final StringListConverter converter = new StringListConverter(); - - @Override - public Set convert(String val) { - List values = converter.convert(val); - Set set = EnumSet.noneOf(enumConverter().enumClass()); - for (String value : values) { - T t = enumConverter().convert(value); - set.add(t); - } - return set; - } - - public abstract C enumConverter(); -} diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java index 435aec3b204..82b28964056 100644 --- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java @@ -28,24 +28,6 @@ public Class enumClass() { } } - @Parameter( - names = "--ignore-missing-smtlib-warning", - description = "Suppress warning when SMTLib translation fails.", - hidden = true) - public boolean ignoreMissingSMTLibWarning = false; - - @Parameter( - names = "--floats-as-po", - description = "Abstracts floating-point values as a partial order relation.", - hidden = true) - public boolean floatsAsPO = false; - - @Parameter( - names = "--maps-as-int-array", - description = "Abstracts map values as an array of ints.", - hidden = true) - public boolean mapAsIntArray = false; - @Parameter( names = {"--smt-prelude", "--smt_prelude"}, description = "Path to the SMT prelude file.", @@ -59,19 +41,4 @@ public Class enumClass() { description = "Timeout for calls to the SMT solver, in milliseconds.", hidden = true) public Integer smtTimeout = null; - - @Parameter( - names = "--z3-jni", - description = - "Invokes Z3 as JNI library. Default is external process. " - + "JNI is slightly faster, but can potentially lead to JVM crash.", - hidden = true) - public boolean z3JNI = false; - - @Parameter( - names = "--z3-tactic", - descriptionKey = "solver", - description = "The path to solver tactic to use to check satisfiability in Z3.", - hidden = true) - public String z3Tactic; } diff --git a/kernel/src/test/java/org/kframework/compile/TestConfiguration.java b/kernel/src/test/java/org/kframework/compile/TestConfiguration.java index f54bb79acda..f048eb6ef7c 100644 --- a/kernel/src/test/java/org/kframework/compile/TestConfiguration.java +++ b/kernel/src/test/java/org/kframework/compile/TestConfiguration.java @@ -11,7 +11,6 @@ import com.google.common.collect.Maps; import java.util.List; import java.util.Map; -import java.util.Set; import org.kframework.kore.KApply; import org.kframework.kore.KLabel; import org.kframework.kore.Sort; @@ -113,11 +112,6 @@ public boolean isCell(Sort k) { return levels.containsKey(k); } - @Override - public boolean isCellCollection(Sort s) { - return cellCollectionSorts.containsKey(s); - } - @Override public boolean isCellLabel(KLabel kLabel) { return getCellSort(kLabel) != null; @@ -186,11 +180,6 @@ public Sort getComputationCell() { return computationCell; } - @Override - public Set getCellSorts() { - return cellLabels.keySet(); - } - @Override public KApply getUnit(Sort k) { return KApply(units.get(k)); diff --git a/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java b/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java index 9cc0bb1393f..58993b3c2e8 100644 --- a/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java +++ b/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java @@ -68,14 +68,14 @@ public void test1() { public void test2() { String selectExp = "k|"; KExceptionManager kem = new KExceptionManager(new GlobalOptions()); - ExtractFencedKCodeFromMarkdown mdExtractor = new ExtractFencedKCodeFromMarkdown(kem, selectExp); + new ExtractFencedKCodeFromMarkdown(kem, selectExp); } @Test(expected = KEMException.class) public void test3() { String selectExp = "k|a b"; KExceptionManager kem = new KExceptionManager(new GlobalOptions()); - ExtractFencedKCodeFromMarkdown mdExtractor = new ExtractFencedKCodeFromMarkdown(kem, selectExp); + new ExtractFencedKCodeFromMarkdown(kem, selectExp); } @Test diff --git a/kore/src/main/java/org/kframework/builtin/KLabels.java b/kore/src/main/java/org/kframework/builtin/KLabels.java index 13703a6208e..041be16289a 100644 --- a/kore/src/main/java/org/kframework/builtin/KLabels.java +++ b/kore/src/main/java/org/kframework/builtin/KLabels.java @@ -31,7 +31,6 @@ public class KLabels { public static final KLabel INIT_GENERATED_COUNTER_CELL = KLabel("initGeneratedCounterCell"); public static final String THIS_CONFIGURATION = "THIS_CONFIGURATION"; - public static final String STRATEGY_CELL_NAME = "s"; public static final KLabel STRATEGY_CELL = KLabel(""); public static final KLabel STUCK = KLabel("#STUCK"); @@ -60,21 +59,11 @@ public class KLabels { public static final KLabel Set = KLabel("_Set_"); public static final KLabel DotSet = KLabel(".Set"); - public static final KLabel EQUALS_K = KLabel("_==K_"); public static final KLabel NOT_EQUALS_K = KLabel("_=/=K_"); public static final KLabel IN_K = KLabel("_:=K_"); public static final KLabel NOT_IN_K = KLabel("_:/=K_"); - public static final KLabel MAP_CHOICE = KLabel("Map:choice"); - public static final KLabel SET_CHOICE = KLabel("Set:choice"); - public static final KLabel LIST_GET = KLabel("List:get"); public static final KLabel MAP_LOOKUP = KLabel("Map:lookup"); - public static final KLabel SET_MEMBERSHIP = KLabel("Set:in"); - public static final KLabel LIST_RANGE = KLabel("List:range"); - public static final KLabel MAP_UPDATE = KLabel("updateMap"); - public static final KLabel MAP_REMOVE_ALL = KLabel("removeAll"); - public static final KLabel SET_REMOVE_ALL = KLabel("Set:difference"); - public static final KLabel MAP_KEYS = KLabel("keys"); public static final String INJ = "inj"; } diff --git a/kore/src/main/java/org/kframework/builtin/Rules.java b/kore/src/main/java/org/kframework/builtin/Rules.java deleted file mode 100644 index 5e6007b6f8a..00000000000 --- a/kore/src/main/java/org/kframework/builtin/Rules.java +++ /dev/null @@ -1,20 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.builtin; - -import static org.kframework.kore.KORE.*; - -import org.kframework.kore.KRewrite; - -public class Rules { - public static final KRewrite STUCK_RULE = - KRewrite( - KApply( - KLabels.STRATEGY_CELL, - KList( - KApply(KLabels.KSEQ, KList(KApply(KLabels.DOTK, KList()), KVariable("#REST"))))), - KApply( - KLabels.STRATEGY_CELL, - KList( - KApply( - KLabels.KSEQ, KList(KApply(KLabels.STUCK, KList()), KVariable("#REST")))))); -} diff --git a/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java b/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java index c9f80d0cbe9..f4f51bd0288 100644 --- a/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java +++ b/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java @@ -2,7 +2,6 @@ package org.kframework.compile; import java.util.List; -import java.util.Set; import org.kframework.kore.KApply; import org.kframework.kore.KLabel; import org.kframework.kore.Sort; @@ -29,9 +28,6 @@ public interface ConfigurationInfo { /** True if sort k is actually a cell sort */ boolean isCell(Sort k); - /** True if sort s is the collection sort for a multiplicity star cell. */ - boolean isCellCollection(Sort s); - /** True if kLabel is the KLabel of a cell */ boolean isCellLabel(KLabel kLabel); @@ -78,9 +74,6 @@ public interface ConfigurationInfo { /** Return the declared computation cell, by default the k cell */ Sort getComputationCell(); - /** Returns the set of cell sorts in this configuration */ - Set getCellSorts(); - /** Returns the unit of a * or ? cell. */ KApply getUnit(Sort k); diff --git a/kore/src/main/java/org/kframework/kore/AttCompare.java b/kore/src/main/java/org/kframework/kore/AttCompare.java index b863be24694..7762a5fe67e 100644 --- a/kore/src/main/java/org/kframework/kore/AttCompare.java +++ b/kore/src/main/java/org/kframework/kore/AttCompare.java @@ -72,8 +72,4 @@ public String toString() { public int hashCode() { return k.hashCode(); } - - public K get() { - return k; - } } diff --git a/kore/src/main/java/org/kframework/parser/KoreParser.java b/kore/src/main/java/org/kframework/parser/KoreParser.java index dd03195d9c9..d66253c02ae 100644 --- a/kore/src/main/java/org/kframework/parser/KoreParser.java +++ b/kore/src/main/java/org/kframework/parser/KoreParser.java @@ -41,9 +41,4 @@ public K parseFile(File koreFile) throws ParseError { Pattern kore = textToKore.parsePattern(koreFile, 0); return koreToK.apply(kore); } - - public K parseFile(File koreFile, int line) throws ParseError { - Pattern kore = textToKore.parsePattern(koreFile, line); - return koreToK.apply(kore); - } } diff --git a/kore/src/main/java/org/kframework/rewriter/SearchType.java b/kore/src/main/java/org/kframework/rewriter/SearchType.java deleted file mode 100644 index f648cf3cb7e..00000000000 --- a/kore/src/main/java/org/kframework/rewriter/SearchType.java +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.rewriter; - -/** Created by manasvi on 9/11/15. */ -public enum SearchType { - ONE, - PLUS, - STAR, - FINAL -} diff --git a/kore/src/main/java/org/kframework/utils/OS.java b/kore/src/main/java/org/kframework/utils/OS.java index f78d2635fcf..57657362373 100644 --- a/kore/src/main/java/org/kframework/utils/OS.java +++ b/kore/src/main/java/org/kframework/utils/OS.java @@ -39,19 +39,4 @@ public String getSharedLibraryExtension() { public List getSharedLibraryCompilerFlags() { return Arrays.asList("-fPIC", "-shared"); } - - public String getNativeExecutable(String executable) { - if (this == UNKNOWN) { - throw KEMException.internalError( - "Unknown OS type. " - + System.getProperty("os.name") - + " not recognized. " - + "Please contact K developers with details of your OS."); - } - if (this == WINDOWS) { - throw KEMException.internalError( - "K is not supported on native windows. Please use the Windows Subsystem for Linux."); - } - return executable; - } } diff --git a/kore/src/main/java/org/kframework/utils/StringUtil.java b/kore/src/main/java/org/kframework/utils/StringUtil.java index 59c20162fe4..92f082d5b71 100644 --- a/kore/src/main/java/org/kframework/utils/StringUtil.java +++ b/kore/src/main/java/org/kframework/utils/StringUtil.java @@ -283,123 +283,6 @@ public static String escapeNonASCII(String value) { return result.toString(); } - /** Returns the two-letter code for a general category of Unicode code point. */ - public static String getCategoryCode(byte cat) { - switch (cat) { - case Character.COMBINING_SPACING_MARK: - return "Mc"; - case Character.CONNECTOR_PUNCTUATION: - return "Pc"; - case Character.CONTROL: - return "Cc"; - case Character.CURRENCY_SYMBOL: - return "Sc"; - case Character.DASH_PUNCTUATION: - return "Pd"; - case Character.DECIMAL_DIGIT_NUMBER: - return "Nd"; - case Character.ENCLOSING_MARK: - return "Me"; - case Character.END_PUNCTUATION: - return "Pe"; - case Character.FINAL_QUOTE_PUNCTUATION: - return "Pf"; - case Character.FORMAT: - return "Cf"; - case Character.INITIAL_QUOTE_PUNCTUATION: - return "Pi"; - case Character.LETTER_NUMBER: - return "Nl"; - case Character.LINE_SEPARATOR: - return "Zl"; - case Character.LOWERCASE_LETTER: - return "Ll"; - case Character.MATH_SYMBOL: - return "Sm"; - case Character.MODIFIER_LETTER: - return "Lm"; - case Character.MODIFIER_SYMBOL: - return "Sk"; - case Character.NON_SPACING_MARK: - return "Mn"; - case Character.OTHER_LETTER: - return "Lo"; - case Character.OTHER_NUMBER: - return "No"; - case Character.OTHER_PUNCTUATION: - return "Po"; - case Character.OTHER_SYMBOL: - return "So"; - case Character.PARAGRAPH_SEPARATOR: - return "Zp"; - case Character.PRIVATE_USE: - return "Co"; - case Character.SPACE_SEPARATOR: - return "Zs"; - case Character.START_PUNCTUATION: - return "Ps"; - case Character.SURROGATE: - return "Cs"; - case Character.TITLECASE_LETTER: - return "Lt"; - case Character.UNASSIGNED: - return "Cn"; - case Character.UPPERCASE_LETTER: - return "Lu"; - default: - assert false : "should be exhaustive list of categories"; - return null; // unreachable - } - } - - public static String getDirectionalityCode(byte cat) { - switch (cat) { - case Character.DIRECTIONALITY_ARABIC_NUMBER: - return "AN"; - case Character.DIRECTIONALITY_BOUNDARY_NEUTRAL: - return "BN"; - case Character.DIRECTIONALITY_COMMON_NUMBER_SEPARATOR: - return "CS"; - case Character.DIRECTIONALITY_EUROPEAN_NUMBER: - return "EN"; - case Character.DIRECTIONALITY_EUROPEAN_NUMBER_SEPARATOR: - return "ES"; - case Character.DIRECTIONALITY_EUROPEAN_NUMBER_TERMINATOR: - return "ET"; - case Character.DIRECTIONALITY_LEFT_TO_RIGHT: - return "L"; - case Character.DIRECTIONALITY_LEFT_TO_RIGHT_EMBEDDING: - return "LRE"; - case Character.DIRECTIONALITY_LEFT_TO_RIGHT_OVERRIDE: - return "LRO"; - case Character.DIRECTIONALITY_NONSPACING_MARK: - return "NSM"; - case Character.DIRECTIONALITY_OTHER_NEUTRALS: - return "ON"; - case Character.DIRECTIONALITY_PARAGRAPH_SEPARATOR: - return "B"; - case Character.DIRECTIONALITY_POP_DIRECTIONAL_FORMAT: - return "PDF"; - case Character.DIRECTIONALITY_RIGHT_TO_LEFT: - return "R"; - case Character.DIRECTIONALITY_RIGHT_TO_LEFT_ARABIC: - return "AL"; - case Character.DIRECTIONALITY_RIGHT_TO_LEFT_EMBEDDING: - return "RLE"; - case Character.DIRECTIONALITY_RIGHT_TO_LEFT_OVERRIDE: - return "RLO"; - case Character.DIRECTIONALITY_SEGMENT_SEPARATOR: - return "S"; - case Character.DIRECTIONALITY_UNDEFINED: - throw new IllegalArgumentException(); - case Character.DIRECTIONALITY_WHITESPACE: - return "WS"; - default: - assert false : "should be exhaustive list of directionalities"; - return null; // unreachable - } - } - /** * split string to lines in a way that no lines will exceed 80 columns NOTE: strings split only at * whitespace character ' ', if string contains no ' ', it's returned as is @@ -497,36 +380,6 @@ public static String unescapeKoreKLabel(String str) { return sb.toString(); } - /** - * Takes the value of a KLabel and returns a string representation, delimited with backticks, of - * the syntax of that KLabel in KORE. - * - *

Used by the KAST pretty printer. - * - * @param value A string value corresponding to a KLabel. - * @return A string which can be parsed back by a KORE parser to reach the original KLabel. - */ - public static String escapeKoreKLabel(String value) { - char delimiter = '`'; - final int length = value.length(); - StringBuilder result = new StringBuilder(); - result.append(delimiter); - for (int offset = 0, codepoint; offset < length; offset += Character.charCount(codepoint)) { - codepoint = value.codePointAt(offset); - if (codepoint == 0x7F || codepoint < 32) { - throw new IllegalArgumentException("Special characters not supported here:" + value); - } else if (codepoint == delimiter) { - result.append("\\" + delimiter); - } else if (codepoint == '\\') { - result.append("\\\\"); - } else { - result.appendCodePoint(codepoint); - } - } - result.append(delimiter); - return result.toString(); - } - public static String[] asciiReadableEncodingDefault = new String[] { null, // 00 diff --git a/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java b/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java index 42941f1fb6c..79e29a24a6e 100644 --- a/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java +++ b/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java @@ -35,10 +35,6 @@ public class KEMException extends RuntimeException { e.getException()); } - public static KEMException debuggerError(String message) { - return create(ExceptionType.ERROR, KExceptionGroup.DEBUGGER, message, null, null, null); - } - public static KEMException criticalError(String message) { return create(ExceptionType.ERROR, KExceptionGroup.CRITICAL, message, null, null, null); } diff --git a/kore/src/main/java/org/kframework/utils/errorsystem/KException.java b/kore/src/main/java/org/kframework/utils/errorsystem/KException.java index cc81a36d069..e05e3a9ad28 100755 --- a/kore/src/main/java/org/kframework/utils/errorsystem/KException.java +++ b/kore/src/main/java/org/kframework/utils/errorsystem/KException.java @@ -149,10 +149,6 @@ public enum ExceptionType { @Override public String toString() { - return toString(false); - } - - public String toString(boolean verbose) { return "[" + (type == ExceptionType.ERROR ? "Error" : "Warning") + "] " diff --git a/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala b/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala index 01e3fca851a..b7af001331c 100644 --- a/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala +++ b/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala @@ -126,7 +126,6 @@ class ConfigurationInfoFromModule(val m: Module) extends ConfigurationInfo { override def getParent(k: Sort): Sort = edges.collectFirst { case (p, `k`) => p } get override def isCell(k: Sort): Boolean = cellSorts.contains(k) - override def isCellCollection(s: Sort): Boolean = cellBagSorts.contains(s) override def isCellLabel(kLabel: KLabel): Boolean = cellLabelsToSorts.contains(kLabel) override def isLeafCell(k: Sort): Boolean = !isParentCell(k) @@ -162,8 +161,7 @@ class ConfigurationInfoFromModule(val m: Module) extends ConfigurationInfo { topCells.head } - override def getComputationCell: Sort = mainCell - override def getCellSorts: util.Set[Sort] = cellSorts.asJava + override def getComputationCell: Sort = mainCell override def getUnit(k: Sort): KApply = if (getMultiplicity(k) == Multiplicity.OPTIONAL) diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 989c942f81a..497eb2acce5 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -4,7 +4,6 @@ package org.kframework.definition import dk.brics.automaton.RegExp import dk.brics.automaton.RunAutomaton -import dk.brics.automaton.SpecialOperations import java.util.Optional import javax.annotation.Nonnull import org.kframework.attributes._ @@ -21,18 +20,6 @@ import scala.collection.Set trait OuterKORE -case class NonTerminalsWithUndefinedSortException(nonTerminals: Set[NonTerminal]) - extends AssertionError(nonTerminals.toString()) - -case class DivergingAttributesForTheSameKLabel(ps: Set[Production]) - extends AssertionError(ps.toString) - -//object NonTerminalsWithUndefinedSortException { -// def apply(nonTerminals: Set[NonTerminal]) = -// new NonTerminalsWithUndefinedSortException(nonTerminals.toString, nonTerminals) -// -//} - case class Definition(mainModule: Module, entryModules: Set[Module], att: Att) extends DefinitionToString with OuterKORE @@ -61,7 +48,7 @@ case class Definition(mainModule: Module, entryModules: Set[Module], att: Att) trait Sorting { def computeSubsortPOSet(sentences: Set[Sentence], syntactic: Boolean) = { val subsortRelations: Set[(Sort, Sort)] = sentences.collect { - case Production(klabel, Seq(), endSort, Seq(NonTerminal(startSort, _)), att) + case Production(klabel, Seq(), endSort, Seq(NonTerminal(startSort, _)), _) if klabel.isEmpty || syntactic => (startSort, endSort) } @@ -209,30 +196,6 @@ case class Module( lazy val localKLabels: Set[KLabel] = localProductionsFor.keys.toSet.filter(!_.isInstanceOf[KVariable]) - lazy val klabelsDefinedInRules: Map[KLabel, Int] = { - def mergeMultiset(map1: Map[KLabel, Int], map2: Map[KLabel, Int]) = map1 ++ map2.map { - case (k, v) => k -> (v + map1.getOrElse(k, 0)) - } - - val transformer = new FoldK[Map[KLabel, Int]] { - override def apply(k: KApply): Map[KLabel, Int] = merge(apply(k.klist), Map((k.klabel, 1))) - - override def apply(k: InjectedKLabel): Map[KLabel, Int] = Map((k.klabel, 1)) - - def unit = Map() - - def merge(map1: Map[KLabel, Int], map2: Map[KLabel, Int]) = mergeMultiset(map1, map2) - } - rules - .map { r => - mergeMultiset( - transformer.apply(r.body), - mergeMultiset(transformer.apply(r.requires), transformer.apply(r.ensures)) - ) - } - .fold(Map())(mergeMultiset) - } - lazy val tokenSorts: Set[Sort] = sentences.collect { case p: Production if p.att.contains(Att.TOKEN) => p.sort @@ -267,11 +230,8 @@ case class Module( @transient lazy val sortFor: Map[KLabel, Sort] = productionsFor.mapValues(_.head.sort) - def isSort(klabel: KLabel, s: Sort): Boolean = subsorts.<(sortFor(klabel), s) - lazy val claims: Set[Claim] = sentences.collect { case c: Claim => c } lazy val rules: Set[Rule] = sentences.collect { case r: Rule => r } - lazy val rulesAndClaims: Set[RuleOrClaim] = Set[RuleOrClaim]().++(claims).++(rules) lazy val rulesFor: Map[KLabel, Set[Rule]] = rules.groupBy(r => matchKLabel(r)) lazy val macroKLabels: Set[KLabel] = macroKLabelsFromRules ++ macroKLabelsFromProductions lazy val macroKLabelsFromRules: Set[KLabel] = @@ -306,9 +266,8 @@ case class Module( lazy val sortedRules: Seq[Rule] = rules.toSeq.sorted - lazy val localRules: Set[Rule] = localSentences.collect { case r: Rule => r } - lazy val localClaims: Set[Claim] = localSentences.collect { case r: Claim => r } - lazy val localRulesAndClaims: Set[RuleOrClaim] = Set[RuleOrClaim]().++(localClaims).++(localRules) + lazy val localRules: Set[Rule] = localSentences.collect { case r: Rule => r } + lazy val localClaims: Set[Claim] = localSentences.collect { case r: Claim => r } // Check that productions with the same klabel have identical attributes // productionsFor.foreach { @@ -371,11 +330,6 @@ case class Module( lazy val localSorts: Set[Sort] = allSorts -- fullImports.flatMap(_.allSorts) lazy val sortedDefinedSorts: Seq[SortHead] = definedSorts.toSeq.sorted lazy val sortedAllSorts: Seq[Sort] = allSorts.toSeq.sorted - lazy val usedCellSorts: Set[Sort] = productions.flatMap { p => - p.items - .collect { case NonTerminal(s, _) => s } - .filter(s => s.name.endsWith("Cell") || s.name.endsWith("CellFragment")) - } lazy val listSorts: Set[Sort] = sentences.collect { case Production(_, _, srt, _, att1) if att1.contains(Att.USER_LIST) => @@ -950,13 +904,7 @@ case class NonTerminal(sort: Sort, name: Option[String]) case class RegexTerminal(precedeRegex: String, regex: String, followRegex: String) extends TerminalLike with RegexTerminalToString { - lazy val pattern = new RunAutomaton(new RegExp(regex).toAutomaton, false) - lazy val followPattern = new RunAutomaton(new RegExp(followRegex).toAutomaton, false) - lazy val precedePattern = { - val unreversed = new RegExp(precedeRegex).toAutomaton - SpecialOperations.reverse(unreversed) - new RunAutomaton(unreversed, false) - } + lazy val pattern = new RunAutomaton(new RegExp(regex).toAutomaton, false) def compareTo(t: TerminalLike): Int = { if (t.isInstanceOf[Terminal]) { diff --git a/kore/src/main/scala/org/kframework/rewriter/Rewriter.scala b/kore/src/main/scala/org/kframework/rewriter/Rewriter.scala index 3a59eff97c9..31191a4c811 100644 --- a/kore/src/main/scala/org/kframework/rewriter/Rewriter.scala +++ b/kore/src/main/scala/org/kframework/rewriter/Rewriter.scala @@ -7,8 +7,6 @@ import org.kframework.definition.Rule import org.kframework.kore import org.kframework.RewriterResult -trait RewriterConstructor extends (Module => Rewriter) - trait Rewriter { // def normalize(k: K): K // def substitute(k: K, s: KVariable => K): K @@ -45,22 +43,9 @@ trait Rewriter { initialConfiguration: kore.K, depth: Optional[Integer], bound: Optional[Integer], - pattern: Rule, - searchType: SearchType + pattern: Rule ): kore.K - def executeAndMatch( - k: kore.K, - depth: Optional[Integer], - rule: Rule - ): Tuple2[RewriterResult, kore.K] - def prove(rules: Module, reuseDef: java.lang.Boolean): RewriterResult - def equivalence( - firstDef: Rewriter, - secondDef: Rewriter, - firstSpec: Module, - secondSpec: Module - ): Boolean } diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java index c81977c38ef..6b1530eefa8 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java @@ -30,7 +30,6 @@ public class LLVMBackend extends KoreBackend { private final LLVMKompileOptions options; private final KExceptionManager kem; private final KompileOptions kompileOptions; - private final Tool tool; @Inject public LLVMBackend( @@ -45,13 +44,12 @@ public LLVMBackend( this.options = options; this.kompileOptions = kompileOptions; this.kem = kem; - this.tool = tool; } @Override public void accept(Backend.Holder h) { Stopwatch sw = new Stopwatch(globalOptions); - String kore = getKompiledString(h.def, true); + String kore = getKompiledString(h.def); h.def = null; files.saveToKompiled("definition.kore", kore); sw.printIntermediate(" Print definition.kore"); diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java index 9893c18768d..3646c96efc6 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java @@ -5,7 +5,7 @@ import com.beust.jcommander.Parameter; import com.google.inject.Inject; import java.util.ArrayList; -import java.util.Arrays; +import java.util.Collections; import java.util.List; import org.kframework.utils.inject.RequestScoped; @@ -31,7 +31,7 @@ public LLVMKompileOptions() {} public static class SingletonListConverter implements IStringConverter> { @Override public List convert(String str) { - return Arrays.asList(str); + return Collections.singletonList(str); } }