Metaprogram that evaluates a function from the env

Stream: metaprogramming / tactics

[Adam Topaz]

Hi all,

I'm trying to write a metaprogram that accomplishes what the title suggests. Namely, I want to evaluate functions from the environment. Here's a possible skeleton:

import Lean

open Lean

def foo : Nat → Nat := fun x => x + 1
def bar : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+2 => bar n + bar (n+1)

def baz (name : Name) (input : Nat) : CoreM Nat := sorry


/-
Expected behavior:
#eval baz `foo 1 -- 2
#eval baz `bar 1 -- 1
-/

Is there an established way to do this? I can think of some hacky approach where I extract the value of the constant associated to the name from the environment as an Expr, and do something with that, but I feel like this is not the best way to go about this. Anyone have any hints?

[Damiano Testa]

I have not looked at this yet, but @Eric Wieser just introduced docs#Mathlib.Meta.elabEvalExpr: does it help?

[Adam Topaz]

oh, nice, yes I think I can make that work.

[Adam Topaz]

or at least extract some code from the implementation

[Damiano Testa]

You probably still have to combine it with some Environment.find?, though.

[Adam Topaz]

yeah, that's not the problem

[Adam Topaz]

oh, but that gives the result as an Expr, which is fine if I'm trying to write an elaborator, but maybe not if I want to use the actual value in another metaprogram.

[Adam Topaz]

so in that case the signature would be CoreM Expr, and not CoreM Nat.

[Damiano Testa]

Oh, then you may have to use evalExpr, or whatever it is called...

[Adam Topaz]

docs#Lean.Meta.evalExpr

[Adam Topaz]

Yes, that will do it! Thanks!

[Damiano Testa]

To be honest, every time that I thought that I needed evalExpr, I realized that I was better off not using it...

[Adam Topaz]

well, it works:

import Lean

open Lean

def foo : Nat → Nat := fun x => x + 1
def bar : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+2 => bar n + bar (n+1)

unsafe
def baz (name : Name) (input : Nat) : MetaM Nat := do
  let e := mkAppN (mkConst name) #[mkNatLit input]
  Lean.Meta.evalExpr Nat (.const `Nat []) e

#eval baz `foo 1 -- 2
#eval baz `bar 1 -- 1

[Adam Topaz]

but in MetaM, which is fine.

[Patrick Massot]

From a recent paper:

unsafe def runFunctionOn (function : String) (a : ℕ) : CoreM ℕ := do
  let myFun ← evalConst (ℕ → ℕ) (Name.mkSimple function)
  return myFun a

def foo (a : ℕ) := 2*a + 1

#eval runFunctionOn "foo" 1 -- returns 3

#eval runFunctionOn "baz" 1 -- fails with error message: unknown declaration baz

def bar (a : String) := a ++ a

#eval runFunctionOn "bar" 1 -- crashes Lean

[Adam Topaz]

Which paper?

[Patrick Massot]

verbose_paper.pdf

[Patrick Massot]

I should put this on arXiv.

[Patrick Massot]

It’s recent almost as in “a recent Mathlib”, it was written two days ago.

[Patrick Massot]

I can’t tell you where it is submitted because it’s a secret, although I heard that crypto people can sometimes break secret through timing attacks.

[Adam Topaz]

I think I can run a timing attack on your secret :)

[Floris van Doorn]

Patrick Massot said:

I can’t tell you where it is submitted because it’s a secret, although I heard that crypto people can sometimes break secret through timing attacks.

Or by looking at the metadata (e.g. layout) :laughing:

[Notification Bot]

21 messages were moved here from #metaprogramming / tactics > Metaprogram that evaluates a function from the env by Gareth Ma.

[Gareth Ma]

Oh my god wait I moved the wrong thread

[Notification Bot]

23 messages were moved here from #metaprogramming / tactics > setm development thread by Gareth Ma.

[Mario Carneiro]

Floris van Doorn said:

Patrick Massot said:

I can’t tell you where it is submitted because it’s a secret, although I heard that crypto people can sometimes break secret through timing attacks.

Or by looking at the metadata (e.g. layout) :laughing:

Yes, as we can see it's for the very prestigious CVIT conference on Very Important Topics