aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test/lux/abstract/predicate.lux
blob: 46c44ceead98ff621efe29e03146a60dc7cd3a55 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
(.using
 [library
  [lux (.except)
   ["_" test (.only Test)]
   [abstract
    [equivalence (.only Equivalence)]
    [monad (.only do)]
    [\\specification
     ["$[0]" monoid]
     [functor
      ["$[0]" contravariant]]]]
   [control
    ["[0]" function]]
   [data
    ["[0]" bit (.open: "[1]#[0]" equivalence)]
    [collection
     ["[0]" list]]]
   [math
    ["[0]" random (.only Random)]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" /]])

(def: (multiple? factor)
  (-> Nat (/.Predicate Nat))
  (case factor
    0 (function.constant false)
    _ (|>> (n.% factor) (n.= 0))))

(def: .public test
  Test
  (<| (_.covering /._)
      (do [! random.monad]
        [sample random.nat
         samples (random.list 10 random.nat)
         .let [equivalence (is (Equivalence (/.Predicate Nat))
                               (implementation
                                (def: (= left right)
                                  (bit#= (left sample)
                                         (right sample)))))]])
      (_.for [/.Predicate])
      (all _.and
           (_.for [/.functor]
                  ($contravariant.spec equivalence (multiple? 2) /.functor))
           (let [generator (is (Random (/.Predicate Nat))
                               (|> random.nat
                                   (random.only (|>> (n.= 0) not))
                                   (# ! each multiple?)))]
             (all _.and
                  (_.for [/.union]
                         ($monoid.spec equivalence /.union generator))
                  (_.for [/.intersection]
                         ($monoid.spec equivalence /.intersection generator))))
           
           (_.coverage [/.none]
             (bit#= false (/.none sample)))
           (_.coverage [/.all]
             (bit#= true (/.all sample)))
           (_.coverage [/.or]
             (bit#= (/.all sample)
                    ((/.or /.none /.all) sample)))
           (_.coverage [/.and]
             (bit#= (/.none sample)
                    ((/.and /.none /.all) sample)))
           (_.coverage [/.complement]
             (and (not (bit#= (/.none sample)
                              ((/.complement /.none) sample)))
                  (not (bit#= (/.all sample)
                              ((/.complement /.all) sample)))))
           (_.coverage [/.difference]
             (let [/2? (multiple? 2)
                   /3? (multiple? 3)]
               (bit#= (and (/2? sample)
                           (not (/3? sample)))
                      ((/.difference /3? /2?) sample))))
           (_.coverage [/.rec]
             (let [even? (multiple? 2)
                   any_even? (is (/.Predicate (List Nat))
                                 (/.rec (function (_ again)
                                          (function (_ values)
                                            (case values
                                              {.#End}
                                              false

                                              {.#Item head tail}
                                              (or (even? head)
                                                  (again tail)))))))]
               (bit#= (list.any? even? samples)
                      (any_even? samples))))
           )))