(.require
 [library
  [lux (.except)
   ["$" documentation]
   [data
    ["[0]" text (.only \n)
     ["%" \\format (.only format)]]
    [collection
     ["[0]" list (.use "[1]#[0]" monoid)]]]
   [meta
    [macro
     ["[0]" template]]]]]
 ["[0]" \\parser]
 [\\library
  ["[0]" /]]
 ["[0]" /
  ["[1][0]" primitive]
  ["[1][0]" check]
  ["[1][0]" dynamic]
  ["[1][0]" implicit]
  ["[1][0]" poly]
  ["[1][0]" quotient]
  ["[1][0]" refinement]
  ["[1][0]" resource]
  ["[1][0]" unit]
  ["[1][0]" variance]])

(`` (def \\parser
      (List $.Documentation)
      (list ($.module \\parser._
                      (format "Parsing of Lux types."
                              \n "Used mostly for polytypic programming."))

            ($.definition \\parser.not_existential)
            ($.definition \\parser.not_recursive)
            ($.definition \\parser.not_named)
            ($.definition \\parser.not_parameter)
            ($.definition \\parser.unknown_parameter)
            ($.definition \\parser.not_function)
            ($.definition \\parser.not_application)
            ($.definition \\parser.not_polymorphic)
            ($.definition \\parser.not_variant)
            ($.definition \\parser.not_tuple)
            ($.definition \\parser.types_do_not_match)
            ($.definition \\parser.wrong_parameter)
            ($.definition \\parser.empty_input)
            ($.definition \\parser.unconsumed_input)
            ($.definition \\parser.parameter)
            ($.definition \\parser.recursive_self)
            ($.definition \\parser.recursive_call)

            ($.definition \\parser.Env
              "An environment for type parsing.")

            ($.definition (\\parser.Parser it)
              "A parser of Lux types.")

            ($.definition \\parser.fresh
              "An empty parsing environment.")

            ($.definition \\parser.result
              (format "Applies a parser against a type."
                      \n "Verifies that the parser fully consumes the type's information.")
              [(result poly type)])

            ($.definition \\parser.env
              "Yields the current parsing environment.")

            ($.definition \\parser.next
              "Inspect a type in the input stream without consuming it.")

            ($.definition \\parser.any
              "Yields a type, without examination.")

            ($.definition \\parser.local
              "Apply a parser to the given inputs."
              [(local types poly)])

            ($.definition \\parser.with_extension
              ""
              [(with_extension type poly)])

            (,, (with_template [<name>]
                  [(`` ($.definition <name>
                         (format "Parses the contents of a " (,, (template.text [<name>])) " type.")))]

                  [\\parser.variant]
                  [\\parser.tuple]
                  ))

            ($.definition \\parser.polymorphic
              ""
              [(polymorphic poly)])

            ($.definition \\parser.function
              "Parses a function's inputs and output."
              [(function in_poly out_poly)])

            ($.definition \\parser.applied
              "Parses a type application."
              [(applied poly)])

            (,, (with_template [<name> <doc>]
                  [($.definition <name>
                     <doc>)]

                  [\\parser.exactly "Parses a type exactly."]
                  [\\parser.sub "Parses a sub type."]
                  [\\parser.super "Parses a super type."]
                  ))

            ($.definition \\parser.argument
              ""
              [(argument env idx)])

            ($.definition \\parser.this_parameter
              ""
              [(this_parameter id)])

            ($.definition \\parser.existential
              "Yields an existential type.")

            ($.definition \\parser.named
              "Yields a named type.")

            ($.definition \\parser.recursive
              ""
              [(recursive poly)])
            )))

(`` (def .public documentation
      (List $.Documentation)
      (list.partial ($.module /._
                              "Basic functionality for working with types.")

                    ($.definition /.equivalence)

                    (,, (with_template [<name>]
                          [($.definition <name>
                             "The number of parameters, and the body, of a quantified type.")]

                          [/.flat_univ_q]
                          [/.flat_ex_q]
                          ))

                    ($.definition /.flat_function
                      "The input, and the output of a function type."
                      [(flat_function type)])

                    ($.definition /.flat_application
                      "The quantified type, and its parameters, for a type-application."
                      [(flat_application type)])

                    (,, (with_template [<name>]
                          [($.definition <name>
                             "The members of a composite type.")]

                          [/.flat_variant]
                          [/.flat_tuple]
                          ))

                    ($.definition /.format
                      "A (readable) textual representable of a type."
                      [(format type)])

                    ($.definition /.applied
                      "To the extend possible, applies a quantified type to the given parameters."
                      [(applied params func)])

                    ($.definition /.code
                      (%.format "A representation of a type as code."
                                \n "The code is such that evaluating it would yield the type value.")
                      [(code type)])

                    ($.definition /.de_aliased
                      "A (potentially named) type that does not have its name shadowed by other names."
                      [(de_aliased type)])

                    ($.definition /.anonymous
                      "A type without any names covering it."
                      [(anonymous type)])

                    (,, (with_template [<name>]
                          [($.definition <name>
                             "A composite type, constituted by the given member types.")]

                          [/.variant]
                          [/.tuple]
                          ))

                    ($.definition /.function
                      "A function type, with the given inputs and output."
                      [(function inputs output)])

                    ($.definition /.application
                      "An un-evaluated type application, with the given quantified type, and parameters."
                      [(application params quant)])

                    (,, (with_template [<name>]
                          [($.definition <name>
                             "A quantified type, with the given number of parameters, and body.")]

                          [/.univ_q]
                          [/.ex_q]
                          ))

                    ($.definition /.quantified?
                      "Only yields #1 for universally or existentially quantified types."
                      [(quantified? type)])

                    ($.definition /.array
                      "An array type, with the given level of nesting/depth, and the given element type."
                      [(array depth element_type)])

                    ($.definition /.flat_array
                      "The level of nesting/depth and element type for an array type."
                      [(flat_array type)])

                    ($.definition /.array?
                      "Is a type an array type?")

                    ($.definition /.log!
                      "Logs to the console/terminal the type of an expression."
                      [(log! (is Foo (foo expression)))
                       "=>"
                       "Expression: (foo expression)"
                       "      Type: Foo"
                       (foo expression)])

                    ($.definition /.as
                      (%.format "Casts a value to a specific type."
                                \n "The specified type can depend on type variables of the original type of the value."
                                \n "NOTE: Careless use of type-casts is an easy way to introduce bugs. USE WITH CAUTION.")
                      [(is (Bar Bit Nat Text)
                           (as [a b c]
                               (Foo a [b c])
                               (Bar a b c)
                               (is (Foo Bit [Nat Text])
                                   (foo expression))))])

                    ($.definition /.sharing
                      "Allows specifing the type of an expression as sharing type-variables with the type of another expression."
                      [(is (Bar Bit Nat Text)
                           (sharing [a b c]
                             (is (Foo a [b c])
                                 (is (Foo Bit [Nat Text])
                                     (foo expression)))
                             (is (Bar a b c)
                                 (bar expression))))])

                    ($.definition /.by_example
                      "Constructs a type that shares type-variables with an expression of some other type."
                      [(is Type
                           (by_example [a b c]
                             (is (Foo a [b c])
                                 (is (Foo Bit [Nat Text])
                                     (foo expression)))
                             (Bar a b c)))
                       "=>"
                       (.type_literal (Bar Bit Nat Text))])

                    ($.definition /.let
                      "Local bindings for types."
                      [(let [side (Either Int Frac)]
                         (List [side side]))])

                    (all list#composite
                         ..\\parser

                         /primitive.documentation
                         /check.documentation
                         /dynamic.documentation
                         /implicit.documentation
                         /poly.documentation
                         /quotient.documentation
                         /refinement.documentation
                         /resource.documentation
                         /unit.documentation
                         /variance.documentation
                         )
                    )))
