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

(.module:
  [lux #*
   ["_" test (#+ Test)]
   [abstract
    [monad (#+ do)]
    {[0 #test]
     [/
      ["$." functor (#+ Injection Comparison)]
      ["$." apply]
      ["$." monad]]}]
   [data
    [number
     ["n" nat]]]
   [math
    ["." random]]]
  {1
   ["." / (#+ Thread)
    [//
     ["." io]]]})

(def: (injection value)
  (Injection (All [a !] (Thread ! a)))
  (:: /.monad wrap value))

(def: comparison
  (Comparison (All [a !] (Thread ! a)))
  (function (_ == left right)
    (== (/.run left) (/.run right))))

(def: #export test
  Test
  (do random.monad
    [sample random.nat
     factor random.nat]
    (<| (_.covering /._)
        ($_ _.and
            (_.with-cover [/.Thread]
              ($_ _.and
                  (_.cover [/.run]
                           (n.= sample
                                (|> sample
                                    (:: /.monad wrap)
                                    /.run)))
                  (_.cover [/.io]
                           (n.= sample
                                (|> sample
                                    (:: /.monad wrap)
                                    /.io
                                    io.run)))
                  
                  (_.with-cover [/.functor]
                    ($functor.spec ..injection ..comparison /.functor))
                  (_.with-cover [/.apply]
                    ($apply.spec ..injection ..comparison /.apply))
                  (_.with-cover [/.monad]
                    ($monad.spec ..injection ..comparison /.monad))
                  ))

            (_.with-cover [/.Box /.box]
              ($_ _.and
                  (_.cover [/.read]
                           (n.= sample
                                (/.run (: (All [!] (Thread ! Nat))
                                          (do /.monad
                                            [box (/.box sample)]
                                            (/.read box))))))

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

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