Parsing a string into an expression

Stream: general

[Jason Rute]

I recently discovered that Lean can read from stdin. So now I'm curious if it is possible to do the following in Lean:

1. read in a string (representing a Lean term)
2. parse that string into an expression
3. evaluate (the term given by) that expression
4. print the output

(1) and (4) are easy, but what about (2) and (3)? I assume (3) is possible with the meta stuff, but (2), I have no idea.

[Jason Rute]

I'm actually more interested in this scenario so feel free to comment on that one also:

1. read in a string (representing a Lean Prop)
2. parse that string into an expression
3. set that expression as a goal
4. apply a tactic to that goal
5. print the result

[Jason Rute]

To be clear, I'm thinking about parsing Lean's syntax. (Of course, since expressions are algebraic data structures, one can could pass in say an s-expression for that expression and write a custom parser for those s-expressions.)

[Jason Rute]

Actually, as I think about it, even if there was no Lean syntax parser, I'd still be interested in the other steps (evaluating an expression and setting an expression as a goal).

[Simon Hudon]

For parsing an expression: lean.parser.with_input interactive.types.texpr my_string

[Simon Hudon]

it will give you a pexpr (plus a string) which you can feed into to_expr to elaborate the term into something that you can evaluate or create a goal from

[Simon Hudon]

To evaluate it, you have to write a routine by hand creating a value of type you're interested in from an expr. It can probably be automated with some meta programming

[Simon Hudon]

To set a goal with your expression:

v <- mk_meta_var e,
gs <- get_goals,
set_goals $ v :: gs

[Jason Rute]

Thanks! I will have to try this out.

[Tim Daly]

@Jason Rute I'm very interested in any code you write for this (obviously). Please make it available either publicly or email me.

[Jason Rute]

Sure, but I will warn you @Tim Daly that I am a hobbist, so I might not get around to it too quickly (or I might wake up tomorrow and want to give it a try :) ).

[Jason Rute]

@Simon Hudon I got this far, but I think I am mixing the parser and tactic monads. Do you know what I need to do here?

def experiment (s : string) : lean.parser unit :=
do
   pe <- lean.parser.with_input interactive.types.texpr s,  -- parser monad
   e <- to_expr pe.1,  -- tactic monad
   v <- mk_meta_var e,
   gs <- get_goals,
   set_goals $ v :: gs,
   t <- target,
   trace t,  -- should output the goal given by the string s
   return ()

[Jason Rute]

@Tim Daly You might be interested also in this thread. For example, I made a python prototype of communicating with Lean using the Lean server.

[Simon Hudon]

Yes, that's a very annoying separation when you need to invoke the parser. You can invoke tactic from parser but not the other way around. Figuring out how to get the user to call your automation can be tricky. If you only want to call tactic from parser, you can use lean.parser.of_tactic

[Simon Hudon]

For the other way around, it depends on how you want to invoke the script. If you want to call it from a normal proof script (in a begin end block), then we use the parse syntax. Otherwise, you can define a user_command using the attribute user_command and then you just write my_command . at the top level and it will call your script

[Mario Carneiro]

I don't think it is possible to use with_input when using lean --run

[Jason Rute]

So this:

meta def experiment (s : string) : lean.parser unit :=
do
   pe <- lean.parser.with_input interactive.types.texpr s,
   e <- lean.parser.of_tactic (tactic.to_expr pe.1),
   v <- lean.parser.of_tactic (tactic.mk_meta_var e),
   gs <- lean.parser.of_tactic (tactic.get_goals),
   lean.parser.of_tactic (tactic.set_goals $ v :: gs),
   t <- lean.parser.of_tactic tactic.target,
   lean.parser.of_tactic (tactic.trace t),
   return ()

run_cmd experiment "true"

is giving me an error at run_cmd: "vm check failed: dynamic_cast<vm_State*>(to_external(o)) (possibly due to incorrect axioms, or sorry)". Maybe this is related to what Mario was talking about about not being able to use lean.parser.with_input with lean --run.

[Sebastian Ullrich]

That's a bug, run_cmd should only accept tactics. lean.parser cannot be used outside of user-defined parser extensions (notations/commands/tactic params).

[Jason Rute]

