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 df3346dc007..84a4fb343da 100644 --- a/kore/src/main/scala/org/kframework/parser/treeNodes.scala +++ b/kore/src/main/scala/org/kframework/parser/treeNodes.scala @@ -2,16 +2,15 @@ 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 java.lang.Iterable -import org.pcollections.{ConsPStack, PStack} -import collection.JavaConverters._ import org.kframework.utils.StringUtil +import org.pcollections.{ConsPStack, PStack} -import scala.collection.mutable; +import java.util._ +import scala.collection.JavaConverters._ +import scala.collection.mutable trait Term extends HasLocation { var location: Optional[Location] = Optional.empty() @@ -20,50 +19,54 @@ trait Term extends HasLocation { trait ProductionReference extends Term { val production: Production - var id: Optional[Integer] = Optional.empty() - - def setId(id: Optional[Integer]) { - 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) + ")" +case class Constant private (value: String, production: Production) extends ProductionReference { + 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) +case class TermCons private (items: PStack[Term], production: Production) + extends ProductionReference + with HasChildren { + def get(i: Int): Term = 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 = + TermCons(items.`with`(items.size() - 1 - i, e), production, location, source) - def replaceChildren(newChildren: Collection[Term]) = TermCons(ConsPStack.from(newChildren), production, location, source, id) + def replaceChildren(newChildren: java.util.Collection[Term]): TermCons = + TermCons(ConsPStack.from(newChildren), production, location, source) - 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: Collection[Term]) = Ambiguity(new HashSet[Term](newChildren), location, source) +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() = "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,25 +75,40 @@ 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] + ): 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, 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) + ) } 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