From 7f217c7ef719dee73863357779be96dfaf0b5bf1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Fri, 15 Dec 2023 01:15:43 -0600 Subject: [PATCH] [core] Initial Propositional Logic Structure and Parsers --- .../data/PropExpression.scala | 53 ++++++ .../dev/librecybernetics/data/PropTerm.scala | 28 ++++ .../data/PropExpressionSpec.scala | 153 ++++++++++++++++++ .../librecybernetics/data/PropTermSpec.scala | 26 +++ .../dev/librecybernetics/data/Util.scala | 15 ++ 5 files changed, 275 insertions(+) create mode 100644 core/src/main/scala/dev/librecybernetics/data/PropExpression.scala create mode 100644 core/src/main/scala/dev/librecybernetics/data/PropTerm.scala create mode 100644 core/src/test/scala/dev/librecybernetics/data/PropExpressionSpec.scala create mode 100644 core/src/test/scala/dev/librecybernetics/data/PropTermSpec.scala create mode 100644 core/src/test/scala/dev/librecybernetics/data/Util.scala diff --git a/core/src/main/scala/dev/librecybernetics/data/PropExpression.scala b/core/src/main/scala/dev/librecybernetics/data/PropExpression.scala new file mode 100644 index 0000000..1ffbca0 --- /dev/null +++ b/core/src/main/scala/dev/librecybernetics/data/PropExpression.scala @@ -0,0 +1,53 @@ +package dev.librecybernetics.data + +import cats.data.NonEmptyList +import cats.parse.Parser + +enum PropExpression: + case Negation(operand: PropTerm | PropExpression) + case Conjunction(operands: NonEmptyList[PropTerm | PropExpression]) + case Disjunction(operands: NonEmptyList[PropTerm | PropExpression]) + case MaterialImplication(antecedent: PropTerm | PropExpression, consequent: PropTerm | PropExpression) +end PropExpression + +object PropExpression: + object Conjunction: + def apply(operands: (PropTerm | PropExpression)*): Conjunction = + new Conjunction(NonEmptyList.fromListUnsafe(operands.toList)) + end Conjunction + + object Disjunction: + def apply(operands: (PropTerm | PropExpression)*): Disjunction = + new Disjunction(NonEmptyList.fromListUnsafe(operands.toList)) + end Disjunction + + private val space = Parser.char(' ') + def spaceSep[A](sep: Parser[A]): Parser[A] = + space.rep0.with1 *> sep <* space.rep0 + def negation(expr: Parser[PropExpression]): Parser[PropExpression] = + Parser.charIn('!', '¬') *> (PropTerm.parser | expr).map(PropExpression.Negation(_)) + + def conjunction(expr: Parser[PropExpression]): Parser[PropExpression] = + (PropTerm.parser | expr) + .repSep(min = 2, sep = spaceSep(Parser.charIn('&', '∧'))) + .map(operands => PropExpression.Conjunction(operands)) + .between(Parser.char('('), Parser.char(')')) + + def disjunction(expr: Parser[PropExpression]): Parser[PropExpression] = + (PropTerm.parser | expr) + .repSep(min = 2, sep = spaceSep(Parser.charIn('|', '∨'))) + .map(operands => PropExpression.Disjunction(operands)) + .between(Parser.char('('), Parser.char(')')) + + def materialImplication(expr: Parser[PropExpression]) = + (for + antecedent <- PropTerm.parser | expr + _ <- spaceSep(Parser.string("->") | Parser.char('→')) + consequent <- PropTerm.parser | expr + yield PropExpression.MaterialImplication(antecedent, consequent)) + .between(Parser.char('('), Parser.char(')')) + + lazy val parser: Parser[PropExpression] = Parser.recursive { parser => + Parser.oneOf(List(negation, conjunction, disjunction, materialImplication).map(_(parser).backtrack)) + } +end PropExpression diff --git a/core/src/main/scala/dev/librecybernetics/data/PropTerm.scala b/core/src/main/scala/dev/librecybernetics/data/PropTerm.scala new file mode 100644 index 0000000..5d5fc64 --- /dev/null +++ b/core/src/main/scala/dev/librecybernetics/data/PropTerm.scala @@ -0,0 +1,28 @@ +package dev.librecybernetics.data + +import cats.parse.Parser + +enum PropTerm: + case False extends PropTerm with PropTerm.PropValue + case True extends PropTerm with PropTerm.PropValue + + case PropVariable(name: String) +end PropTerm + +object PropTerm: + sealed trait PropValue + + object PropValue: + val falseParser: Parser[PropTerm.False.type] = Parser.stringIn(Set("false", "⊥")).as(PropTerm.False) + val trueParser: Parser[PropTerm.True.type] = Parser.stringIn(Set("true", "⊤")).as(PropTerm.True) + + val parser: Parser[PropTerm with PropValue] = Parser.oneOf(List(falseParser, trueParser)) + end PropValue + + object PropVariable: + val parser: Parser[PropVariable] = + Parser.charsWhile(_.isLetter).map(PropVariable(_)) + end PropVariable + + val parser: Parser[PropTerm] = Parser.oneOf(List(PropValue.parser, PropVariable.parser)) +end PropTerm diff --git a/core/src/test/scala/dev/librecybernetics/data/PropExpressionSpec.scala b/core/src/test/scala/dev/librecybernetics/data/PropExpressionSpec.scala new file mode 100644 index 0000000..7a5645c --- /dev/null +++ b/core/src/test/scala/dev/librecybernetics/data/PropExpressionSpec.scala @@ -0,0 +1,153 @@ +package dev.librecybernetics.data + +import org.scalatest.matchers.should.Matchers.* +import org.scalatest.wordspec.AnyWordSpec + +class PropExpressionSpec extends AnyWordSpec { + "simple expressions" should { + "negation" in { + PropExpression.parser.shouldParse("!false", PropExpression.Negation(PropTerm.False)) + PropExpression.parser.shouldParse("!⊥", PropExpression.Negation(PropTerm.False)) + PropExpression.parser.shouldParse("!true", PropExpression.Negation(PropTerm.True)) + PropExpression.parser.shouldParse("!⊤", PropExpression.Negation(PropTerm.True)) + PropExpression.parser.shouldParse("!a", PropExpression.Negation(PropTerm.PropVariable("a"))) + } + + "conjunction" in { + PropExpression.parser.shouldParse("(false ∧ false)", PropExpression.Conjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(⊥ ∧ ⊥)", PropExpression.Conjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(false ∧ true)", PropExpression.Conjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(⊥ ∧ ⊤)", PropExpression.Conjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(true ∧ false)", PropExpression.Conjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(⊤ ∧ ⊥)", PropExpression.Conjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(true ∧ true)", PropExpression.Conjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse("(⊤ ∧ ⊤)", PropExpression.Conjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse( + "(a ∧ b)", + PropExpression.Conjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b")) + ) + PropExpression.parser.shouldParse( + "(a ∧ b ∧ c)", + PropExpression.Conjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b"), PropTerm.PropVariable("c")) + ) + PropExpression.parser.shouldParse( + "(a ∧ b ∧ c ∧ d)", + PropExpression.Conjunction( + PropTerm.PropVariable("a"), + PropTerm.PropVariable("b"), + PropTerm.PropVariable("c"), + PropTerm.PropVariable("d") + ) + ) + PropExpression.parser.shouldParse("(false & false)", PropExpression.Conjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(⊥ & ⊥)", PropExpression.Conjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(false & true)", PropExpression.Conjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(⊥ & ⊤)", PropExpression.Conjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(true & false)", PropExpression.Conjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(⊤ & ⊥)", PropExpression.Conjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(true & true)", PropExpression.Conjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse("(⊤ & ⊤)", PropExpression.Conjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse( + "(a & b)", + PropExpression.Conjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b")) + ) + PropExpression.parser.shouldParse( + "(a & b & c)", + PropExpression.Conjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b"), PropTerm.PropVariable("c")) + ) + PropExpression.parser.shouldParse( + "(a & b & c & d)", + PropExpression.Conjunction( + PropTerm.PropVariable("a"), + PropTerm.PropVariable("b"), + PropTerm.PropVariable("c"), + PropTerm.PropVariable("d") + ) + ) + } + + "disjunction" in { + PropExpression.parser.shouldParse("(false ∨ false)", PropExpression.Disjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(⊥ ∨ ⊥)", PropExpression.Disjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(false ∨ true)", PropExpression.Disjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(⊥ ∨ ⊤)", PropExpression.Disjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(true ∨ false)", PropExpression.Disjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(⊤ ∨ ⊥)", PropExpression.Disjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(true ∨ true)", PropExpression.Disjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse("(⊤ ∨ ⊤)", PropExpression.Disjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse( + "(a ∨ b)", + PropExpression.Disjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b")) + ) + PropExpression.parser.shouldParse( + "(c ∨ d)", + PropExpression.Disjunction(PropTerm.PropVariable("c"), PropTerm.PropVariable("d")) + ) + PropExpression.parser.shouldParse( + "(a ∨ b ∨ c)", + PropExpression.Disjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b"), PropTerm.PropVariable("c")) + ) + PropExpression.parser.shouldParse( + "(a ∨ b ∨ c ∨ d)", + PropExpression.Disjunction( + PropTerm.PropVariable("a"), + PropTerm.PropVariable("b"), + PropTerm.PropVariable("c"), + PropTerm.PropVariable("d") + ) + ) + PropExpression.parser.shouldParse("(false | false)", PropExpression.Disjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(⊥ | ⊥)", PropExpression.Disjunction(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse("(false | true)", PropExpression.Disjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(⊥ | ⊤)", PropExpression.Disjunction(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse("(true | false)", PropExpression.Disjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(⊤ | ⊥)", PropExpression.Disjunction(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse("(true | true)", PropExpression.Disjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse("(⊤ | ⊤)", PropExpression.Disjunction(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse( + "(a | b)", + PropExpression.Disjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b")) + ) + PropExpression.parser.shouldParse( + "(a | b | c)", + PropExpression.Disjunction(PropTerm.PropVariable("a"), PropTerm.PropVariable("b"), PropTerm.PropVariable("c")) + ) + PropExpression.parser.shouldParse( + "(a | b | c | d)", + PropExpression.Disjunction( + PropTerm.PropVariable("a"), + PropTerm.PropVariable("b"), + PropTerm.PropVariable("c"), + PropTerm.PropVariable("d") + ) + ) + } + + "material implication" in { + PropExpression.parser.shouldParse( + "(false → false)", + PropExpression.MaterialImplication(PropTerm.False, PropTerm.False) + ) + PropExpression.parser.shouldParse("(⊥ → ⊥)", PropExpression.MaterialImplication(PropTerm.False, PropTerm.False)) + PropExpression.parser.shouldParse( + "(false → true)", + PropExpression.MaterialImplication(PropTerm.False, PropTerm.True) + ) + PropExpression.parser.shouldParse("(⊥ → ⊤)", PropExpression.MaterialImplication(PropTerm.False, PropTerm.True)) + PropExpression.parser.shouldParse( + "(true → false)", + PropExpression.MaterialImplication(PropTerm.True, PropTerm.False) + ) + PropExpression.parser.shouldParse("(⊤ → ⊥)", PropExpression.MaterialImplication(PropTerm.True, PropTerm.False)) + PropExpression.parser.shouldParse( + "(true → true)", + PropExpression.MaterialImplication(PropTerm.True, PropTerm.True) + ) + PropExpression.parser.shouldParse("(⊤ → ⊤)", PropExpression.MaterialImplication(PropTerm.True, PropTerm.True)) + PropExpression.parser.shouldParse( + "(a → b)", + PropExpression.MaterialImplication(PropTerm.PropVariable("a"), PropTerm.PropVariable("b")) + ) + } + } +} diff --git a/core/src/test/scala/dev/librecybernetics/data/PropTermSpec.scala b/core/src/test/scala/dev/librecybernetics/data/PropTermSpec.scala new file mode 100644 index 0000000..6244f54 --- /dev/null +++ b/core/src/test/scala/dev/librecybernetics/data/PropTermSpec.scala @@ -0,0 +1,26 @@ +package dev.librecybernetics.data + +import org.scalatest.matchers.should.Matchers.* +import org.scalatest.wordspec.AnyWordSpec + +class PropTermSpec extends AnyWordSpec { + "constants" should { + "false" in { + PropTerm.parser.shouldParse("false", PropTerm.False) + PropTerm.parser.shouldParse("⊥", PropTerm.False) + } + + "true" in { + PropTerm.parser.shouldParse("true", PropTerm.True) + PropTerm.parser.shouldParse("⊤", PropTerm.True) + } + } + + "variables" should { + "parse" in { + PropTerm.parser.shouldParse("a", PropTerm.PropVariable("a")) + PropTerm.parser.shouldParse("b", PropTerm.PropVariable("b")) + PropTerm.parser.shouldParse("c", PropTerm.PropVariable("c")) + } + } +} diff --git a/core/src/test/scala/dev/librecybernetics/data/Util.scala b/core/src/test/scala/dev/librecybernetics/data/Util.scala new file mode 100644 index 0000000..7b48f9b --- /dev/null +++ b/core/src/test/scala/dev/librecybernetics/data/Util.scala @@ -0,0 +1,15 @@ +package dev.librecybernetics.data + +import cats.parse.Parser +import org.scalatest.Assertion +import org.scalatest.Assertions.fail +import org.scalatest.matchers.should.Matchers.shouldBe + +extension [A](parser: Parser[A]) + def shouldParse(input: String, expected: A): Assertion = + parser.parseAll(input) match + case Right(actual) => actual shouldBe expected + case Left(error) => fail(s"$input failed to parse: $error") + end match + end shouldParse +end extension