How do I run a def-like command from inside a run_cmd?

Stream: new members

[Eduardo Ochs]

Hi all,

I am a newbie trying to do advanced things :oh_no:, like manipulating Syntax and TSyntax objects, and generating several kinds of diagrams from them - see this thread, and my page on Lean...

[Eduardo Ochs]

Now I am looking for a way to, ahem, "export a syntax object from a run_cmd by calling a def-like function inside the run_cmd". For example, this code prints a syntax object both "as a term" and "as its repr":

import Lean

run_cmd do
  let stx <- `(fun a => a+2)
  Lean.logInfo m!"{stx}"
  Lean.logInfo m!"{repr stx}"
  -- mydef `bla stx

-- #eval bla
-- #eval repr bla

[Eduardo Ochs]

Screenshot:
sshot.png

[Eduardo Ochs]

The commented lines above - the mydef and the two last #evals - show what I would like to have. The mydef `bla stx would do something like def bla := <currentvalueofstx>, and this bla would accessible outside the run_cmd; the two commented #evals would print the value of that bla.

[Eduardo Ochs]

It seems that mkDefViewOfDef - that generates a DefView structure - does a part of what I need, but its code is too complex for me...

[Eduardo Ochs]

Anyone knows how to write that mydef? A fragile one-minute hack with no error-checking at all would be more than enough! Thanks in advance... :upside_down::upside_down::upside_down:

[Mario Carneiro]

import Lean

open Lean Elab Command
def mydef (name : Name) (stx : TSyntax `term) : CommandElabM Unit := do
  elabCommand (← `(command| def $(mkIdent name) := $stx))

run_cmd
  let stx ← `(fun a => a+2)
  Lean.logInfo m!"{stx}"
  Lean.logInfo m!"{repr stx}"
  mydef `bla stx

#eval (bla 1)
#eval repr (bla 1)

[Mario Carneiro]

note that your original #eval bla fails because the resulting expression has type Nat -> Nat

[Mario Carneiro]

you can #print bla if you want to see that it was defined as intended

[Eduardo Ochs]

Wow and thanks, but that's not exactly what I was looking for... I wanted to store in bla the syntax object that appears in the right side of the screenshot, and that looks like this: { raw := ... }

[Eduardo Ochs]

I think that we will have to modify the environment in a more low-level-ish way - and that's why I was trying to understand DefViews...

[Eric Wieser]

def bla := Unhygienic.run `(fun a => a+2)?

[Eduardo Ochs]

@Eric Wieser, perfect! Thanks! =)