From 04812a8b86ada9d63830b8bc570d30537d6ed7e4 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Fri, 24 Nov 2023 16:04:51 -0500 Subject: [PATCH 1/3] Apply scalafmt with 100 column width. --- .../org/kframework/parser/treeNodes.scala | 72 ++++++++++++++----- 1 file changed, 54 insertions(+), 18 deletions(-) diff --git a/kore/src/main/scala/org/kframework/parser/treeNodes.scala b/kore/src/main/scala/org/kframework/parser/treeNodes.scala index df3346dc007..f1c38e7db97 100644 --- a/kore/src/main/scala/org/kframework/parser/treeNodes.scala +++ b/kore/src/main/scala/org/kframework/parser/treeNodes.scala @@ -11,7 +11,7 @@ import org.pcollections.{ConsPStack, PStack} import collection.JavaConverters._ import org.kframework.utils.StringUtil -import scala.collection.mutable; +import scala.collection.mutable trait Term extends HasLocation { var location: Optional[Location] = Optional.empty() @@ -33,37 +33,45 @@ trait HasChildren { def replaceChildren(newChildren: Collection[Term]): Term } -case class Constant private(value: String, production: Production) extends ProductionReference { +case class Constant private (value: String, production: Production) extends ProductionReference { override def toString = "#token(" + production.sort + "," + StringUtil.enquoteKString(value) + ")" override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(Constant.this); } // note that items is reversed because it is more efficient to generate it this way during parsing -case class TermCons private(items: PStack[Term], production: Production) - extends ProductionReference with HasChildren { +case class TermCons private (items: PStack[Term], production: Production) + extends ProductionReference + with HasChildren { def get(i: Int) = items.get(items.size() - 1 - i) - def `with`(i: Int, e: Term) = TermCons(items.`with`(items.size() - 1 - i, e), production, location, source, id) + def `with`(i: Int, e: Term) = + TermCons(items.`with`(items.size() - 1 - i, e), production, location, source, id) - def replaceChildren(newChildren: Collection[Term]) = TermCons(ConsPStack.from(newChildren), production, location, source, id) + def replaceChildren(newChildren: Collection[Term]) = + TermCons(ConsPStack.from(newChildren), production, location, source, id) override def toString() = new TreeNodesToKORE(s => Sort(s)).apply(this).toString() override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(TermCons.this); } -case class Ambiguity(items: Set[Term]) - extends Term with HasChildren { - def replaceChildren(newChildren: Collection[Term]) = Ambiguity(new HashSet[Term](newChildren), location, source) +case class Ambiguity(items: Set[Term]) extends Term with HasChildren { + def replaceChildren(newChildren: java.util.Collection[Term]) = + Ambiguity(new java.util.HashSet[Term](newChildren), location, source) - override def toString() = "amb(" + (items.asScala mkString ",") + ")" + override def toString: String = "amb(" + (items.asScala mkString ",") + ")" - override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(Ambiguity.this); + override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(Ambiguity.this) } object Constant { - def apply(value: String, production: Production, location: Optional[Location], source: Optional[Source]): Constant = { + def apply( + value: String, + production: Production, + location: Optional[Location], + source: Optional[Source] + ): Constant = { val res = Constant(value, production) res.location = location res.source = source @@ -72,7 +80,13 @@ object Constant { } object TermCons { - def apply(items: PStack[Term], production: Production, location: Optional[Location], source: Optional[Source], id: Optional[Integer]): TermCons = { + def apply( + items: PStack[Term], + production: Production, + location: Optional[Location], + source: Optional[Source], + id: Optional[Integer] + ): TermCons = { val res = TermCons(items, production) res.location = location res.source = source @@ -80,17 +94,39 @@ object TermCons { res } - def apply(items: PStack[Term], production: Production, location: Optional[Location], source: Optional[Source]): TermCons = { + def apply( + items: PStack[Term], + production: Production, + location: Optional[Location], + source: Optional[Source] + ): TermCons = { TermCons(items, production, location, source, Optional.empty()) } - def apply(items: PStack[Term], production: Production, location: Location, source: Source): TermCons = TermCons(items, production, Optional.of(location), Optional.of(source), Optional.empty()) + def apply( + items: PStack[Term], + production: Production, + location: Location, + source: Source + ): TermCons = TermCons( + items, + production, + Optional.of(location), + Optional.of(source), + Optional + .empty() + ) } object Ambiguity { - @annotation.varargs def apply(items: Term*): Ambiguity = Ambiguity(items.to[mutable.Set].asJava) - - def apply(items: Set[Term], location: Optional[Location], source: Optional[Source]): Ambiguity = { + @annotation.varargs + def apply(items: Term*): Ambiguity = Ambiguity(items.to[mutable.Set].asJava) + + def apply( + items: java.util.Set[Term], + location: Optional[Location], + source: Optional[Source] + ): Ambiguity = { val res = Ambiguity(items) res.location = location res.source = source From 2dd81773a6d2ea38ae0a63b0763126a25494d806 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Fri, 24 Nov 2023 16:14:18 -0500 Subject: [PATCH 2/3] Fix all IntelliJ warnings. --- .../org/kframework/parser/treeNodes.scala | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/kore/src/main/scala/org/kframework/parser/treeNodes.scala b/kore/src/main/scala/org/kframework/parser/treeNodes.scala index f1c38e7db97..47c5d996c19 100644 --- a/kore/src/main/scala/org/kframework/parser/treeNodes.scala +++ b/kore/src/main/scala/org/kframework/parser/treeNodes.scala @@ -6,7 +6,6 @@ import org.kframework.attributes.{Source, Location, HasLocation} import org.kframework.definition.Production import org.kframework.kore.KORE.Sort import java.util._ -import java.lang.Iterable import org.pcollections.{ConsPStack, PStack} import collection.JavaConverters._ import org.kframework.utils.StringUtil @@ -22,42 +21,43 @@ trait ProductionReference extends Term { val production: Production var id: Optional[Integer] = Optional.empty() - def setId(id: Optional[Integer]) { + def setId(id: Optional[Integer]): Unit = { this.id = id } } trait HasChildren { - def items: Iterable[Term] + def items: java.lang.Iterable[Term] - def replaceChildren(newChildren: Collection[Term]): Term + def replaceChildren(newChildren: java.util.Collection[Term]): Term } case class Constant private (value: String, production: Production) extends ProductionReference { - override def toString = "#token(" + production.sort + "," + StringUtil.enquoteKString(value) + ")" + override def toString: String = + "#token(" + production.sort + "," + StringUtil.enquoteKString(value) + ")" - override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(Constant.this); + override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(Constant.this) } // note that items is reversed because it is more efficient to generate it this way during parsing case class TermCons private (items: PStack[Term], production: Production) extends ProductionReference with HasChildren { - def get(i: Int) = items.get(items.size() - 1 - i) + def get(i: Int): Term = items.get(items.size() - 1 - i) - def `with`(i: Int, e: Term) = + def `with`(i: Int, e: Term): TermCons = TermCons(items.`with`(items.size() - 1 - i, e), production, location, source, id) - def replaceChildren(newChildren: Collection[Term]) = + def replaceChildren(newChildren: java.util.Collection[Term]): TermCons = TermCons(ConsPStack.from(newChildren), production, location, source, id) - override def toString() = new TreeNodesToKORE(s => Sort(s)).apply(this).toString() + override def toString: String = new TreeNodesToKORE(s => Sort(s)).apply(this).toString() - override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(TermCons.this); + override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(TermCons.this) } -case class Ambiguity(items: Set[Term]) extends Term with HasChildren { - def replaceChildren(newChildren: java.util.Collection[Term]) = +case class Ambiguity(items: java.util.Set[Term]) extends Term with HasChildren { + def replaceChildren(newChildren: java.util.Collection[Term]): Ambiguity = Ambiguity(new java.util.HashSet[Term](newChildren), location, source) override def toString: String = "amb(" + (items.asScala mkString ",") + ")" From e7942770874733b0cad85f9f8d3ab75e57008a77 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Fri, 24 Nov 2023 17:07:27 -0500 Subject: [PATCH 3/3] Remove id from ProductionReference and store in Map instead. --- .../inner/disambiguation/TypeInferencer.java | 19 ++++++----- .../org/kframework/parser/treeNodes.scala | 34 +++++-------------- 2 files changed, 18 insertions(+), 35 deletions(-) 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 d298381d849..8798ac1151d 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 @@ -66,6 +66,7 @@ public enum Status { private final boolean debug; private final Module mod; private final java.util.Set sorts; + private final Map prIds = new IdentityHashMap<>(); // logic QF_DT is best if it exists as it will be faster than ALL. However, some z3 versions do // not have this logic. @@ -593,7 +594,7 @@ public String apply(Term t) { boolean isTopSort = expectedSort.equals(Sorts.RuleContent()) || expectedSort.name().equals("#RuleBody"); int id = nextId; - boolean shared = pr.id().isPresent() && variablesById.size() > pr.id().get(); + boolean shared = prIds.containsKey(pr) && variablesById.size() > prIds.get(pr); if (!shared) { // if this is the first time reaching this term, initialize data structures with the // variables associated with @@ -601,7 +602,7 @@ public String apply(Term t) { nextId++; variablesById.add(new ArrayList<>()); cacheById.add(new HashSet<>()); - pr.setId(Optional.of(id)); + prIds.put(pr, id); for (Sort param : iterable(pr.production().params())) { String name = "FreshVar" + param.name() + locStr(pr); if (!variables.contains(name)) { @@ -612,7 +613,7 @@ public String apply(Term t) { } } else { // get cached id - id = pr.id().get(); + id = prIds.get(pr); } if (pr instanceof TermCons tc) { boolean wasStrict = isStrictEquality; @@ -682,7 +683,7 @@ public String apply(Term t) { nextId++; variablesById.add(new ArrayList<>()); cacheById.add(new HashSet<>()); - pr.setId(Optional.of(id)); + prIds.put(pr, id); if (isAnonVar(c)) { name = "Var" + c.value() + locStr(c); isStrictEquality = true; @@ -799,7 +800,7 @@ private String printSort(Sort s, Optional t, boolean isIncr Map params = new HashMap<>(); if (t.isPresent()) { if (t.get().production().params().nonEmpty()) { - int id = t.get().id().get(); + int id = prIds.get(t.get()); List names = variablesById.get(id); Seq formalParams = t.get().production().params(); assert (names.size() == formalParams.size()); @@ -945,8 +946,8 @@ void pushNotModel() { } public Seq getArgs(ProductionReference pr) { - if (pr.id().isPresent()) { - int id = pr.id().get(); + if (prIds.containsKey(pr)) { + int id = prIds.get(pr); List names = variablesById.get(id); return names.stream().map(this::getValue).collect(Collections.toList()); } else { @@ -1023,7 +1024,7 @@ private void reset() { } } - private static String locStr(ProductionReference pr) { + private String locStr(ProductionReference pr) { String suffix = ""; if (pr.production().klabel().isDefined()) { suffix = "_" + pr.production().klabel().get().name().replace("|", ""); @@ -1040,7 +1041,7 @@ private static String locStr(ProductionReference pr) { + l.endColumn() + suffix; } - return pr.id().get() + suffix; + return prIds.get(pr) + suffix; } private StringBuilder sb = new StringBuilder(); diff --git a/kore/src/main/scala/org/kframework/parser/treeNodes.scala b/kore/src/main/scala/org/kframework/parser/treeNodes.scala index 47c5d996c19..84a4fb343da 100644 --- a/kore/src/main/scala/org/kframework/parser/treeNodes.scala +++ b/kore/src/main/scala/org/kframework/parser/treeNodes.scala @@ -2,14 +2,14 @@ package org.kframework.parser -import org.kframework.attributes.{Source, Location, HasLocation} +import org.kframework.attributes.{HasLocation, Location, Source} import org.kframework.definition.Production import org.kframework.kore.KORE.Sort -import java.util._ -import org.pcollections.{ConsPStack, PStack} -import collection.JavaConverters._ import org.kframework.utils.StringUtil +import org.pcollections.{ConsPStack, PStack} +import java.util._ +import scala.collection.JavaConverters._ import scala.collection.mutable trait Term extends HasLocation { @@ -19,11 +19,6 @@ trait Term extends HasLocation { trait ProductionReference extends Term { val production: Production - var id: Optional[Integer] = Optional.empty() - - def setId(id: Optional[Integer]): Unit = { - this.id = id - } } trait HasChildren { @@ -46,10 +41,10 @@ case class TermCons private (items: PStack[Term], production: Production) def get(i: Int): Term = items.get(items.size() - 1 - i) def `with`(i: Int, e: Term): TermCons = - TermCons(items.`with`(items.size() - 1 - i, e), production, location, source, id) + TermCons(items.`with`(items.size() - 1 - i, e), production, location, source) def replaceChildren(newChildren: java.util.Collection[Term]): TermCons = - TermCons(ConsPStack.from(newChildren), production, location, source, id) + TermCons(ConsPStack.from(newChildren), production, location, source) override def toString: String = new TreeNodesToKORE(s => Sort(s)).apply(this).toString() @@ -84,25 +79,14 @@ object TermCons { items: PStack[Term], production: Production, location: Optional[Location], - source: Optional[Source], - id: Optional[Integer] + source: Optional[Source] ): TermCons = { val res = TermCons(items, production) res.location = location res.source = source - res.id = id res } - def apply( - items: PStack[Term], - production: Production, - location: Optional[Location], - source: Optional[Source] - ): TermCons = { - TermCons(items, production, location, source, Optional.empty()) - } - def apply( items: PStack[Term], production: Production, @@ -112,9 +96,7 @@ object TermCons { items, production, Optional.of(location), - Optional.of(source), - Optional - .empty() + Optional.of(source) ) }