Transforming nondependent lets into haves

A let expression let x : t := v; b is nondependent if fun x : t => b is type correct. Nondependent lets are those that can be transformed into have x := v; b. This module has a procedure that detects which lets are nondependent and does the transformation, attempting to do so efficiently.

Dependence checking is approximated using the withTrackingZetaDelta technique: given let x := v; b, we add a x := v declaration to the local context, and then type check b with withTrackingZetaDelta enabled to record whether x is unfolded. If x is not unfolded, then we know that b does not depend on v. This is a conservative check, since isDefEq may unfold local definitions unnecessarily.

We do not use Lean.Meta.check directly. A naive algorithm would be to do Meta.check (b.instantiate1 x) for each let body, which would involve rechecking subexpressions multiple times when there are nested lets, and furthermore we do not need to fully typecheck the body when evaluating dependence. Instead, we re-implement a type checking algorithm here to be able to interleave checking and transformation.

The trace class trace.Meta.letToHave reports statistics.

The transformation has very limited support for metavariables. Any let that contains a metavariable remains a let for now.

Optimizations, present and future:

• We can avoid doing the transformation if the expression has no lets.
• We can also avoid doing the transformation to let-free subexpressions that are not inside a let, however checking for lets is O(n), so we only try this for expressions with a small approxDepth. (We can consider precomputing this somehow.)
  • The cache is currently responsible for the check.
  • We also do it before entering telescopes, to avoid unnecesasry fvar overhead.
• If we are not currently inside a let, then we do not need to do full typechecking.
• We try to reuse Exprs to promote subexpression sharing.
• We might consider not transforming lets to haves if we are in a proof that is not inside a let. For now we assume abstractNestedProofs has already been applied.

instance Lean.Meta.LetToHave.instInhabitedResult : Inhabited Lean.Meta.LetToHave.Result✝

Equations

• Lean.Meta.LetToHave.instInhabitedResult = { default := { expr := default, type? := default } }

def Lean.Meta.letToHave (e : Expr) : MetaM Expr

Transforms nondependent let expressions into have expressions. If e is not type correct, returns e. The Meta.letToHave trace class logs errors and messages.

Equations

• One or more equations did not get rendered due to their size.