Tactics to manipulate let expressions

let extraction

Extracting lets means to locate let/haves 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/haves toward the root of a term.

structure Lean.Meta.ExtractLets.LocalDecl' : Type

• decl : LocalDecl

  An ldecl with nondep := false.

• isLet : Bool

  If true, is a let, if false, is a have. 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 with nondep := false.

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) : Expr

Closes all the local declarations in e, creating let and have 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 have.

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 have. 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) (e : Expr) (isLet : Bool) (n : Name) (t v b : Expr) (topLevel : Bool) : M Expr

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 have 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 have 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 have 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 have 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.

Let-to-have transformation

A meta tactic version of Lean.Meta.letToHave.

def Lean.MVarId.letToHave (mvarId : MVarId) (failIfUnchanged : Bool := true) : MetaM MVarId

Transforms lets to haves in the target. Throws an error if no progress is made.

def Lean.MVarId.letToHaveLocalDecl (mvarId : MVarId) (fvarId : FVarId) (failIfUnchanged : Bool := true) : MetaM MVarId

Transforms lets to haves in the type of fvarId. Throws an error if no progress is made.