(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [abstract
    [monad {"+" do}]
    [\\specification
     ["$[0]" functor {"+" Injection Comparison}]
     ["$[0]" apply]
     ["$[0]" monad]
     ["$[0]" equivalence]]]
   [control
    ["[0]" pipe]
    ["[0]" io]]
   [data
    ["[0]" text ("[1]#[0]" equivalence)]]
   [math
    ["[0]" random {"+" Random}]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" / {"+" Try}]])

(def: injection
  (Injection Try)
  (|>> {/.#Success}))

(def: comparison
  (Comparison Try)
  (function (_ ==)
    (# (/.equivalence ==) =)))

(def: .public (attempt element)
  (All (_ a) (-> (Random a) (Random (Try a))))
  ($_ random.or
      (random.unicode 1)
      element))

(def: .public test
  Test
  (<| (_.covering /._)
      (_.for [/.Try])
      (do random.monad
        [expected random.nat
         alternative (|> random.nat (random.only (|>> (n.= expected) not)))
         error (random.unicode 1)
         .let [(open "io#[0]") io.monad]])
      ($_ _.and
          (_.for [/.equivalence]
                 ($equivalence.spec (/.equivalence n.equivalence) (..attempt random.nat)))
          (_.for [/.functor]
                 ($functor.spec ..injection ..comparison /.functor))
          (_.for [/.apply]
                 ($apply.spec ..injection ..comparison /.apply))
          (_.for [/.monad]
                 ($monad.spec ..injection ..comparison /.monad))

          (_.cover [/.trusted]
                   (n.= expected
                        (/.trusted {/.#Success expected})))
          (_.cover [/.of_maybe]
                   (case [(/.of_maybe {.#Some expected})
                          (/.of_maybe {.#None})]
                     [{/.#Success actual} {/.#Failure _}]
                     (n.= expected actual)

                     _
                     false))
          (_.cover [/.maybe]
                   (case [(/.maybe {/.#Success expected})
                          (/.maybe (is (/.Try Nat) {/.#Failure error}))]
                     [{.#Some actual} {.#None}]
                     (n.= expected actual)

                     _
                     false))
          (_.cover [/.else]
                   (and (n.= expected
                             (/.else alternative {/.#Success expected}))
                        (n.= alternative
                             (/.else alternative (is (Try Nat) {/.#Failure error})))))
          (_.cover [/.with /.lifted]
                   (let [lifted (/.lifted io.monad)]
                     (|> (do (/.with io.monad)
                           [a (lifted (io#in expected))
                            b (in alternative)]
                           (in (n.+ a b)))
                         io.run!
                         (pipe.case
                           {/.#Success result}
                           (n.= (n.+ expected alternative)
                                result)

                           _
                           false))))
          )))