Zulip Chat Archive

Stream: new members

Topic: Parser


Pablo Le Hénaff (Aug 08 2018 at 10:40):

Hello !

Kenny Lau (Aug 08 2018 at 10:40):

bienvenu

Pablo Le Hénaff (Aug 08 2018 at 10:40):

Can one use lean.parser to actually parse strings? If so, how do I run a parser on a string? That's what I want to do.

Pablo Le Hénaff (Aug 08 2018 at 11:40):

Should I ask this on the other #general stream?

Sean Leather (Aug 08 2018 at 11:42):

You could try pinging @Gabriel Ebner and @Sebastian Ullrich. (Actually, I just did that. :smile:)

Rob Lewis (Aug 08 2018 at 11:45):

@Pablo Le Hénaff You can. Here's an example: https://github.com/robertylewis/mathematica/blob/master/mathematica_parser.lean

Scott Morrison (Aug 08 2018 at 11:46):

@Rob Lewis cool! Last time I asked about this, I got the impression it couldn't be done.

Rob Lewis (Aug 08 2018 at 11:46):

Er, wait a sec. lean.parser is different from data.buffer.parser.

Pablo Le Hénaff (Aug 08 2018 at 11:47):

I didn't know about data.buffer.parser

Rob Lewis (Aug 08 2018 at 11:49):

data.buffer.parser is a parser monad. lean.parser exposes a bit of the built-in parser, I think.

Rob Lewis (Aug 08 2018 at 11:49):

So you can use the former to write your own string parser. But you don't get access to any of the built in stuff.

Pablo Le Hénaff (Aug 08 2018 at 11:49):

I think data.buffer.parser is what I need, thanks!

Rob Lewis (Aug 08 2018 at 11:51):

@Scott Morrison What can't be done (easily, anyway) is parsing a string into an expr.

Scott Morrison (Aug 08 2018 at 11:54):

ah, okay. The thing I really wanted to do was parse a string into a tactic.

Scott Morrison (Aug 08 2018 at 11:56):

(I have some "self-describing" tactics, which you can ask to output a string, which is meant to be a tactic block that achieves whatever the invoked tactic just did (probably only using lower-level tactics). I really want to verify the output by parsing it and replaying it on the original goal, but never worked out how to do the parsing step.)

Rob Lewis (Aug 08 2018 at 12:01):

Yeah, you'd need to access the Lean parser to do that.

Rob Lewis (Aug 08 2018 at 12:01):

Can you make them output an expr instead of a string?

Johan Commelin (Aug 08 2018 at 12:01):

Hmm, can't you save the tactics from just before you generate the strings

Scott Morrison (Aug 08 2018 at 12:05):

Sure, certainly I can save the tactics: the point is to double-check that the copy-and-pasteable text you're about to present to the human really does what you promise.


Last updated: Dec 20 2023 at 11:08 UTC