(.module:
  [lux #*
   [abstract ["." monad (#+ do)]]
   [data
    ["%" text/format (#+ format)]
    ["." name ("#@." equivalence)]]
   ["r" math/random (#+ Random) ("#@." monad)]
   ["_" test (#+ Test)]
   [control
    pipe]
   [data
    ["." error]
    ["." maybe]
    ["." product]
    ["." text ("#@." equivalence)]
    [collection
     ["." list ("#@." functor)]]]
   ["." type]
   ["." macro
    ["." code]]]
  [//
   ["_." primitive]
   ["_." structure]]
  {1
   ["." /
    ["/#" //
     ["#." module]
     ["#." type]
     ["/#" //
      ["/#" //
       ["#." reference]
       ["#." analysis (#+ Analysis Operation)]]]]]})

(def: (check-apply expectedT num-args analysis)
  (-> Type Nat (Operation Analysis) Bit)
  (|> analysis
      (//type.with-type expectedT)
      (///.run _primitive.state)
      (case> (#error.Success applyA)
             (let [[funcA argsA] (////analysis.application applyA)]
               (n/= num-args (list.size argsA)))

             (#error.Failure error)
             false)))

(def: abstraction
  (do r.monad
    [func-name (r.unicode 5)
     arg-name (|> (r.unicode 5) (r.filter (|>> (text@= func-name) not)))
     [outputT outputC] _primitive.primitive
     [inputT _] _primitive.primitive
     #let [g!arg (code.local-identifier arg-name)]]
    (<| (_.context (%.name (name-of /.function)))
        ($_ _.and
            (_.test "Can analyse function."
                    (and (|> (//type.with-type (All [a] (-> a outputT))
                               (/.function _primitive.phase func-name arg-name outputC))
                             _structure.check-succeeds)
                         (|> (//type.with-type (All [a] (-> a a))
                               (/.function _primitive.phase func-name arg-name g!arg))
                             _structure.check-succeeds)))
            (_.test "Generic functions can always be specialized."
                    (and (|> (//type.with-type (-> inputT outputT)
                               (/.function _primitive.phase func-name arg-name outputC))
                             _structure.check-succeeds)
                         (|> (//type.with-type (-> inputT inputT)
                               (/.function _primitive.phase func-name arg-name g!arg))
                             _structure.check-succeeds)))
            (_.test "The function's name is bound to the function's type."
                    (|> (//type.with-type (Rec self (-> inputT self))
                          (/.function _primitive.phase func-name arg-name (code.local-identifier func-name)))
                        _structure.check-succeeds))
            ))))

(def: apply
  (do r.monad
    [full-args (|> r.nat (:: @ map (|>> (n/% 10) (n/max 2))))
     partial-args (|> r.nat (:: @ map (n/% full-args)))
     var-idx (|> r.nat (:: @ map (|>> (n/% full-args) (n/max 1))))
     inputsTC (r.list full-args _primitive.primitive)
     #let [inputsT (list@map product.left inputsTC)
           inputsC (list@map product.right inputsTC)]
     [outputT outputC] _primitive.primitive
     #let [funcT (type.function inputsT outputT)
           partialT (type.function (list.drop partial-args inputsT) outputT)
           varT (#.Parameter 1)
           polyT (<| (type.univ-q 1)
                     (type.function (list.concat (list (list.take var-idx inputsT)
                                                       (list varT)
                                                       (list.drop (inc var-idx) inputsT))))
                     varT)
           poly-inputT (maybe.assume (list.nth var-idx inputsT))
           partial-poly-inputsT (list.drop (inc var-idx) inputsT)
           partial-polyT1 (<| (type.function partial-poly-inputsT)
                              poly-inputT)
           partial-polyT2 (<| (type.univ-q 1)
                              (type.function (#.Cons varT partial-poly-inputsT))
                              varT)
           dummy-function (#////analysis.Function (list) (#////analysis.Reference (////reference.local 1)))]]
    (<| (_.context (%.name (name-of /.apply)))
        ($_ _.and
            (_.test "Can analyse monomorphic type application."
                    (|> (/.apply _primitive.phase funcT dummy-function (' []) inputsC)
                        (check-apply outputT full-args)))
            (_.test "Can partially apply functions."
                    (|> (/.apply _primitive.phase funcT dummy-function (' []) (list.take partial-args inputsC))
                        (check-apply partialT partial-args)))
            (_.test "Can apply polymorphic functions."
                    (|> (/.apply _primitive.phase polyT dummy-function (' []) inputsC)
                        (check-apply poly-inputT full-args)))
            (_.test "Polymorphic partial application propagates found type-vars."
                    (|> (/.apply _primitive.phase polyT dummy-function (' []) (list.take (inc var-idx) inputsC))
                        (check-apply partial-polyT1 (inc var-idx))))
            (_.test "Polymorphic partial application preserves quantification for type-vars."
                    (|> (/.apply _primitive.phase polyT dummy-function (' []) (list.take var-idx inputsC))
                        (check-apply partial-polyT2 var-idx)))
            ))))

(def: #export test
  Test
  (<| (_.context (name.module (name-of /._)))
      ($_ _.and
          ..abstraction
          ..apply
          )))