adapt code to parser changes

leoprover · Mar 16, 2023 · de64e6d · de64e6d
1 parent 36abb25
commit de64e6d
Show file tree

Hide file tree

Showing 6 changed files with 48 additions and 33 deletions.
diff --git a/tptp-utils-app/src/main/scala/leo/modules/TPTPUtilsApp.scala b/tptp-utils-app/src/main/scala/leo/modules/TPTPUtilsApp.scala
@@ -10,7 +10,7 @@ import java.io.{File, FileNotFoundException, PrintWriter}
 
 object TPTPUtilsApp {
   final val name: String = "tptputils"
-  final val version: String = "1.2.1"
+  final val version: String = "1.2.3"
 
   private[this] var inputFileName = ""
   private[this] var outputFileName: Option[String] = None

diff --git a/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/Import.scala b/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/Import.scala
@@ -96,24 +96,36 @@ object Import {
     }
     private[this] def tptpProhibition(bearer: Option[TPTP.TFF.Term], left: TPTP.TFF.Formula, right: TPTP.TFF.Formula): TPTP.TFF.Formula = {
       bearer match {
-        case Some(value) => TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$prohibition", Seq(Right((TPTP.TFF.AtomicTerm("bearer", Seq.empty), value)))), Seq(left,right))
-        case None => TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$prohibition", Seq.empty), Seq(left,right))
+        case Some(value) => TPTP.TFF.NonclassicalPolyaryFormula(
+          TPTP.TFF.NonclassicalLongOperator("$$prohibition", None, Seq((TPTP.TFF.AtomicTerm("bearer", Seq.empty), value))),
+          Seq(left,right))
+        case None => TPTP.TFF.NonclassicalPolyaryFormula(
+          TPTP.TFF.NonclassicalLongOperator("$$prohibition", None, Seq.empty),
+          Seq(left,right))
       }
     }
     private[this] def tptpObligation(bearer: Option[TPTP.TFF.Term], left: TPTP.TFF.Formula, right: TPTP.TFF.Formula): TPTP.TFF.Formula = {
       bearer match {
-        case Some(value) => TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$obligation", Seq(Right((TPTP.TFF.AtomicTerm("bearer", Seq.empty), value)))), Seq(left,right))
-        case None => TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$obligation", Seq.empty), Seq(left,right))
+        case Some(value) => TPTP.TFF.NonclassicalPolyaryFormula(
+            TPTP.TFF.NonclassicalLongOperator("$$obligation", None, Seq((TPTP.TFF.AtomicTerm("bearer", Seq.empty), value))),
+            Seq(left, right))
+        case None => TPTP.TFF.NonclassicalPolyaryFormula(
+          TPTP.TFF.NonclassicalLongOperator("$$obligation", None, Seq.empty),
+          Seq(left, right))
       }
     }
     private[this] def tptpPermission(bearer: Option[TPTP.TFF.Term], left: TPTP.TFF.Formula, right: TPTP.TFF.Formula): TPTP.TFF.Formula = {
       bearer match {
-        case Some(value) => TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$permission", Seq(Right((TPTP.TFF.AtomicTerm("bearer", Seq.empty), value)))), Seq(left,right))
-        case None => TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$permission", Seq.empty), Seq(left,right))
+        case Some(value) => TPTP.TFF.NonclassicalPolyaryFormula(
+          TPTP.TFF.NonclassicalLongOperator("$$permission", None, Seq((TPTP.TFF.AtomicTerm("bearer", Seq.empty), value))),
+          Seq(left, right))
+        case None => TPTP.TFF.NonclassicalPolyaryFormula(
+          TPTP.TFF.NonclassicalLongOperator("$$permission", None, Seq.empty),
+          Seq(left, right))
       }
     }
     private[this] def tptpConstitutive(left: TPTP.TFF.Formula, right: TPTP.TFF.Formula): TPTP.TFF.Formula =
-      TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$constitutive", Seq.empty), Seq(left,right))
+      TPTP.TFF.NonclassicalPolyaryFormula(TPTP.TFF.NonclassicalLongOperator("$$constitutive", None, Seq.empty), Seq(left,right))
 
     private[this] def lrmlStatement(elem: xml.Node, associations: Map[String, Seq[String]]): TPTP.AnnotatedFormula = {
       val formulaName = elem.attribute("key")

diff --git a/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/Linter.scala b/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/Linter.scala
@@ -147,13 +147,15 @@ object Linter {
           case _ if arg.startsWith("$modal_axiom_") => ()
           case _ => buffer.append(error(s"Unknown argument $arg to parameter $name."))
         }
-        case THF.BinaryFormula(THF.==, op@THF.ConnectiveTerm(conn), rhs) =>
+        case THF.BinaryFormula(THF.==, op@THF.NonclassicalPolyaryFormula(conn, _), rhs) =>
           conn match {
-            case THF.NonclassicalLongOperator(connName, params) if Seq("$box", "$diamond").contains(connName) =>
+            case THF.NonclassicalLongOperator(connName, idx, params) if Seq("$box", "$diamond").contains(connName) =>
+              idx match {
+                case Some(_) => ()
+                case None => buffer.append(error("Assigning properties to non-indexed modal operator, use parameter default value for this."))
+              }
               params match {
-                case Seq(Left(_)) => ()
-                case Seq() => buffer.append(error("Assigning properties to non-indexed modal operator, use parameter default value for this."))
-                case _ => buffer.append(error(s"Malformed arguments to modal operator ${op.pretty}, use parameter default value for this."))
+                case _ => buffer.append(error(s"Malformed arguments to modal operator ${op.pretty}."))
               }
             case THF.NonclassicalBox(idx) => idx match {
               case Some(_) => ()

diff --git a/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/ParseTree.scala b/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/ParseTree.scala
@@ -52,6 +52,7 @@ object ParseTree {
     case THF.ConnectiveTerm(conn) => s"{ type : 'connectiveTerm' , connective : '${conn.pretty}' }"
     case THF.DistinctObject(name) => s"{ type : 'distinct' , name : '$name' }"
     case THF.NumberTerm(value) => s"{ type : 'number' , value : '${value.pretty}' }"
+    case THF.NonclassicalPolyaryFormula(connective, args) => s"{ type: 'connective', connective : '${connective.pretty}', body : [${args.map(thfFormula).mkString(",")}] }"
   }
 
   private[this] final def tffStatement(tffStatement: TPTP.TFF.Statement): String = tffStatement match {

diff --git a/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/SyntaxDowngrade.scala b/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/SyntaxDowngrade.scala
@@ -101,20 +101,6 @@ object SyntaxDowngrade {
 
         function match {
           case THF.FunctionTerm(f, Seq()) => TFF.AtomicFormula(f, arguments.map(thfLogicFormulaToTFFTerm))
-          case THF.ConnectiveTerm(conn) =>
-            val convertedConnective = conn match {
-              case THF.NonclassicalLongOperator(name, params) =>
-                val convertedParams = params.map {
-                  case Left(value) => Left(thfLogicFormulaToTFFTerm(value))
-                  case Right((l,r)) => Right((thfLogicFormulaToTFFTerm(l), thfLogicFormulaToTFFTerm(r)))
-                }
-                TFF.NonclassicalLongOperator(name,  convertedParams)
-              case THF.NonclassicalBox(idx) => TFF.NonclassicalBox(idx.map(thfLogicFormulaToTFFTerm))
-              case THF.NonclassicalDiamond(idx) => TFF.NonclassicalDiamond(idx.map(thfLogicFormulaToTFFTerm))
-              case THF.NonclassicalCone(idx) => TFF.NonclassicalCone(idx.map(thfLogicFormulaToTFFTerm))
-              case _ => throw new IllegalArgumentException(s"Unsupported formula in downgrade: ${formula.pretty}")
-            }
-            TFF.NonclassicalPolyaryFormula(convertedConnective, arguments.map(thfLogicFormulaToTFFFormula))
           case _ => throw new IllegalArgumentException(s"Unsupported formula in downgrade: ${formula.pretty}")
         }
       case THF.BinaryFormula(connective, left, right) =>
@@ -159,6 +145,20 @@ object SyntaxDowngrade {
         val convertedTyping = typing.map { case (name, typ) => (name, thfTypeToTFF(typ))}
         val convertedBinding = binding.map { case (lhs, rhs) => (thfLogicFormulaToTFFTerm(lhs), thfLogicFormulaToTFFTerm(rhs)) }
         TFF.LetFormula(convertedTyping, convertedBinding, thfLogicFormulaToTFFTerm(body))
+      case THF.NonclassicalPolyaryFormula(connective, args) =>
+        val convertedConnective = connective match {
+          case THF.NonclassicalLongOperator(name, idx, params) =>
+            val convertedIdx = idx.map(thfLogicFormulaToTFFTerm)
+            val convertedParams = params.map {
+              case (l, r) => (thfLogicFormulaToTFFTerm(l), thfLogicFormulaToTFFTerm(r))
+            }
+            TFF.NonclassicalLongOperator(name, convertedIdx, convertedParams)
+          case THF.NonclassicalBox(idx) => TFF.NonclassicalBox(idx.map(thfLogicFormulaToTFFTerm))
+          case THF.NonclassicalDiamond(idx) => TFF.NonclassicalDiamond(idx.map(thfLogicFormulaToTFFTerm))
+          case THF.NonclassicalCone(idx) => TFF.NonclassicalCone(idx.map(thfLogicFormulaToTFFTerm))
+          case _ => throw new IllegalArgumentException(s"Unsupported formula in downgrade: ${formula.pretty}")
+        }
+        TFF.NonclassicalPolyaryFormula(convertedConnective, args.map(thfLogicFormulaToTFFFormula))
       case _ => throw new IllegalArgumentException(s"Unsupported formula in downgrade: ${formula.pretty}")
     }
   }

diff --git a/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/SyntaxTransform.scala b/tptp-utils-runtime/src/main/scala/leo/modules/tptputils/SyntaxTransform.scala
@@ -137,18 +137,18 @@ object SyntaxTransform {
       case TFF.Assignment(lhs, rhs) => THF.BinaryFormula(THF.:=, tffTermToTHF(lhs), tffTermToTHF(rhs))
       case TFF.MetaIdentity(lhs, rhs) => THF.BinaryFormula(THF.==, tffTermToTHF(lhs), tffTermToTHF(rhs))
       case TFF.NonclassicalPolyaryFormula(connective, args) =>
-        val connective0: THF.VararyConnective = connective match {
-          case TFF.NonclassicalLongOperator(name, parameters) =>
+        val connective0: THF.VararyNonclassicalOperator = connective match {
+          case TFF.NonclassicalLongOperator(name, idx, parameters) =>
+            val idx0 = idx.map(tffTermToTHF)
             val parameters0 = parameters.map {
-              case Left(index) => Left(tffTermToTHF(index))
-              case Right((lhs, rhs)) => Right((tffTermToTHF(lhs), tffTermToTHF(rhs)))
+              case (lhs, rhs) => (tffTermToTHF(lhs), tffTermToTHF(rhs))
             }
-            THF.NonclassicalLongOperator(name, parameters0)
+            THF.NonclassicalLongOperator(name, idx0, parameters0)
           case TFF.NonclassicalBox(index) => THF.NonclassicalBox(index.map(tffTermToTHF))
           case TFF.NonclassicalDiamond(index) => THF.NonclassicalDiamond(index.map(tffTermToTHF))
           case TFF.NonclassicalCone(index) => THF.NonclassicalCone(index.map(tffTermToTHF))
         }
-        args.foldLeft[THF.Formula](THF.ConnectiveTerm(connective0)) { case (expr, arg) => THF.BinaryFormula(THF.App, expr, tffLogicFormulaToTHF(arg)) }
+        THF.NonclassicalPolyaryFormula(connective0, args.map(tffLogicFormulaToTHF))
     }
   }
   final def tffUnaryConnectiveToTHF(conn: TPTP.TFF.UnaryConnective): TPTP.THF.UnaryConnective = {