eval mere String as Lean code

Stream: Is there code for X?

[Asei Inoue]

Is there a way to evaluate a String as Lean code?

For example, is there a way to implement evalString function which can be used as following?

def str := "Nat.zero"

-- this should report `0 : Nat`
#eval evalString str

[Siddhartha Gadgil]

You can get term syntax by using runParserCategory and then use elabTerm.

[Asei Inoue]

@Siddhartha Gadgil Thank you.

I have tried writing code based on your suggestion, but I get an error.

import Lean

open Lean Parser Elab Command Term

def evalString (cat : Name) (s : String) : MetaM Unit := do
  let output := runParserCategory (← getEnv) cat s
  match output with
  | .error e => throwError e
  | .ok s =>
    /-
    type mismatch
      elabTerm s (some (Lean.mkConst `String))
    has type
      TermElabM Expr : Type
    but is expected to have type
      MetaM ?m.415 : Type
    -/
    let term ← elabTerm s (expectedType? := mkConst `String)
    logInfo m!"{term}"

run_meta evalString `term "Nat.zero"

[Siddhartha Gadgil]

Your type must be TermElabM String

[Siddhartha Gadgil]

You can use run' to reduce to MetaM from TermElabM