(.module:
  [library
   [lux #*
    ["_" test (#+ Test)]
    [abstract
     [monad (#+ do)]
     [\\specification
      ["$." functor (#+ Injection Comparison)]
      ["$." apply]
      ["$." monad]]]
    [math
     ["." random]
     [number
      ["n" nat]]]]]
  [\\library
   ["." / (#+ Reader)
    [//
     ["." io (#+ IO)]]]])

(def: (injection value)
  (Injection (All [a r] (Reader r a)))
  (function (_ env)
    value))

(def: comparison
  (Comparison (All [a r] (Reader r a)))
  (function (_ == left right)
    (== (/.result [] left) (/.result [] right))))

(def: .public test
  Test
  (<| (_.covering /._)
      (_.for [/.Reader])
      (do random.monad
        [sample random.nat
         factor random.nat]
        ($_ _.and
            (_.for [/.functor]
                   ($functor.spec ..injection ..comparison /.functor))
            (_.for [/.apply]
                   ($apply.spec ..injection ..comparison /.apply))
            (_.for [/.monad]
                   ($monad.spec ..injection ..comparison /.monad))

            (_.cover [/.result /.read]
                     (n.= sample
                          (/.result sample /.read)))
            (_.cover [/.local]
                     (n.= (n.* factor sample)
                          (/.result sample (/.local (n.* factor) /.read))))
            (let [(^open "io\.") io.monad]
              (_.cover [/.with /.lift]
                       (|> (: (/.Reader Any (IO Nat))
                              (do (/.with io.monad)
                                [a (/.lift (io\in sample))
                                 b (in factor)]
                                (in (n.* b a))))
                           (/.result [])
                           io.run!
                           (n.= (n.* factor sample)))))))))