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

(def .public (spec (open "/#[0]") random)
  (All (_ a) (-> (/.Enum a) (Random a) Test))
  (do random.monad
    [sample random]
    (<| (_.for [/.Enum])
        (all _.and
             (_.for [/.order]
                    (orderT.spec /#order random))
             (_.coverage [/.succ /.pred]
               (and (/#= (|> sample /#succ /#pred)
                         sample)
                    (/#= (|> sample /#pred /#succ)
                         sample)
                    (not (/#= (/#succ sample)
                              sample))
                    (not (/#= (/#pred sample)
                              sample))))
             ))))