... 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
   [program (.only program)]
   ["$" documentation]
   ["[0]" debug]
   [control
    ["[0]" io]]
   [data
    ["[0]" text (.only \n)
     ["%" \\format (.only format)]]
    [collection
     ["[0]" list (.use "[1]#[0]" monoid)]
     ["[0]" set]]]]]
 [\\library
  ["[0]" / (.except)]]
 ["[0]" /
  ["[1][0]" abstract]
  ["[1][0]" control]
  ["[1][0]" data]
  ["[1][0]" debug]
  ["[1][0]" documentation]
  ["[1][0]" ffi]
  ["[1][0]" math]
  ["[1][0]" meta]
  ["[1][0]" program]
  ["[1][0]" test]
  ["[1][0]" world]])

(def all_1/4
  (List $.Documentation)
  (list ($.definition /.prelude
          (format "The name of the prelude module."
                  \n "Value: " (%.text /.prelude)))

        ($.definition /.Any
          (format "The type of things whose type is irrelevant."
                  \n "It can be used to write functions or data-structures that can take, or return, anything."))

        ($.definition /.Nothing
          (format "The type of things whose type is undefined."
                  \n "Useful for expressions that cause errors or other 'extraordinary' conditions."))

        ($.definition (/.List item)
          "A potentially empty list of values.")

        ($.definition /.Bit
          "Your standard, run-of-the-mill boolean values (as #0 or #1 bits).")

        ($.definition (/.I64 kind)
          "64-bit integers without any semantics.")

        ($.definition /.Nat
          (format "Natural numbers (unsigned integers)."
                  \n "They start at zero (0) and extend in the positive direction."))

        ($.definition /.Int
          "Your standard, run-of-the-mill integer numbers.")

        ($.definition /.Rev
          (format "Fractional numbers that live in the interval [0,1)."
                  \n "Useful for probability, and other domains that work within that interval."))

        ($.definition /.Frac
          "Your standard, run-of-the-mill floating-point (fractional) numbers.")

        ($.definition /.Text
          "Your standard, run-of-the-mill string values.")

        ($.definition /.Symbol
          (format "A name for a Lux definition."
                  \n "It includes the module of provenance."))

        ($.definition (/.Maybe value)
          "A potentially missing value.")

        ($.definition /.Type
          "This type represents the data-structures that are used to specify types themselves.")

        ($.definition /.Location
          "Locations are for specifying the location of Code nodes in Lux files during compilation.")

        ($.definition (/.Ann meta_data datum)
          "The type of things that can be annotated with meta-data of arbitrary types.")

        ($.definition /.Code
          "The type of Code nodes for Lux syntax.")

        ($.definition /.private
          "The export policy for private/local definitions.")

        ($.definition /.local
          "The export policy for private/local definitions.")

        ($.definition /.public
          "The export policy for public/global definitions.")

        ($.definition /.global
          "The export policy for public/global definitions.")

        ($.definition /.Definition
          "Represents all the data associated with a definition: its type, its annotations, and its value.")

        ($.definition /.Global
          "Represents all the data associated with a global constant.")

        ($.definition (/.Either left right)
          "A choice between two values of different types.")

        ($.definition /.Module
          "All the information contained within a Lux module.")

        ($.definition /.Mode
          "A sign that shows the conditions under which the compiler is running.")

        ($.definition /.Info
          "Information about the current version and type of compiler that is running.")

        ($.definition /.Lux
          (format "Represents the state of the Lux compiler during a run."
                  \n "It is provided to macros during their invocation, so they can access compiler data."
                  \n "Caveat emptor: Avoid fiddling with it, unless you know what you're doing."))

        ($.definition (/.Meta it)
          (format "Computations that can have access to the state of the compiler."
                  \n "These computations may fail, or modify the state of the compiler."))

        ($.definition /.Macro
          "Functions that run at compile-time and allow you to transform and extend the language in powerful ways.")

        ($.definition /.comment
          (format "Throws away any code given to it."
                  \n "Great for commenting-out code, while retaining syntax high-lighting and formatting in your text editor.")
          ($.example (comment
                       (def (this will not)
                         (Be Defined)
                         (because it will be (commented out))))))

        ($.definition /.All
          "Universal quantification."

          ($.example (All (_ a)
                       (-> a a)))

          ($.comment "A name can be provided, to specify a recursive type.")
          ($.example (All (List a)
                       (Or Any
                           [a (List a)]))))

        ($.definition /.Ex
          "Existential quantification."

          ($.example (Ex (_ a)
                       [(Codec Text a) a]))
          
          ($.comment "A name can be provided, to specify a recursive type.")
          ($.example (Ex (Self a)
                       [(Codec Text a)
                        a
                        (List (Self a))])))
        ))

