(.require
 [lux (.except)
  ["_" test (.only Test)]
  ["[0]" ffi (.only import)]
  [abstract
   [monad (.only do)]]
  [control
   ["[0]" pipe]
   ["[0]" maybe]
   ["[0]" try]]
  [data
   [number
    ["n" nat]
    ["i" int]]
   ["[0]" text (.use "[1]#[0]" equivalence)
    ["%" \\format (.only format)]]
   [collection
    ["[0]" array (.only Array)]
    ["[0]" list (.use "[1]#[0]" functor)]]]
  [math
   ["r" random]]
  [meta
   [compiler
    ["[0]" analysis]
    ["[0]" synthesis]]]]
 [///
  [common (.only Runner)]])

(import java/lang/Integer)

(def (variant run)
  (-> Runner Test)
  (do [! r.monad]
    [num_tags (|> r.nat (at ! each (|>> (n.% 10) (n.max 2))))
     tag_in (|> r.nat (at ! each (n.% num_tags)))
     .let [last?_in (|> num_tags -- (n.= tag_in))]
     value_in r.i64]
    (_.property (%.symbol (symbol synthesis.variant))
      (|> (synthesis.variant [analysis.#lefts (if last?_in
                                                (-- tag_in)
                                                tag_in)
                              analysis.#right? last?_in
                              analysis.#value (synthesis.i64 value_in)])
          (run "variant")
          (pipe.case
            {try.#Success valueT}
            (let [valueT (as (Array Any) valueT)]
              (and (n.= 3 (array.size valueT))
                   (let [tag_out (as java/lang/Integer (maybe.trusted (array.read! 0 valueT)))
                         last?_out (array.read! 1 valueT)
                         value_out (as Any (maybe.trusted (array.read! 2 valueT)))
                         same_tag? (|> tag_out ffi.int_to_long (as Nat) (n.= tag_in))
                         same_flag? (case last?_out
                                      {.#Some last?_out'}
                                      (and last?_in (text#= "" (as Text last?_out')))

                                      {.#None}
                                      (not last?_in))
                         same_value? (|> value_out (as Int) (i.= value_in))]
                     (and same_tag?
                          same_flag?
                          same_value?))))

            {try.#Failure _}
            false)))))

(def (tuple run)
  (-> Runner Test)
  (do [! r.monad]
    [size (|> r.nat (at ! each (|>> (n.% 10) (n.max 2))))
     tuple_in (r.list size r.i64)]
    (_.property (%.symbol (symbol synthesis.tuple))
      (|> (synthesis.tuple (list#each (|>> synthesis.i64) tuple_in))
          (run "tuple")
          (pipe.case
            {try.#Success tuple_out}
            (let [tuple_out (as (Array Any) tuple_out)]
              (and (n.= size (array.size tuple_out))
                   (list.every? (function (_ [left right])
                                  (i.= left (as Int right)))
                                (list.zipped_2 tuple_in (array.list tuple_out)))))

            {try.#Failure _}
            false)))))

(def .public (spec runner)
  (-> Runner Test)
  (all _.and
       (..variant runner)
       (..tuple runner)
       ))