Idiomatic way to add declarations to a LocalContext

Stream: metaprogramming / tactics

[Ernest Ng]

Hi! I was wondering what is the idiomatic way to add extra declarations to a LocalContext?

For context, I am inheriting a codebase in which the following function is used to add extra decls to the LocalContext, and I am unsure if this implementation is the correct way of doing things:

-- For each `(arg, ty)` pair in `Array.zip argNames input_types`,
-- `mkInputLocalContext` adds a new declaration `arg : ty` is added to the local
-- context. The resultant LocalContext is returned by this function.
-- Invariant: `input_types.size == argNames.size`
def mkInputLocalContext (input_types : Array Expr) (argNames: Array String)
: MetaM LocalContext
:= do
   let mut lctx ← getLCtx
   for (arg, ty) in argNames.zip input_types do
    let argname := Name.mkStr1 arg
    let fvarid ←  mkFreshFVarId
    input_args := input_args.push fvarid
    lctx :=  mkLocalDecl lctx fvarid argname ty
  return lctx

Specifically, I am unsure whether the technique of first calling mkFreshFVarId and then calling mkLocalDecl is the recommended way of adding decls, since the docs for mkLocalDecl that mkLocalDecl should not be called directly.

I was wondering if the idiomatic solution is instead to use Meta.withLocalDecl instead? However, I see that Meta.withLocalDecl reverts the context after it is called, and I was wondering if there is an function analogous to withLocalDecl which provides the caller with the updated local context (after the extra decls have been added)?

Thanks!

[Kyle Miller]

withLocalDecl is idiomatic, and you can get the local context from inside it with getLCtx

[Kyle Miller]

withLocalDecls lets you add many at once

[Ernest Ng]

Thanks for the quick reply! I saw in the docs for withLocalDecl that it "reverts the context" after it is called, and I was wondering if there is a variant of withLocalDecl that doesn't revert the context?

[Kyle Miller]

No, that's not possible, since the local context is part of the monad's reader state. It's not actively being reverted, but rather you leave the scope where it's temporarily been changed.

[Kyle Miller]

In any case, that doesn't matter, because you can use getLCtx from within that callback to obtain the local context. You can do whatever you want with it.

[Kyle Miller]

import Lean

open Lean Meta

def mkInputLocalContext (inputTypes : Array Expr) (argNames: Array String) :
    MetaM LocalContext := do
  let spec := inputTypes.zip argNames |>.map fun (ty, name) => (Name.mkSimple name, .default, fun _ => return ty)
  withLocalDecls spec fun _ => getLCtx

[Ernest Ng]

Ah I see that makes sense, thanks! It seems like calling getLCtx within the callback (continuation) that is passed to withLocalDecls is the preferred way of "explicitly threading" the LocalContext between different function calls.

[Kyle Miller]

That's not necessarily the case; it's often better to run your code from within withLocalDecls rather than working with the local context itself, threading it around.

That said, it does happen, and for that there's withLCtx. Notice that it also takes a list that caches the local instances. That's one of the things that withLocalDecl properly manages for you.

[Kyle Miller]

(I should say that there's a good amount of code out there that uses the mkLocalDecl interface, but it's pretty low level and it's usually done for some specialized low-level optimization. It's best to avoid it unless you know you really need it.)

[Ernest Ng]

Ah that's fair, good point! It looks like withLocalDecl also properly handles the low-level operations associated with managing FVarIds (since it takes in a Name and a type and adds it to the context for you), and using withLocalDeclsto add a bunch of declarations to the LocalContext is to be preferred over managing FVarIds yourself.