aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test/lux/meta/type/implicit.lux
blob: 233c121ca33231ccd1991049c6160ec7de61b8f9 (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
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
(.require
 [library
  [lux (.except)
   [abstract
    [equivalence (.only)]
    [functor (.only)]
    [monoid (.only)]
    [monad (.only do)]
    ["[0]" enum]]
   [data
    ["[0]" bit (.use "[1]#[0]" equivalence)]
    [collection
     ["[0]" list]]]
   [math
    ["[0]" random (.only Random)]
    [number
     ["n" nat]]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" /]])

(/.implicitly n.multiplication)

(def .public test
  Test
  (<| (_.covering /._)
      (do [! random.monad]
        [.let [digit (at ! each (n.% 10) random.nat)]
         left digit
         right digit
         .let [start (n.min left right)
               end (n.max left right)]

         left random.nat
         right random.nat]
        (all _.and
             (_.coverage [/.a/an /.a /.an]
               (let [first_order!
                     (let [(open "list#[0]") (list.equivalence n.equivalence)]
                       (and (bit#= (at n.equivalence = left right)
                                   (/.a = left right))
                            (list#= (at list.functor each ++ (enum.range n.enum start end))
                                    (/.an each ++ (enum.range n.enum start end)))))

                     second_order!
                     (/.a/an =
                             (enum.range n.enum start end)
                             (enum.range n.enum start end))

                     third_order!
                     (let [lln (/.a/an each (enum.range n.enum start)
                                       (enum.range n.enum start end))]
                       (/.a/an = lln lln))]
                 (and first_order!
                      second_order!
                      third_order!)))
             (_.coverage [/.with]
               (/.with [n.addition]
                 (n.= (at n.addition composite left right)
                      (/.a/an composite left right))))
             (_.coverage [/.implicitly]
               (n.= (at n.multiplication composite left right)
                    (/.a/an composite left right)))
             ))))