Skip to content

Commit 201d9a9

Browse files
author
Alexander Steen
committed
updated hybrid logic embedding to new modal-like parameter names
1 parent 47a1908 commit 201d9a9

File tree

1 file changed

+22
-29
lines changed

1 file changed

+22
-29
lines changed

‎embedding-runtime/src/main/scala/leo/modules/embeddings/HybridLogicEmbedding.scala‎

Lines changed: 22 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,13 @@ package embeddings
55
import datastructures.{FlexMap, TPTP}
66
import TPTP.{AnnotatedFormula, THF}
77

8-
object HybridLogicEmbedding extends Embedding {
8+
import scala.annotation.unused
9+
10+
object HybridLogicEmbedding extends Embedding with ModalEmbeddingLike {
911
object HybridLogicEmbeddingOption extends Enumeration {
1012
// Hidden on purpose, to allow distinction between the object itself and its values.
1113
// type ModalEmbeddingOption = Value
14+
@unused
1215
final val MONOMORPHIC, POLYMORPHIC,
1316
MODALITIES_SEMANTICAL, MODALITIES_SYNTACTICAL,
1417
DOMAINS_SEMANTICAL, DOMAINS_SYNTACTICAL = Value
@@ -18,22 +21,10 @@ object HybridLogicEmbedding extends Embedding {
1821
override final def embeddingParameter: HybridLogicEmbeddingOption.type = HybridLogicEmbeddingOption
1922

2023
override final def name: String = "$$hybrid"
21-
override final def version: String = "1.0"
22-
23-
private[this] final val defaultConstantSpec = "$rigid"
24-
private[this] final val defaultQuantificationSpec = "$constant"
25-
private[this] final val defaultModalitiesSpec = "$modal_system_K"
26-
override final def generateSpecification(specs: Map[String, String]): TPTP.THFAnnotated = {
27-
import modules.input.TPTPParser.annotatedTHF
28-
val spec: StringBuilder = new StringBuilder
29-
spec.append("thf(logic_spec, logic, (")
30-
spec.append("$$hybrid == [")
31-
spec.append("$constants == "); spec.append(specs.getOrElse("$constants", defaultConstantSpec)); spec.append(",")
32-
spec.append("$quantification == "); spec.append(specs.getOrElse("$quantification", defaultQuantificationSpec)); spec.append(",")
33-
spec.append("$modalities == "); spec.append(specs.getOrElse("$modalities", defaultModalitiesSpec))
34-
spec.append("] )).")
35-
annotatedTHF(spec.toString)
36-
}
24+
override final def version: String = "1.0.1"
25+
26+
override final def generateSpecification(specs: Map[String, String]): TPTP.THFAnnotated =
27+
generateTHFSpecification(name, logicSpecParamNames, specs)
3728

3829
override final def apply(problem: TPTP.Problem,
3930
embeddingOptions: Set[HybridLogicEmbeddingOption.Value]): TPTP.Problem =
@@ -97,15 +88,15 @@ object HybridLogicEmbedding extends Embedding {
9788
TPTP.Problem(problem.includes, result, Map.empty)
9889
}
9990

100-
def convertDefinitionFormula(formula: AnnotatedFormula): AnnotatedFormula = {
91+
private[this] def convertDefinitionFormula(formula: AnnotatedFormula): AnnotatedFormula = {
10192
formula match {
10293
case TPTP.THFAnnotated(name, "definition", THF.Logical(THF.BinaryFormula(THF.Eq, THF.FunctionTerm(symbolName, Seq()), body)), annotations) =>
10394
TPTP.THFAnnotated(name, "definition", THF.Logical(THF.BinaryFormula(THF.Eq, THF.FunctionTerm(symbolName, Seq()), convertFormula(body))), annotations)
10495
case _ => convertAnnotatedFormula(formula)
10596
}
10697
}
10798

108-
def convertAnnotatedFormula(formula: AnnotatedFormula): AnnotatedFormula = {
99+
private[this] def convertAnnotatedFormula(formula: AnnotatedFormula): AnnotatedFormula = {
109100
import leo.modules.tptputils._
110101
formula match {
111102
case TPTP.THFAnnotated(name, role, TPTP.THF.Logical(formula), annotations) =>
@@ -179,15 +170,15 @@ object HybridLogicEmbedding extends Embedding {
179170
case THF.NonclassicalPolyaryFormula(connective, args) =>
180171
connective match {
181172
case THF.NonclassicalLongOperator(name, index, parameters) => name match {
182-
case "$box" | "$necessary" | "$obligatory" | "$knows" =>
173+
case x if synonymsForBox.contains(x) =>
183174
if (parameters.nonEmpty) throw new EmbeddingException(s"Only up to one index is allowed in box operator, but parameters '${parameters.toString()}' was given.")
184175
val convertedConnective = index match {
185176
case Some(index0) => mboxIndexed(index0)
186177
case None => str2Fun("mbox")
187178
}
188179
val convertedArgs = args.map(convertFormula)
189180
convertedArgs.foldLeft(convertedConnective)(THF.BinaryFormula(THF.App, _, _))
190-
case "$dia" | "$possible" | "$permissible" =>
181+
case x if synonymsForDiamond.contains(x) =>
191182
if (parameters.nonEmpty) throw new EmbeddingException(s"Only up to one index is allowed in diamond operator, but parameters '${parameters.toString()}' was given.")
192183
val convertedConnective = index match {
193184
case Some(index0) => mdiaIndexed(index0)
@@ -822,7 +813,7 @@ object HybridLogicEmbedding extends Embedding {
822813
}
823814
}
824815

825-
lazy val semanticAxiomTable: Map[String, Option[TPTP.AnnotatedFormula]] = {
816+
private[this] lazy val semanticAxiomTable: Map[String, Option[TPTP.AnnotatedFormula]] = {
826817
import modules.input.TPTPParser.annotatedTHF
827818
Map(
828819
"$modal_axiom_K" -> None,
@@ -853,7 +844,7 @@ object HybridLogicEmbedding extends Embedding {
853844
// TODO: More axiom schemes
854845
)
855846
}
856-
lazy val syntacticAxiomTable: Map[String, Option[TPTP.AnnotatedFormula]] = {
847+
private[this] lazy val syntacticAxiomTable: Map[String, Option[TPTP.AnnotatedFormula]] = {
857848
import modules.input.TPTPParser.{annotatedTHF, thf}
858849

859850
Map(
@@ -933,7 +924,7 @@ object HybridLogicEmbedding extends Embedding {
933924
)
934925
}
935926

936-
lazy val indexedSyntacticAxiomTable: Map[String, Option[THF.Formula => TPTP.AnnotatedFormula]] = {
927+
private[this] lazy val indexedSyntacticAxiomTable: Map[String, Option[THF.Formula => TPTP.AnnotatedFormula]] = {
937928
import modules.input.TPTPParser.{annotatedTHF, thf}
938929
Map(
939930
"$modal_axiom_K" -> None,
@@ -1054,7 +1045,7 @@ object HybridLogicEmbedding extends Embedding {
10541045
)
10551046
}
10561047

1057-
lazy val indexedSemanticAxiomTable: Map[String, Option[THF.Formula => TPTP.AnnotatedFormula]] = {
1048+
private[this] lazy val indexedSemanticAxiomTable: Map[String, Option[THF.Formula => TPTP.AnnotatedFormula]] = {
10581049
import modules.input.TPTPParser.annotatedTHF
10591050
Map(
10601051
"$modal_axiom_K" -> None,
@@ -1087,7 +1078,7 @@ object HybridLogicEmbedding extends Embedding {
10871078
}
10881079

10891080
private def isModalSystemName(name: String): Boolean = name.startsWith("$modal_system_")
1090-
lazy val modalSystemTable: Map[String, Seq[String]] = Map(
1081+
private[this] lazy val modalSystemTable: Map[String, Seq[String]] = Map(
10911082
"$modal_system_K" -> Seq("$modal_axiom_K"),
10921083
"$modal_system_K4" -> Seq("$modal_axiom_K", "$modal_axiom_4"),
10931084
"$modal_system_K5" -> Seq("$modal_axiom_K", "$modal_axiom_5"),
@@ -1123,7 +1114,9 @@ object HybridLogicEmbedding extends Embedding {
11231114
spec0 foreach {
11241115
case THF.BinaryFormula(THF.==, THF.FunctionTerm(propertyName, Seq()), rhs) =>
11251116
propertyName match {
1126-
case "$constants" =>
1117+
case `logicSpecParamNameTermDesignation` =>
1118+
throw new EmbeddingException(s"Parameter '$logicSpecParamNameTermDesignation' currently unsupported; omitting it will probably coincide with global terms.")
1119+
case `logicSpecParamNameRigidity` =>
11271120
val (default, map) = parseTHFSpecRHS(rhs)
11281121
default match {
11291122
case Some("$rigid") => state.setDefault(RIGIDITY, RIGIDITY_RIGID)
@@ -1140,7 +1133,7 @@ object HybridLogicEmbedding extends Embedding {
11401133
case _ => throw new EmbeddingException(s"Unrecognized semantics option: '$rigidity'")
11411134
}
11421135
}
1143-
case "$quantification" =>
1136+
case `logicSpecParamNameQuantification` =>
11441137
val (default, map) = parseTHFSpecRHS(rhs)
11451138
default match {
11461139
case Some("$constant") => state.setDefault(DOMAIN, DOMAIN_CONSTANT)
@@ -1159,7 +1152,7 @@ object HybridLogicEmbedding extends Embedding {
11591152
case _ => throw new EmbeddingException(s"Unrecognized semantics option: '$quantification'")
11601153
}
11611154
}
1162-
case "$modalities" => val (default, map) = parseTHFListSpecRHS(rhs)
1155+
case `logicSpecParamNameModalities` => val (default, map) = parseTHFListSpecRHS(rhs)
11631156
if (default.nonEmpty) state.setDefault(MODALS, default)
11641157
map foreach { case (name, modalspec) =>
11651158
val realIndex = name match {

0 commit comments

Comments
 (0)