(.require
 [library
  [lux (.except)
   ["_" test (.only Test)]
   [abstract
    [predicate (.only Predicate)]
    [monad (.only do)]]
   [control
    ["[0]" maybe (.use "[1]#[0]" monad)]]
   [data
    [collection
     ["[0]" list (.use "[1]#[0]" functor)]]]
   [math
    ["[0]" random]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" /]])

(def _refiner
  (/.refiner (n.> 123)))

(def _type
  (/.type _refiner))

(def .public test
  Test
  (<| (_.covering /._)
      (_.for [/.Refined])
      (do [! random.monad]
        [raw random.nat
         modulus (at ! each (|>> (n.% 10) (n.+ 2)) random.nat)
         .let [predicate (is (Predicate Nat)
                             (|>> (n.% modulus) (n.= 0)))]
         total_raws (at ! each (|>> (n.% 20) ++) random.nat)
         raws (random.list total_raws random.nat)]
        (all _.and
             (_.for [/.Refiner]
                    (all _.and
                         (_.coverage [/.refiner]
                           (case (/.refiner predicate raw)
                             {.#Some refined}
                             (predicate raw)
                             
                             {.#None}
                             (not (predicate raw))))
                         (_.coverage [/.predicate]
                           (|> (/.refiner predicate modulus)
                               (maybe#each (|>> /.predicate (same? predicate)))
                               (maybe.else false)))
                         ))
             (_.coverage [/.value]
               (|> (/.refiner predicate modulus)
                   (maybe#each (|>> /.value (n.= modulus)))
                   (maybe.else false)))
             (_.coverage [/.lifted]
               (and (|> (/.refiner predicate modulus)
                        (maybe#each (/.lifted (n.+ modulus)))
                        maybe#conjoint
                        (maybe#each (|>> /.value (n.= (n.+ modulus modulus))))
                        (maybe.else false))
                    (|> (/.refiner predicate modulus)
                        (maybe#each (/.lifted (n.+ (++ modulus))))
                        maybe#conjoint
                        (maybe#each (|>> /.value (n.= (n.+ modulus (++ modulus)))))
                        (maybe.else false)
                        not)))
             (_.coverage [/.only]
               (let [expected (list.only predicate raws)
                     actual (/.only (/.refiner predicate) raws)]
                 (and (n.= (list.size expected)
                           (list.size actual))
                      (at (list.equivalence n.equivalence) =
                          expected
                          (list#each /.value actual)))))
             (_.coverage [/.partition]
               (let [expected (list.only predicate raws)
                     [actual alternative] (/.partition (/.refiner predicate) raws)]
                 (and (n.= (list.size expected)
                           (list.size actual))
                      (n.= (n.- (list.size expected) total_raws)
                           (list.size alternative))
                      (at (list.equivalence n.equivalence) =
                          expected
                          (list#each /.value actual)))))
             (_.coverage [/.type]
               (exec (is (Maybe .._type)
                         (.._refiner raw))
                 true))
             ))))