Reading Expr

Stream: lean4

[Tomaz Gomes]

Is there a way to transform Syntax representing directly an Expr into an Expr? For instance, in the following code:

elab "%dynDelab" t:term : term => sorry

def t : (%dynDelab (Expr.const `Nat [])) → (%dynDelab (Expr.const `Nat [])) := fun x => x

how could I fill the sorry? I tried using elabTerm but then I got the following error in t:

type expected, got
  (Expr.const `Nat [] : Expr)

It seems that Lean delaborated it back to the Expr, instead of Nat... I printed the representation of the output of elabTerm and it was something a lot bigger than the original Expr:

h = Lean.Expr.app
  (Lean.Expr.app
    (Lean.Expr.const `Lean.Expr.const [])
    (Lean.Expr.app (Lean.Expr.const `Lean.Name.mkStr1 []) (Lean.Expr.lit (Lean.Literal.strVal "Nat"))))
  (Lean.Expr.app
    (Lean.Expr.const `List.nil [Lean.Level.mvar (Lean.Name.mkNum `_uniq 1621)])
    (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 1622)))

I believe I need something like deriving Read from Haskell in the type Expr

[Henrik Böving]

So, what you are giving elabTerm here is a Syntax object that described the construction of an Expr object. Not actually an Expr object itself (you are basically confusing the meta level and the language level here). I guess what you really want is more or less an eval type of stuff? I know we have evalConst but I'm not sure whether we also have evalExpr.

[Eric Wieser]

Tangentially; we have docs#ToExpr for turning a value into the Expr that represents it; do we have something similar that converts things to the corresponding syntax?

[Eric Wieser]

Or is the idea to convert to an expression, and then hand that to the global delaborators?

[Mario Carneiro]

We do have docs4#Lean.Meta.evalExpr

[Mario Carneiro]

to be more precise, what is needed for dynDelab% is to call elabTerm to convert the result into an Expr representing an expr, and then call evalExpr on the result to turn it into the expr you want

[Mario Carneiro]

Regarding @Eric Wieser 's question, to turn an expr into syntax requires the delaborator, the entry point is docs4#Lean.PrettyPrinter.delab

[Kyle Miller]

Eric Wieser said:

Tangentially; we have docs#ToExpr for turning a value into the Expr that represents it; do we have something similar that converts things to the corresponding syntax?

There's docs4#Lean.Quote.quote. There's also docs4#Lean.Elab.Term.exprToSyntax for embedding an Expr into syntax, which can often work.

[Eric Wieser]

Can I use any of these in MacroM?

[Tomaz Gomes]

thanks, I could get exactly the effect I wanted:

import Std
import Lean

open Lean Meta Elab

elab "%dynDelab" t:term : term => do
  let h ← Term.elabTerm t none
  let h' ← unsafe (evalExpr Expr (mkConst ``Expr) h)
  return h'

def idNat' : (%dynDelab (Expr.const `Nat [])) → (%dynDelab (Expr.const `Nat [])) :=
  fun x => x

#check idNat' -- idNat' (a : Nat) : Nat