@Simon Hudon Can you point me to examples of what you mean by "the parse syntax" or using user_command? (Or does Mario's comment mean what I want to do is ultimately doomed to fail?)

[Simon Hudon]

While it is fresh, can you file this run_cmd issue? I'd like to make the error message better.

[Simon Hudon]

I wouldn't say your project is doomed. I would only say that you'll have to run your experiment while parsing / elaborating Lean files, not as a Lean program (with a main, etc)

[Simon Hudon]

Now about the user_command idea (which I think is what you need):

setup_tactic_parser -- this is actually a user command too

@[user_command]
meta def my_command (meta_info : decl_meta_info) (_ : parse (tk "my_command")) : lean.parser unit :=
do parser.of_tactic $ trace "hello world"
.

my_command . -- prints "hello world"

[Simon Hudon]

Then if you want to user to write in an expression, you can do:

@[user_command]
meta def my_command (meta_info : decl_meta_info) (_ : parse (tk "my_command")) : lean.parser unit :=
do e <- texpr,
   parser.of_tactic $ trace e
.

my_command 1 + 1 . -- prints "1 + 1"

(be sure not to forget the .)

[Simon Hudon]

Then you can skip the part where you parse from a string. If you read the string from a file, this is where I would use the with_input trick

[Jason Rute]

While it is fresh, can you file this run_cmd issue? I'd like to make the error message better.

https://github.com/leanprover-community/mathlib/issues/1928

[Jason Rute]

@Simon Hudon Thanks for all the help! I am wondering if I need to take a step back however. Maybe I don't want/need parsing of Lean code in the first place.

[Simon Hudon]

Can you explain a bit more how you'd like the user to call your program?

[Bryan Gin-ge Chen]

The issue should probably be on leanprover-community/lean instead. I bet @Simon Hudon can transfer it over though.

[Simon Hudon]

Done

[Simon Hudon]

Good call @Bryan Gin-ge Chen

[Jason Rute]

@Simon Hudon The user will be a machine and it will call lean --run my_program and communicate via stdin and stdout. Specifically the user will send some string representing a theorem to be proved (more on that in a second) via stdin. The program will read that string in, convert it to an expression, make a goal of that type, apply a tactic (this may also be specified by the user, but for now I'm worried about the goal itself), and print (to stdout) whether the tactic succeeded and the resulting goal (in some serialization). This will be a loop. So the program waits for the next input. I'm starting to realize that it is better to directly serialize the expression than to directly parse Lean code. I was just about to ask on a new topic if there is a standard serialization of Lean expressions or if I should make my own?

[Jason Rute]

For motivation, I'm trying to make a better and more reliable version of what I made here.

[Jason Rute]

There I used the Lean server, but I think stdin and stdout of a running Lean program is better, faster, and more reliable.

[Simon Hudon]

I see. For serialization, have a look here: https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/library/system/io.lean

[Rob Lewis]

What imports will your lean program use? If it's a large environment, e.g. all of mathlib, you might still be better off with the server interface. There's overhead to building the environment even if the dependencies are precompiled. Keeping a single server instance going will avoid this.

[Jason Rute]

It would be nice to try both. To be clear, I intend to keep either instance "going". If I use stdin/stdout, it will be in a loop.

[Jason Rute]

@Simon Hudon That looks really promising! I need to upgrade Lean apparently to get that... Do you by chance know what the serialization looks like?

[Simon Hudon]

I don't remember what it looks like. I'll have a look

[Simon Hudon]

The serialization is not really legible. It's binary serialization format

[Jason Rute]

Thanks Simon!

[Jason Rute]

Ignoring the details of serialization for now (which have and could be solved in a number of ways), here is what I have in mind. I tested it (with dummy serializations). This code works (and is very fast to call from say Python).

import system.io
open io

meta def serialize_expr (e : expr) : string := sorry
meta def deserialize_expr(s : string) : expr := sorry

meta def apply_tactic_to_goal (t : tactic unit) (goal : expr) : tactic (list expr) :=
do
  -- set expression as goal
  v <- tactic.mk_meta_var goal,
  tactic.set_goals $ [v],
  -- run tactic on goal
  t,
  -- return results
  gs <- tactic.get_goals,
  return gs

meta def read_eval_print (_ : unit) : io_core error (option unit) :=
do
  do
    -- get serialized expression from stdin
    expr_str ← get_line,
    let e := deserialize_expr expr_str,
    -- run tactic (skip tactic in this case) on goal
    gs ← io.run_tactic (apply_tactic_to_goal tactic.skip e),
    -- print serialized goals to stdout
    let goal_strs := gs.map serialize_expr,
    put_str (to_string goal_strs),
    return ()

meta def main : io unit :=
  -- loop forever
  do iterate () read_eval_print,
  return ()

[Jason Rute]

When I say fast, I mean that the first call is slow, but after that it is really fast compared to the lean server.

[Jason Rute]

Of course this is a prototype. A better version needs error handling (and more features around selecting which tactics to apply).

[Jason Rute]

@Rob Lewis I just discovered expr.to_raw_fmt from your other post. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.3F.3F.3F/near/187757930 I don't suppose that hidden somewhere in Lean is a parser for this format (which takes a string of this format and converts it to an expr)?

[Mario Carneiro]

no

[Mario Carneiro]

It's almost good enough that you can use it as lean surface syntax for an object of type expr though (i.e. using the constructors directly)

[Mario Carneiro]

expr.to_raw_fmt is defined in lean though and it's a relatively short definition so you can modify it to suit your needs

[Jason Rute]

Thanks Mario! I actually already have made my own expr to string function before I discovered this and made a parser too (although I haven't finished covering all the cases, like macros). I just thought it was better to use built-in tools when possible. Thanks!

[Jason Rute]

Mario Carneiro said:

I don't think it is possible to use with_input when using lean --run

I'm reviving this thread. It is not possible to run the parser monad inside the tactic monad or the io monad.* I'm curious if this is by necessity (i.e. the parser monad requires information that shouldn't be available in the tactic monad or the io monad) or by omission (no one has bothered to implement io.run_parser). I know the io monad in particular has access to the tactic environment (so one can run io.run_tactic), but I don't know if it also has (or could have) access to the parser state. I'm getting by with the user command trick, but I'm curious nonetheless.

[Jason Rute]

*It isn't entirely true that you can't run a parser in a tactic monad. You could start in the parser monad, grab the parser state, run a tactic inside the parser, and in that tactic, invoke the parser_state, but I think we can agree I'm being pedantic now. :slight_smile: