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

(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [abstract
    [monad {"+" do}]
    [\\specification
     ["$[0]" functor {"+" Injection Comparison}]
     ["$[0]" apply]
     ["$[0]" monad]]]
   [math
    ["[0]" random]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" / {"+" Thread}
   [//
    ["[0]" io]]]])

(def: (injection value)
  (Injection (All (_ a !) (Thread ! a)))
  (# /.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 /._)
        ($_ _.and
            (_.for [/.Thread]
                   ($_ _.and
                       (_.cover [/.result]
                                (n.= sample
                                     (|> sample
                                         (# /.monad in)
                                         /.result)))
                       (_.cover [/.io]
                                (n.= sample
                                     (|> sample
                                         (# /.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]
                   ($_ _.and
                       (_.cover [/.read!]
                                (n.= sample
                                     (/.result (is (All (_ !) (Thread ! Nat))
                                                   (do /.monad
                                                     [box (/.box sample)]
                                                     (/.read! box))))))

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

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