aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test/lux/abstract/predicate.lux
blob: 09982b5605a330a3631113bca612c717ecbb2c52 (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
(.module:
  [library
   [lux "*"
    ["_" test {"+" Test}]
    [abstract
     [equivalence {"+" Equivalence}]
     [monad {"+" do}]
     [\\specification
      ["$[0]" monoid]
      [functor
       ["$[0]" contravariant]]]]
    [control
     ["[0]" function]]
    [data
     ["[0]" bit ("[1]#[0]" equivalence)]
     [collection
      ["[0]" list]]]
    [math
     ["[0]" random {"+" 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 (: (Equivalence (/.Predicate Nat))
                              (implementation
                               (def: (= left right)
                                 (bit#= (left sample)
                                        (right sample)))))]])
      (_.for [/.Predicate])
      ($_ _.and
          (_.for [/.functor]
                 ($contravariant.spec equivalence (multiple? 2) /.functor))
          (let [generator (: (Random (/.Predicate Nat))
                             (|> random.nat
                                 (random.only (|>> (n.= 0) not))
                                 (# ! each multiple?)))]
            ($_ _.and
                (_.for [/.union]
                       ($monoid.spec equivalence /.union generator))
                (_.for [/.intersection]
                       ($monoid.spec equivalence /.intersection generator))))
          
          (_.cover [/.none]
                   (bit#= false (/.none sample)))
          (_.cover [/.all]
                   (bit#= true (/.all sample)))
          (_.cover [/.or]
                   (bit#= (/.all sample)
                          ((/.or /.none /.all) sample)))
          (_.cover [/.and]
                   (bit#= (/.none sample)
                          ((/.and /.none /.all) sample)))
          (_.cover [/.complement]
                   (and (not (bit#= (/.none sample)
                                    ((/.complement /.none) sample)))
                        (not (bit#= (/.all sample)
                                    ((/.complement /.all) sample)))))
          (_.cover [/.difference]
                   (let [/2? (multiple? 2)
                         /3? (multiple? 3)]
                     (bit#= (and (/2? sample)
                                 (not (/3? sample)))
                            ((/.difference /3? /2?) sample))))
          (_.cover [/.rec]
                   (let [even? (multiple? 2)
                         any_even? (: (/.Predicate (List Nat))
                                      (/.rec (function (_ recur)
                                               (function (_ values)
                                                 (case values
                                                   {.#End}
                                                   false

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