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

(.module:
  [library
   [lux #*
    ["_" test (#+ Test)]
    [abstract
     [monad (#+ do)]
     [\\specification
      ["$." functor (#+ Injection Comparison)]
      ["$." apply]
      ["$." monad]]]
    [math
     ["." random]
     [number
      ["n" nat]]]]]
  [\\library
   ["." / (#+ Thread)
    [//
     ["." 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 (: (All (_ !) (Thread ! Nat))
                                                  (do /.monad
                                                    [box (/.box sample)]
                                                    (/.read! box))))))

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

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