(.using
 [library
  [lux "*"
   ["_" test (.only Test)]
   [abstract
    [functor (.only)]
    [monad (.only do)]
    ["[0]" monoid
     ["$[1]" \\specification]]
    ["[0]" mix (.only Mix)
     ["$[1]" \\specification]]
    [\\specification
     ["$[0]" equivalence]
     ["$[0]" functor (.only Injection)]]]
   [control
    ["[0]" maybe ("[1]#[0]" functor)]]
   [data
    ["[0]" bit]
    ["[0]" text ("[1]#[0]" equivalence)]
    [collection
     ["[0]" list]
     ["[0]" set]]]
   [math
    ["[0]" random (.only Random)]
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" / (.only Array)
   ["!" \\unsafe]]])

(def: injection
  (Injection Array)
  (|>> list /.of_list))

(def: bounded_size
  (Random Nat)
  (# random.monad each (|>> (n.% 20) ++)
     random.nat))

(def: structures
  Test
  (do [! random.monad]
    [size ..bounded_size]
    (all _.and
         (_.for [/.equivalence]
                ($equivalence.spec (/.equivalence n.equivalence) (random.array size random.nat)))
         (_.for [/.monoid]
                ($monoid.spec (/.equivalence n.equivalence) /.monoid (random.array size random.nat)))
         (_.for [/.functor]
                ($functor.spec ..injection /.equivalence /.functor))
         (_.for [/.mix]
                ($mix.spec ..injection /.equivalence /.mix))
         )))

(def: search
  Test
  (do [! random.monad]
    [size ..bounded_size
     base random.nat
     shift random.nat
     .let [expected (n.+ base shift)]
     the_array (random.array size random.nat)
     evens (random.array size (random.only n.even? random.nat))]
    (all _.and
         (let [(open "/#[0]") /.functor
               choose (is (-> Nat (Maybe Text))
                          (function (_ value)
                            (if (n.even? value)
                              {.#Some (# n.decimal encoded value)}
                              {.#None})))]
           (_.coverage [/.one]
             (case [(|> evens
                        (/#each (# n.decimal encoded))
                        (/.item 0))
                    (/.one choose evens)]
               [{.#Some expected} {.#Some actual}]
               (text#= expected actual)

               [{.#None} {.#None}]
               true

               _
               false)))
         (_.coverage [/.example]
           (# (maybe.equivalence n.equivalence) =
              (/.example n.even? the_array)
              (list.example n.even? (/.list {.#None} the_array))))
         (_.coverage [/.example']
           (case [(/.example n.even? the_array)
                  (/.example' (function (_ idx member)
                                (n.even? member))
                              the_array)]
             [{.#Some expected} {.#Some [idx actual]}]
             (case (/.item idx the_array)
               {.#Some again}
               (and (n.= expected actual)
                    (n.= actual again))
               
               {.#None}
               false)

             [{.#None} {.#None}]
             true

             _
             false))
         (_.coverage [/.every?]
           (# bit.equivalence =
              (list.every? n.even? (/.list {.#None} the_array))
              (/.every? n.even? the_array)))
         (_.coverage [/.any?]
           (# bit.equivalence =
              (list.any? n.even? (/.list {.#None} the_array))
              (/.any? n.even? the_array)))
         )))

(def: test|unsafe
  Test
  (<| (_.covering !._)
      (_.for [!.Array])
      (do [! random.monad]
        [size ..bounded_size
         base random.nat
         shift random.nat
         dummy (random.only (|>> (n.= base) not) random.nat)
         .let [expected (n.+ base shift)]
         the_array (random.array size random.nat)
         evens (random.array size (random.only n.even? random.nat))]
        (`` (all _.and
                 (_.for [!.=]
                        ($equivalence.spec (function (_ left right)
                                             (!.= n.equivalence left right))
                                           (random.array size random.nat)))
                 (_.for [!.composite]
                        ($monoid.spec (/.equivalence n.equivalence)
                                      (implementation
                                       (def: identity (!.empty 0))
                                       (def: (composite left right)
                                         (!.composite left right)))
                                      (random.array size random.nat)))
                 (_.for [!.each]
                        ($functor.spec ..injection /.equivalence
                                       (function (_ $ it)
                                         (!.each $ it))))
                 (_.for [!.mix]
                        ($mix.spec ..injection /.equivalence
                                   (is (Mix !.Array)
                                       (function (_ $ init it)
                                         (!.mix (function (_ index item output)
                                                  ($ item output))
                                                init
                                                it)))))
                 
                 (_.coverage [!.empty !.size]
                   (n.= size (!.size (is (Array Nat)
                                         (!.empty size)))))
                 (_.coverage [!.type]
                   (case !.Array
                     (pattern (<| {.#Named (symbol !.Array)}
                                  {.#UnivQ (list)}
                                  {.#Primitive nominal_type (list {.#Parameter 1})}))
                     (same? !.type nominal_type)

                     _
                     false))
                 (_.coverage [!.lacks?]
                   (let [the_array (|> (!.empty 2)
                                       (is (Array Nat))
                                       (!.has! 0 expected))]
                     (and (not (!.lacks? 0 the_array))
                          (!.lacks? 1 the_array))))
                 (_.coverage [!.item !.has!]
                   (|> (!.empty 2)
                       (is (Array Nat))
                       (!.has! 0 expected)
                       (!.item 0)
                       (n.= expected)))
                 (_.coverage [!.lacks!]
                   (|> (!.empty 1)
                       (is (Array Nat))
                       (!.has! 0 expected)
                       (!.lacks! 0)
                       (!.lacks? 0)))
                 (_.coverage [!.lacks?]
                   (let [the_array (|> (!.empty 2)
                                       (is (Array Nat))
                                       (!.has! 0 expected))]
                     (and (not (!.lacks? 0 the_array))
                          (!.lacks? 1 the_array))))
                 (_.coverage [!.has?]
                   (let [the_array (|> (!.empty 2)
                                       (is (Array Nat))
                                       (!.has! 0 expected))]
                     (and (!.has? 0 the_array)
                          (not (!.has? 1 the_array)))))
                 (_.coverage [!.revised!]
                   (|> (!.empty 1)
                       (is (Array Nat))
                       (!.has! 0 base)
                       (!.revised! 0 (n.+ shift))
                       (!.item 0)
                       (n.= expected)))
                 (_.coverage [!.upsert!]
                   (let [the_array (|> (!.empty 2)
                                       (is (Array Nat))
                                       (!.has! 0 base)
                                       (!.upsert! 0 dummy (n.+ shift))
                                       (!.upsert! 1 base (n.+ shift)))]
                     (and (n.= expected (!.item 0 the_array))
                          (n.= expected (!.item 1 the_array)))))
                 (do !
                   [occupancy (# ! each (n.% (++ size)) random.nat)]
                   (_.coverage [!.occupancy !.vacancy]
                     (let [the_array (loop (again [output (is (Array Nat)
                                                              (!.empty size))
                                                   idx 0])
                                       (if (n.< occupancy idx)
                                         (again (!.has! idx expected output)
                                                (++ idx))
                                         output))]
                       (and (n.= occupancy (!.occupancy the_array))
                            (n.= size (n.+ (!.occupancy the_array)
                                           (!.vacancy the_array)))))))
                 (do !
                   [the_list (random.list size random.nat)
                    .let [the_array (!.clone the_array)
                          members (|> the_array (!.list {.#None}) (set.of_list n.hash))]
                    default (random.only (function (_ value)
                                           (not (or (n.even? value)
                                                    (set.member? members value))))
                                         random.nat)]
                   (_.coverage [!.of_list !.list]
                     (and (|> the_list !.of_list (!.list {.#None})
                              (# (list.equivalence n.equivalence) = the_list))
                          (|> the_array (!.list {.#None}) !.of_list
                              (!.= n.equivalence the_array))
                          (exec
                            (!.only! n.even? the_array)
                            (list.every? (function (_ value)
                                           (or (n.even? value)
                                               (same? default value)))
                                         (!.list {.#Some default} the_array))))))
                 (do !
                   [amount (# ! each (n.% (++ size)) random.nat)]
                   (_.coverage [!.copy!]
                     (let [copy (is (Array Nat)
                                    (!.empty size))]
                       (exec (!.copy! amount 0 the_array 0 copy)
                         (# (list.equivalence n.equivalence) =
                            (list.first amount (!.list {.#None} the_array))
                            (!.list {.#None} copy))))))
                 (_.coverage [!.clone]
                   (let [clone (!.clone the_array)]
                     (and (not (same? the_array clone))
                          (!.= n.equivalence the_array clone))))
                 (let [the_array (!.clone the_array)
                       evens (|> the_array (!.list {.#None}) (list.only n.even?))
                       odds (|> the_array (!.list {.#None}) (list.only n.odd?))]
                   (_.coverage [!.only!]
                     (exec (!.only! n.even? the_array)
                       (and (n.= (list.size evens) (!.occupancy the_array))
                            (n.= (list.size odds) (!.vacancy the_array))
                            (|> the_array
                                (!.list {.#None})
                                (# (list.equivalence n.equivalence) = evens))))))
                 (let [choose (is (-> Nat (Maybe Text))
                                  (function (_ value)
                                    (if (n.even? value)
                                      {.#Some (# n.decimal encoded value)}
                                      {.#None})))]
                   (_.coverage [!.one]
                     (|> evens
                         (!.one choose)
                         (maybe#each (text#= (|> evens
                                                 (!.each (# n.decimal encoded))
                                                 (!.item 0))))
                         (maybe.else false))))
                 (_.coverage [!.example]
                   (# (maybe.equivalence n.equivalence) =
                      (!.example n.even? the_array)
                      (list.example n.even? (!.list {.#None} the_array))))
                 (_.coverage [!.example']
                   (case [(!.example n.even? the_array)
                          (!.example' (function (_ idx member)
                                        (n.even? member))
                                      the_array)]
                     [{.#Some expected} {.#Some [idx actual]}]
                     (and (not (!.lacks? idx the_array))
                          (n.= expected actual)
                          (n.= actual (!.item idx the_array)))

                     [{.#None} {.#None}]
                     true

                     _
                     false))
                 (_.coverage [!.every?]
                   (# bit.equivalence =
                      (list.every? n.even? (!.list {.#None} the_array))
                      (!.every? n.even? the_array)))
                 (_.coverage [!.any?]
                   (# bit.equivalence =
                      (list.any? n.even? (!.list {.#None} the_array))
                      (!.any? n.even? the_array)))
                 )))))

(def: .public test
  Test
  (<| (_.covering /._)
      (_.for [/.Array])
      (do [! random.monad]
        [size ..bounded_size
         base random.nat
         shift random.nat
         dummy (random.only (|>> (n.= base) not) random.nat)
         .let [expected (n.+ base shift)]
         the_array (random.array size random.nat)]
        (all _.and
             ..structures
             ..search

             (_.coverage [/.empty /.size]
               (n.= size (/.size (is (Array Nat)
                                     (/.empty size)))))
             (_.coverage [/.type_name]
               (case /.Array
                 (pattern (<| {.#Named (symbol /.Array)}
                              {.#Named (symbol !.Array)}
                              {.#UnivQ (list)}
                              {.#Primitive nominal_type (list {.#Parameter 1})}))
                 (same? /.type_name nominal_type)

                 _
                 false))
             (_.coverage [/.item /.has!]
               (let [the_array (|> (/.empty 2)
                                   (is (Array Nat))
                                   (/.has! 0 expected))]
                 (case [(/.item 0 the_array)
                        (/.item 1 the_array)]
                   [{.#Some actual} {.#None}]
                   (n.= expected actual)

                   _
                   false)))
             (_.coverage [/.lacks!]
               (let [the_array (|> (/.empty 1)
                                   (is (Array Nat))
                                   (/.has! 0 expected))]
                 (case [(/.item 0 the_array)
                        (/.item 0 (/.lacks! 0 the_array))]
                   [{.#Some actual} {.#None}]
                   (n.= expected actual)

                   _
                   false)))
             (_.coverage [/.lacks?]
               (let [the_array (|> (/.empty 2)
                                   (is (Array Nat))
                                   (/.has! 0 expected))]
                 (and (not (/.lacks? 0 the_array))
                      (/.lacks? 1 the_array))))
             (_.coverage [/.has?]
               (let [the_array (|> (/.empty 2)
                                   (is (Array Nat))
                                   (/.has! 0 expected))]
                 (and (/.has? 0 the_array)
                      (not (/.has? 1 the_array)))))
             (_.coverage [/.revised!]
               (let [the_array (|> (/.empty 1)
                                   (is (Array Nat))
                                   (/.has! 0 base)
                                   (/.revised! 0 (n.+ shift)))]
                 (case (/.item 0 the_array)
                   {.#Some actual}
                   (n.= expected actual)

                   _
                   false)))
             (_.coverage [/.upsert!]
               (let [the_array (|> (/.empty 2)
                                   (is (Array Nat))
                                   (/.has! 0 base)
                                   (/.upsert! 0 dummy (n.+ shift))
                                   (/.upsert! 1 base (n.+ shift)))]
                 (case [(/.item 0 the_array)
                        (/.item 1 the_array)]
                   [{.#Some actual/0} {.#Some actual/1}]
                   (and (n.= expected actual/0)
                        (n.= expected actual/1))

                   _
                   false)))
             (do !
               [occupancy (# ! each (n.% (++ size)) random.nat)]
               (_.coverage [/.occupancy /.vacancy]
                 (let [the_array (loop (again [output (is (Array Nat)
                                                          (/.empty size))
                                               idx 0])
                                   (if (n.< occupancy idx)
                                     (again (/.has! idx expected output)
                                            (++ idx))
                                     output))]
                   (and (n.= occupancy (/.occupancy the_array))
                        (n.= size (n.+ (/.occupancy the_array)
                                       (/.vacancy the_array)))))))
             (do !
               [the_list (random.list size random.nat)
                .let [the_array (/.clone the_array)
                      members (|> the_array (/.list {.#None}) (set.of_list n.hash))]
                default (random.only (function (_ value)
                                       (not (or (n.even? value)
                                                (set.member? members value))))
                                     random.nat)]
               (_.coverage [/.of_list /.list]
                 (and (|> the_list /.of_list (/.list {.#None})
                          (# (list.equivalence n.equivalence) = the_list))
                      (|> the_array (/.list {.#None}) /.of_list
                          (# (/.equivalence n.equivalence) = the_array))
                      (exec
                        (/.only! n.even? the_array)
                        (list.every? (function (_ value)
                                       (or (n.even? value)
                                           (same? default value)))
                                     (/.list {.#Some default} the_array))))))
             (do !
               [amount (# ! each (n.% (++ size)) random.nat)]
               (_.coverage [/.copy!]
                 (let [copy (is (Array Nat)
                                (/.empty size))]
                   (exec (/.copy! amount 0 the_array 0 copy)
                     (# (list.equivalence n.equivalence) =
                        (list.first amount (/.list {.#None} the_array))
                        (/.list {.#None} copy))))))
             (_.coverage [/.clone]
               (let [clone (/.clone the_array)]
                 (and (not (same? the_array clone))
                      (# (/.equivalence n.equivalence) = the_array clone))))
             (let [the_array (/.clone the_array)
                   evens (|> the_array (/.list {.#None}) (list.only n.even?))
                   odds (|> the_array (/.list {.#None}) (list.only n.odd?))]
               (_.coverage [/.only!]
                 (exec (/.only! n.even? the_array)
                   (and (n.= (list.size evens) (/.occupancy the_array))
                        (n.= (list.size odds) (/.vacancy the_array))
                        (|> the_array (/.list {.#None}) (# (list.equivalence n.equivalence) = evens))))))

             ..test|unsafe
             ))))