add soundness and completeness to glossary

This commit is contained in:
Mark Mansi 2018-02-13 11:00:42 -06:00 committed by Who? Me?!
parent 63b6666b77
commit 35a13bae33
1 changed files with 2 additions and 0 deletions

View File

@ -7,6 +7,7 @@ Term | Meaning
------------------------|-------- ------------------------|--------
AST | the abstract syntax tree produced by the syntax crate; reflects user syntax very closely. AST | the abstract syntax tree produced by the syntax crate; reflects user syntax very closely.
codegen unit | when we produce LLVM IR, we group the Rust code into a number of codegen units. Each of these units is processed by LLVM independently from one another, enabling parallelism. They are also the unit of incremental re-use. codegen unit | when we produce LLVM IR, we group the Rust code into a number of codegen units. Each of these units is processed by LLVM independently from one another, enabling parallelism. They are also the unit of incremental re-use.
completeness | soundness is a technical term in type theory. Completeness means that every type-safe program also type-checks. Having both soundness and completeness is very hard, and usually soundness is more important. (see "soundness").
cx | we tend to use "cx" as an abbrevation for context. See also `tcx`, `infcx`, etc. cx | we tend to use "cx" as an abbrevation for context. See also `tcx`, `infcx`, etc.
DAG | a directed acyclic graph is used during compilation to keep track of dependencies between queries. ([see more](incremental-compilation.html)) DAG | a directed acyclic graph is used during compilation to keep track of dependencies between queries. ([see more](incremental-compilation.html))
DefId | an index identifying a definition (see `librustc/hir/def_id.rs`). Uniquely identifies a `DefPath`. DefId | an index identifying a definition (see `librustc/hir/def_id.rs`). Uniquely identifies a `DefPath`.
@ -25,6 +26,7 @@ provider | the function that executes a query ([see more](query.
query | perhaps some sub-computation during compilation ([see more](query.html)) query | perhaps some sub-computation during compilation ([see more](query.html))
sess | the compiler session, which stores global data used throughout compilation sess | the compiler session, which stores global data used throughout compilation
side tables | because the AST and HIR are immutable once created, we often carry extra information about them in the form of hashtables, indexed by the id of a particular node. side tables | because the AST and HIR are immutable once created, we often carry extra information about them in the form of hashtables, indexed by the id of a particular node.
soundness | soundness is a technical term in type theory. Roughly, if a type system is sound, then if a program type-checks, it is type-safe; i.e. I can never (in safe rust) force a value into a variable of the wrong type. (see "completeness").
span | a location in the user's source code, used for error reporting primarily. These are like a file-name/line-number/column tuple on steroids: they carry a start/end point, and also track macro expansions and compiler desugaring. All while being packed into a few bytes (really, it's an index into a table). See the Span datatype for more. span | a location in the user's source code, used for error reporting primarily. These are like a file-name/line-number/column tuple on steroids: they carry a start/end point, and also track macro expansions and compiler desugaring. All while being packed into a few bytes (really, it's an index into a table). See the Span datatype for more.
substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap<i32, u32>`) substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap<i32, u32>`)
tcx | the "typing context", main data structure of the compiler ([see more](ty.html)) tcx | the "typing context", main data structure of the compiler ([see more](ty.html))