typelevel / algebra
1
package algebra.laws
2

3
import algebra._
4
import algebra.lattice._
5

6
import org.scalacheck.{Arbitrary, Prop}
7
import org.scalacheck.Prop._
8

9
object LatticeLaws {
10 0
  def apply[A: Eq: Arbitrary] = new LatticeLaws[A] {
11 0
    def Equ = Eq[A]
12 0
    def Arb = implicitly[Arbitrary[A]]
13
  }
14
}
15

16
trait LatticeLaws[A] extends GroupLaws[A] {
17

18
  implicit def Equ: Eq[A]
19
  implicit def Arb: Arbitrary[A]
20

21 3
  def joinSemilattice(implicit A: JoinSemilattice[A]) = new LatticeProperties(
22 3
    name = "joinSemilattice",
23 3
    parents = Nil,
24 3
    join = Some(semilattice(A.joinSemilattice)),
25 3
    meet = None,
26 3
    Rules.serializable(A)
27
  )
28

29 3
  def meetSemilattice(implicit A: MeetSemilattice[A]) = new LatticeProperties(
30 3
    name = "meetSemilattice",
31 3
    parents = Nil,
32 3
    join = None,
33 3
    meet = Some(semilattice(A.meetSemilattice)),
34 3
    Rules.serializable(A)
35
  )
36

37 3
  def lattice(implicit A: Lattice[A]) = new LatticeProperties(
38 3
    name = "lattice",
39 3
    parents = Seq(joinSemilattice, meetSemilattice),
40 3
    join = Some(semilattice(A.joinSemilattice)),
41 3
    meet = Some(semilattice(A.meetSemilattice)),
42 3
    "absorption" -> forAll { (x: A, y: A) =>
43 3
      (A.join(x, A.meet(x, y)) ?== x) && (A.meet(x, A.join(x, y)) ?== x)
44
    }
45
  )
46

47 3
  def distributiveLattice(implicit A: DistributiveLattice[A]) = new LatticeProperties(
48 3
    name = "distributiveLattice",
49 3
    parents = Seq(lattice),
50 3
    join = Some(semilattice(A.joinSemilattice)),
51 3
    meet = Some(semilattice(A.meetSemilattice)),
52 3
    "distributive" -> forAll { (x: A, y: A, z: A) =>
53 3
      (A.join(x, A.meet(y, z)) ?== A.meet(A.join(x, y), A.join(x, z))) &&
54 3
        (A.meet(x, A.join(y, z)) ?== A.join(A.meet(x, y), A.meet(x, z)))
55
    }
56
  )
57

58 3
  def boundedJoinSemilattice(implicit A: BoundedJoinSemilattice[A]) = new LatticeProperties(
59 3
    name = "boundedJoinSemilattice",
60 3
    parents = Seq(joinSemilattice),
61 3
    join = Some(boundedSemilattice(A.joinSemilattice)),
62 3
    meet = None
63
  )
64

65 3
  def boundedMeetSemilattice(implicit A: BoundedMeetSemilattice[A]) = new LatticeProperties(
66 3
    name = "boundedMeetSemilattice",
67 3
    parents = Seq(meetSemilattice),
68 3
    join = None,
69 3
    meet = Some(boundedSemilattice(A.meetSemilattice))
70
  )
71

72 0
  def boundedJoinLattice(implicit A: Lattice[A] with BoundedJoinSemilattice[A]) = new LatticeProperties(
73 0
    name = "boundedJoinLattice",
74 0
    parents = Seq(boundedJoinSemilattice, lattice),
75 0
    join = Some(boundedSemilattice(A.joinSemilattice)),
76 0
    meet = Some(semilattice(A.meetSemilattice))
77
  )
78

79 0
  def boundedMeetLattice(implicit A: Lattice[A] with BoundedMeetSemilattice[A]) = new LatticeProperties(
80 0
    name = "boundedMeetLattice",
81 0
    parents = Seq(boundedMeetSemilattice, lattice),
82 0
    join = Some(semilattice(A.joinSemilattice)),
83 0
    meet = Some(boundedSemilattice(A.meetSemilattice))
84
  )
85

86 3
  def boundedLattice(implicit A: BoundedLattice[A]) = new LatticeProperties(
87 3
    name = "boundedLattice",
88 3
    parents = Seq(boundedJoinSemilattice, boundedMeetSemilattice, lattice),
89 3
    join = Some(boundedSemilattice(A.joinSemilattice)),
90 3
    meet = Some(boundedSemilattice(A.meetSemilattice))
91
  )
92

93 3
  def boundedDistributiveLattice(implicit A: BoundedDistributiveLattice[A]) = new LatticeProperties(
94 3
    name = "boundedLattice",
95 3
    parents = Seq(boundedLattice, distributiveLattice),
96 3
    join = Some(boundedSemilattice(A.joinSemilattice)),
97 3
    meet = Some(boundedSemilattice(A.meetSemilattice))
98
  )
99

100
  class LatticeProperties(
101
    val name: String,
102
    val parents: Seq[LatticeProperties],
103
    val join: Option[GroupProperties],
104
    val meet: Option[GroupProperties],
105
    val props: (String, Prop)*
106
  ) extends RuleSet {
107 3
    private val _m = meet map { "meet" -> _ }
108 3
    private val _j = join map { "join" -> _ }
109

110 3
    val bases = _m.toList ::: _j.toList
111
  }
112

113
}

Read our documentation on viewing source code .

Loading