From 0164d62e6e921e958bf95e6e33f47efdb5a9afcf Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Tue, 30 Jan 2024 19:02:28 +0100 Subject: [PATCH] Delete dead classes (#3935) More dead code deletion; this is all the classes that IntelliJ reports as being globally-unused. Co-authored-by: rv-jenkins --- .../DeconstructIntegerAndFloatLiterals.java | 165 ------------------ .../kframework/compile/LiftToKSequence.java | 85 --------- .../main/AnnotatedByDefinitionModule.java | 42 ----- .../org/kframework/utils/inject/Builtins.java | 16 -- .../utils/options/OnOffConverter.java | 24 --- kore/src/main/java/org/kframework/API.java | 12 -- .../src/main/java/org/kframework/Warning.java | 5 - 7 files changed, 349 deletions(-) delete mode 100644 kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java delete mode 100644 kernel/src/main/java/org/kframework/compile/LiftToKSequence.java delete mode 100644 kernel/src/main/java/org/kframework/main/AnnotatedByDefinitionModule.java delete mode 100644 kernel/src/main/java/org/kframework/utils/inject/Builtins.java delete mode 100644 kernel/src/main/java/org/kframework/utils/options/OnOffConverter.java delete mode 100644 kore/src/main/java/org/kframework/API.java delete mode 100644 kore/src/main/java/org/kframework/Warning.java diff --git a/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java b/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java deleted file mode 100644 index c7e8f735642..00000000000 --- a/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java +++ /dev/null @@ -1,165 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.compile; - -import static org.kframework.definition.Constructors.*; -import static org.kframework.kore.KORE.*; - -import java.util.HashSet; -import java.util.Optional; -import java.util.Set; -import org.kframework.builtin.BooleanUtils; -import org.kframework.builtin.Sorts; -import org.kframework.definition.Context; -import org.kframework.definition.Rule; -import org.kframework.definition.Sentence; -import org.kframework.kore.*; - -/** - * Transforms patterns in the LHS of rules which have tokens of sort Int or Float into side - * conditions generating equality over a reconstructed value. Thus, - * - *

rule 5 => .K - * - *

becomes - * - *

rule I:Int => .K when I ==K 5 - */ -public class DeconstructIntegerAndFloatLiterals { - - private final Set state = new HashSet<>(); - private final Set vars = new HashSet<>(); - - void reset() { - state.clear(); - vars.clear(); - } - - void gatherVars(K term) { - new VisitK() { - @Override - public void apply(KVariable v) { - vars.add(v); - super.apply(v); - } - }.apply(term); - } - - public Sentence convert(Sentence s) { - if (ExpandMacros.isMacro(s)) { - return s; - } - if (s instanceof Rule) { - return convert((Rule) s); - } else if (s instanceof Context) { - return convert((Context) s); - } else { - return s; - } - } - - private Rule convert(Rule rule) { - reset(); - gatherVars(rule.body()); - gatherVars(rule.requires()); - gatherVars(rule.ensures()); - K body = convert(rule.body()); - K requires = convertLookups(rule.requires()); - return Rule(body, addSideCondition(requires), rule.ensures(), rule.att()); - } - - private K convertLookups(K requires) { - return new Transformer(false).apply(requires); - } - - private Context convert(Context context) { - reset(); - gatherVars(context.body()); - gatherVars(context.requires()); - K body = convert(context.body()); - return Context(body, addSideCondition(context.requires()), context.att()); - } - - private int counter = 0; - - KVariable newDotVariable(Sort sort) { - KVariable newLabel; - do { - newLabel = KVariable("_Gen" + (counter++), Att().add(Sort.class, sort)); - } while (vars.contains(newLabel)); - vars.add(newLabel); - return newLabel; - } - - K addSideCondition(K requires) { - Optional sideCondition = state.stream().reduce(BooleanUtils::and); - if (sideCondition.isEmpty()) { - return requires; - } else if (requires.equals(BooleanUtils.TRUE) && sideCondition.isPresent()) { - return sideCondition.get(); - } else { - return BooleanUtils.and(requires, sideCondition.get()); - } - } - - private K convert(K term) { - return new Transformer(true).apply(term); - } - - private class Transformer extends TransformK { - - @Override - public K apply(KToken k) { - if (lhs) { - if (k.sort().equals(Sorts.Int()) || k.sort().equals(Sorts.Float())) { - KVariable var = newDotVariable(k.sort()); - state.add(KApply(KLabel("_==" + k.sort().name() + "_"), var, k)); - return var; - } - } - return super.apply(k); - } - - private boolean lhs; - - public Transformer(boolean lhs) { - this.lhs = lhs; - } - - public boolean isLookupKLabel(KLabel k) { - return k.name().equals("#match") - || k.name().equals("#mapChoice") - || k.name().equals("#filterMapChoice") - || k.name().equals("#setChoice"); - } - - @Override - public K apply(KApply k) { - if (isLookupKLabel(k.klabel())) { - assert k.klist().size() == 2; - K r = apply(k.klist().items().get(1)); - lhs = true; - K l = apply(k.klist().items().get(0)); - lhs = false; - if (l != k.klist().items().get(0) || r != k.klist().items().get(1)) { - return KApply(k.klabel(), l, r); - } else { - return k; - } - } - return super.apply(k); - } - - @Override - public K apply(KRewrite k) { - K l = apply(k.left()); - lhs = false; - K r = apply(k.right()); - lhs = true; - if (l != k.left() || r != k.right()) { - return KRewrite(l, r, k.att()); - } else { - return k; - } - } - } -} diff --git a/kernel/src/main/java/org/kframework/compile/LiftToKSequence.java b/kernel/src/main/java/org/kframework/compile/LiftToKSequence.java deleted file mode 100644 index 6e54a69593e..00000000000 --- a/kernel/src/main/java/org/kframework/compile/LiftToKSequence.java +++ /dev/null @@ -1,85 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.compile; - -import static org.kframework.definition.Constructors.*; -import static org.kframework.kore.KORE.*; - -import java.util.ArrayList; -import java.util.List; -import org.kframework.builtin.KLabels; -import org.kframework.builtin.Sorts; -import org.kframework.definition.Context; -import org.kframework.definition.Rule; -import org.kframework.definition.Sentence; -import org.kframework.kore.*; - -/** - * Raises all rules into a form with a KSequence in every position that expects a term of sort K. - */ -public class LiftToKSequence { - - public Sentence lift(Sentence s) { - if (s instanceof Rule) { - return lift((Rule) s); - } else if (s instanceof Context) { - return lift((Context) s); - } else { - return s; - } - } - - private Rule lift(Rule rule) { - return Rule(lift(rule.body()), lift(rule.requires()), lift(rule.ensures()), rule.att()); - } - - private Context lift(Context context) { - return Context(lift(context.body()), lift(context.requires()), context.att()); - } - - public K lift(K term) { - K result = - new TransformK() { - @Override - public K apply(KApply k) { - List children = new ArrayList<>(); - for (K child : k.klist().items()) { - K res = apply(child); - if (res instanceof KSequence || k.klabel().equals(KLabels.ML_OR)) { - children.add(res); - } else { - children.add(KSequence(res)); - } - } - return KApply(k.klabel(), KList(children), k.att()); - } - - @Override - public K apply(KAs k) { - K res = apply(k.pattern()); - KVariable var = (KVariable) k.alias(); - if (!(res instanceof KSequence) - && var.att().getOptional(Sort.class).orElse(Sorts.K()).equals(Sorts.K())) { - res = KSequence(res); - } - return KAs(res, k.alias(), k.att()); - } - }.apply(term); - if (result instanceof KSequence) { - return result; - } else { - return KSequence(result); - } - } - - public K lower(K term) { - return new TransformK() { - @Override - public K apply(KSequence k) { - if (k.items().size() == 1) { - return super.apply(k.items().get(0)); - } - return super.apply(k); - } - }.apply(term); - } -} diff --git a/kernel/src/main/java/org/kframework/main/AnnotatedByDefinitionModule.java b/kernel/src/main/java/org/kframework/main/AnnotatedByDefinitionModule.java deleted file mode 100644 index ac4b2bf3e8a..00000000000 --- a/kernel/src/main/java/org/kframework/main/AnnotatedByDefinitionModule.java +++ /dev/null @@ -1,42 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.main; - -import com.google.inject.Binding; -import com.google.inject.Key; -import com.google.inject.Module; -import com.google.inject.PrivateModule; -import com.google.inject.spi.DefaultElementVisitor; -import com.google.inject.spi.Element; -import com.google.inject.spi.Elements; -import java.lang.annotation.Annotation; -import java.util.List; -import java.util.function.Function; - -public abstract class AnnotatedByDefinitionModule extends PrivateModule { - - public void exposeBindings(List modules, Class cls, Function func) { - for (Element element : Elements.getElements(modules)) { - element.acceptVisitor( - new DefaultElementVisitor() { - @Override - public Void visit(Binding binding) { - Key key = binding.getKey(); - if (key.getAnnotation() == null && key.getAnnotationType() == null) { - bind(key.getTypeLiteral()).annotatedWith(cls).to(key.getTypeLiteral()); - expose(key.getTypeLiteral()).annotatedWith(cls); - } else if (key.getAnnotationType() != null - && !key.getAnnotationType() - .getPackage() - .equals(Package.getPackage("com.google.inject.multibindings"))) { - bind(key.getTypeLiteral()) - .annotatedWith(func.apply(key.getAnnotationType())) - .to(key); - expose(key.getTypeLiteral()).annotatedWith(func.apply(key.getAnnotationType())); - } - return null; - } - }); - } - modules.forEach(AnnotatedByDefinitionModule.this::install); - } -} diff --git a/kernel/src/main/java/org/kframework/utils/inject/Builtins.java b/kernel/src/main/java/org/kframework/utils/inject/Builtins.java deleted file mode 100644 index 7cd73a2ee7c..00000000000 --- a/kernel/src/main/java/org/kframework/utils/inject/Builtins.java +++ /dev/null @@ -1,16 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.utils.inject; - -import static java.lang.annotation.ElementType.FIELD; -import static java.lang.annotation.ElementType.METHOD; -import static java.lang.annotation.ElementType.PARAMETER; -import static java.lang.annotation.RetentionPolicy.RUNTIME; - -import com.google.inject.BindingAnnotation; -import java.lang.annotation.Retention; -import java.lang.annotation.Target; - -@BindingAnnotation -@Target({FIELD, PARAMETER, METHOD}) -@Retention(RUNTIME) -public @interface Builtins {} diff --git a/kernel/src/main/java/org/kframework/utils/options/OnOffConverter.java b/kernel/src/main/java/org/kframework/utils/options/OnOffConverter.java deleted file mode 100644 index ee60c792ed8..00000000000 --- a/kernel/src/main/java/org/kframework/utils/options/OnOffConverter.java +++ /dev/null @@ -1,24 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.utils.options; - -import com.beust.jcommander.ParameterException; -import com.beust.jcommander.converters.BaseConverter; - -public class OnOffConverter extends BaseConverter { - - public OnOffConverter(String optionName) { - super(optionName); - } - - @Override - public Boolean convert(String arg0) { - if (arg0.equals("on")) { - return true; - } else if (arg0.equals("off")) { - return false; - } else { - throw new ParameterException( - "\"" + getOptionName() + "\": must be either \"on\" or \"off\"."); - } - } -} diff --git a/kore/src/main/java/org/kframework/API.java b/kore/src/main/java/org/kframework/API.java deleted file mode 100644 index aa1aecdffe2..00000000000 --- a/kore/src/main/java/org/kframework/API.java +++ /dev/null @@ -1,12 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework; - -import java.lang.annotation.ElementType; -import java.lang.annotation.Target; - -/** - * Marker for classes we consider as part fo the K API. It is particularly important for these - * classes to be well-documented. - */ -@Target(ElementType.TYPE) -public @interface API {} diff --git a/kore/src/main/java/org/kframework/Warning.java b/kore/src/main/java/org/kframework/Warning.java deleted file mode 100644 index 16c858e45ea..00000000000 --- a/kore/src/main/java/org/kframework/Warning.java +++ /dev/null @@ -1,5 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework; - -@API -public interface Warning {}