aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test/lux/abstract/predicate.lux
blob: fe942a044b1daa05e914654f8a35c8a2138185e5 (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
(.module:
  [lux #*
   ["_" test (#+ Test)]
   [abstract
    [equivalence (#+ Equivalence)]
    [monad (#+ do)]]
   [control
    ["." function]]
   [data
    ["." bit ("#@." equivalence)]
    [text
     ["%" format (#+ format)]]
    [number
     ["n" nat]]]
   [math
    ["r" random (#+ Random)]]]
  ["." // #_
   ["#." monoid]]
  {1
   ["." / (#+ Predicate)]})

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

(def: #export test
  Test
  (let [/2? (multiple? 2)
        /3? (multiple? 3)]
    (<| (_.context (%.name (name-of /.Predicate)))
        (do r.monad
          [sample r.nat])
        ($_ _.and
            (_.test (%.name (name-of /.none))
                    (bit@= false (/.none sample)))
            (_.test (%.name (name-of /.all))
                    (bit@= true (/.all sample)))
            (_.test (%.name (name-of /.unite))
                    (bit@= (/.all sample)
                           ((/.unite /.none /.all) sample)))
            (_.test (%.name (name-of /.intersect))
                    (bit@= (/.none sample)
                           ((/.intersect /.none /.all) sample)))
            (_.test (%.name (name-of /.complement))
                    (and (not (bit@= (/.none sample)
                                     ((/.complement /.none) sample)))
                         (not (bit@= (/.all sample)
                                     ((/.complement /.all) sample)))))
            (_.test (%.name (name-of /.difference))
                    (bit@= (and (/2? sample)
                                (not (/3? sample)))
                           ((/.difference /3? /2?) sample)))
            (let [equivalence (: (Equivalence (/.Predicate Nat))
                                 (structure
                                  (def: (= left right)
                                    (bit@= (left sample)
                                           (right sample)))))
                  generator (: (Random (/.Predicate Nat))
                               (|> r.nat
                                   (r.filter (|>> (n.= 0) not))
                                   (:: @ map multiple?)))]
              ($_ _.and
                  (//monoid.spec equivalence /.union generator)
                  (//monoid.spec equivalence /.intersection generator)))
            ))))