(.require
 [library
  [lux (.except)
   [abstract
    [monad (.only do)]
    [\\specification
     ["$[0]" equivalence]]
    ["[0]" codec
     ["[1]T" \\test]]
    ["[0]" order
     ["[1]T" \\test]]
    ["[0]" monoid
     ["[1]T" \\test]]]
   [control
    ["[0]" try]
    ["[0]" exception]
    [function
     ["[0]" predicate]]]
   [data
    ["[0]" product]
    ["[0]" bit (.use "[1]#[0]" equivalence)]]
   [math
    ["[0]" random (.only Random)]
    [number
     ["i" int]]]
   [meta
    ["[0]" type (.use "[1]#[0]" equivalence)]]
   [test
    ["_" property (.only Test)]]]]
 [///
  ["//T" modulus]]
 [\\library
  ["[0]" / (.only)
   [///
    ["//" modulus]]]])

(def .public (random modulus)
  (All (_ %)
    (-> (//.Modulus %)
        (Random (/.Mod %))))
  (of random.monad each
      (/.modular modulus)
      random.int))

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

         subject::% (random.only (predicate.and (|>> //.divisor (i.> +2))
                                                (|>> (//.= param::%) not))
                                 (//T.random +1,000,000))
         subject (..random subject::%)
         another (..random subject::%)]
        (`` (all _.and
                 (_.for [/.equivalence /.=]
                        ($equivalence.spec /.equivalence (..random subject::%)))
                 (_.for [/.order /.<]
                        (orderT.spec /.order (..random subject::%)))
                 (,, (with_template [<composite> <monoid>]
                       [(_.for [<monoid> <composite>]
                               (monoidT.spec /.equivalence (<monoid> subject::%) (..random subject::%)))]
                       
                       [/.+ /.addition]
                       [/.* /.multiplication]
                       ))
                 (_.for [/.codec]
                        (codecT.spec /.equivalence (/.codec subject::%) (..random subject::%)))

                 (_.coverage [/.incorrect_modulus]
                   (when (|> param
                             (of (/.codec param::%) encoded)
                             (of (/.codec subject::%) decoded))
                     {try.#Failure error}
                     (exception.match? /.incorrect_modulus error)
                     
                     {try.#Success _}
                     false))
                 (_.coverage [/.modulus]
                   (and (type#= (type_of (/.modulus subject))
                                (type_of (/.modulus subject)))
                        (not (type#= (type_of (/.modulus subject))
                                     (type_of (/.modulus param))))))
                 (_.coverage [/.modular /.value]
                   (/.= subject
                        (/.modular (/.modulus subject) (/.value subject))))
                 (_.coverage [/.>]
                   (bit#= (/.> another subject)
                          (/.< subject another)))
                 (_.coverage [/.<= /.>=]
                   (bit#= (/.<= another subject)
                          (/.>= subject another)))
                 (_.coverage [/.-]
                   (let [zero (/.modular (/.modulus subject) +0)]
                     (and (/.= zero
                               (/.- subject subject))
                          (/.= subject
                               (/.- zero subject)))))
                 (_.coverage [/.inverse]
                   (let [one (/.modular (/.modulus subject) +1)
                         co_prime? (i.co_prime? (//.divisor (/.modulus subject))
                                                (/.value subject))]
                     (when (/.inverse subject)
                       {.#Some subject^-1}
                       (and co_prime?
                            (|> subject
                                (/.* subject^-1)
                                (/.= one)))
                       
                       {.#None}
                       (not co_prime?))))
                 (_.coverage [/.adapter]
                   (<| (try.else false)
                       (do try.monad
                         [copy::% (//.modulus (//.divisor subject::%))
                          adapt (/.adapter subject::% copy::%)]
                         (in (|> subject
                                 /.value
                                 (/.modular copy::%)
                                 adapt
                                 (/.= subject))))))
                 (_.coverage [/.moduli_are_not_equal]
                   (when (/.adapter subject::% param::%)
                     {try.#Failure error}
                     (exception.match? /.moduli_are_not_equal error)
                     
                     {try.#Success _}
                     false))
                 )))))