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 2
  def joinSemilattice(implicit A: JoinSemilattice[A]) = new LatticeProperties(
22 2
    name = "joinSemilattice",
23 2
    parents = Nil,
24 2
    join = Some(semilattice(A.joinSemilattice)),
25 2
    meet = None,
26 2
    Rules.serializable(A)
27
  )
28

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

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

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

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

65 2
  def boundedMeetSemilattice(implicit A: BoundedMeetSemilattice[A]) = new LatticeProperties(
66 2
    name = "boundedMeetSemilattice",
67 2
    parents = Seq(meetSemilattice),
68 2
    join = None,
69 2
    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 2
  def boundedLattice(implicit A: BoundedLattice[A]) = new LatticeProperties(
87 2
    name = "boundedLattice",
88 2
    parents = Seq(boundedJoinSemilattice, boundedMeetSemilattice, lattice),
89 2
    join = Some(boundedSemilattice(A.joinSemilattice)),
90 2
    meet = Some(boundedSemilattice(A.meetSemilattice))
91
  )
92

93 2
  def boundedDistributiveLattice(implicit A: BoundedDistributiveLattice[A]) = new LatticeProperties(
94 2
    name = "boundedLattice",
95 2
    parents = Seq(boundedLattice, distributiveLattice),
96 2
    join = Some(boundedSemilattice(A.joinSemilattice)),
97 2
    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 2
    private val _m = meet map { "meet" -> _ }
108 2
    private val _j = join map { "join" -> _ }
109

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

113
}

Read our documentation on viewing source code .

Loading