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

(def: bit
  Test
  (do {! random.monad}
    [pattern random.nat
     idx (\ ! map (n.% /.width) random.nat)]
    ($_ _.and
        (_.cover [/.set? /.set]
                 (if (/.set? idx pattern)
                   (\= pattern (/.set idx pattern))
                   (not (\= pattern (/.set idx pattern)))))
        (_.cover [/.clear? /.clear]
                 (if (/.clear? idx pattern)
                   (\= pattern (/.clear idx pattern))
                   (not (\= pattern (/.clear idx pattern)))))
        (_.cover [/.flip]
                 (\= (/.flip idx pattern)
                     (if (/.set? idx pattern)
                       (/.clear idx pattern)
                       (/.set idx pattern))))
        (_.cover [/.bit]
                 (bit\= (/.clear? idx pattern)
                        (\= /.false (/.and (/.bit idx) pattern))))
        )))

(def: shift
  Test
  (do {! random.monad}
    [pattern random.nat]
    ($_ _.and
        (do !
          [idx (\ ! map (|>> (n.% (dec /.width)) inc) random.nat)]
          (_.cover [/.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 (\ ! map (n.% /.width) random.nat)
         signed random.int]
        ($_ _.and
            (_.cover [/.sign]
                     (bit\= (\= (.i64 0) (/.and /.sign signed))
                            (i.positive? signed)))
            (_.cover [/.mask]
                     (let [mask (/.mask idx)
                           idempotency! (\= (/.and mask pattern)
                                            (/.and mask (/.and mask pattern)))

                           limit (inc (.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 (\ ! map (n.% /.width) random.nat)
               .let [spare (n.- size /.width)]
               offset (\ ! map (n.% spare) random.nat)]
              (_.cover [/.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 (\ ! map (n.% /.width) random.nat)]
           (case (/.sub size)
             #.None
             (_.cover [/.sub]
                      (n.= 0 size))

             (#.Some sub)
             (do {! random.monad}
               [.let [limit (|> (dec (\ sub width))
                                /.mask
                                .int
                                inc)]
                expected (\ ! map (i.% limit) random.int)
                .let [random (: (All [size]
                                  (-> (-> I64 (I64 size)) (Random (I64 size))))
                                (function (_ narrow)
                                  (\ random.functor map narrow random.i64)))]]
               ($_ _.and
                   ($equivalence.spec (\ sub &equivalence) (random (\ sub narrow)))
                   (_.cover [/.sub]
                            (let [actual (|> expected .i64 (\ sub narrow) (\ sub widen))]
                              (\= expected actual)))
                   ))))))

(def: signature
  Test
  ($_ _.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 (\ ! map (n.% /.width) random.nat)]
        ($_ _.and
            (_.cover [/.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))))
            (_.cover [/.false]
                     (n.= 0 (/.ones /.false)))
            (_.cover [/.or]
                     (and (\= /.true (/.or /.true pattern))
                          (\= pattern (/.or /.false pattern))))
            (_.cover [/.true]
                     (n.= /.width (/.ones /.true)))
            (_.cover [/.and]
                     (and (\= pattern (/.and /.true pattern))
                          (\= /.false (/.and /.false pattern))))
            (_.cover [/.not]
                     (and (\= /.false
                              (/.and pattern
                                     (/.not pattern)))
                          (\= /.true
                              (/.or pattern
                                    (/.not pattern)))))
            (_.cover [/.xor]
                     (and (\= /.true
                              (/.xor pattern
                                     (/.not pattern)))
                          (\= /.false
                              (/.xor pattern
                                     pattern))))
            (_.cover [/.ones]
                     (let [clear&set!
                           (if (/.set? idx pattern)
                             (n.= (dec (/.ones pattern)) (/.ones (/.clear idx pattern)))
                             (n.= (inc (/.ones pattern)) (/.ones (/.set idx pattern))))

                           complementarity!
                           (n.= /.width
                                (n.+ (/.ones pattern)
                                     (/.ones (/.not pattern))))]
                       (and clear&set!
                            complementarity!)))
            (_.cover [/.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!)))
            (_.cover [/.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
            ))))