From e6a26a0d190ab6b7e1e3308c4c7d36466bfd7b8d Mon Sep 17 00:00:00 2001
From: Katja Goltsova <14182676+cache-nez@users.noreply.github.com>
Date: Wed, 5 Oct 2022 11:28:57 +0200
Subject: [PATCH] Change Iff.id to match Implies.id (#51)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
* Change Iff.id to match Implies.id
* Recognize more arrows as iff / implies
* Update printer tests to use new Iff.id
Co-authored-by: Viktor KunÄak <vkuncak@users.noreply.github.com>
---
.../kernel/fol/FormulaLabelDefinitions.scala | 2 +-
.../src/main/scala/lisa/utils/Parser.scala | 4 ++--
.../src/test/scala/lisa/utils/ParserTest.scala | 1 +
.../src/test/scala/lisa/utils/PrinterTest.scala | 16 ++++++++--------
4 files changed, 12 insertions(+), 11 deletions(-)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index fb6e3bc7..cb97199b 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -48,7 +48,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
case object Implies extends ConstantConnectorLabel("⇒", 2)
- case object Iff extends ConstantConnectorLabel("↔", 2)
+ case object Iff extends ConstantConnectorLabel("⇔", 2)
case object And extends ConstantConnectorLabel("∧", -1)
diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index 1cb6546d..b4d179bb 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -161,8 +161,8 @@ object Parser {
elem('=') |> { _ => EqualityToken },
elem('∧') | word("/\\") |> { _ => AndToken },
elem('∨') | word("\\/") |> { _ => OrToken },
- elem('⇒') | word("=>") | word("==>") |> { _ => ImpliesToken },
- elem('↔') | word("<=>") | word("<==>") |> { _ => IffToken },
+ word(Implies.id) | word("=>") | word("==>") | elem('→') |> { _ => ImpliesToken },
+ word(Iff.id) | word("<=>") | word("<==>") | elem('⟷') | elem('↔') |> { _ => IffToken },
elem('⊤') | elem('T') | word("True") | word("true") |> { _ => TrueToken },
elem('⊥') | elem('F') | word("False") | word("false") |> { _ => FalseToken },
elem('¬') | elem('!') |> { _ => NegationToken },
diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
index 8930b571..f945193d 100644
--- a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
@@ -74,6 +74,7 @@ class ParserTest extends AnyFunSuite with TestUtils {
assert(Parser.parseFormula("a ∨ b") == ConnectorFormula(Or, Seq(a, b)))
assert(Parser.parseFormula("a ⇒ b") == ConnectorFormula(Implies, Seq(a, b)))
assert(Parser.parseFormula("a ↔ b") == ConnectorFormula(Iff, Seq(a, b)))
+ assert(Parser.parseFormula("a ⇔ b") == ConnectorFormula(Iff, Seq(a, b)))
}
test("ascii connectors") {
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index e8c2a63c..a15b86b8 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -90,7 +90,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b))) == "a ∧ b")
assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b))) == "a ∨ b")
assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, b))) == "a ⇒ b")
- assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, b))) == "a ↔ b")
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, b))) == "a ⇔ b")
}
test("connector associativity") {
@@ -129,13 +129,13 @@ class PrinterTest extends AnyFunSuite with TestUtils {
assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ⇒ b ∨ c")
// (a ∧ b) <=> c
- assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ↔ c")
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ⇔ c")
// a <=> (b ∧ c)
- assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ↔ b ∧ c")
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ⇔ b ∧ c")
// (a ∨ b) <=> c
- assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ↔ c")
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ⇔ c")
// a <=> (b ∨ c)
- assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ↔ b ∨ c")
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ⇔ b ∨ c")
}
test("connector parentheses") {
@@ -228,7 +228,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
Set(BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(x === x1, sPhi1(x))))),
Set((z === sf1(x1)) ==> exists(x, (z === sf1(x)) /\ sPhi1(x)))
)
- ) == "∀ ?x. ?x = ?x1 ↔ ?phi(?x) ⊢ ?z = ?f(?x1) ⇒ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+ ) == "∀ ?x. ?x = ?x1 ⇔ ?phi(?x) ⊢ ?z = ?f(?x1) ⇒ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
)
assert(
Parser.printSequent(
@@ -236,7 +236,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
z1,
forall(z, (z === z1) <=> exists(x, (z === sf1(x)) /\ sPhi1(x)))
)
- ) == "∃ ?x1. ∀ ?x. ?x = ?x1 ↔ ?phi(?x) ⊢ ∃ ?z1. ∀ ?z. ?z = ?z1 ↔ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+ ) == "∃ ?x1. ∀ ?x. ?x = ?x1 ⇔ ?phi(?x) ⊢ ∃ ?z1. ∀ ?z. ?z = ?z1 ⇔ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
)
assert(Parser.printSequent((() |- (x === x) \/ (x === y))) == "⊢ ?x = ?x ∨ ?x = ?y")
assert(
@@ -245,7 +245,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
(x === x) \/ (x === y),
((x === x) \/ (x === y)) <=> ((x === xPrime) \/ (x === yPrime))
) |- (x === xPrime) \/ (x === yPrime)
- ) == "?x = ?x ∨ ?x = ?y; ?x = ?x ∨ ?x = ?y ↔ ?x = ?x' ∨ ?x = ?y' ⊢ ?x = ?x' ∨ ?x = ?y'"
+ ) == "?x = ?x ∨ ?x = ?y; ?x = ?x ∨ ?x = ?y ⇔ ?x = ?x' ∨ ?x = ?y' ⊢ ?x = ?x' ∨ ?x = ?y'"
)
}
}
--
GitLab