(.module:
  [lux #*
   [control
    [monad (#+ do)]
    pipe]
   [data
    ["." error]
    ["." maybe]
    ["." product]
    ["." text ("#/." equivalence)
     format]
    [collection
     ["." list ("#/." functor)]]]
   [math
    ["r" random]]
   ["." type]
   ["." macro
    ["." code]]
   [compiler
    [default
     ["." reference]
     ["." init]
     ["." phase
      ["." analysis (#+ Analysis Operation)
       [".A" type]
       ["." expression]
       ["/" function]]
      [extension
       [".E" analysis]]]]]
   test]
  [//
   ["_." primitive]
   ["_." structure]])

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

             (#error.Failure error)
             #0)))

(context: "Function definition."
  (<| (times 100)
      (do @
        [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)]]
        ($_ seq
            (test "Can analyse function."
                  (and (|> (typeA.with-type (All [a] (-> a outputT))
                             (/.function _primitive.phase func-name arg-name outputC))
                           _structure.check-succeeds)
                       (|> (typeA.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 (|> (typeA.with-type (-> inputT outputT)
                             (/.function _primitive.phase func-name arg-name outputC))
                           _structure.check-succeeds)
                       (|> (typeA.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."
                  (|> (typeA.with-type (Rec self (-> inputT self))
                        (/.function _primitive.phase func-name arg-name (code.local-identifier func-name)))
                      _structure.check-succeeds))
            ))))

(context: "Function application."
  (<| (times 100)
      (do @
        [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)))]]
        ($_ seq
            (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)))
            ))))