(.module:
  [lux #*
   ["_" test (#+ Test)]
   [abstract
    [equivalence (#+ Equivalence)]
    [monoid (#+ Monoid)]
    [monad (#+ do)]
    {[0 #spec]
     [/
      ["$." functor (#+ Injection Comparison)]
      ["$." apply]
      ["$." monad]]}]
   [control
    ["." io]]
   [data
    ["." product]
    ["." text ("#\." equivalence)]]
   [math
    ["." random]
    [number
     ["n" nat]]]]
  {1
   ["." / (#+ Writer)]})

(def: (injection monoid value)
  (All [w] (-> (Monoid w) (Injection (Writer w))))
  [(\ monoid identity) value])

(def: comparison
  (All [w] (Comparison (Writer w)))
  (function (_ == [_ left] [_ right])
    (== left right)))

(def: #export test
  Test
  (do random.monad
    [log (random.ascii 1)
     left random.nat
     right random.nat]
    (<| (_.covering /._)
        (_.for [/.Writer])
        ($_ _.and
            (_.for [/.functor]
                   ($functor.spec (..injection text.monoid) ..comparison /.functor))
            (_.for [/.apply]
                   ($apply.spec (..injection text.monoid) ..comparison (/.apply text.monoid)))
            (_.for [/.monad]
                   ($monad.spec (..injection text.monoid) ..comparison (/.monad text.monoid)))

            (_.cover [/.write]
                     (text\= log
                             (product.left (/.write log))))
            (_.cover [/.with /.lift]
                     (let [lift (/.lift text.monoid io.monad)
                           (^open "io\.") io.monad]
                       (|> (io.run (do (/.with text.monoid io.monad)
                                     [a (lift (io\wrap left))
                                      b (wrap right)]
                                     (wrap (n.+ a b))))
                           product.right
                           (n.= (n.+ left right)))))
            ))))