Tactics to manipulate let expressions

let extraction

Extracting lets means to locate let/letFuns in a term and to extract them from the term, extending the local context with new declarations in the process. A related process is lifting lets, which means to move let/letFuns toward the root of a term.

structure Lean.Meta.ExtractLets.LocalDecl' : Type

• decl : LocalDecl
• isLet : Bool

  If true, is a let, if false, is a letFun. Used in lift mode.

structure Lean.Meta.ExtractLets.State : Type

• givenNames : List Name

  Names to use for local definitions for the extracted lets.

• decls : Array LocalDecl'

  Saved declarations for the extracted lets.

• valueMap : ExprStructMap FVarId

  Map from let values to fvars. To support the merge option.

instance Lean.Meta.ExtractLets.instInhabitedState : Inhabited State

@[reducible, inline]

abbrev Lean.Meta.ExtractLets.M (α : Type) : Type

def Lean.Meta.ExtractLets.hasNextName : M Bool

Returns true if nextName? would return a name.

def Lean.Meta.ExtractLets.nextName? : M (Option Name)

Gets the next name to use for extracted lets

def Lean.Meta.ExtractLets.nextNameForBinderName? (binderName : Name) : M (Option Name)

Generate a name to use for a new local declaration, derived possibly from the given binder name. Returns none iff hasNextName is false.

def Lean.Meta.ExtractLets.extractable (fvars : List Expr) (e : Expr) : Bool

Returns 'true' if e does not depend on any of the fvars in fvars.

def Lean.Meta.ExtractLets.isExtractableLet (fvars : List Expr) (n : Name) (t v : Expr) : M (Bool × Name)

Returns whether a let-like expression with the given type and value is extractable, given the list fvars of binders that inhibit extraction.

def Lean.Meta.ExtractLets.addDecl (decl : LocalDecl) (isLet : Bool) : M Unit

Adds the decl to the decls list. Assumes that decl is an ldecl.

def Lean.Meta.ExtractLets.flushDecls (fvar : FVarId) : M (Array LocalDecl')

Removes and returns all local declarations that (transitively) depend on fvar.

def Lean.Meta.ExtractLets.withEnsuringDeclsInContext {m : Type → Type} {α : Type} [Monad m] [MonadControlT MetaM m] [MonadLCtx m] (decls : Array LocalDecl') (k : m α) : m α

Ensures that the given local declarations are in context. Runs k in that context.

def Lean.Meta.ExtractLets.mkLetDecls (decls : Array LocalDecl') (e : Expr) : MetaM Expr

Closes all the local declarations in e, creating let and letFun expressions. Does not require that any of the declarations are in context. Assumes that e contains no metavariables with local contexts that contain any of these metavariables (the extraction procedure creates no new metavariables, so this is the case).

This should not be used when closing lets for new goal metavariables, since

1. The goal contains the decls in its local context, violating the assumption.
2. We need to use true lets in that case, since tactics may zeta-delta reduce these declarations.

def Lean.Meta.ExtractLets.ensureIsLet (fvarId : FVarId) : M Unit

Makes sure the declaration for fvarId is marked with isLet := true. Used in lift + merge mode to ensure that, after merging, if any version was a let then it's a let rather than a letFun.

def Lean.Meta.ExtractLets.withDeclInContext {α : Type} (fvarId : FVarId) (k : M α) : M α

Ensures that the given fvarId is in context by adding decls from the state. Simplification: since we are not recording which decls depend on which, but we do know all dependencies come before a particular decl, we add all the decls up to and including fvarId.

Used for merge feature.

def Lean.Meta.ExtractLets.initializeValueMap : M Unit

Initializes the valueMap with all the local definitions that aren't implementation details. Used for merge feature when useContext is enabled.

def Lean.Meta.ExtractLets.containsLet (e : Expr) : Bool

Returns true if the expression contains a let expression or a letFun (this does not verify that the letFuns are well-formed). Its purpose is to be a check for whether a subexpression can be skipped.

partial def Lean.Meta.ExtractLets.extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false) : M Expr

Extracts lets from e.

• fvars is an array of all the local variables from going under binders, used to detect whether an expression is extractable. Extracted lets do not have their fvarids in this list. This is not part of the cache key since it's an optimization and in principle derivable.
• topLevel is whether we are still looking at the top-level expression. The body of an extracted top-level let is also considered to be top-level. This is part of the cache key since it affects what is extracted.

Note: the return value may refer to fvars that are not in the current local context, but they are in the decls list.

partial def Lean.Meta.ExtractLets.extractCore.extractBinder (fvars : List Expr) (n : Name) (t b : Expr) (i : BinderInfo) (mk : Expr → Expr → Expr) : M Expr

partial def Lean.Meta.ExtractLets.extractCore.extractLetLike (fvars : List Expr) (isLet : Bool) (n : Name) (t v b : Expr) (mk : Expr → Expr → Expr → M Expr) (topLevel : Bool) : M Expr

partial def Lean.Meta.ExtractLets.extractCore.extractLetFun (fvars : List Expr) (e : Expr) (topLevel : Bool) : M Expr

e is the letFun expression

partial def Lean.Meta.ExtractLets.extractCore.extractApp (fvars : List Expr) (f : Expr) (args : Array Expr) : M Expr

def Lean.Meta.ExtractLets.extractTopLevel (e : Expr) : M Expr

def Lean.Meta.ExtractLets.extract (es : Array Expr) : M (Array Expr)

Main entry point for extracting lets.

def Lean.Meta.extractLets {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT MetaM m] (es : Array Expr) (givenNames : List Name) (k : Array FVarId → Array Expr → List Name → m α) (config : ExtractLetsConfig := { }) : m α

Extracts let and letFun expressions into local definitions, evaluating k at the post-extracted expressions and the extracted fvarids, within a context containing those local declarations.

• The givenNames is a list of explicit names to use for extracted local declarations. If a name is _ (or if there is no provided given name and config.onlyGivenNames is true) then uses a hygienic name based on the existing binder name.

def Lean.Meta.liftLets (e : Expr) (config : LiftLetsConfig := { }) : MetaM Expr

Lifts let and letFun expressions in the given expression as far out as possible.

def Lean.MVarId.extractLets (mvarId : MVarId) (givenNames : List Name) (config : Meta.ExtractLetsConfig := { }) : MetaM ((Array FVarId × List Name) × MVarId)

Extracts let and letFun expressions from the target, returning FVarIds for the extracted let declarations along with the new goal.

• The givenNames is a list of explicit names to use for extracted local declarations. If a name is _ (or if there is no provided given name and config.onlyGivenNames is true) then uses a hygienic name based on the existing binder name.

def Lean.MVarId.extractLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (givenNames : List Name) (config : Meta.ExtractLetsConfig := { }) : MetaM ((Array FVarId × List Name) × MVarId)

Like Lean.MVarId.extractLets but extracts lets from a local declaration. If the local declaration has a value, then both its type and value are modified.

def Lean.MVarId.liftLets (mvarId : MVarId) (config : Meta.LiftLetsConfig := { }) : MetaM MVarId

Lifts let and letFun expressions in target as far out as possible. Throws an exception if nothing is lifted.

Like Lean.MVarId.extractLets, but top-level lets are not added to the local context.

def Lean.MVarId.liftLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (config : Meta.LiftLetsConfig := { }) : MetaM MVarId

Like Lean.MVarId.liftLets but lifts lets in a local declaration. If the local declaration has a value, then both its type and value are modified.