typelevel / algebra
1
package algebra.laws
2

3
import algebra._
4
import algebra.lattice._
5
import org.scalacheck.{Arbitrary, Prop}
6
import org.scalacheck.Prop._
7
import org.typelevel.discipline.Laws
8

9
object DeMorganLaws {
10 2
  def apply[A: Eq : Arbitrary : LatticeLaws] = new DeMorganLaws[A] {
11 2
    def Equ = Eq[A]
12 2
    def Arb = implicitly[Arbitrary[A]]
13 2
    def LL = implicitly[LatticeLaws[A]]
14
  }
15
}
16
/* TODO:
17
 *  This is separated for LogicLaws for binary compatibility reasons.
18
 *  Merge with LogicLaws when possible.
19
 */
20
trait DeMorganLaws[A] extends Laws {
21

22
  implicit def Equ: Eq[A]
23
  implicit def Arb: Arbitrary[A]
24
  def LL: LatticeLaws[A]
25

26 2
  def logic(implicit A: Logic[A]) = new DeMorganProperties(
27 2
    name = "logic",
28 2
    parents = Seq(),
29 2
    ll = LL.boundedDistributiveLattice,
30

31 2
    Rules.distributive(A.or)(A.and),
32

33 2
    "¬(x∨y) = ¬x∧¬y" -> forAll { (x: A, y: A) => A.not(A.or(x, y)) ?== A.and(A.not(x), A.not(y)) },
34 2
    "¬(x∧y) = ¬¬(¬x∨¬y)" -> forAll { (x: A, y: A) => A.not(A.and(x, y)) ?== A.not(A.not(A.or(A.not(x), A.not(y)))) }
35
  )
36

37 2
  def deMorgan(implicit A: DeMorgan[A]) = new DeMorganProperties(
38 2
    name = "deMorgan",
39 2
    parents = Seq(logic),
40 2
    ll = LL.boundedDistributiveLattice,
41

42 2
    Rules.distributive(A.or)(A.and),
43

44 2
    "involutive" -> forAll { (x: A) => A.not(A.not(x)) ?== x }
45
  )
46

47

48
  class DeMorganProperties(
49
                            val name: String,
50
                            val parents: Seq[DeMorganProperties],
51
                            val ll: LatticeLaws[A]#LatticeProperties,
52
                            val props: (String, Prop)*
53
                          ) extends RuleSet {
54 2
    val bases = Seq("lattice" -> ll)
55
  }
56

57
}

Read our documentation on viewing source code .

Loading