stdlib/source/test/lux/control/thread.lux


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

(.require
 [library
  [lux (.except)
   [abstract
    [monad (.only do)]
    [\\specification
     ["$[0]" functor (.only Injection Comparison)]
     ["$[0]" apply]
     ["$[0]" monad]]]
   [math
    ["[0]" random]
    [number
     ["n" nat]]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" / (.only Thread)
   [//
    ["[0]" io]]]])

(def (injection value)
  (Injection (All (_ a !) (Thread ! a)))
  (of /.monad in value))

(def comparison
  (Comparison (All (_ a !) (Thread ! a)))
  (function (_ == left right)
    (== (/.result left) (/.result right))))

(def .public test
  Test
  (do random.monad
    [sample random.nat
     factor random.nat]
    (<| (_.covering /._)
        (all _.and
             (_.for [/.Thread]
                    (all _.and
                         (_.coverage [/.result]
                           (n.= sample
                                (|> sample
                                    (of /.monad in)
                                    /.result)))
                         (_.coverage [/.io]
                           (n.= sample
                                (|> sample
                                    (of /.monad in)
                                    /.io
                                    io.run!)))
                         
                         (_.for [/.functor]
                                ($functor.spec ..injection ..comparison /.functor))
                         (_.for [/.apply]
                                ($apply.spec ..injection ..comparison /.apply))
                         (_.for [/.monad]
                                ($monad.spec ..injection ..comparison /.monad))
                         ))

             (_.for [/.Box /.box]
                    (all _.and
                         (_.coverage [/.read!]
                           (n.= sample
                                (/.result (is (All (_ !) (Thread ! Nat))
                                              (do /.monad
                                                [box (/.box sample)]
                                                (/.read! box))))))

                         (_.coverage [/.write!]
                           (n.= factor
                                (/.result (is (All (_ !) (Thread ! Nat))
                                              (do /.monad
                                                [box (/.box sample)
                                                 _ (/.write! factor box)]
                                                (/.read! box))))))

                         (_.coverage [/.update!]
                           (n.= (n.* factor sample)
                                (/.result (is (All (_ !) (Thread ! Nat))
                                              (do /.monad
                                                [box (/.box sample)
                                                 [old new] (/.update! (n.* factor) box)]
                                                (in new))))))))
             ))))