max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: few updates to Expr documentation

Browse source
This commit is contained in:
Yuri de Wit 2022-09-19 16:52:39 -03:00 • committed by Leonardo de Moura
parent b922483ebc
commit 64a0ec91fa
1 changed files with 73 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

115
src/Lean/Expr.lean
View file

@ -291,36 +291,53 @@ instance : Inhabited (MVarIdMap α) where
default := {}
/--
Lean expressions. This datastructure is used in the kernel and
Lean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.
Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use. -/
We considered using «...», but it is too inconvenient to use.
-/
inductive Expr where
/--
Bound variables. The natural number is the "de Bruijn" index
for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information.
Example, the expression `fun x : Nat => forall y : Nat, x = y`
The `bvar` constructor represents bound variables, i.e. occurrences
of a variable in the expression where there is a variable binder
above it (i.e. introduced by a `lam`, `forallE`, or `letE`).
The `deBruijnIndex` parameter is the *de-Bruijn* index for the bound
variable. See [here](https://en.wikipedia.org/wiki/De_Bruijn_index)
for additional information on de-Bruijn indexes.
For example, consider the expression `fun x : Nat => forall y : Nat, x = y`.
The `x` and `y` variables in the equality expression are constructed
using `bvar` and bound to the binders introduced by the earlier
`lam` and `forallE` constructors. Here is the corresponding `Expr` representation
for the same expression:
```lean
.lam `x (.const `Nat [])
(.forall `y (.const `Nat [])
(.app (.app (.app (.const `Eq [.succ .zero])
(.const `Nat [])) (.bvar 1))
(.bvar 0))
(.forallE `y (.const `Nat [])
(.app (.app (.app (.const `Eq [.succ .zero]) (.const `Nat [])) (.bvar 1)) (.bvar 0))
.default)
.default
```
-/
| bvar (deBruijnIndex : Nat)
/--
Free variable. Lean uses the locally nameless approach.
See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details.
When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables
are converted into free variables using a unique identifier, and their user-facing name, type,
value (for `LetE`), and binder annotation are stored in the `LocalContext`.
The `fvar` constructor represent free variables. These /free/ variable
occurrences are not bound by an earlier `lam`, `forallE`, or `letE`
contructor and its binder exists in a local context only.
Note that Lean uses the /locally nameless approach/. See [here](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf)
for additional details.
When "visiting" the body of a binding expression (i.e. `lam`, `forallE`, or `letE`),
bound variables are converted into free variables using a unique identifier,
and their user-facing name, type, value (for `LetE`), and binder annotation
are stored in the `LocalContext`.
-/
| fvar (fvarId : FVarId)
/--
Metavariables are used to represent "holes" in expressions, and goals in the
tactic framework. Metavariable declarations are stored in the `MetavarContext`.
@ -328,50 +345,61 @@ inductive Expr where
or in the code generator.
-/
| mvar (mvarId : MVarId)
/--
`Type u`, `Sort u`, `Prop`. -
Used for `Type u`, `Sort u`, and `Prop`:
- `Prop` is represented as `.sort .zero`,
- `Sort u` as ``.sort (.param `u)``, and
- `Type u` as ``.sort (.succ (.param `u))``
-/
| sort (u : Level)
/--
A (universe polymorphic) constant. For example,
`@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and
`@Array.map.{0, 0}` is represented as ``.const `Array.map [.zero, .zero]``.
A (universe polymorphic) constant that has been defined earlier in the module or
by another imported module. For example, `@Eq.{1}` is represented
as ``Expr.const `Eq [.succ .zero]``, and `@Array.map.{0, 0}` is represented
as ``Expr.const `Array.map [.zero, .zero]``.
-/
| const (declName : Name) (us : List Level)
/--
Function application. `Nat.succ Nat.zero` is represented as
```
.app (.const `Nat.succ []) (.const .zero [])
```
A function application.
For example, the natural number one, i.e. `Nat.succ Nat.zero` is represented as
`Expr.app (.const `Nat.succ []) (.const .zero [])`
Note that multiple arguments are represented using partial application.
For example, the two argument application `f x y` is represented as
`Expr.app (.app f x) y`.
-/
| app (fn : Expr) (arg : Expr)
/--
Lambda abstraction (aka anonymous functions).
- `fun x : Nat => x` is represented as
A lambda abstraction (aka anonymous functions). It introduces a new binder for
variable `x` in scope for the lambda body.
For example, the expression `fun x : Nat => x` is represented as
```
.lam `x (.const `Nat []) (.bvar 0) .default
Expr.lam `x (.const `Nat []) (.bvar 0) .default
```
-/
| lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
/--
A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows.
Examples:
- `forall x : Prop, x ∧ x` is represented as
A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may dependent
on `a`. Note that this constructor is also used to represent non-dependent arrows
where `β` does not depend on `a`.
For example:
- `forall x : Prop, x ∧ x`:
```lean
Expr.forallE `x (.sort .zero)
(.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) .default
```
.forallE `x
(.sort .zero)
(.app (.app (.const `And []) (.bvar 0)) (.bvar 0))
.default
```
- `Nat → Bool` as
```
.forallE `a (.const `Nat []) (.const `Bool []) .default
- `Nat → Bool`:
```lean
Expr.forallE `a (.const `Nat [])
(.const `Bool []) .default
```
-/
| forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
/--
Let-expressions. The field `nonDep` is not currently used, but will be used in the future
by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent
@ -388,29 +416,32 @@ inductive Expr where
`(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.
The let-expression `let x : Nat := 2; Nat.succ x` is represented as
```
.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
```
-/
| letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)
/--
Natural number and string literal values. They are not really needed, but provide a more
compact representation in memory for these two kinds of literals, and are used to implement
efficient reduction in the elaborator and kernel.
The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is
definitionally equal to
```
.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
definitionally equal to:
```lean
Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
-/
| lit : Literal → Expr
| lit : Literal → Expr
/--
Metadata (aka annotations). We use annotations to provide hints to the pretty-printer,
store references to `Syntax` nodes, position information, and save information for
elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to
mark `Expr`s that correspond to inaccessible patterns).
Note that `.mdata data e` is definitionally equal to `e`.
Note that `Expr.mdata data e` is definitionally equal to `e`.
-/
| mdata (data : MData) (expr : Expr)
/--
Projection-expressions. They are redundant, but are used to create more compact
terms, speedup reduction, and implement eta for structures.