(.using
 [library
  [lux {"-" function local parameter}
   [abstract
    ["[0]" monad {"+" do}]]
   [control
    ["[0]" try {"+" Try}]
    ["[0]" exception {"+" exception:}]
    ["[0]" function]]
   [data
    ["[0]" text ("[1]#[0]" monoid)
     ["%" format {"+" format}]]
    [collection
     ["[0]" list ("[1]#[0]" functor)]
     ["[0]" dictionary {"+" Dictionary}]]]
   [macro
    ["^" pattern]
    ["[0]" code]]
   [math
    [number
     ["n" nat ("[1]#[0]" decimal)]]]
   ["[0]" type ("[1]#[0]" equivalence)
    ["[0]" check]]]]
 ["[0]" //])

(template: (|recursion_dummy|)
  [{.#Primitive "" {.#End}}])

(template [<name>]
  [(exception: .public (<name> [type Type])
     (exception.report
      "Type" (%.type type)))]

  [not_existential]
  [not_recursive]
  [not_named]
  [not_parameter]
  [unknown_parameter]
  [not_function]
  [not_application]
  [not_polymorphic]
  [not_variant]
  [not_tuple]
  )

(template [<name>]
  [(exception: .public (<name> [expected Type
                                actual Type])
     (exception.report
      "Expected" (%.type expected)
      "Actual" (%.type actual)))]

  [types_do_not_match]
  [wrong_parameter]
  )

(exception: .public empty_input)

(exception: .public (unconsumed_input [remaining (List Type)])
  (exception.report
   "Types" (|> remaining
               (list#each (|>> %.type (format text.new_line "* ")))
               (text.interposed ""))))

(type: .public Env
  (Dictionary Nat [Type Code]))

(type: .public (Parser a)
  (//.Parser [Env (List Type)] a))

(def: .public fresh
  Env
  (dictionary.empty n.hash))

(def: (result' env poly types)
  (All (_ a) (-> Env (Parser a) (List Type) (Try a)))
  (case (//.result poly [env types])
    {try.#Failure error}
    {try.#Failure error}

    {try.#Success [[env' remaining] output]}
    (case remaining
      {.#End}
      {try.#Success output}

      _
      (exception.except ..unconsumed_input remaining))))

(def: .public (result poly type)
  (All (_ a) (-> (Parser a) Type (Try a)))
  (result' ..fresh poly (list type)))

(def: .public env
  (Parser Env)
  (.function (_ [env inputs])
    {try.#Success [[env inputs] env]}))

(def: (with_env temp poly)
  (All (_ a) (-> Env (Parser a) (Parser a)))
  (.function (_ [env inputs])
    (case (//.result poly [temp inputs])
      {try.#Failure error}
      {try.#Failure error}

      {try.#Success [[_ remaining] output]}
      {try.#Success [[env remaining] output]})))

(def: .public next
  (Parser Type)
  (.function (_ [env inputs])
    (case inputs
      {.#End}
      (exception.except ..empty_input [])

      {.#Item headT tail}
      {try.#Success [[env inputs] headT]})))

(def: .public any
  (Parser Type)
  (.function (_ [env inputs])
    (case inputs
      {.#End}
      (exception.except ..empty_input [])

      {.#Item headT tail}
      {try.#Success [[env tail] headT]})))

(def: .public (local types poly)
  (All (_ a) (-> (List Type) (Parser a) (Parser a)))
  (.function (_ [env pass_through])
    (case (result' env poly types)
      {try.#Failure error}
      {try.#Failure error}

      {try.#Success output}
      {try.#Success [[env pass_through] output]})))

(def: (label idx)
  (-> Nat Code)
  (code.local ($_ text#composite "label" text.tab (n#encoded idx))))

(def: .public (with_extension type poly)
  (All (_ a) (-> Type (Parser a) (Parser [Code a])))
  (.function (_ [env inputs])
    (let [current_id (dictionary.size env)
          g!var (label current_id)]
      (case (//.result poly
                       [(dictionary.has current_id [type g!var] env)
                        inputs])
        {try.#Failure error}
        {try.#Failure error}

        {try.#Success [[_ inputs'] output]}
        {try.#Success [[env inputs'] [g!var output]]}))))

(template [<name> <flattener> <exception>]
  [(`` (def: .public (<name> poly)
         (All (_ a) (-> (Parser a) (Parser a)))
         (do //.monad
           [headT ..any]
           (let [members (<flattener> (type.anonymous headT))]
             (if (n.> 1 (list.size members))
               (local members poly)
               (//.failure (exception.error <exception> headT)))))))]

  [variant type.flat_variant ..not_variant]
  [tuple   type.flat_tuple   ..not_tuple]
  )

(def: polymorphic'
  (Parser [Nat Type])
  (do //.monad
    [headT any
     .let [[num_arg bodyT] (type.flat_univ_q (type.anonymous headT))]]
    (if (n.= 0 num_arg)
      (//.failure (exception.error ..not_polymorphic headT))
      (in [num_arg bodyT]))))

(def: .public (polymorphic poly)
  (All (_ a) (-> (Parser a) (Parser [Code (List Code) a])))
  (do [! //.monad]
    [headT any
     funcI (# ! each dictionary.size ..env)
     [num_args non_poly] (local (list headT) ..polymorphic')
     env ..env
     .let [funcL (label funcI)
           [all_varsL env'] (loop (again [current_arg 0
                                          env' env
                                          all_varsL (is (List Code) (list))])
                              (if (n.< num_args current_arg)
                                (if (n.= 0 current_arg)
                                  (let [varL (label (++ funcI))]
                                    (again (++ current_arg)
                                           (|> env'
                                               (dictionary.has funcI [headT funcL])
                                               (dictionary.has (++ funcI) [{.#Parameter (++ funcI)} varL]))
                                           {.#Item varL all_varsL}))
                                  (let [partialI (|> current_arg (n.* 2) (n.+ funcI))
                                        partial_varI (++ partialI)
                                        partial_varL (label partial_varI)
                                        partialC (` ((~ funcL) (~+ (|> (list.indices num_args)
                                                                       (list#each (|>> (n.* 2) ++ (n.+ funcI) label))
                                                                       list.reversed))))]
                                    (again (++ current_arg)
                                           (|> env'
                                               (dictionary.has partialI [(|recursion_dummy|) partialC])
                                               (dictionary.has partial_varI [{.#Parameter partial_varI} partial_varL]))
                                           {.#Item partial_varL all_varsL})))
                                [all_varsL env']))]]
    (<| (with_env env')
        (local (list non_poly))
        (do !
          [output poly]
          (in [funcL all_varsL output])))))

(def: .public (function in_poly out_poly)
  (All (_ i o) (-> (Parser i) (Parser o) (Parser [i o])))
  (do //.monad
    [headT any
     .let [[inputsT outputT] (type.flat_function (type.anonymous headT))]]
    (if (n.> 0 (list.size inputsT))
      (//.and (local inputsT in_poly)
              (local (list outputT) out_poly))
      (//.failure (exception.error ..not_function headT)))))

(def: .public (applied poly)
  (All (_ a) (-> (Parser a) (Parser a)))
  (do //.monad
    [headT any
     .let [[funcT paramsT] (type.flat_application (type.anonymous headT))]]
    (if (n.= 0 (list.size paramsT))
      (//.failure (exception.error ..not_application headT))
      (..local {.#Item funcT paramsT} poly))))

(template [<name> <test>]
  [(def: .public (<name> expected)
     (-> Type (Parser Any))
     (do //.monad
       [actual any]
       (if (<test> expected actual)
         (in [])
         (//.failure (exception.error ..types_do_not_match [expected actual])))))]

  [exactly type#=]
  [sub     check.subsumes?]
  [super   (function.flipped check.subsumes?)]
  )

(def: .public (argument env idx)
  (-> Env Nat Nat)
  (let [env_level (n./ 2 (dictionary.size env))
        parameter_level (n./ 2 idx)
        parameter_idx (n.% 2 idx)]
    (|> env_level -- (n.- parameter_level) (n.* 2) (n.+ parameter_idx))))

(def: .public parameter
  (Parser Code)
  (do //.monad
    [env ..env
     headT any]
    (case headT
      {.#Parameter idx}
      (case (dictionary.value (..argument env idx) env)
        {.#Some [poly_type poly_code]}
        (in poly_code)

        {.#None}
        (//.failure (exception.error ..unknown_parameter headT)))

      _
      (//.failure (exception.error ..not_parameter headT)))))

(def: .public (this_parameter id)
  (-> Nat (Parser Any))
  (do //.monad
    [env ..env
     headT any]
    (case headT
      {.#Parameter idx}
      (if (n.= id (..argument env idx))
        (in [])
        (//.failure (exception.error ..wrong_parameter [{.#Parameter id} headT])))

      _
      (//.failure (exception.error ..not_parameter headT)))))

(def: .public existential
  (Parser Nat)
  (do //.monad
    [headT any]
    (case headT
      {.#Ex ex_id}
      (in ex_id)

      _
      (//.failure (exception.error ..not_existential headT)))))

(def: .public named
  (Parser [Symbol Type])
  (do //.monad
    [inputT any]
    (case inputT
      {.#Named name anonymousT}
      (in [name anonymousT])

      _
      (//.failure (exception.error ..not_named inputT)))))

(def: .public (recursive poly)
  (All (_ a) (-> (Parser a) (Parser [Code a])))
  (do [! //.monad]
    [headT any]
    (case (type.anonymous headT)
      (pattern {.#Apply (|recursion_dummy|) {.#UnivQ _ headT'}})
      (do !
        [[recT _ output] (|> poly
                             (with_extension (|recursion_dummy|))
                             (with_extension headT)
                             (local (list headT')))]
        (in [recT output]))

      _
      (//.failure (exception.error ..not_recursive headT)))))

(def: .public recursive_self
  (Parser Code)
  (do //.monad
    [env ..env
     headT any]
    (case (type.anonymous headT)
      (^.multi (pattern {.#Apply (|recursion_dummy|) {.#Parameter funcT_idx}})
               (n.= 0 (..argument env funcT_idx))
               [(dictionary.value 0 env) {.#Some [self_type self_call]}])
      (in self_call)

      _
      (//.failure (exception.error ..not_recursive headT)))))

(def: .public recursive_call
  (Parser Code)
  (do [! //.monad]
    [env ..env
     [funcT argsT] (..applied (//.and any (//.many any)))
     _ (local (list funcT) (..this_parameter 0))
     allC (let [allT (partial_list funcT argsT)]
            (|> allT
                (monad.each ! (function.constant ..parameter))
                (local allT)))]
    (in (` ((~+ allC))))))