(.module:
  [library
   [lux #*
    ["_" test (#+ Test)]
    [abstract
     [monad (#+ do)]
     [\\specification
      [functor
       ["$." contravariant]]]]
    [data
     ["." bit ("#\." equivalence)]]
    [math
     ["." random (#+ Random)]
     [number
      ["n" nat]
      ["i" int]]]]]
  [\\library
   ["." / (#+ Equivalence)]])

(def: #export test
  Test
  (do random.monad
    [leftN random.nat
     rightN random.nat
     leftI random.int
     rightI random.int
     sample random.nat
     different (|> random.nat (random.filter (|>> (n.= sample) not)))
     #let [equivalence (: (Equivalence (Equivalence Nat))
                          (implementation
                           (def: (= left right)
                             (and (bit\= (\ left = leftN leftN)
                                         (\ right = leftN leftN))
                                  (bit\= (\ left = rightN rightN)
                                         (\ right = rightN rightN))
                                  (bit\= (\ left = leftN rightN)
                                         (\ right = leftN rightN))))))]]
    (<| (_.covering /._)
        ($_ _.and
            (_.for [/.functor]
                   ($contravariant.spec equivalence n.equivalence /.functor))
            (_.cover [/.rec]
                     (let [equivalence (: (Equivalence (List Nat))
                                          (/.rec (function (_ equivalence)
                                                   (implementation
                                                    (def: (= left right)
                                                      (case [left right]
                                                        [#.Nil #.Nil]
                                                        true

                                                        [(#.Cons leftH lefT) (#.Cons rightH rightT)]
                                                        (and (n.= leftH rightH)
                                                             (\ equivalence = lefT rightT))

                                                        _
                                                        false))))))]
                       (and (\ equivalence = (list sample sample) (list sample sample))
                            (not (\ equivalence = (list sample sample) (list sample)))
                            (not (\ equivalence = (list sample sample) (list different different))))))
            ))))