Converting between Expr and Syntax objects

Stream: lean4

[Leni Aniva]

What is the canonical way to convert from Strings to (parsing) Syntax to (elaboration) Exprs and back? I found an old thread about ToExpr which can convert a few types to Expr objects. I think it has something to do with the elaborator.

[Leni Aniva]

When I looked at the code of lean-gym (from lean 3,
https://github.com/openai/lean-gym/blob/main/src/util/tactic.lean) I see this:

meta def parse_itactic_reflected (tactic_string : string) : tactic expr := do
let itactic_string := "{ " ++ tactic_string ++  " }",
r ← run_on_input parser.itactic_reflected itactic_string,
pure $ reflected_value.expr r

/-- Parse an interactive tactic from a string. -/
meta def parse_itactic (tactic_string : string) : tactic (tactic string) :=
do
  rtac ← parse_itactic_reflected tactic_string,
  u ← eval_expr (tactic unit) rtac,
  pure (u *> pure tactic_string)

and I don't know where is the analogous structure in lean 4. Is there any documentation about the parser that i can read up?

[Leni Aniva]

For expr and tactic printing there's the PrettyPrinter but I don't know about parsing

[Mario Carneiro]

• Strings are parsed into Syntax by the Parser module
• Syntax is parsed into Expr by elaboration, e.g. elabTerm
• Expr is turned back into Syntax by delaboration, i.e. delab

[Mario Carneiro]

the lean 3 code will not be very helpful, the internals have changed quite significantly

[Mario Carneiro]

could you explain more precisely what you want to do? (#xy)

[Leni Aniva]

Mario Carneiro said:

could you explain more precisely what you want to do? (#xy)

I want to recreate lean-gym in lean4, and it boils down to 1. creating environments (I know how to do now) 2. running tactics 3. parsing tactics from inputs 4. printing current proof state

[Mario Carneiro]

I think you might find https://github.com/leanprover-community/repl useful, it is primarily intended as a gym-like environment

[Leni Aniva]

Mario Carneiro said:

I think you might find https://github.com/leanprover-community/repl useful, it is primarily intended as a gym-like environment

I've read into the code of this and it seem to delegate proof state manipulation and parsing to lean's internals, so I am asking about it here.

[Mario Carneiro]

what about those internals do you want to know?

[Mario Carneiro]

parsing is done by delegating to lean to do the parsing

[Mario Carneiro]

that's true in lean 3 as well

[Leni Aniva]

Mario Carneiro said:

what about those internals do you want to know?

I want to know how to parse expressions/tactics from strings into syntax trees, how to elaborate syntaxes into expressions, and how to pretty print expressions back into strings (which I think uses the PrettyPrinter)

[Mario Carneiro]

Isn't that all being done in the repl code?

[Mario Carneiro]

start from a string -> parse it into a command -> elaborate the command -> print the result

[Mario Carneiro]

the only difference is that you might want a different syntax category for the parser if you are parsing a tactic instead of a command

[Leni Aniva]

Yes, but the REPL doesn't allow me access to the syntax and proof state objects generated by executing the user commands. Do you think it would be a good idea to look into IO.processInput in order to get a whole picture of what Lean is doing under the hood?

[Mario Carneiro]

it does

[Mario Carneiro]

the syntax is literally manipulated by the program

[Mario Carneiro]

Actually you might find the ast_export branch a bit more useful: https://github.com/leanprover-community/repl/blob/ast_export/REPL/Main.lean

[Mario Carneiro]

the main function here replaces the original top level command loop to collect the AST from every command and then print it out as json

[Mario Carneiro]

specifically this line

    let s ← IO.processCommands inputCtx parserState commandState

runs the lean frontend and the resulting s.commands contains the AST for every command

[Mario Carneiro]

This is assuming you are doing parsing "outside lean", i.e. you have to run the frontend command loop yourself

[Mario Carneiro]

if you are "inside lean", i.e. writing a command or tactic which when elaborated needs to parse something, it is a bit easier

[Anand Rao Tadipatri]

Leni V. Aniva said:

Mario Carneiro said:

could you explain more precisely what you want to do? (#xy)

I want to recreate lean-gym in lean4, and it boils down to 1. creating environments (I know how to do now) 2. running tactics 3. parsing tactics from inputs 4. printing current proof state

@Leni V. Aniva There are a few existing implementations of lean-gym in Lean4 that you might find useful: Daniel Selsam's code works for an older version of Lean4, Patrick Massot's code is a more up-to-date version, and my code contains minor modifications for more user-friendly input.