From 09aa845940fdf8b03bfbb74419dcd3c588b31534 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 21 Jan 2024 20:58:29 -0600 Subject: [PATCH] doc: clarify and expand docstrings for the `instantiate` functions (#3183) Co-authored-by: Sebastian Ullrich --- src/Lean/Expr.lean | 70 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 61 insertions(+), 9 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 92eb53ae2d..afc7e9038f 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -1227,32 +1227,84 @@ def inferImplicit : Expr → Nat → Bool → Expr | e, _, _ => e /-- -Instantiate the loose bound variables in `e` using `subst`. -That is, a loose `Expr.bvar i` is replaced with `subst[i]`. +Instantiates the loose bound variables in `e` using the `subst` array, +where a loose `Expr.bvar i` at "binding depth" `d` is instantiated with `subst[i - d]` if `0 <= i - d < subst.size`, +and otherwise it is replaced with `Expr.bvar (i - subst.size)`; non-loose bound variables are not touched. + +If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, +then conceptually `instantiate` is instantiating the last `n` of these and reindexing the remaining ones. +Warning: `instantiate` uses the de Bruijn indexing to index the `subst` array, which might be the reverse order from what you might expect. +See also `Lean.Expr.instantiateRev`. + +**Terminology.** The "binding depth" of a subexpression is the number of bound variables available to that subexpression +by virtue of being in the bodies of `Expr.forallE`, `Expr.lam`, and `Expr.letE` expressions. +A bound variable `Expr.bvar i` is "loose" if its de Bruijn index `i` is not less than its binding depth.) + +**About instantiation.** Instantiation isn't mere substitution. +When an expression from `subst` is being instantiated, its internal loose bound variables have their de Bruijn indices incremented +by the binding depth of the replaced loose bound variable. +This is necessary for the substituted expression to still refer to the correct binders after instantiation. +Similarly, the reason loose bound variables not instantiated using `subst` have their de Bruijn indices decremented like `Expr.bvar (i - subst.size)` +is that `instantiate` can be used to eliminate binding expressions internal to a larger expression, +and this adjustment keeps these bound variables referring to the same binders. -/ @[extern "lean_expr_instantiate"] opaque instantiate (e : @& Expr) (subst : @& Array Expr) : Expr +/-- +Instantiates loose bound variable `0` in `e` using the expression `subst`, +where in particular a loose `Expr.bvar i` at binding depth `d` is instantiated with `subst` if `i = d`, +and otherwise it is replaced with `Expr.bvar (i - 1)`; non-loose bound variables are not touched. + +If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, +then conceptually `instantiate1` is instantiating the last one of these and reindexing the remaining ones. + +This function is equivalent to `instantiate e #[subst]`, but it avoids allocating an array. + +See the documentation for `Lean.Expr.instantiate` for a description of instantiation. +In short, during instantiation the loose bound variables in `subst` have their own de Bruijn indices updated to account +for the binding depth of the replaced loose bound variable. +-/ @[extern "lean_expr_instantiate1"] opaque instantiate1 (e : @& Expr) (subst : @& Expr) : Expr -/-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/ +/-- +Instantiates the loose bound variables in `e` using the `subst` array. +This is equivalent to `Lean.Expr.instantiate e subst.reverse`, but it avoids reversing the array. +In particular, rather than instantiating `Expr.bvar i` with `subst[i - d]` it instantiates with `subst[subst.size - 1 - (i - d)]`, +where `d` is the binding depth. + +This function instantiates with the "forwards" indexing scheme. +For example, if `e` represents the expression `fun x y => x + y`, +then `instantiateRev e.bindingBody!.bindingBody! #[a, b]` yields `a + b`. +The `instantiate` function on the other hand would yield `b + a`, since de Bruijn indices count outwards. + -/ @[extern "lean_expr_instantiate_rev"] opaque instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr /-- -Similar to `instantiate`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`. -Function panics if `beginIdx <= endIdx <= xs.size` does not hold. +Similar to `Lean.Expr.instantiate`, but considers only the substitutions `subst` in the range `[beginIdx, endIdx)`. +Function panics if `beginIdx <= endIdx <= subst.size` does not hold. + +This function is equivalent to `instantiate e (subst.extract beginIdx endIdx)`, but it does not allocate a new array. + +This instantiates with the "backwards" indexing scheme. +See also `Lean.Expr.instantiateRevRange`, which instantiates with the "forwards" indexing scheme. -/ @[extern "lean_expr_instantiate_range"] -opaque instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr +opaque instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (subst : @& Array Expr) : Expr /-- -Similar to `instantiateRev`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`. -Function panics if `beginIdx <= endIdx <= xs.size` does not hold. +Similar to `Lean.Expr.instantiateRev`, but considers only the substitutions `subst` in the range `[beginIdx, endIdx)`. +Function panics if `beginIdx <= endIdx <= subst.size` does not hold. + +This function is equivalent to `instantiateRev e (subst.extract beginIdx endIdx)`, but it does not allocate a new array. + +This instantiates with the "forwards" indexing scheme (see the docstring for `Lean.Expr.instantiateRev` for an example). +See also `Lean.Expr.instantiateRange`, which instantiates with the "backwards" indexing scheme. -/ @[extern "lean_expr_instantiate_rev_range"] -opaque instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr +opaque instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (subst : @& Array Expr) : Expr /-- Replace free (or meta) variables `xs` with loose bound variables. -/ @[extern "lean_expr_abstract"]