-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[core] Initial Propositional Logic Structure and Parsers
- Loading branch information
Showing
5 changed files
with
275 additions
and
0 deletions.
There are no files selected for viewing
53 changes: 53 additions & 0 deletions
53
core/src/main/scala/dev/librecybernetics/data/PropExpression.scala
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
28 changes: 28 additions & 0 deletions
28
core/src/main/scala/dev/librecybernetics/data/PropTerm.scala
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
153 changes: 153 additions & 0 deletions
153
core/src/test/scala/dev/librecybernetics/data/PropExpressionSpec.scala
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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")) | ||
| ) | ||
| } | ||
| } | ||
| } |
26 changes: 26 additions & 0 deletions
26
core/src/test/scala/dev/librecybernetics/data/PropTermSpec.scala
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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")) | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |