Zulip Chat Archive

Stream: general

Topic: Parsing a string into an expression


view this post on Zulip Jason Rute (Jan 29 2020 at 03:15):

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.

view this post on Zulip Jason Rute (Jan 29 2020 at 03:17):

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

view this post on Zulip Jason Rute (Jan 29 2020 at 03:21):

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.)

view this post on Zulip Jason Rute (Jan 29 2020 at 03:29):

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).

view this post on Zulip Simon Hudon (Jan 29 2020 at 03:45):

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

view this post on Zulip Simon Hudon (Jan 29 2020 at 03:46):

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

view this post on Zulip Simon Hudon (Jan 29 2020 at 03:50):

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

view this post on Zulip Simon Hudon (Jan 29 2020 at 03:51):

To set a goal with your expression:

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

view this post on Zulip Jason Rute (Jan 29 2020 at 03:55):

Thanks! I will have to try this out.

view this post on Zulip Tim Daly (Jan 29 2020 at 04:22):

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

view this post on Zulip Jason Rute (Jan 29 2020 at 04:32):

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 :) ).

view this post on Zulip Jason Rute (Jan 29 2020 at 05:48):

@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 ()

view this post on Zulip Jason Rute (Jan 29 2020 at 05:51):

@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.

view this post on Zulip Simon Hudon (Jan 29 2020 at 05:55):

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

view this post on Zulip Simon Hudon (Jan 29 2020 at 06:00):

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

view this post on Zulip Mario Carneiro (Jan 29 2020 at 06:41):

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

view this post on Zulip Jason Rute (Jan 29 2020 at 13:31):

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.

view this post on Zulip Sebastian Ullrich (Jan 29 2020 at 13:38):

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).

view this post on Zulip Jason Rute (Jan 29 2020 at 13:42):

@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?)

view this post on Zulip Simon Hudon (Jan 29 2020 at 16:59):

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

view this post on Zulip Simon Hudon (Jan 29 2020 at 17:01):

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)

view this post on Zulip Simon Hudon (Jan 29 2020 at 17:11):

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"

view this post on Zulip Simon Hudon (Jan 29 2020 at 17:12):

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 .)

view this post on Zulip Simon Hudon (Jan 29 2020 at 17:16):

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

view this post on Zulip Jason Rute (Jan 29 2020 at 23:10):

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

view this post on Zulip Jason Rute (Jan 29 2020 at 23:11):

@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.

view this post on Zulip Simon Hudon (Jan 29 2020 at 23:13):

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

view this post on Zulip Bryan Gin-ge Chen (Jan 29 2020 at 23:13):

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

view this post on Zulip Simon Hudon (Jan 29 2020 at 23:15):

Done

view this post on Zulip Simon Hudon (Jan 29 2020 at 23:16):

Good call @Bryan Gin-ge Chen

view this post on Zulip Jason Rute (Jan 29 2020 at 23:22):

@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?

view this post on Zulip Jason Rute (Jan 29 2020 at 23:23):

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

view this post on Zulip Jason Rute (Jan 29 2020 at 23:25):

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

view this post on Zulip Simon Hudon (Jan 29 2020 at 23:26):

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

view this post on Zulip Rob Lewis (Jan 29 2020 at 23:34):

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.

view this post on Zulip Jason Rute (Jan 29 2020 at 23:41):

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.

view this post on Zulip Jason Rute (Jan 29 2020 at 23:42):

@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?

view this post on Zulip Simon Hudon (Jan 29 2020 at 23:50):

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

view this post on Zulip Simon Hudon (Jan 30 2020 at 01:49):

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

view this post on Zulip Jason Rute (Jan 30 2020 at 13:20):

Thanks Simon!

view this post on Zulip Jason Rute (Jan 30 2020 at 13:33):

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 ()

view this post on Zulip Jason Rute (Jan 30 2020 at 13:34):

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

view this post on Zulip Jason Rute (Jan 30 2020 at 13:36):

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

view this post on Zulip Jason Rute (Feb 09 2020 at 14:04):

@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)?

view this post on Zulip Mario Carneiro (Feb 09 2020 at 14:05):

no

view this post on Zulip Mario Carneiro (Feb 09 2020 at 14:06):

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)

view this post on Zulip Mario Carneiro (Feb 09 2020 at 14:07):

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

view this post on Zulip Jason Rute (Feb 09 2020 at 14:11):

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!

view this post on Zulip Jason Rute (May 21 2020 at 23:09):

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.

view this post on Zulip Jason Rute (May 21 2020 at 23:11):

*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:


Last updated: May 08 2021 at 10:12 UTC