## Stream: general

### Topic: Parsing a string into an expression

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

#### 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

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

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

#### Simon Hudon (Jan 29 2020 at 03:45):

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

#### 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

#### 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

#### 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  #### Jason Rute (Jan 29 2020 at 03:55): Thanks! I will have to try this out. #### 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. #### 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 :) ). #### 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 ()


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

#### 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

#### 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

#### Mario Carneiro (Jan 29 2020 at 06:41):

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

#### 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. #### 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). #### 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?) #### 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. #### 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) #### 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"


#### 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 .) #### 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 #### 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 #### 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. #### Simon Hudon (Jan 29 2020 at 23:13): Can you explain a bit more how you'd like the user to call your program? #### 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. #### Simon Hudon (Jan 29 2020 at 23:15): Done #### Simon Hudon (Jan 29 2020 at 23:16): Good call @Bryan Gin-ge Chen #### 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? #### 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. #### 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. #### 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 #### 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. #### 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. #### 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? #### Simon Hudon (Jan 29 2020 at 23:50): I don't remember what it looks like. I'll have a look #### Simon Hudon (Jan 30 2020 at 01:49): The serialization is not really legible. It's binary serialization format #### Jason Rute (Jan 30 2020 at 13:20): Thanks Simon! #### 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
return ()


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

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

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

no

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

#### 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

#### 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!

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

#### 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