(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [abstract
    [equivalence {"+" Equivalence}]
    [monoid {"+" Monoid}]
    [monad {"+" do}]
    [\\specification
     ["$[0]" functor {"+" Injection Comparison}]
     ["$[0]" apply]
     ["$[0]" monad]]]
   [control
    ["[0]" io]]
   [data
    ["[0]" product]
    ["[0]" text ("[1]#[0]" equivalence)]]
   [math
    ["[0]" random]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" / {"+" 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: .public 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 /.lifted]
                     (let [lifted (/.lifted text.monoid io.monad)
                           (open "io#[0]") io.monad]
                       (|> (do (/.with text.monoid io.monad)
                             [a (lifted (io#in left))
                              b (in right)]
                             (in (n.+ a b)))
                           io.run!
                           product.right
                           (n.= (n.+ left right)))))
            ))))