From 0ada1234b23c28402b4de6aa6909f20056fdf72e Mon Sep 17 00:00:00 2001 From: Alexander Steen Date: Fri, 24 Mar 2023 23:23:55 +0100 Subject: [PATCH] left side of meta identity can be anything --- README.md | 7 ++++--- src/main/scala/leo/datastructures/TPTP.scala | 4 ++-- src/main/scala/leo/modules/input/TPTPParser.scala | 13 +++++-------- 3 files changed, 11 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index 5b61106..312f47c 100644 --- a/README.md +++ b/README.md @@ -22,7 +22,7 @@ constantly being updated to follow more recent developments. ## Install [![Maven Central](https://img.shields.io/maven-central/v/io.github.leoprover/scala-tptp-parser_2.13.svg?label=Maven%20Central)](https://search.maven.org/search?q=g:%22io.github.leoprover%22%20AND%20a:%22scala-tptp-parser_2.13%22) -The Scala TPTP parser is available on [Maven Central](https://search.maven.org/artifact/io.github.leoprover/scala-tptp-parser_2.13) (current version: 1.7.0). +The Scala TPTP parser is available on [Maven Central](https://search.maven.org/artifact/io.github.leoprover/scala-tptp-parser_2.13) (current version: 1.7.1). Snapshots are available on [Sonatype](https://s01.oss.sonatype.org/content/repositories/snapshots/io/github/leoprover/scala-tptp-parser_2.13/). ### Maven @@ -32,7 +32,7 @@ In order to include `scala-tptp-parser` into your project via Maven, just add th io.github.leoprover scala-tptp-parser_2.13 - 1.7.0 + 1.7.1 ``` @@ -40,7 +40,7 @@ In order to include `scala-tptp-parser` into your project via Maven, just add th In order to include `scala-tptp-parser` into your project via SBT, just add the following dependency to your `build.sbt`: ```scala -libraryDependencies += "io.github.leoprover" %% "scala-tptp-parser" % "1.7.0" +libraryDependencies += "io.github.leoprover" %% "scala-tptp-parser" % "1.7.1" ``` ### Non-sbt-projects @@ -92,6 +92,7 @@ try { ## Version history + - 1.7.1: Allow any TFF terms on the left side of a meta equality (==). - 1.7.0: Rework non-classical formulas in TFF and THF, so that both languages now have their dedicated case class for non-classical formulas, called `NonclassicalPolyaryFormula`. This breaks a few things from previous versions (new formula structure for NCL formulas). Also, the NCL short-form connectives `[.]` and `<.>` are now unary connectives (and can be used as such). The long-form connectives `{name}` still require an explicit application with `@`. - 1.6.5: Fix usage of single-quoted identifiers that start with $ (or $$). Now the single quotes are retained in the functor name (in the AST) if the name is not a TPTP lower word. So the functor with name (as string) "$true" is not equal to "'$true'", as it should be (note the single quotes in the second variant). Single quotes are stripped automatically, if they are not necessary (i.e., parsing "'abc'" will produce functor "abc" without single quotes). diff --git a/src/main/scala/leo/datastructures/TPTP.scala b/src/main/scala/leo/datastructures/TPTP.scala index d3ed5d3..2966479 100644 --- a/src/main/scala/leo/datastructures/TPTP.scala +++ b/src/main/scala/leo/datastructures/TPTP.scala @@ -761,11 +761,11 @@ object TPTP { } override def symbols: Set[String] = typing.keySet ++ body.symbols } - final case class Assignment(lhs: AtomicTerm, rhs: Term) extends Formula { + final case class Assignment(lhs: Term, rhs: Term) extends Formula { override def pretty: String = s"(${lhs.pretty}) := (${rhs.pretty})" override def symbols: Set[String] = lhs.symbols ++ rhs.symbols } - final case class MetaIdentity(lhs: AtomicTerm, rhs: Term) extends Formula { + final case class MetaIdentity(lhs: Term, rhs: Term) extends Formula { override def pretty: String = s"(${lhs.pretty}) == (${rhs.pretty})" override def symbols: Set[String] = lhs.symbols ++ rhs.symbols } diff --git a/src/main/scala/leo/modules/input/TPTPParser.scala b/src/main/scala/leo/modules/input/TPTPParser.scala index 1c0d25f..6063966 100644 --- a/src/main/scala/leo/modules/input/TPTPParser.scala +++ b/src/main/scala/leo/modules/input/TPTPParser.scala @@ -1562,11 +1562,12 @@ object TPTPParser { // To allow := bindings with arbitrary formulas (w/o parentheses), i.e., have := a very low binding strength val f1 = tffLogicFormula0(tfx) if (tfx && o(IDENTITY, null) != null) { // Only allow '==' in TFX mode + val f2 = tffLogicFormulaOrTerm0() // Terms are more general, since they can also be formulas in TFX f1 match { case TFF.AtomicFormula(f, args) => - val f2 = tffLogicFormulaOrTerm0() // Terms are more general, since they can also be formulas in TFX TFF.MetaIdentity(TFF.AtomicTerm(f, args), f2) - case _ => error2(s"Parse error: Unexpected left-hand side of assignmeht '${f1.pretty}'. Only atomic terms are permitted.", lastTok) + case TFF.FormulaVariable(name) => TFF.MetaIdentity(TFF.Variable(name), f2) + case _ => TFF.MetaIdentity(TFF.FormulaTerm(f1), f2) } } else f1 } @@ -1993,12 +1994,8 @@ object TPTPParser { // To allow '==' bindings with arbitrary formulas or terms (w/o parentheses), i.e., have '==' a very low binding strength val f1 = tffLogicFormulaOrTerm0() if (o(IDENTITY, null) != null) { - f1 match { - case at@TFF.AtomicTerm(_, _) => - val f2 = tffLogicFormulaOrTerm0() - TFF.FormulaTerm(TFF.MetaIdentity(at, f2)) - case _ => error2(s"Parse error: Unexpected left-hand side of assignmeht '${f1.pretty}'. Only atomic terms are permitted.", lastTok) - } + val f2 = tffLogicFormulaOrTerm0() + TFF.FormulaTerm(TFF.MetaIdentity(f1, f2)) } else f1 }