(.module:
  [lux (#- type)
   ["%" data/text/format (#+ format)]
   ["_" test (#+ Test)]
   [abstract
    ["." monad (#+ do)]]
   [control
    pipe]
   [data
    ["." maybe]
    [collection
     ["." list]]]
   [math
    ["." random (#+ Random)]
    [number
     ["n" nat]]]]
  {1
   ["." / ("#\." equivalence)]}
  ["." / #_
   ["#." abstract]
   ["#." check]
   ["#." dynamic]
   ["#." implicit]
   ["#." quotient]
   ["#." refinement]
   ["#." resource]])

(def: short
  (Random Text)
  (do {! random.monad}
    [size (|> random.nat (\ ! map (n.% 10)))]
    (random.unicode size)))

(def: name
  (Random Name)
  (random.and ..short ..short))

(def: #export random
  (Random Type)
  (let [(^open "R\.") random.monad]
    (random.rec (function (_ recur)
                  (let [pairG (random.and recur recur)
                        idG random.nat
                        quantifiedG (random.and (R\wrap (list)) recur)]
                    ($_ random.or
                        (random.and ..short (R\wrap (list)))
                        pairG
                        pairG
                        pairG
                        idG
                        idG
                        idG
                        quantifiedG
                        quantifiedG
                        pairG
                        (random.and ..name recur)
                        ))))))

(def: #export test
  Test
  (<| (_.context (%.name (name_of /._)))
      ($_ _.and
          (do random.monad
            [sample ..random]
            (_.test "Every type is equal to itself."
                    (\ /.equivalence = sample sample)))
          (_.test "Can apply quantified types (universal and existential quantification)."
                  (and (maybe.default #0
                                      (do maybe.monad
                                        [partial (/.apply (list Bit) Ann)
                                         full (/.apply (list Int) partial)]
                                        (wrap (\ /.equivalence = full (#.Product Bit Int)))))
                       (|> (/.apply (list Bit) Text)
                           (case> #.None #1 _ #0))))
          (let [base (#.Named ["" "a"] (#.Product Bit Int))
                aliased (#.Named ["" "c"]
                                 (#.Named ["" "b"]
                                          base))]
            ($_ _.and
                (_.test "Can remove aliases from an already-named type."
                        (\ /.equivalence =
                           base
                           (/.un_alias aliased)))
                (_.test "Can remove all names from a type."
                        (and (not (\ /.equivalence =
                                     base
                                     (/.un_name aliased)))
                             (\ /.equivalence =
                                (/.un_name base)
                                (/.un_name aliased))))))
          (do {! random.monad}
            [size (|> random.nat (\ ! map (n.% 3)))
             members (|> ..random
                         (random.filter (function (_ type)
                                          (case type
                                            (^or (#.Sum _) (#.Product _))
                                            #0

                                            _
                                            #1)))
                         (list.repeat size)
                         (monad.seq !))
             #let [(^open "/\.") /.equivalence
                   (^open "list\.") (list.equivalence /.equivalence)]]
            (`` ($_ _.and
                    (~~ (template [<desc> <ctor> <dtor> <unit>]
                          [(_.test (format "Can build and tear-down " <desc> " types.")
                                   (let [flat (|> members <ctor> <dtor>)]
                                     (or (list\= members flat)
                                         (and (list\= (list) members)
                                              (list\= (list <unit>) flat)))))]

                          ["variant" /.variant /.flatten_variant Nothing]
                          ["tuple"   /.tuple   /.flatten_tuple   Any]
                          ))
                    )))
          (do {! random.monad}
            [size (|> random.nat (\ ! map (n.% 3)))
             members (monad.seq ! (list.repeat size ..random))
             extra (|> ..random
                       (random.filter (function (_ type)
                                        (case type
                                          (^or (#.Function _) (#.Apply _))
                                          #0

                                          _
                                          #1))))
             #let [(^open "/\.") /.equivalence
                   (^open "list\.") (list.equivalence /.equivalence)]]
            ($_ _.and
                (_.test "Can build and tear-down function types."
                        (let [[inputs output] (|> (/.function members extra) /.flatten_function)]
                          (and (list\= members inputs)
                               (/\= extra output))))

                (_.test "Can build and tear-down application types."
                        (let [[tfunc tparams] (|> extra (/.application members) /.flatten_application)]
                          (n.= (list.size members) (list.size tparams))))
                ))
          (do {! random.monad}
            [size (|> random.nat (\ ! map (n.% 3)))
             extra (|> ..random
                       (random.filter (function (_ type)
                                        (case type
                                          (^or (#.UnivQ _) (#.ExQ _))
                                          #0

                                          _
                                          #1))))
             #let [(^open "/\.") /.equivalence]]
            (`` ($_ _.and
                    (~~ (template [<desc> <ctor> <dtor>]
                          [(_.test (format "Can build and tear-down " <desc> " types.")
                                   (let [[flat_size flat_body] (|> extra (<ctor> size) <dtor>)]
                                     (and (n.= size flat_size)
                                          (/\= extra flat_body))))]

                          ["universally-quantified"   /.univ_q /.flatten_univ_q]
                          ["existentially-quantified" /.ex_q   /.flatten_ex_q]
                          ))
                    )))
          (_.test (%.name (name_of /.:by_example))
                  (let [example (: (Maybe Nat)
                                   #.None)]
                    (/\= (.type (List Nat))
                         (/.:by_example [a]
                                        {(Maybe a) example}
                                        (List a)))))

          /abstract.test
          /check.test
          /dynamic.test
          /implicit.test
          /quotient.test
          /refinement.test
          /resource.test
          )))