(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [data
    ["[0]" bit ("[1]#[0]" equivalence)]]
   [abstract
    [monad {"+" do}]
    [\\specification
     ["$[0]" equivalence]
     ["$[0]" hash]
     ["$[0]" monoid]]]
   [math
    ["[0]" random {"+" Random}]]]]
 [\\library
  ["[0]" / ("#[0]" equivalence)
   [// {"+" hex}
    ["n" nat]
    ["i" int]]]])

(def: bit
  Test
  (do [! random.monad]
    [pattern random.nat
     idx (# ! each (n.% /.width) random.nat)]
    (all _.and
         (_.coverage [/.one? /.one]
           (if (/.one? idx pattern)
             (#= pattern (/.one idx pattern))
             (not (#= pattern (/.one idx pattern)))))
         (_.coverage [/.zero? /.zero]
           (if (/.zero? idx pattern)
             (#= pattern (/.zero idx pattern))
             (not (#= pattern (/.zero idx pattern)))))
         (_.coverage [/.flipped]
           (#= (/.flipped idx pattern)
               (if (/.one? idx pattern)
                 (/.zero idx pattern)
                 (/.one idx pattern))))
         (_.coverage [/.bit]
           (bit#= (/.zero? idx pattern)
                  (#= /.false (/.and (/.bit idx) pattern))))
         )))

(def: shift
  Test
  (do [! random.monad]
    [pattern random.nat]
    (all _.and
         (do !
           [idx (# ! each (|>> (n.% (-- /.width)) ++) random.nat)]
           (_.coverage [/.left_shifted /.right_shifted]
             (let [nullity!
                   (and (#= pattern (/.left_shifted 0 pattern))
                        (#= pattern (/.right_shifted 0 pattern)))

                   idempotency!
                   (and (#= pattern (/.left_shifted /.width pattern))
                        (#= pattern (/.right_shifted /.width pattern)))

                   movement!
                   (let [shift (n.- idx /.width)]
                     (#= (/.and (/.mask idx) pattern)
                         (|> pattern
                             (/.left_shifted shift)
                             (/.right_shifted shift))))]
               (and nullity!
                    idempotency!
                    movement!))))
         )))

(def: mask
  Test
  (<| (_.for [/.Mask])
      (do [! random.monad]
        [pattern random.nat
         idx (# ! each (n.% /.width) random.nat)
         signed random.int]
        (all _.and
             (_.coverage [/.sign]
               (bit#= (#= (.i64 0) (/.and /.sign signed))
                      (i.positive? signed)))
             (_.coverage [/.mask]
               (let [mask (/.mask idx)
                     idempotency! (#= (/.and mask pattern)
                                      (/.and mask (/.and mask pattern)))

                     limit (++ (.nat mask))
                     limit! (if (n.< limit pattern)
                              (#= pattern (/.and mask pattern))
                              (n.< limit (/.and mask pattern)))

                     empty! (#= /.false (/.mask 0))
                     full! (#= /.true (/.mask /.width))]
                 (and idempotency!
                      limit!

                      empty!
                      full!)))
             (do !
               [size (# ! each (n.% /.width) random.nat)
                .let [spare (n.- size /.width)]
                offset (# ! each (n.% spare) random.nat)]
               (_.coverage [/.region]
                 (case size
                   0 (#= /.false (/.region offset size))
                   _ (#= (|> pattern
                             ... NNNNYYYYNNNN
                             (/.right_shifted offset)
                             ... ____NNNNYYYY
                             (/.left_shifted spare)
                             ... YYYY________
                             (/.right_shifted spare)
                             ... ________YYYY
                             (/.left_shifted offset)
                             ... ____YYYY____
                             )
                         (/.and (/.region offset size) pattern)))))
             ))))

(def: sub
  Test
  (_.for [/.Sub]
         (do [! random.monad]
           [size (# ! each (n.% /.width) random.nat)]
           (case (/.sub size)
             {.#None}
             (_.coverage [/.sub]
               (n.= 0 size))

             {.#Some sub}
             (do [! random.monad]
               [.let [limit (|> (-- (# sub bits))
                                /.mask
                                .int
                                ++)]
                expected (# ! each (i.% limit) random.int)
                .let [random (is (All (_ size)
                                   (-> (-> I64 (I64 size)) (Random (I64 size))))
                                 (function (_ narrow)
                                   (# random.functor each narrow random.i64)))]]
               (all _.and
                    ($equivalence.spec (# sub sub_equivalence) (random (# sub narrow)))
                    (_.coverage [/.sub]
                      (let [actual (|> expected .i64 (# sub narrow) (# sub wide))]
                        (#= expected actual)))
                    ))))))

(def: signature
  Test
  (all _.and
       (_.for [/.equivalence]
              ($equivalence.spec /.equivalence random.i64))
       (_.for [/.hash]
              ($hash.spec /.hash random.i64))
       (_.for [/.disjunction]
              ($monoid.spec n.equivalence /.disjunction random.nat))
       (_.for [/.conjunction]
              ($monoid.spec n.equivalence /.conjunction random.nat))
       ))

(def: .public test
  Test
  (<| (_.covering /._)
      (_.for [.I64])
      (do [! random.monad]
        [pattern random.nat
         idx (# ! each (n.% /.width) random.nat)]
        (all _.and
             (_.coverage [/.width /.bits_per_byte /.bytes_per_i64]
               (and (n.= /.bytes_per_i64
                         (n./ /.bits_per_byte /.width))
                    (n.= /.bits_per_byte
                         (n./ /.bytes_per_i64 /.width))))
             (_.coverage [/.false]
               (n.= 0 (/.ones /.false)))
             (_.coverage [/.or]
               (and (#= /.true (/.or /.true pattern))
                    (#= pattern (/.or /.false pattern))))
             (_.coverage [/.true]
               (n.= /.width (/.ones /.true)))
             (_.coverage [/.and]
               (and (#= pattern (/.and /.true pattern))
                    (#= /.false (/.and /.false pattern))))
             (_.coverage [/.not]
               (and (#= /.false
                        (/.and pattern
                               (/.not pattern)))
                    (#= /.true
                        (/.or pattern
                              (/.not pattern)))))
             (_.coverage [/.xor]
               (and (#= /.true
                        (/.xor pattern
                               (/.not pattern)))
                    (#= /.false
                        (/.xor pattern
                               pattern))))
             (_.coverage [/.ones]
               (let [zero&one!
                     (if (/.one? idx pattern)
                       (n.= (-- (/.ones pattern)) (/.ones (/.zero idx pattern)))
                       (n.= (++ (/.ones pattern)) (/.ones (/.one idx pattern))))

                     complementarity!
                     (n.= /.width
                          (n.+ (/.ones pattern)
                               (/.ones (/.not pattern))))]
                 (and zero&one!
                      complementarity!)))
             (_.coverage [/.left_rotated /.right_rotated]
               (let [false!
                     (and (#= /.false (/.left_rotated idx /.false))
                          (#= /.false (/.right_rotated idx /.false)))

                     true!
                     (and (#= /.true (/.left_rotated idx /.true))
                          (#= /.true (/.right_rotated idx /.true)))

                     inverse!
                     (and (|> pattern
                              (/.left_rotated idx)
                              (/.right_rotated idx)
                              (#= pattern))
                          (|> pattern
                              (/.right_rotated idx)
                              (/.left_rotated idx)
                              (#= pattern)))

                     nullity!
                     (and (|> pattern
                              (/.left_rotated 0)
                              (#= pattern))
                          (|> pattern
                              (/.right_rotated 0)
                              (#= pattern)))

                     futility!
                     (and (|> pattern
                              (/.left_rotated /.width)
                              (#= pattern))
                          (|> pattern
                              (/.right_rotated /.width)
                              (#= pattern)))]
                 (and false!
                      true!
                      inverse!
                      nullity!
                      futility!)))
             (_.coverage [/.reversed]
               (and (|> pattern /.reversed /.reversed (#= pattern))
                    (or (|> pattern /.reversed (#= pattern) not)
                        (let [high (/.and (hex "FFFFFFFF00000000")
                                          pattern)
                              low (/.and (hex "00000000FFFFFFFF")
                                         pattern)]
                          (#= (/.reversed high)
                              low)))))
             
             ..bit
             ..shift
             ..mask
             ..sub
             ..signature
             ))))