diff --git a/Manual.lean b/Manual.lean index 2140237..8a2003a 100644 --- a/Manual.lean +++ b/Manual.lean @@ -11,7 +11,7 @@ import Manual.Language import Manual.Terms import Manual.Tactics import Manual.Simp -import Manual.BuiltInTypes +import Manual.BasicTypes open Verso.Genre Manual @@ -36,7 +36,11 @@ set_option pp.rawOnError true {include 0 Manual.Simp} -{include 0 Manual.BuiltInTypes} +{include 0 Manual.BasicTypes} + +# Standard Library + +## Optional Values # Notations and Macros %%% diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean new file mode 100644 index 0000000..2feacbf --- /dev/null +++ b/Manual/BasicTypes.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2024 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual + +import Manual.Meta +import Manual.BasicTypes.Nat +import Manual.BasicTypes.String + +open Manual.FFIDocType + +open Verso.Genre Manual + +set_option pp.rawOnError true + + +#doc (Manual) "Basic Types" => + +Lean includes a number of built-in datatypes that are specially supported by the compiler. +Some, such as {lean}`Nat`, additionally have special support in the kernel. +Other types don't have special compiler support _per se_, but rely in important ways on the internal representation of types for performance reasons. + +{include 0 Manual.BasicTypes.Nat} + +# Integers + +# Fixed-Precision Integer Types + +# Floating-Point Numbers + +# Characters + +{docstring Char} + +## Syntax + +## Logical Model + + + +## Run-Time Representation + +In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a datatype or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed. + + +## API Reference + +### Character Classes + +{docstring Char.isAlpha} + +{docstring Char.isAlphanum} + +{docstring Char.isDigit} + +{docstring Char.isLower} + +{docstring Char.isUpper} + +{docstring Char.isWhitespace} + + +{include 0 Manual.BasicTypes.String} + +# Linked Lists + +# Arrays + +::: planned 91 +Description and API reference for {name}`Thunk`: + * Logical model as wrapper around a function from {lean}`Unit` + * Run-time realization as a lazy computation + * API reference +::: + + +# Lazy Computations + +::: planned 92 +Description and API reference for {name}`Thunk`: + * Logical model as wrapper around a function from {lean}`Unit` + * Run-time realization as a lazy computation + * API reference +::: + +# Tasks and Threads + +::: planned 90 +Description and API reference for {name}`Task` and runtime threads, including {lean}`IO.Promise` + + * Scheduling model + * Things to be careful of + +This section may be moved to the section on {name}`IO` in particular. +::: diff --git a/Manual/BuiltInTypes/Nat.lean b/Manual/BasicTypes/Nat.lean similarity index 100% rename from Manual/BuiltInTypes/Nat.lean rename to Manual/BasicTypes/Nat.lean diff --git a/Manual/BuiltInTypes/String.lean b/Manual/BasicTypes/String.lean similarity index 96% rename from Manual/BuiltInTypes/String.lean rename to Manual/BasicTypes/String.lean index 8e516e0..d24731e 100644 --- a/Manual/BuiltInTypes/String.lean +++ b/Manual/BasicTypes/String.lean @@ -8,9 +8,9 @@ import VersoManual import Manual.Meta -import Manual.BuiltInTypes.String.Logical -import Manual.BuiltInTypes.String.Literals -import Manual.BuiltInTypes.String.FFI +import Manual.BasicTypes.String.Logical +import Manual.BasicTypes.String.Literals +import Manual.BasicTypes.String.FFI open Manual.FFIDocType @@ -32,7 +32,7 @@ The fact that strings are internally represented as UTF-8-encoded byte arrays is * There is no operation to project a particular character out of the string, as this would be a performance trap. {ref "string-iterators"}[Use a {name}`String.Iterator`] in a loop instead of a {name}`Nat`. * Strings are indexed by {name}`String.Pos`, which internally records _byte counts_ rather than _character counts_, and thus takes constant time. Aside from `0`, these should not be constructed directly, but rather updated using {name}`String.next` and {name}`String.prev`. -{include 0 Manual.BuiltInTypes.String.Logical} +{include 0 Manual.BasicTypes.String.Logical} # Run-Time Representation %%% @@ -72,7 +72,7 @@ Otherwise, a new string must be allocated. Despite the fact that they appear to be an ordinary constructor and projection, {name}`String.mk` and {name}`String.data` take *time linear in the length of the string*. This is because they must implement the conversions between lists of characters and packed arrays of bytes, which must necessarily visit each character. -{include 0 Manual.BuiltInTypes.String.Literals} +{include 0 Manual.BasicTypes.String.Literals} # API Reference @@ -367,4 +367,4 @@ TODO Substring API xref {docstring String.crlfToLf} -{include 0 Manual.BuiltInTypes.String.FFI} +{include 0 Manual.BasicTypes.String.FFI} diff --git a/Manual/BuiltInTypes/String/FFI.lean b/Manual/BasicTypes/String/FFI.lean similarity index 100% rename from Manual/BuiltInTypes/String/FFI.lean rename to Manual/BasicTypes/String/FFI.lean diff --git a/Manual/BuiltInTypes/String/Literals.lean b/Manual/BasicTypes/String/Literals.lean similarity index 100% rename from Manual/BuiltInTypes/String/Literals.lean rename to Manual/BasicTypes/String/Literals.lean diff --git a/Manual/BuiltInTypes/String/Logical.lean b/Manual/BasicTypes/String/Logical.lean similarity index 100% rename from Manual/BuiltInTypes/String/Logical.lean rename to Manual/BasicTypes/String/Logical.lean diff --git a/Manual/BuiltInTypes.lean b/Manual/BuiltInTypes.lean deleted file mode 100644 index 22895db..0000000 --- a/Manual/BuiltInTypes.lean +++ /dev/null @@ -1,64 +0,0 @@ -/- -Copyright (c) 2024 Lean FRO LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: David Thrane Christiansen --/ - -import VersoManual - -import Manual.Meta -import Manual.BuiltInTypes.Nat -import Manual.BuiltInTypes.String - -open Manual.FFIDocType - -open Verso.Genre Manual - -set_option pp.rawOnError true - - -#doc (Manual) "Built-In Types" => - -Lean includes a number of built-in datatypes that are specially supported by the compiler. -Some additionally have special support in the kernel. - -{include 0 Manual.BuiltInTypes.Nat} - -# Fixed-Precision Integer Types - - - -# Characters - -{docstring Char} - -## Syntax - -## Logical Model - - - -## Run-Time Representation - -In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a datatype or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed. - - -## API Reference - -### Character Classes - -{docstring Char.isAlpha} - -{docstring Char.isAlphanum} - -{docstring Char.isDigit} - -{docstring Char.isLower} - -{docstring Char.isUpper} - -{docstring Char.isWhitespace} - -{include 0 Manual.BuiltInTypes.String} - -# Arrays