diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/documentation/lux/meta/type.lux | 506 |
1 files changed, 257 insertions, 249 deletions
diff --git a/stdlib/source/documentation/lux/meta/type.lux b/stdlib/source/documentation/lux/meta/type.lux index b0736757a..4e2d13faa 100644 --- a/stdlib/source/documentation/lux/meta/type.lux +++ b/stdlib/source/documentation/lux/meta/type.lux @@ -4,7 +4,9 @@ ["$" documentation] [data ["[0]" text (.only \n) - ["%" \\format (.only format)]]] + ["%" \\format (.only format)]] + [collection + ["[0]" list (.use "[1]#[0]" monoid)]]] [meta [macro ["[0]" template]]]]] @@ -23,251 +25,257 @@ ["[1][0]" unit] ["[1][0]" variance]]) -(`` (.def \\parser - (.List $.Module) - ($.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 $.Module) - ($.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]))])] - [..\\parser - - /primitive.documentation - /check.documentation - /dynamic.documentation - /implicit.documentation - /poly.documentation - /quotient.documentation - /refinement.documentation - /resource.documentation - /unit.documentation - /variance.documentation]))) +(`` (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 + ) + ))) |