typelevel / algebra
1
package algebra.laws
2

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

6
import org.typelevel.discipline.Laws
7

8
import org.scalacheck.{Arbitrary, Prop}
9
import org.scalacheck.Prop._
10

11
import algebra.instances.boolean._
12

13
object LatticePartialOrderLaws {
14 3
  def apply[A: Eq: Arbitrary] = new LatticePartialOrderLaws[A] {
15 0
    def Equ = Eq[A]
16 3
    def Arb = implicitly[Arbitrary[A]]
17
  }
18
}
19

20
trait LatticePartialOrderLaws[A] extends Laws {
21

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

25 3
  def joinSemilatticePartialOrder(implicit A: JoinSemilattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
26 3
    name = "joinSemilatticePartialOrder",
27 3
    parents = Seq.empty,
28 3
    "join+lteqv" -> forAll { (x: A, y: A) =>
29 3
      P.lteqv(x, y) ?== P.eqv(y, A.join(x, y))
30
    }
31
  )
32

33 3
  def meetSemilatticePartialOrder(implicit A: MeetSemilattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
34 3
    name = "meetSemilatticePartialOrder",
35 3
    parents = Seq.empty,
36 3
    "meet+lteqv" -> forAll { (x: A, y: A) =>
37 3
      P.lteqv(x, y) ?== P.eqv(x, A.meet(x, y))
38
    }
39
  )
40

41 0
  def latticePartialOrder(implicit A: Lattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
42 0
    name = "latticePartialOrder",
43 0
    parents = Seq(joinSemilatticePartialOrder, meetSemilatticePartialOrder)
44
  )
45

46 3
  def boundedJoinSemilatticePartialOrder(implicit A: BoundedJoinSemilattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
47 3
    name = "boundedJoinSemilatticePartialOrder",
48 3
    parents = Seq(joinSemilatticePartialOrder),
49 3
    "lteqv+zero" -> forAll { (x: A) => A.zero ?<= x }
50
  )
51

52 3
  def boundedMeetSemilatticePartialOrder(implicit A: BoundedMeetSemilattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
53 3
    name = "boundedMeetSemilatticePartialOrder",
54 3
    parents = Seq(meetSemilatticePartialOrder),
55 3
    "lteqv+one" -> forAll { (x: A) => x ?<= A.one }
56
  )
57

58 0
  def boundedBelowLatticePartialOrder(implicit A: Lattice[A] with BoundedJoinSemilattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
59 0
    name = "boundedBelowLatticePartialOrder",
60 0
    parents = Seq(boundedJoinSemilatticePartialOrder, latticePartialOrder)
61
  )
62

63 0
  def boundedAboveLatticePartialOrder(implicit A: Lattice[A] with BoundedMeetSemilattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
64 0
    name = "boundedAboveLatticePartialOrder",
65 0
    parents = Seq(boundedMeetSemilatticePartialOrder, latticePartialOrder)
66
  )
67
  
68 3
  def boundedLatticePartialOrder(implicit A: BoundedLattice[A], P: PartialOrder[A]) = new LatticePartialOrderProperties(
69 3
    name = "boundedLatticePartialOrder",
70 3
    parents = Seq(boundedJoinSemilatticePartialOrder, boundedMeetSemilatticePartialOrder)
71
  )
72
  
73
  class LatticePartialOrderProperties(
74
    val name: String,
75
    val parents: Seq[LatticePartialOrderProperties],
76
    val props: (String, Prop)*
77
  ) extends RuleSet {
78 3
    def bases = Nil
79
  }
80

81
}

Read our documentation on viewing source code .

Loading