02c8c2f9e1
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x : t := v; b` is called *nondependent* if `fun x : t => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface: - Local context `ldecl`s with `nondep := true` are generally treated as `cdecl`s. This is because in the body of a `have` expression the variable is opaque. Functions like `LocalDecl.isLet` by default return `false` for nondependent `ldecl`s. In the rare case where it is needed, they take an additional optional `allowNondep : Bool` flag (defaults to `false`) if the variable is being processed in a context where the value is relevant. - Functions such as `mkLetFVars` by default generalize nondependent let variables and create lambda expressions for them. The `generalizeNondepLet` flag (default true) can be set to false if `have` expressions should be produced instead. **Breaking change:** Uses of `letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet := false`. See the next item. - There are now some mapping functions to make telescoping operations more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`. There is also `mapLetDecl` as a counterpart to `withLetDecl` for creating `let`/`have` expressions. - Important note about the `generalizeNondepLet` flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the `value` field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using `mapLetDecl` is always fine. - The simplifier will cache its let dependence calculations in the nondep field of let expressions. - The `intro` tactic still produces *dependent* local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent `intro` from creating a local variable whose value cannot be used. Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck `letE n t v b true` as if it were `app (lam n t b default) v` and please report issues. This PR follows up from #8751, which made sure the nondep flag was preserved in the C++ interface.
175 lines
7.5 KiB
Text
175 lines
7.5 KiB
Text
/-
|
||
Copyright (c) 2022 E.W.Ayers. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: E.W.Ayers
|
||
-/
|
||
prelude
|
||
import Lean.Meta.Basic
|
||
import Lean.SubExpr
|
||
|
||
/-!
|
||
|
||
# Expression Lenses
|
||
|
||
Functions for manipulating subexpressions using `SubExpr.Pos`.
|
||
|
||
-/
|
||
|
||
namespace Lean.Meta
|
||
|
||
section ExprLens
|
||
|
||
open Lean.SubExpr
|
||
|
||
variable [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
|
||
|
||
/-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it.
|
||
If the subexpression is under a binder it will instantiate and abstract the binder body correctly.
|
||
Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types.
|
||
|
||
See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/
|
||
private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
|
||
match n, e with
|
||
| 0, .app f a => return e.updateApp! (← g f) a
|
||
| 1, .app f a => return e.updateApp! f (← g a)
|
||
| 0, .lam _ y b _ => return e.updateLambdaE! (← g y) b
|
||
| 1, .lam n y b c => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
|
||
| 0, .forallE _ y b _ => return e.updateForallE! (← g y) b
|
||
| 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
|
||
| 0, .letE _ y a b _ => return e.updateLetE! (← g y) a b
|
||
| 1, .letE _ y a b _ => return e.updateLetE! y (← g a) b
|
||
| 2, .letE n y a b nondep => mapLetDecl n y a (nondep := nondep) (usedLetOnly := false) fun x => g <| b.instantiate1 x
|
||
| 0, .proj _ _ b => e.updateProj! <$> g b
|
||
| n, .mdata _ a => e.updateMData! <$> lensCoord g n a
|
||
| 3, _ => throwError "Lensing on types is not supported"
|
||
| c, e => throwError "Invalid coordinate {c} for {e}"
|
||
|
||
private def lensAux (g : Expr → M Expr) : List Nat → Expr → M Expr
|
||
| [], e => g e
|
||
| head::tail, e => lensCoord (lensAux g tail) head e
|
||
|
||
/-- Run the given `replace` function to replace the expression at the subexpression position. If the subexpression is below a binder
|
||
the bound variables will be appropriately instantiated with free variables and reabstracted after the replacement.
|
||
If the subexpression is invalid or points to a type then this will throw. -/
|
||
def replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Expr) : M Expr :=
|
||
lensAux replace p.toArray.toList root
|
||
|
||
/-- Runs `k` on the given coordinate, including handling binders properly.
|
||
The subexpression value passed to `k` is not instantiated with respect to the
|
||
array of free variables. -/
|
||
private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) (n : Nat) (e : Expr) : M α := do
|
||
match n, e with
|
||
| 3, _ => throwError "Internal: Types should be handled by viewAux"
|
||
| 0, .app f _ => k fvars f
|
||
| 1, .app _ a => k fvars a
|
||
| 0, .lam _ y _ _ => k fvars y
|
||
| 1, .lam n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
|
||
| 0, .forallE _ y _ _ => k fvars y
|
||
| 1, .forallE n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
|
||
| 0, .letE _ y _ _ _ => k fvars y
|
||
| 1, .letE _ _ a _ _ => k fvars a
|
||
| 2, .letE n y a b _ => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
|
||
| 0, .proj _ _ b => k fvars b
|
||
| n, .mdata _ a => viewCoordAux k fvars n a
|
||
| c, e => throwError "Invalid coordinate {c} for {e}"
|
||
|
||
private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α
|
||
| [], e => k fvars <| e.instantiateRev fvars
|
||
| 3::tail, e => do
|
||
let y ← inferType <| e.instantiateRev fvars
|
||
viewAux (fun otherFvars => k (fvars ++ otherFvars)) #[] tail y
|
||
| head::tail, e => viewCoordAux (fun fvars => viewAux k fvars tail) fvars head e
|
||
|
||
/-- `view visit p e` runs `visit fvars s` where `s : Expr` is the subexpression of `e` at `p`.
|
||
and `fvars` are the free variables for the binders that `s` is under.
|
||
`s` is already instantiated with respect to these.
|
||
The role of the `visit` function is analogous to the `k` function in `Lean.Meta.forallTelescope`. -/
|
||
def viewSubexpr
|
||
(visit : (fvars : Array Expr) → (subexpr : Expr) → M α)
|
||
(p : Pos) (root : Expr) : M α :=
|
||
viewAux visit #[] p.toArray.toList root
|
||
|
||
private def foldAncestorsAux
|
||
(k : Array Expr → Expr → Nat → α → M α)
|
||
(acc : α) (address : List Nat) (fvars : Array Expr) (current : Expr) : M α :=
|
||
match address with
|
||
| [] => return acc
|
||
| 3 :: tail => do
|
||
let current := current.instantiateRev fvars
|
||
let y ← inferType current
|
||
let acc ← k fvars current 3 acc
|
||
foldAncestorsAux (fun otherFvars => k (fvars ++ otherFvars)) acc tail #[] y
|
||
| head :: tail => do
|
||
let acc ← k fvars (current.instantiateRev fvars) head acc
|
||
viewCoordAux (foldAncestorsAux k acc tail) fvars head current
|
||
|
||
/-- `foldAncestors k init p e` folds over the strict ancestor subexpressions of the given expression `e` above position `p`, starting at the root expression and working down.
|
||
The fold function `k` is given the newly instantiated free variables, the ancestor subexpression, and the coordinate
|
||
that will be explored next.-/
|
||
def foldAncestors
|
||
(k : (fvars: Array Expr) → (subexpr : Expr) → (nextCoord : Nat) → α → M α)
|
||
(init : α) (p : Pos) (e : Expr) : M α :=
|
||
foldAncestorsAux k init p.toArray.toList #[] e
|
||
|
||
end ExprLens
|
||
|
||
end Lean.Meta
|
||
|
||
namespace Lean.Core
|
||
|
||
open Lean.SubExpr
|
||
|
||
section ViewRaw
|
||
|
||
variable [Monad M] [MonadError M]
|
||
|
||
/-- Get the raw subexpression without performing any instantiation. -/
|
||
private def viewCoordRaw (e : Expr) (n : Nat) : M Expr := do
|
||
match e, n with
|
||
| e, 3 => throwError "Can't viewRaw the type of {e}"
|
||
| .app f _, 0 => pure f
|
||
| .app _ a, 1 => pure a
|
||
| .lam _ y _ _, 0 => pure y
|
||
| .lam _ _ b _, 1 => pure b
|
||
| .forallE _ y _ _, 0 => pure y
|
||
| .forallE _ _ b _, 1 => pure b
|
||
| .letE _ y _ _ _, 0 => pure y
|
||
| .letE _ _ a _ _, 1 => pure a
|
||
| .letE _ _ _ b _, 2 => pure b
|
||
| .proj _ _ b, 0 => pure b
|
||
| .mdata _ a, n => viewCoordRaw a n
|
||
| e, c => throwError "Bad coordinate {c} for {e}"
|
||
|
||
/-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
|
||
If the given `SubExpr` has a type subexpression coordinate, then throw an error.
|
||
|
||
This is a cheaper version of `Lean.Meta.viewSubexpr` and can be used to quickly view the
|
||
subexpression at a position. Note that because the resulting expression may contain
|
||
loose bound variables it can't be used in any `MetaM` methods. -/
|
||
def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
|
||
p.foldlM viewCoordRaw root
|
||
|
||
private def viewBindersCoord : Nat → Expr → Option (Name × Expr)
|
||
| 1, .lam n y _ _ => some (n, y)
|
||
| 1, .forallE n y _ _ => some (n, y)
|
||
| 2, .letE n y _ _ _ => some (n, y)
|
||
| _, _ => none
|
||
|
||
/-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/
|
||
def viewBinders (p : Pos) (root : Expr) : M (Array (Name × Expr)) := do
|
||
let (acc, _) ← p.foldlM (init := (#[], root)) fun (acc, e) c => do
|
||
let e₂ ← viewCoordRaw e c
|
||
let acc :=
|
||
match viewBindersCoord c e with
|
||
| none => acc
|
||
| some b => acc.push b
|
||
return (acc, e₂)
|
||
return acc
|
||
|
||
/-- Returns the number of binders above a given subexpr position. -/
|
||
def numBinders (p : Pos) (e : Expr) : M Nat :=
|
||
Array.size <$> viewBinders p e
|
||
|
||
end ViewRaw
|
||
|
||
end Lean.Core
|