aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/order.lux
blob: 1bf62b3cc1e10b6311d788f082be909807778ec6 (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
(.require
 [library
  [lux (.except)
   [abstract
    [monad (.only do)]]
   [data
    ["[0]" bit (.use "[1]#[0]" equivalence)]]
   [math
    ["[0]" random (.only Random)]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" /]]
 [//
  ["[0]S" equivalence]])

(def .public (spec (open "/#[0]") random)
  (All (_ of)
    (-> (/.Order of) (Random of)
        Test))
  (<| (_.for [/.Order])
      (all _.and
           (_.for [/.equivalence]
                  (equivalenceS.spec /#equivalence random))
           
           (do random.monad
             [parameter random
              subject random
              .let [equal_or_ordered!
                    (let [equal!
                          (/#= parameter subject)

                          ordered!
                          (or (and (/#< parameter subject)
                                   (not (/#< subject parameter)))
                              (and (/#< subject parameter)
                                   (not (/#< parameter subject))))]
                      (bit#= equal! (not ordered!)))]

              subject (random.only (|>> (/#= parameter) not)
                                   random)
              extra (random.only (function (_ value)
                                   (not (or (/#= parameter value)
                                            (/#= subject value))))
                                 random)
              .let [transitive_property!
                    (if (/#< parameter subject)
                      (let [greater? (and (/#< subject extra)
                                          (/#< parameter extra))
                            lesser? (and (/#< extra parameter)
                                         (/#< extra subject))
                            in_between? (and (/#< parameter extra)
                                             (/#< extra subject))]
                        (or greater?
                            lesser?
                            in_between?))
                      ... (/#< subject parameter)
                      (let [greater? (and (/#< extra subject)
                                          (/#< extra parameter))
                            lesser? (and (/#< parameter extra)
                                         (/#< subject extra))
                            in_between? (and (/#< subject extra)
                                             (/#< extra parameter))]
                        (or greater?
                            lesser?
                            in_between?)))]]
             (_.coverage [/.<]
               (and equal_or_ordered!
                    transitive_property!)))
           )))