Accessing environment during tests

Stream: lean4

[Thomas Murrills]

Many functions take an environment as an argument. Is there a nice way to test them using the current environment? For example, in the following example I need both the type annotation and the do block:

structure Foo where
makeFoo ::
  x : Nat

#eval ((do return ((getStructureCtor (← getEnv) ``Foo).name)) : CoreM Name)
-- <namespace>.Foo.makeFoo

It would be nicer to use something like

#evalWithEnv (getStructureCtor #env ``Foo).name

Does something like this already exist? (If not, I might want to make it!)

[Mario Carneiro]

Is this only for non-monadic code?

[Thomas Murrills]

What do you mean by that? (Like, am I just trying to get rid of the monadic code, or, am I only trying to address the case where the return type is non-monadic, or something else? Yes and yes if either of the first two! Maybe I'm overestimating the number of functions that depend on the environment but don't wind up in a monad? I do have a very small sample after all... Also, remember that it's possible that there's a very basic way to play with the current environment and I just don't know about it...!)

[Mario Carneiro]

One simple option would be to give a MetaEval instance for Env -> A functions

[Mario Carneiro]

import Lean
open Lean

structure Foo where
makeFoo ::
  x : Nat

instance [Eval α] : MetaEval (Environment → α) where
  eval env _ f hideUnit := do Eval.eval (fun _ => f env) hideUnit; pure env

#eval fun env => (getStructureCtor env ``Foo).name

[Thomas Murrills]

Wow, nice! That's really neat! :D That's pretty close to perfect. I'll need to learn more about how eval works before I understand how it works, though :) In the meantime it'll still be extremely useful! Thanks!