(.module:
  [library
   [lux #*
    ["_" test (#+ Test)]
    ["." type ("#\." equivalence)]
    [abstract
     [monad (#+ do)]
     ["." predicate]
     [\\specification
      ["$." equivalence]
      ["$." order]
      ["$." monoid]
      ["$." codec]]]
    [control
     ["." try]
     ["." exception]]
    [data
     ["." product]
     ["." bit ("#\." equivalence)]]
    [math
     ["." random (#+ Random)]
     [number
      ["i" int]]]]]
  ["$." // #_
   ["#" modulus]]
  [\\library
   ["." /
    ["/#" // #_
     ["#" modulus]]]])

(def: #export (random modulus)
  (All [%] (-> (//.Modulus %) (Random (/.Mod %))))
  (\ random.monad map
     (/.modular modulus)
     random.int))

(def: #export test
  Test
  (<| (_.covering /._)
      (_.for [/.Mod])
      (do random.monad
        [param\\% ($//.random +1,000,000)
         param (..random param\\%)

         subject\\% (random.only (predicate.intersect (|>> //.divisor (i.> +2))
                                                      (|>> (//.= param\\%) not))
                                 ($//.random +1,000,000))
         subject (..random subject\\%)
         another (..random subject\\%)]
        (`` ($_ _.and
                (_.for [/.equivalence /.=]
                       ($equivalence.spec /.equivalence (..random subject\\%)))
                (_.for [/.order /.<]
                       ($order.spec /.order (..random subject\\%)))
                (~~ (template [<compose> <monoid>]
                      [(_.for [<monoid> <compose>]
                              ($monoid.spec /.equivalence (<monoid> subject\\%) (..random subject\\%)))]
                      
                      [/.+ /.addition]
                      [/.* /.multiplication]
                      ))
                (_.for [/.codec]
                       ($codec.spec /.equivalence (/.codec subject\\%) (..random subject\\%)))

                (_.cover [/.incorrect_modulus]
                         (case (|> param
                                   (\ (/.codec param\\%) encode)
                                   (\ (/.codec subject\\%) decode))
                           (#try.Failure error)
                           (exception.match? /.incorrect_modulus error)
                           
                           (#try.Success _)
                           false))
                (_.cover [/.modulus]
                         (and (type\= (:of (/.modulus subject))
                                      (:of (/.modulus subject)))
                              (not (type\= (:of (/.modulus subject))
                                           (:of (/.modulus param))))))
                (_.cover [/.modular /.value]
                         (/.= subject
                              (/.modular (/.modulus subject) (/.value subject))))
                (_.cover [/.>]
                         (bit\= (/.> another subject)
                                (/.< subject another)))
                (_.cover [/.<= /.>=]
                         (bit\= (/.<= another subject)
                                (/.>= subject another)))
                (_.cover [/.-]
                         (let [zero (/.modular (/.modulus subject) +0)]
                           (and (/.= zero
                                     (/.- subject subject))
                                (/.= subject
                                     (/.- zero subject)))))
                (_.cover [/.inverse]
                         (let [one (/.modular (/.modulus subject) +1)
                               co_prime? (i.co_prime? (//.divisor (/.modulus subject))
                                                      (/.value subject))]
                           (case (/.inverse subject)
                             (#.Some subject^-1)
                             (and co_prime?
                                  (|> subject
                                      (/.* subject^-1)
                                      (/.= one)))
                             
                             #.None
                             (not co_prime?))))
                (_.cover [/.adapter]
                         (<| (try.default false)
                             (do try.monad
                               [copy\\% (//.modulus (//.divisor subject\\%))
                                adapt (/.adapter subject\\% copy\\%)]
                               (wrap (|> subject
                                         /.value
                                         (/.modular copy\\%)
                                         adapt
                                         (/.= subject))))))
                (_.cover [/.moduli_are_not_equal]
                         (case (/.adapter subject\\% param\\%)
                           (#try.Failure error)
                           (exception.match? /.moduli_are_not_equal error)
                           
                           (#try.Success _)
                           false))
                )))))