(.module:
  [library
   [lux #*
    ["_" test (#+ Test)]
    [abstract
     ["." monad (#+ do)]
     ["." enum]
     [\\spec
      ["$." equivalence]
      ["$." monoid]]]
    [control
     ["." try (#+ Try)]
     ["." exception (#+ Exception)]]
    [data
     [collection
      ["." list]]]
    [math
     ["." random (#+ Random)]
     [number
      ["." i64]
      ["n" nat]]]]]
  [\\library
   ["." / (#+ Binary)]])

(def: (succeed result)
  (-> (Try Bit) Bit)
  (case result
    (#try.Failure _)
    false

    (#try.Success output)
    output))

(def: #export (random size)
  (-> Nat (Random Binary))
  (let [output (/.create size)]
    (loop [idx 0]
      (if (n.< size idx)
        (do random.monad
          [byte random.nat]
          (exec (try.assume (/.write/8 idx byte output))
            (recur (inc idx))))
        (\ random.monad wrap output)))))

(def: (throws? exception try)
  (All [e a] (-> (Exception e) (Try a) Bit))
  (case try
    (#try.Failure error)
    (exception.match? exception error)

    (#try.Success _)
    false))

(def: (binary_io power read write value)
  (-> Nat (-> Nat Binary (Try Nat)) (-> Nat Nat Binary (Try Any)) Nat Bit)
  (let [bytes (i64.left_shift power 1)
        binary (/.create bytes)
        cap (case bytes
              8 (dec 0)
              _ (|> 1 (i64.left_shift (n.* 8 bytes)) dec))
        capped_value (i64.and cap value)]
    (and (..succeed
          (do try.monad
            [pre (read 0 binary)
             _ (write 0 value binary)
             post (read 0 binary)]
            (wrap (and (n.= 0 pre)
                       (n.= capped_value post)))))
         (throws? /.index_out_of_bounds (read 1 binary))
         (throws? /.index_out_of_bounds (write 1 value binary)))))

(def: as_list
  (-> /.Binary (List Nat))
  (/.fold (function (_ head tail)
            (#.Cons head tail))
          (list)))

(def: #export test
  Test
  (<| (_.covering /._)
      (do {! random.monad}
        [#let [gen_size (|> random.nat (\ ! map (|>> (n.% 100) (n.max 8))))]
         size gen_size
         sample (..random size)
         value random.nat
         #let [gen_idx (|> random.nat (\ ! map (n.% size)))]
         offset gen_idx
         length (\ ! map (n.% (n.- offset size)) random.nat)]
        (_.for [/.Binary]
               ($_ _.and
                   (_.for [/.equivalence]
                          ($equivalence.spec /.equivalence (..random size)))
                   (_.for [/.monoid]
                          ($monoid.spec /.equivalence /.monoid (..random size)))
                   (_.cover [/.fold]
                            (n.= (\ list.fold fold n.+ 0 (..as_list sample))
                                 (/.fold n.+ 0 sample)))
                   
                   (_.cover [/.create]
                            (\ /.equivalence =
                               (/.create size)
                               (/.create size)))
                   (_.cover [/.size]
                            (|> (/.create size) /.size (n.= size)))
                   (_.for [/.index_out_of_bounds]
                          ($_ _.and
                              (_.cover [/.read/8 /.write/8]
                                       (..binary_io 0 /.read/8 /.write/8 value))
                              (_.cover [/.read/16 /.write/16]
                                       (..binary_io 1 /.read/16 /.write/16 value))
                              (_.cover [/.read/32 /.write/32]
                                       (..binary_io 2 /.read/32 /.write/32 value))
                              (_.cover [/.read/64 /.write/64]
                                       (..binary_io 3 /.read/64 /.write/64 value))))
                   (_.cover [/.slice]
                            (let [random_slice (try.assume (/.slice offset length sample))
                                  idxs (: (List Nat)
                                          (case length
                                            0 (list)
                                            _ (enum.range n.enum 0 (dec length))))
                                  reader (function (_ binary idx)
                                           (/.read/8 idx binary))]
                              (and (n.= length (/.size random_slice))
                                   (case [(monad.map try.monad (|>> (n.+ offset) (reader sample)) idxs)
                                          (monad.map try.monad (reader random_slice) idxs)]
                                     [(#try.Success binary_vals) (#try.Success slice_vals)]
                                     (\ (list.equivalence n.equivalence) = binary_vals slice_vals)

                                     _
                                     #0))))
                   (_.cover [/.slice_out_of_bounds]
                            (and (throws? /.slice_out_of_bounds (/.slice size size sample))
                                 (let [verdict (throws? /.slice_out_of_bounds (/.slice offset size sample))]
                                   (case offset
                                     0 (not verdict)
                                     _ verdict))))
                   (_.cover [/.drop]
                            (and (\ /.equivalence = sample (/.drop 0 sample))
                                 (\ /.equivalence = (/.create 0) (/.drop size sample))
                                 (case (list.reverse (..as_list sample))
                                   #.Nil
                                   false

                                   (#.Cons head tail)
                                   (n.= (list.fold n.+ 0 tail)
                                        (/.fold n.+ 0 (/.drop 1 sample))))))
                   (_.cover [/.copy]
                            (and (case (/.copy size 0 sample 0 (/.create size))
                                   (#try.Success output)
                                   (and (not (is? sample output))
                                        (\ /.equivalence = sample output))

                                   (#try.Failure _)
                                   false)
                                 (succeed
                                  (do try.monad
                                    [sample/0 (/.read/8 0 sample)
                                     copy (/.copy 1 0 sample 0 (/.create 2))
                                     copy/0 (/.read/8 0 copy)
                                     copy/1 (/.read/8 1 copy)]
                                    (wrap (and (n.= sample/0 copy/0)
                                               (n.= 0 copy/1)))))))
                   )))))