... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/.

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

(`` (the \\projection
      (List $.Documentation)
      (list ($.module \\projection._
                      (%.message "Parsing of Lux types."
                                 \n "Used mostly for polytypic programming."))

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

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

            ($.definition (\\projection.Projection it)
              "A projection of Lux types.")

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

            ($.definition \\projection.value
              (%.message "Applies a projection against a type."
                         \n "Verifies that the projection fully consumes the type's information.")
              ($.example (' (value poly type))))

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

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

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

            ($.definition \\projection.local
              "Apply a projection to the given inputs."
              ($.example (' (local types poly))))

            ($.definition \\projection.with_extension
              ""
              ($.example (' (with_extension type poly))))

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

                  [\\projection.variant]
                  [\\projection.tuple]
                  ))

            ($.definition \\projection.polymorphic
              ""
              ($.example (' (polymorphic poly))))

            ($.definition \\projection.function
              "Parses a function's inputs and output."
              ($.example (' (function in_poly out_poly))))

            ($.definition \\projection.applied
              "Parses a type application."
              ($.example (' (applied poly))))

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

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

            ($.definition \\projection.argument
              ""
              ($.example (' (argument env idx))))

            ($.definition \\projection.this_parameter
              ""
              ($.example (' (this_parameter id))))

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

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

            ($.definition \\projection.recursive
              ""
              ($.example (' (recursive poly))))
            )))

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

                    ($.definition /.equivalence)

                    (,, (template.with [<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."
                      ($.example (' (flat_function type))))

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

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

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

                    ($.definition /.absolute_injection
                      "A (readable) textual representable of a type."
                      ($.example (' (absolute_injection type))))

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

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

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

                    ($.definition /.anonymous
                      "A type without any names covering it."
                      ($.example (' (anonymous type))))

                    (,, (template.with [<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."
                      ($.example (' (function inputs output))))

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

                    (,, (template.with [<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."
                      ($.example (' (quantified? type))))

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

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

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

                    ($.definition /.log!
                      "Logs to the console/terminal the type of an expression."

                      ($.example (' (log! (is Foo (foo expression)))))
                      ($.comment "=>")
                      ($.comment "Expression: (foo expression)")
                      ($.comment "      Type: Foo")
                      ($.example (' (foo expression))))

                    ($.definition /.as
                      (%.message "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.")
                      ($.example (' (is (Bar Bit Natural Text)
                                        (as [a b c]
                                            (Foo a [b c])
                                            (Bar a b c)
                                            (is (Foo Bit [Natural Text])
                                                (foo expression)))))))

                    ($.definition /.sharing
                      "Allows specifing the type of an expression as sharing type-variables with the type of another expression."
                      ($.example (' (is (Bar Bit Natural Text)
                                        (sharing [a b c]
                                          (is (Foo a [b c])
                                              (is (Foo Bit [Natural 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."
                      
                      ($.example (' (is Type
                                        (by_example [a b c]
                                          (is (Foo a [b c])
                                              (is (Foo Bit [Natural Text])
                                                  (foo expression)))
                                          (Bar a b c)))))
                      ($.comment "=>")
                      ($.example (' (/.literal (Bar Bit Natural Text)))))

                    ($.definition /.let
                      "Local bindings for types."
                      ($.example (' (let [side (Either Integer Decimal)]
                                      (List [side side])))))

                    ... ($.definition /.literal
                    ...   "Takes a type expression and returns its representation as data-structure."
                    ...   ($.example (' (/.literal
                    ...                  (for_any (_ of)
                    ...                    (Maybe (List of)))))))

                    (all list#composite
                         ..\\projection

                         /nominal.documentation
                         /check.documentation
                         /dynamic.documentation
                         /implicit.documentation
                         /poly.documentation
                         /quotient.documentation
                         /refinement.documentation
                         /linear.documentation
                         /unit.documentation
                         /variance.documentation
                         )
                    )))
