(.require
 [library
  [lux (.except)
   [data
    ["[0]" bit (.use "[1]#[0]" equivalence)]]
   [abstract
    [monad (.only do)]
    ["[0]" equivalence
     ["[1]T" \\test]]
    [\\specification
     ["$[0]" hash]]
    ["[0]" monoid
     ["[1]T" \\test]]]
   [math
    ["[0]" random (.only Random)]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" / (.use "[1]#[0]" equivalence)
   [// (.only hex)
    ["n" nat]
    ["i" int]]]])

(def bit
  Test
  (do [! random.monad]
    [pattern random.nat
     idx (of ! 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 (of ! 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 (of ! 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 (of ! each (n.% /.width) random.nat)
                .let [spare (n.- size /.width)]
                offset (of ! each (n.% spare) random.nat)]
               (_.coverage [/.region]
                 (when 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 (of ! each (n.% /.width) random.nat)]
           (when (/.sub size)
             {.#None}
             (_.coverage [/.sub]
               (n.= 0 size))

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

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

(def .public test
  Test
  (<| (_.covering /._)
      (_.for [.I64])
      (do [! random.monad]
        [pattern random.nat
         idx (of ! 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
             ))))