diff --git a/docs/spec/README.md b/docs/spec/README.md index 433fc1dfa32e..1dbc19fe956d 100644 --- a/docs/spec/README.md +++ b/docs/spec/README.md @@ -12,3 +12,8 @@ detailed to allow independent implementations of the language. While we plan to have a reference implementation, we think having a specification as well is an important tool to ensure that the behavior of the language is well understood and holds together. + +The work-in-progress specification is available here: + +- [Language specification](lang) +- [Library specification](lib) diff --git a/docs/spec/lang/README.md b/docs/spec/lang/README.md new file mode 100644 index 000000000000..2b5210d27b95 --- /dev/null +++ b/docs/spec/lang/README.md @@ -0,0 +1,79 @@ +# Carbon language specification + + + +## Program structure + +1. A _program_ is a collection of one or more linkage units that are + [linked](#linkage) together. + +2. A _Carbon linkage unit_ is the result of [translating](#translation) a + source file. A _foreign linkage unit_ is an artifact produced by a + translation process for some other programming language. A linkage unit is + either a Carbon linkage unit or a foreign linkage unit. + +3. A _source file_ is a sequence of Unicode code points. + + > Note: Source files are typically stored on disk in files with a `.carbon` + > file extension, encoded in UTF-8. + +## Conformance + +1. A program is _valid_ if it contains no constructs that violate "shall" + constraints in this specification. Otherwise, the program is _invalid_. + +2. An implementation is _conforming_ if it accepts all valid programs, it + rejects all invalid programs for which a diagnostic is required, and the + [execution](execution.md) semantics of all accepted programs is as specified + in this specification. + +## Translation + +1. Translation of a source file into a Carbon linkage unit proceeds as follows: + + - [Lexical analysis](lex.md) decomposes the sequence of code points into a + sequence of lexical elements. + - Whitespace and text comments are discarded, leaving a sequence of + [tokens](lex.md). + - The tokens are [parsed](parsing.md) into an abstract syntax tree. + - [Unqualified names are bound](names.md) to declarations in the abstract + syntax tree. + - A translated form of each imported [library](libs.md) is located and + loaded. + - [Semantic analysis](semantics.md) is performed: types are determined and + semantic checks are performed for all non-template-dependent constructs + in the abstract syntax tree, constant expressions are evaluated, and + templates are instantiated and semantically analyzed. + +2. > Note: After semantic analysis, an implementation may optionally + > monomorphize generics by a process similar to template instantiation. + +3. The resulting linkage unit comprises all entities in the translated source + file that are either [external](#linkage) or are reachable from an external + entity. + + > Note: A linkage unit can include non-monomorphized generics, but never + > includes templates. Constant evaluation can eliminate references to + > entities. + +## Linkage + +1. Two declarations declare the same entity if both declarations are in the + same library and the same [scope](names.md#scopes) and declare the same + [name](names.md). + + TODO: Linkage rules for foreign entities. TODO: Ability to declare + file-local entities. + +2. All declarations of an entity shall use the same type. + +3. Every entity that is reachable from a linkage unit in a program shall be + defined by a linkage unit in the program; no diagnostic is required unless + an entity that can be referenced during the [execution](execution.md) of the + program is not defined. + +4. There shall not be more than one definition of an entity in a program. diff --git a/docs/spec/lang/execution.md b/docs/spec/lang/execution.md new file mode 100644 index 000000000000..bc97b7f5b128 --- /dev/null +++ b/docs/spec/lang/execution.md @@ -0,0 +1,17 @@ +# Execution + + + +## Entry points + +TODO: Entry points (Carbon and foreign). `fn Run()`. + +## Object model + +## Sequential execution + +## Threads and data races diff --git a/docs/spec/lang/lex.md b/docs/spec/lang/lex.md new file mode 100644 index 000000000000..b7962ef97db9 --- /dev/null +++ b/docs/spec/lang/lex.md @@ -0,0 +1,25 @@ +# Lexical analysis + + + +TODO + +## Lexical elements + +1. The sequence of Unicode code points in a source file is partitioned into + contiguous subsequences called _lexical elements_. Formation of lexical + elements begins with the first code point in the source file and proceeds in + code point order. + +2. At each step, the longest valid lexical element that can be formed from a + prefix of the remaining code points is formed, even if this would result in + a failure to form a later lexical element. Repeating this process shall + convert the entire source file into lexical elements. + +3. Valid lexical elements are: + + TODO: Add a list of lexical elements once we've decided on them. diff --git a/docs/spec/lang/libs.md b/docs/spec/lang/libs.md new file mode 100644 index 000000000000..d8b0e83f2188 --- /dev/null +++ b/docs/spec/lang/libs.md @@ -0,0 +1,9 @@ +# Libraries and packages + + + +TODO diff --git a/docs/spec/lang/names.md b/docs/spec/lang/names.md new file mode 100644 index 000000000000..c2d03a64fb7d --- /dev/null +++ b/docs/spec/lang/names.md @@ -0,0 +1,34 @@ +# Names + + + +TODO + +## Names + +1. A _name_ is an [identifier](lex.md). Two names are the same if they comprise + the same sequence of Unicode code points. + + TODO: Normalization? + +## Scopes + +1. A _scope_ is one of: + + - The top level in a source file. + - A pattern scope. + - A block scope. + - A type definition. + +2. Every construct that declares a name _binds_ the name to the declared entity + within the innermost enclosing scope. + +## Unqualified name lookup + +1. Unqualified name lookup associates a name with an entity. The associated + entity is the entity to which the name is bound in the innermost enclosing + scope in which the name is bound. diff --git a/docs/spec/lang/parsing.md b/docs/spec/lang/parsing.md new file mode 100644 index 000000000000..641ab4b25d0b --- /dev/null +++ b/docs/spec/lang/parsing.md @@ -0,0 +1,9 @@ +# Parsing + + + +TODO diff --git a/docs/spec/lang/semantics.md b/docs/spec/lang/semantics.md new file mode 100644 index 000000000000..fd1b2234dfd2 --- /dev/null +++ b/docs/spec/lang/semantics.md @@ -0,0 +1,9 @@ +# Semantic analysis + + + +TODO diff --git a/docs/spec/lib/README.md b/docs/spec/lib/README.md new file mode 100644 index 000000000000..455fa7317fc5 --- /dev/null +++ b/docs/spec/lib/README.md @@ -0,0 +1,9 @@ +# Carbon standard library specification + + + +TODO diff --git a/proposals/p0140.md b/proposals/p0140.md new file mode 100644 index 000000000000..3f09bfff405b --- /dev/null +++ b/proposals/p0140.md @@ -0,0 +1,88 @@ +# Create initial rough framework for specification + + + +[Pull request](https://github.com/carbon-language/carbon-lang/pull/140) + +## Table of contents + + + +## Table of contents + +- [Problem](#problem) +- [Proposal](#proposal) +- [Details](#details) + - [Conventions](#conventions) +- [Alternatives considered](#alternatives-considered) + - [Maintain the specification in a different language.](#maintain-the-specification-in-a-different-language) + + + +## Problem + +We need a rough layout for our specification so that we can start adding details +to it once they're decided. + +## Proposal + +Split the specification into a language and a library section. In the language +section, use one file per broad area of functionality. Divide the language up +based on the intended layering of the language design. + +For now, maintain the specification sources in Markdown. + +## Details + +Proposed top-level structure of the `spec/` directory as of this pull request: + +- `README.md` Introduction to the specification +- `lang` + - `README.md` Language specification overview and basics + - `execution.md` Execution semantics + - `lex.md` Lexical analysis + - `libs.md` Libraries and packages + - `names.md` Names and name binding / lookup + - `parsing.md` Parsing + - `semantics.md` Semantic analysis +- `lib` + - `README.md` Library specification overview and basics + +This is only a starting point; the structure should be expected to change and +grow as the specification is filled out. Most of the proposed files are empty or +nearly-empty placeholders. + +### Conventions + +All paragraphs within the specification are numbered so that they can be +referenced more easily. + +Defined terms are introduced in italics. + +Hyperlinks between sections of the specification are used liberally. + +## Alternatives considered + +### Maintain the specification in a different language. + +Advantages: + +- An alternative language may provide better support for custom typesetting, + representing grammars, linking to definitions, and so on. + +Disadvantages: + +- Using a different language would add complexity and inconsistency to our + documentation. +- There is unlikely to be any existing documentation language that is + well-suited to our needs without significant customization. +- Conversion from a more sophisticated language is likely to be more complex + than converting from Markdown. + +Conversion of Markdown to another language at a later point (either manually or +using a tool like Sphinx) is expected to remain a relatively low-cost option, +due to the relative simplicitly of Markdown-formatted documents.