fix bug where goal types of symbols are not correctly used for local …

…terms in modal logic embeddings
leoprover · Feb 13, 2024 · c1ec1b3 · c1ec1b3
1 parent 5418679
commit c1ec1b3
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 5 deletions.
diff --git a/build.sbt b/build.sbt
@@ -1,6 +1,6 @@
 lazy val commonSettings = Seq(
   organization := "org.leo",
-  version := "1.8.3",
+  version := "1.8.4",
   scalaVersion := "2.13.12",
   scalacOptions ++= Seq(
       "-deprecation",

diff --git a/embedding-app/src/main/scala/leo/modules/EmbeddingApp.scala b/embedding-app/src/main/scala/leo/modules/EmbeddingApp.scala
@@ -12,7 +12,7 @@ import scala.collection.mutable
 
 object EmbeddingApp {
   final val name: String = "embedproblem"
-  final val version: String = "1.8.3"
+  final val version: String = "1.8.4"
 
   private[this] var inputFileName = ""
   private[this] var outputFileName: Option[String] = None

diff --git a/...ng-runtime/src/main/scala/leo/modules/embeddings/FirstOrderManySortedToTXFEmbedding.scala b/...ng-runtime/src/main/scala/leo/modules/embeddings/FirstOrderManySortedToTXFEmbedding.scala
@@ -40,7 +40,7 @@ object FirstOrderManySortedToTXFEmbedding extends Embedding with ModalEmbeddingL
   override final def embeddingParameter: FOMLToTXFEmbeddingParameter.type = FOMLToTXFEmbeddingParameter
 
   override final val name: String = "$$fomlModel"
-  override final val version: String = "1.3.3"
+  override final val version: String = "1.3.4"
 
   override final def generateSpecification(specs: Map[String, String]): TPTP.TFFAnnotated =
     generateTFFSpecification(name, logicSpecParamNames, specs)
@@ -179,7 +179,7 @@ object FirstOrderManySortedToTXFEmbedding extends Embedding with ModalEmbeddingL
             case o@TFF.AtomicType("$o", _) => TFF.MappingType(worldType +: argTypes, o)
             case _ => escapedTyp
           }
-          symbolsWithGoalType = symbolsWithGoalType + (argumentTypesAndGoalTypeOfTFFType(typ)._2 -> (symbolsWithGoalType(typ) + ((atom, typ))))
+          symbolsWithGoalType = symbolsWithGoalType + (goalTy -> (symbolsWithGoalType(goalTy) + ((atom, typ))))
           TFFAnnotated(input.name, input.role, TFF.Typing(atom, convertedType), input.annotations)
         case _ => throw new EmbeddingException(s"Malformed type definition in formula '${input.name}', aborting.")
       }

diff --git a/embedding-runtime/src/main/scala/leo/modules/embeddings/ModalEmbedding.scala b/embedding-runtime/src/main/scala/leo/modules/embeddings/ModalEmbedding.scala
@@ -630,7 +630,8 @@ object ModalEmbedding extends Embedding with ModalEmbeddingLike {
           val rigidity = getRigidityOfSymbol(symbol, typ)
           rigidityMap = rigidityMap + (symbol -> rigidity) // add to table in case it was implicit (e.g. a predicate)
           val convertedType = convertConstantSymbolType(symbol, typ)
-          symbolsWithGoalType = symbolsWithGoalType + (goalType(typ) -> (symbolsWithGoalType(typ) + ((symbol, typ))))
+          val goalTy = goalType(typ)
+          symbolsWithGoalType = symbolsWithGoalType + (goalTy -> (symbolsWithGoalType(goalTy) + ((symbol, typ))))
           val convertedTyping = TPTP.THF.Typing(symbol, convertedType)
           TPTP.THFAnnotated(formula.name, formula.role, convertedTyping, formula.annotations)
         case _ => throw new EmbeddingException(s"Malformed type definition in formula '${formula.name}', aborting.")