Lean 4 version of eval_expr

Stream: lean4

[Notification Bot]

Tomas Skrivan has marked this topic as unresolved.

[Tomas Skrivan]

Ok I'm confused on how to use it. I want to synthesize an instance of a class and extract one field. Here is my attempt:

import Lean
open Lean Elab Meta Term

#eval ((do

  let E ← mkAppM `Add #[mkConst `Nat]
  let e ← synthInstance E
  let add_expr ← whnf (← mkProj `add 0 e)
  let T ← whnfD (← inferType add_expr)

  IO.println add_expr
  IO.println T.isConst  -- this is false .. so I can't use evalExpr?

  let add ← evalExpr (Nat → Nat → Nat) (???) add_expr   --- What should be `typeName`?

) : TermElabM Unit)

It looks like that evalExpr can't be used in this scenario :/

[Mario Carneiro]

I think you can just make def Foo := Nat -> Nat -> Nat and pass `Foo for typeName

[Tomas Skrivan]

Nope, getting unexpected type at evalExpr

[Mario Carneiro]

you can also skip evalExpr and use evalConst directly

[Tomas Skrivan]

But where it the dependence on add_expr ?

[Mario Carneiro]

?

[Mario Carneiro]

the code for elabEval, for example, contains a use of evalConst for a function type

[Tomas Skrivan]

In the code above:

- E - expression for Add Nat
- e - expression for instance of Add Nat
- add_expr - expression for Nat.add
- T - expression for Nat -> Nat -> Nat
I want to somehow convert add_expr : Expr to an actual element of Nat -> Nat -> Nat.

[Mario Carneiro]

Here's an adaptation of the elabEval code:

#eval show TermElabM Unit from do
  let E ← mkAppM `Add #[mkConst `Nat]
  let e ← synthInstance E

  let env ← getEnv
  let opts ← getOptions
  try
    let type ← inferType e
    let decl := Declaration.defnDecl {
      name        := `_bla
      levelParams := []
      type        := type
      value       := e
      hints       := ReducibilityHints.opaque
      safety      := DefinitionSafety.unsafe
    }
    Term.ensureNoUnassignedMVars decl
    addAndCompile decl
    let f ← evalConst (Nat → Nat → Nat) `_bla
    IO.println (f 1 2)
  finally setEnv env

[Gabriel Ebner]

If you're willing to (import / copy) from mathlib4, we have a slightly nicer API for evalExpr: https://github.com/leanprover-community/mathlib4/blob/e59238956369b84c3b506ef49ef7e5ceada183e5/Mathlib/Tactic/RunTac.lean#L15-L16

def mkArrow (a b : Expr) : Expr :=
  mkForall Name.anonymous BinderInfo.default a b

#eval show TermElabM _ from do
  let e ← synthInstance (← mkAppM `Add #[mkConst `Nat])
  let f ← unsafe evalExpr (Nat → Nat → Nat)
    (mkArrow (mkConst ``Nat) (mkArrow (mkConst ``Nat) (mkConst ``Nat))) e
  return f 1 2

[Tomas Skrivan]

Thanks a lot! Is there some documentation/part of a paper about the elaborator? It is a part of Lean I still have no clue about.

[Mario Carneiro]

Here's that code again in a more convenient package:

unsafe def withEvalExpr [Monad m] [MonadError m] [MonadFinally m]
  [MonadEnv m] [MonadOptions m] [MonadLiftT TermElabM m]
  (α : Type) (e : Expr) (f : α → m Unit) : m Unit := do
  let env ← getEnv
  let opts ← getOptions
  try
    let type ← (inferType e : TermElabM _)
    let decl := Declaration.defnDecl {
      name        := `_bla
      levelParams := []
      type        := type
      value       := e
      hints       := ReducibilityHints.opaque
      safety      := DefinitionSafety.unsafe
    }
    Term.ensureNoUnassignedMVars decl
    addAndCompile decl
    f (← evalConst α `_bla)
  finally setEnv env

#eval show TermElabM Unit from do
  let E ← mkAppM `Add #[mkConst `Nat]
  let e ← synthInstance E
  withEvalExpr (Nat → Nat → Nat) e fun f => do
    IO.println (f 1 2)

[Mario Carneiro]

not sure how this compares to the mathlib4 version

[Mario Carneiro]

no paper, it's the wild west

[Mario Carneiro]

yeah, the mathlib4 version is better, use that