aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test/lux/type/implicit.lux
blob: 2e694abf10dae267d57cf66cb98205bbf2353fee (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
(.module:
  [library
   [lux #*
    ["_" test (#+ Test)]
    [abstract
     [equivalence (#+)]
     [functor (#+)]
     [monoid (#+)]
     [monad (#+ do)]
     ["." enum]]
    [data
     ["." bit ("#\." equivalence)]
     [collection
      ["." list]]]
    [math
     ["." random (#+ Random)]
     [number
      ["n" nat]]]]]
  [\\library
   ["." /]])

(/.implicit: [n.multiplication])

(def: .public test
  Test
  (<| (_.covering /._)
      (do {! random.monad}
        [.let [digit (\ ! 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]
        ($_ _.and
            (_.cover [/.\\]
                     (let [first_order!
                           (let [(^open "list\.") (list.equivalence n.equivalence)]
                             (and (bit\= (\ n.equivalence = left right)
                                         (/.\\ = left right))
                                  (list\= (\ list.functor each ++ (enum.range n.enum start end))
                                          (/.\\ each ++ (enum.range n.enum start end)))))

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

                           third_order!
                           (let [lln (/.\\ each (enum.range n.enum start)
                                           (enum.range n.enum start end))]
                             (/.\\ = lln lln))]
                       (and first_order!
                            second_order!
                            third_order!)))
            (_.cover [/.with]
                     (/.with [n.addition]
                       (n.= (\ n.addition composite left right)
                            (/.\\ composite left right))))
            (_.cover [/.implicit:]
                     (n.= (\ n.multiplication composite left right)
                          (/.\\ composite left right)))
            ))))