(def all_2/4
  (List $.Documentation)
  (list ($.definition /.->
          "Function types."
          ($.comment "This is the type of a function that takes 2 Ints and returns an Int.")
          ($.example (-> Int Int Int)))

        ($.definition /.list
          "List literals."
          ($.example (is (List Nat)
                         (list 0 1 2 3))))

        ($.definition /.Union
          "Union types."
          ($.example (Union Bit Nat Text))
          ($.example (= Nothing
                        (Union))))

        ($.definition /.Tuple
          "Tuple types."
          ($.example (Tuple Bit Nat Text))
          ($.example (= Any
                        (Tuple))))

        ($.definition /.Or
          "An alias for the Union type constructor."
          ($.example (= (Union Bit Nat Text)
                        (Or Bit Nat Text)))
          ($.example (= (Union)
                        (Or))))

        ($.definition /.And
          "An alias for the Tuple type constructor."
          ($.example (= (Tuple Bit Nat Text)
                        (And Bit Nat Text)))
          ($.example (= (Tuple)
                        (And))))

        ($.definition /.left
          "Left-association for the application of binary functions over variadic arguments."

          ($.example (left text#composite "Hello, " name ". How are you?"))
          ($.comment "=>")
          ($.example (text#composite (text#composite "Hello, " name) ". How are you?")))

        ($.definition /.all
          "Right-association for the application of binary functions over variadic arguments."
          ($.example (all text#composite "Hello, " name ". How are you?"))
          ($.comment "=>")
          ($.example (text#composite "Hello, " (text#composite name ". How are you?"))))

        ($.definition /.if
          "Picks which expression to evaluate based on a bit test value."
          ($.example (if #1
                       "Oh, yeah!"
                       "Aw hell naw!"))
          ($.comment "=>")
          ($.example "Oh, yeah!")

          ($.example (if #0
                       "Oh, yeah!"
                       "Aw hell naw!"))
          ($.comment "=>")
          ($.example "Aw hell naw!"))

        ($.definition /.Nominal
          "Macro to treat define new nominal types."
          ($.example (Nominal "java.lang.Object"))
          ($.example (Nominal "java.util.List" [(Nominal "java.lang.Long")])))

        ($.definition /.`
          (format "Hygienic quasi-quotation as a macro."
                  \n "Unquote (,) and unquote-splice (,*) must also be used as forms."
                  \n "All unprefixed macros will receive their parent module's prefix if imported; otherwise will receive the prefix of the module on which the quasi-quote is being used.")
          ($.example (` (def (, name)
                          (function ((,' _) (,* args))
                            (, body))))))

        ($.definition /.`'
          (format "Unhygienic quasi-quotation as a macro."
                  \n "Unquote (,) and unquote-splice (,*) must also be used as forms.")
          ($.example (`' (def (, name)
                           (function (_ (,* args))
                             (, body))))))

        ($.definition /.'
          "Quotation as a macro."
          ($.example (' YOLO)))

        ($.definition /.|>
          "Piping macro."
          ($.example (|> elems
                         (list#each int#encoded)
                         (interposed " ")
                         (mix text#composite "")))
          ($.comment "=>")
          ($.example (mix text#composite ""
                          (interposed " "
                                      (list#each int#encoded
                                                 elems)))))

        ($.definition /.<|
          "Reverse piping macro."
          ($.example (<| (mix text#composite "")
                         (interposed " ")
                         (list#each int#encoded)
                         elems))
          ($.comment "=>")
          ($.example (mix text#composite ""
                          (interposed " "
                                      (list#each int#encoded
                                                 elems)))))

        ($.definition /.template
          ""
          ($.comment "By specifying a pattern (with holes), and the input data to fill those holes, repeats the pattern as many times as necessary.")
          ($.example (with_template [<name> <diff>]
                       [(def .public <name>
                          (-> Int Int)
                          (+ <diff>))]
                       
                       [++ +1]
                       [-- -1]
                       )))
        ))

(`` (def all_3/4
      (List $.Documentation)
      (list ($.definition /.not
              "Bit negation."
              ($.example (not #1))
              ($.comment "=>")
              ($.example #0)
              
              ($.example (not #0))
              ($.comment "=>")
              ($.example #1))

            ($.definition /.type
              "Takes a type expression and returns its representation as data-structure."
              ($.example (type_literal (All (_ a)
                                         (Maybe (List a))))))

            ($.definition /.is
              "The type-annotation macro."
              ($.example (is (List Int)
                             (list +1 +2 +3))))

            ($.definition /.as
              "The type-coercion macro."
              ($.example (as Dinosaur
                             (list +1 +2 +3))))

            ($.definition /.Rec
              "Parameter-less recursive types."
              ($.comment "A name has to be given to the whole type, to use it within its body.")
              ($.example (Rec Int_List
                           (Or Any
                               [Int Int_List])))

              ($.comment "Can also be used with type and labelled-type definitions.")
              ($.example (type Type
                           (Rec @
                             (Variant
                              {#Nominal Text (List @)}
                              {#Sum @ @}
                              {#Product @ @}
                              {#Function @ @}
                              {#Parameter Nat}
                              {#Var Nat}
                              {#Ex Nat}
                              {#UnivQ (List @) @}
                              {#ExQ (List @) @}
                              {#Apply @ @}
                              {#Named Symbol @})))))

            ($.definition /.exec
              "Sequential execution of expressions (great for side-effects)."
              ($.example (exec
                           (log! "#1")
                           (log! "#2")
                           (log! "#3")
                           "YOLO")))

            ($.definition /.when
              (format "The pattern-matching macro."
                      \n "Allows the usage of macros within the patterns to provide custom syntax.")
              ($.example (when (is (List Int)
                                   (list +1 +2 +3))
                           {#Item x {#Item y {#Item z {#End}}}}
                           {#Some (all * x y z)}

                           _
                           {#None})))

            ($.definition /.pattern
              (format "Macro-expanding patterns."
                      \n "It's a special macro meant to be used with 'when'.")
              ($.example (when (is (List Int)
                                   (list +1 +2 +3))
                           (list x y z)
                           {#Some (all * x y z)}

                           _
                           {#None})))

            ... ($.definition /.^or
            ...   (format "Or-patterns."
            ...           \n "It's a special macro meant to be used with 'when'.")
            ...   ($.example (type Weekday
            ...                (Variant
            ...                 {#Monday}
            ...                 {#Tuesday}
            ...                 {#Wednesday}
            ...                 {#Thursday}
            ...                 {#Friday}
            ...                 {#Saturday}
            ...                 {#Sunday})))
            ...   ($.example (def (weekend? day)
            ...                (-> Weekday Bit)
            ...                (when day
            ...                  (^or {#Saturday} {#Sunday})
            ...                  true

            ...                  _
            ...                  false))))

            ($.definition /.let
              (format "Creates local bindings."
                      \n "Can (optionally) use pattern-matching macros when binding.")
              ($.example (let [x (foo bar)
                               y (baz quux)]
                           (op x y))))

            ($.definition /.function
              "Syntax for creating functions."
              ($.example (is (All (_ a b)
                               (-> a b a))
                             (function (_ x y)
                               x)))

              ($.comment "Allows for giving the function itself a name, for the sake of recursion.")
              ($.example (is (-> Nat Nat)
                             (function (factorial n)
                               (when n
                                 0 1
                                 _ (* n  (factorial (-- n))))))))

            ($.definition /.def
              "Defines global constants/functions."
              ($.example (def branching_exponent
                           Int
                           +5))

              ($.comment "The type is optional.")
              ($.example (def branching_exponent
                           +5))

              ($.example (def (pair_list pair)
                           (-> [Code Code] (List Code))
                           (let [[left right] pair]
                             (list left right))))

              ($.comment "Can pattern-match on the inputs to functions.")
              ($.example (def (pair_list [left right])
                           (-> [Code Code] (List Code))
                           (list left right))))

            ($.definition /.macro
              "Macro-definition macro."
              ($.example (def .public symbol
                           (macro (_ tokens)
                             (when tokens
                               (^with_template [<tag>]
                                               [(list [_ {<tag> [module name]}])
                                                (in (list (` [(, (text$ module)) (, (text$ name))])))])
                               ([#Symbol])
                               
                               _
                               (failure "Wrong syntax for symbol"))))))

            ($.definition /.and
              "Short-circuiting 'and'."
              ($.example (and #1 #0))
              ($.comment "=>")
              ($.example #0)
              
              ($.example (and #1 #1))
              ($.comment "=>")
              ($.example #1))

            ($.definition /.or
              "Short-circuiting 'or'."
              ($.example (or #1 #0))
              ($.comment "=>")
              ($.example #1)

              ($.example (or #0 #0))
              ($.comment "=>")
              ($.example #0))

            ($.definition /.panic!
              "Causes an error, with the given error message."
              ($.example (panic! "OH NO!")))

            ($.definition /.implementation
              "Express a value that implements an interface."
              ($.example (is (Order Int)
                             (implementation
                              (def equivalence
                                equivalence)
                              (def (< reference subject)
                                (< reference subject))
                              ))))

            ($.definition /.Variant
              (format "Syntax for defining labelled/tagged sum/union types."
                      \n "WARNING: Only use it within the type macro.")
              ($.example (type Referrals
                           (Variant
                            {#All}
                            {#Only (List Text)}
                            {#Exclude (List Text)}
                            {#Ignore}
                            {#Nothing}))))

            ($.definition /.Record
              (format "Syntax for defining labelled/slotted product/tuple types."
                      \n "WARNING: Only use it within the type macro.")
              ($.example (type Refer
                           (Record
                            [#refer_defs Referrals
                             #refer_open (List Openings)]))))

            ($.definition /.type
              "The type-definition macro."
              ($.example (type (List a)
                           {#End}
                           {#Item a (List a)})))

            ($.definition /.Interface
              "Interface definition."
              ($.example (type .public (Order a)
                           (Interface
                            (is (Equivalence a)
                                equivalence)
                            (is (-> a a Bit)
                                <)))))

            (,, (with_template [<name>]
                  [($.definition <name>
                     "Safe type-casting for I64 values.")]

                  [/.i64]
                  [/.nat]
                  [/.int]
                  [/.rev]
                  ))

            ($.definition /.module_separator
              (format "Character used to separate the parts of module names."
                      \n "Value: " (%.text /.module_separator)))

            ($.definition /.open
              (format "Same as the 'open' macro, but meant to be used as a pattern-matching macro for generating local bindings."
                      \n "Takes an 'alias' text for the generated local bindings.")
              ($.example (def .public (range enum from to)
                           (All (_ a) (-> (Enum a) a a (List a)))
                           (let [(open "[0]") enum]
                             (loop (again [end to
                                           output {.#End}])
                               (cond (< end from)
                                     (again (pred end) {.#Item end output})

                                     (< from end)
                                     (again (succ end) {.#Item end output})

                                     ... (= end from)
                                     {.#Item end output}))))))

            ($.definition /.cond
              "Conditional branching with multiple test conditions."
              ($.example (cond (even? num) "WHEN even"
                               (odd? num) "WHEN odd"
                               "ELSE")))

            ($.definition /.the
              "Accesses the value of a record at a given tag."
              ($.example (the #field my_record))

              ($.comment "Can also work with multiple levels of nesting.")
              ($.example (the [#foo #bar #baz] my_record))

              ($.comment "And, if only the slot/path is given, generates an accessor function.")
              ($.example (let [getter (the [#foo #bar #baz])]
                           (getter my_record))))

            ($.definition /.use
              "Opens a implementation and generates a definition for each of its members (including nested members)."
              ($.example (use "i:[0]" order))
              ($.comment "=>")
              ($.example (def i:= (of order =)))
              ($.example (def i:< (of order <))))

            ($.definition /.|>>
              "Similar to the piping macro, but rather than taking an initial object to work on, creates a function for taking it."
              ($.example (|>> (list#each int#encoded)
                              (interposed " ")
                              (mix text#composite "")))
              ($.comment "=>")
              ($.example (function (_ <it>)
                           (mix text#composite ""
                                (interposed " "
                                            (list#each int#encoded <it>))))))

            ($.definition /.<<|
              "Similar to the reverse piping macro, but rather than taking an initial object to work on, creates a function for taking it."
              ($.example (<<| (mix text#composite "")
                              (interposed " ")
                              (list#each int#encoded)))
              ($.comment "=>")
              ($.example (function (_ <it>)
                           (mix text#composite ""
                                (interposed " "
                                            (list#each int#encoded
                                                       <it>))))))

            ($.definition /.require
              "Module-definition macro."
              ($.example (.require
                          [lux (.except)
                           [control
                            ["M" monad (.except)]]
                           [data
                            maybe
                            ["[0]" name (.use "[1]#[0]" codec)]]
                           [macro
                            code]]
                          [//
                           [type (.use "[0]" equivalence)]])))

            ($.definition /.of
              "Allows accessing the value of a implementation's member."
              ($.example (of codec encoded))

              ($.comment "Also allows using that value as a function.")
              ($.example (of codec encoded +123)))

            ($.definition /.has
              "Sets the value of a record at a given tag."
              ($.example (has #name "Lux" lang))

              ($.comment "Can also work with multiple levels of nesting.")
              ($.example (has [#foo #bar #baz] value my_record))

              ($.comment "And, if only the slot/path and (optionally) the value are given, generates a mutator function.")
              ($.example (let [setter (has [#foo #bar #baz] value)]
                           (setter my_record)))
              ($.example (let [setter (has [#foo #bar #baz])]
                           (setter value my_record))))
            )))

(`` (def all_4/4
      (List $.Documentation)
      (list ($.definition /.revised
              "Modifies the value of a record at a given tag, based on some function."
              ($.example (revised #age ++ person))

              ($.comment "Can also work with multiple levels of nesting.")
              ($.example (revised [#foo #bar #baz] func my_record))

              ($.comment "And, if only the slot/path and (optionally) the value are given, generates a mutator function.")
              ($.example (let [updater (revised [#foo #bar #baz] func)]
                           (updater my_record)))
              ($.example (let [updater (revised [#foo #bar #baz])]
                           (updater func my_record))))

            ... ($.definition /.^template
            ...   "It's similar to template, but meant to be used during pattern-matching."
            ...   ($.example (def (reduced env type)
            ...                (-> (List Type) Type Type)
            ...                (when type
            ...                  {.#Nominal name params}
            ...                  {.#Nominal name (list#each (reduced env) params)}

            ...                  (^with_template [<tag>]
            ...                                  [{<tag> left right}
            ...                                   {<tag> (reduced env left) (reduced env right)}])
            ...                  ([.#Sum] [.#Product])

            ...                  (^with_template [<tag>]
            ...                                  [{<tag> left right}
            ...                                   {<tag> (reduced env left) (reduced env right)}])
            ...                  ([.#Function] [.#Apply])

            ...                  (^with_template [<tag>]
            ...                                  [{<tag> old_env def}
            ...                                   (when old_env
            ...                                     {.#End}
            ...                                     {<tag> env def}

            ...                                     _
            ...                                     type)])
            ...                  ([.#UnivQ] [.#ExQ])

            ...                  {.#Parameter idx}
            ...                  (else type (list.item idx env))

            ...                  _
            ...                  type
            ...                  ))))

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

                  [/.++ "Increment function."]
                  [/.-- "Decrement function."]
                  ))

            ($.definition /.loop
              (format "Allows arbitrary looping, using the 'again' form to re-start the loop."
                      \n "Can be used in monadic code to create monadic loops.")
              ($.example (loop (again [count +0
                                       x init])
                           (if (< +10 count)
                             (again (++ count) (f x))
                             x)))

              ($.comment "Loops can also be given custom names.")
              ($.example (loop (my_loop [count +0
                                         x init])
                           (if (< +10 count)
                             (my_loop (++ count) (f x))
                             x))))

            ($.definition /.with_expansions
              (format "Controlled macro-expansion."
                      \n "Bind an arbitraty number of Code nodes resulting from macro-expansion to local bindings."
                      \n "Wherever a binding appears, the bound Code nodes will be spliced in there.")
              ($.example (def test
                           Test
                           (with_expansions
                             [<tests> (with_template [<function> <parameter> <expected>]
                                        [(cover [<function>]
                                                (compare <text>
                                                         (of codec encoded <function> <parameter>)))]

                                        [bit #1                "#1"]
                                        [int +123              "+123"]
                                        [frac +123.0           "+123.0"]
                                        [text "123"            "'123'"]
                                        [symbol ["yolo" "lol"] "yolo.lol"]
                                        [form (list (bit #1))  "(#1)"]
                                        [tuple (list (bit #1)) "[#1]"]
                                        )]
                             (all and
                                  <tests>
                                  )))))

            ($.definition /.static
              (format "Resolves the names of definitions to their values at compile-time, assuming their values are either:"
                      \n "* Bit"
                      \n "* Nat"
                      \n "* Int"
                      \n "* Rev"
                      \n "* Frac"
                      \n "* Text")
              ($.example (def my_nat 123))
              ($.example (def my_text "456"))
              ($.example (and (when [my_nat my_text]
                                (static [..my_nat ..my_text])
                                true

                                _
                                false)
                              (when [my_nat my_text]
                                [(static ..my_nat) (static ..my_text)]
                                true

                                _
                                false))))

            ... ($.definition /.^multi
            ...   (format "Multi-level pattern matching."
            ...           \n "Useful in situations where the result of a branch depends on further refinements on the values being matched.")
            ...   ($.example (when (split (size static) uri)
            ...                (^multi {#Some [chunk uri']}
            ...                        [(text#= static chunk) .true])
            ...                (match_uri endpoint? parts' uri')

            ...                _
            ...                {#Left (format "Static part " (%t static) " does not match URI: " uri)}))

            ...   ($.comment "Short-cuts can be taken when using bit tests.")
            ...   ($.comment "The example above can be rewritten as...")
            ...   ($.example (when (split (size static) uri)
            ...                (^multi {#Some [chunk uri']}
            ...                        (text#= static chunk))
            ...                (match_uri endpoint? parts' uri')

            ...                _
            ...                {#Left (format "Static part " (%t static) " does not match URI: " uri)})))

            ($.definition /.symbol
              "Gives back a 2 tuple with the module and name parts, both as Text."
              ($.example (symbol ..#doc))
              ($.comment "=>")
              ($.example ["documentation/lux" "#doc"]))

            ($.definition /.parameter
              (format "WARNING: Please stay away from this macro; it's very likely to be removed in a future version of Lux."
                      "Allows you to refer to the type-variables in a polymorphic function's type, by their index.")
              ($.comment "In the example below, 0 corresponds to the 'a' variable.")
              ($.example (def .public (of_list list)
                           (All (_ a) (-> (List a) (Sequence a)))
                           (list#mix add
                                     (is (Sequence (parameter 0))
                                         empty)
                                     list))))

            ($.definition /.same?
              "Tests whether the 2 values are identical (not just 'equal')."
              ($.comment "This one should succeed:")
              ($.example (let [value +5]
                           (same? value
                                  value)))
              
              ($.comment "This one should fail:")
              ($.example (same? +5
                                (+ +2 +3))))

            ($.alias /.alias?)

            ... ($.definition /.^let
            ...   "Allows you to simultaneously bind and de-structure a value."
            ...   ($.example (def (hash (^let set [member_hash _]))
            ...                (list#mix (function (_ elem acc)
            ...                            (+ acc
            ...                               (of member_hash hash elem)))
            ...                          0
            ...                          (set.list set)))))

            ... ($.definition /.^|>
            ...   "Pipes the value being pattern-matched against prior to binding it to a variable."
            ...   ($.example (when input
            ...                (^|> value [++ (% 10) (max 1)])
            ...                (foo value))))

            ($.definition /.as_expected
              "Coerces the given expression to the type of whatever is expected."
              ($.example (is Dinosaur
                             (as_expected (is (List Nat)
                                              (list 1 2 3))))))

            ($.definition /.undefined
              (format "Meant to be used as a stand-in for functions with undefined implementations."
                      \n "Undefined expressions will type-check against everything, so they make good dummy implementations."
                      \n "However, if an undefined expression is ever evaluated, it will raise a runtime error.")
              ($.example (def (square x)
                           (-> Int Int)
                           (undefined))))

            ($.definition /.type_of
              "Generates the type corresponding to a given expression."
              ($.example (let [my_num +123]
                           (type_of my_num)))
              ($.comment "==")
              ($.example Int)
              
              ($.example (type_of +123))
              ($.comment "==")
              ($.example Int))

            ($.definition /.template
              (format "Define macros in the style of with_template."
                      \n "For simple macros that do not need any fancy features.")
              ($.example (def square
                           (template (square x)
                             (* x x)))))

            ($.definition /.these
              (format "Given a (potentially empty) list of codes, just returns them immediately, without any work done."
                      \n "This may seen useless, but it has its utility when dealing with controlled-macro-expansion macros.")
              ($.example (with_expansions [<operands> (these 1
                                                             2
                                                             3
                                                             4)]
                           (all + <operands>))))

            ($.definition /.char
              "If given a 1-character text literal, yields the char-code of the sole character."
              ($.example (is Nat
                             (char "A")))
              ($.comment "=>")
              ($.example 65))

            ($.definition /.for
              (format "Selects the appropriate code for a given target-platform when compiling Lux to it."
                      \n "Look-up the available targets in library/lux/target.")
              ($.example (def js
                           "JavaScript"))
              ($.example (for "JVM" (do jvm stuff)
                              js (do js stuff)
                              (do default stuff))))

            ($.definition /.``
              (format "Delimits a controlled (spliced) macro-expansion."
                      \n "Uses a (,,) special form to specify where to expand.")
              ($.example (`` (some expression
                                   (,, (some macro which may yield 0 or more results))))))

            ... ($.definition /.^code
            ...   "Generates pattern-matching code for Code values in a way that looks like code-templating."
            ...   ($.example (is (Maybe Nat)
            ...                  (when (` (#0 123 +456.789))
            ...                    (^code (#0 (, [_ {.#Nat number}]) +456.789))
            ...                    {.#Some number}

            ...                    _
            ...                    {.#None}))))

            ($.definition /.false
              "The boolean FALSE value.")

            ($.definition /.true
              "The boolean TRUE value.")

            ($.definition /.try
              ""
              ($.example (is Foo
                             (when (is (Either Text Bar)
                                       (try (is Bar
                                                (risky computation which may panic))))
                               {.#Right success}
                               (is Foo
                                   (do something after success))

                               {.#Left error}
                               (is Foo
                                   (recover from error))))))
            
            ($.definition (/.Code' w))
            ($.definition /.Alias)
            ($.definition (/.Bindings key value))
            ($.definition /.Ref)
            ($.definition /.Scope)
            ($.definition /.Source)
            ($.definition /.Module_State)
            ($.definition /.Type_Context)
            ($.definition /.Macro')
            ($.definition /.Label)
            ($.definition /.macro)
            )))

(def .public documentation
  (List $.Documentation)
  (all list#composite
       (list ($.module /._
                       "The prelude for Lux's standard library."))
       all_1/4
       all_2/4
       all_3/4
       all_4/4

       /abstract.documentation
       /control.documentation
       /data.documentation
       /debug.documentation
       /documentation.documentation
       /ffi.documentation
       /math.documentation
       /meta.documentation
       /program.documentation
       /test.documentation
       /world.documentation
       ))

(def _
  (program inputs
    (io.io (debug.log! ($.markdown ..documentation)))))