1
+ package kategory.optics
2
+
3
+ import io.kotlintest.properties.Gen
4
+ import io.kotlintest.properties.forAll
5
+ import kategory.Applicative
6
+ import kategory.Eq
7
+ import kategory.Law
8
+ import kategory.Lens
9
+ import kategory.compose
10
+ import kategory.exists
11
+ import kategory.identity
12
+
13
+ object LensLaws {
14
+
15
+ inline fun <A , B , reified F > laws (lens : Lens <A , B >, aGen : Gen <A >, bGen : Gen <B >, funcGen : Gen <(B ) -> B >, EQA : Eq <A >, EQB : Eq <B >, FA : Applicative <F >) = listOf (
16
+ Law (" Lens law: get set" , { lensGetSet(lens, aGen, EQA ) }),
17
+ Law (" Lens law: set get" , { lensSetGet(lens, aGen, bGen, EQB ) }),
18
+ Law (" Lens law: is set idempotent" , { lensSetIdempotent(lens, aGen, bGen, EQA ) }),
19
+ Law (" Lens law: modify identity" , { lensModifyIdentity(lens, aGen, bGen, EQA ) }),
20
+ Law (" Lens law: compose modify" , { lensComposeModify(lens, aGen, funcGen, EQA ) }),
21
+ Law (" Lens law: consistent set modify" , { lensConsistentSetModify(lens, aGen, bGen, EQA ) }),
22
+ Law (" Lens law: consistent modify modify id" , { lensConsistentModifyModifyId(lens, aGen, funcGen, EQA , FA ) }),
23
+ Law (" Lens law: consistent get modify id" , { lensConsistentGetModifyid(lens, aGen, EQB , FA ) })
24
+ )
25
+
26
+ fun <A , B > lensGetSet (lens : Lens <A , B >, aGen : Gen <A >, EQA : Eq <A >) =
27
+ forAll(aGen, { a ->
28
+ EQA .eqv(lens.set(lens.get(a))(a), a)
29
+ })
30
+
31
+ fun <A , B > lensSetGet (lens : Lens <A , B >, aGen : Gen <A >, bGen : Gen <B >, EQB : Eq <B >) =
32
+ forAll(aGen, bGen, { a, b ->
33
+ EQB .eqv(lens.get(lens.set(b)(a)), b)
34
+ })
35
+
36
+ fun <A , B > lensSetIdempotent (lens : Lens <A , B >, aGen : Gen <A >, bGen : Gen <B >, EQA : Eq <A >) =
37
+ forAll(aGen, bGen, { a, b ->
38
+ EQA .eqv(lens.set(b)(lens.set(b)(a)), lens.set(b)(a))
39
+ })
40
+
41
+ fun <A , B > lensModifyIdentity (lens : Lens <A , B >, aGen : Gen <A >, bGen : Gen <B >, EQA : Eq <A >) =
42
+ forAll(aGen, bGen, { a, b ->
43
+ EQA .eqv(lens.modify(::identity, a), a)
44
+ })
45
+
46
+ fun <A , B > lensComposeModify (lens : Lens <A , B >, aGen : Gen <A >, funcGen : Gen <(B ) -> B >, EQA : Eq <A >) =
47
+ forAll(aGen, funcGen, funcGen, { a, f, g ->
48
+ EQA .eqv(lens.modify(g, lens.modify(f, a)), lens.modify(g compose f, a))
49
+ })
50
+
51
+ fun <A , B > lensConsistentSetModify (lens : Lens <A , B >, aGen : Gen <A >, bGen : Gen <B >, EQA : Eq <A >) =
52
+ forAll(aGen, bGen, { a, b ->
53
+ EQA .eqv(lens.set(b)(a), lens.modify({ b }, a))
54
+ })
55
+
56
+ inline fun <A , B , reified F > lensConsistentModifyModifyId (lens : Lens <A , B >, aGen : Gen <A >, funcGen : Gen <(B ) -> B >, EQA : Eq <A >, FA : Applicative <F >) =
57
+ forAll(aGen, funcGen, { a, f ->
58
+ lens.modifyF(FA , { FA .pure(f(it)) }, a).exists { EQA .eqv(lens.modify(f, a), it) }
59
+ })
60
+
61
+ inline fun <A , B , reified F > lensConsistentGetModifyid (lens : Lens <A , B >, aGen : Gen <A >, EQB : Eq <B >, FA : Applicative <F >) =
62
+ forAll(aGen, { a ->
63
+ lens.modifyF(FA , { FA .pure(it) }, a).exists { EQB .eqv(lens.get(a), lens.get(it)) }
64
+ })
65
+
66
+ }
0 commit comments