Parser

Stream: new members

[Pablo Le Hénaff]

Hello !

[Kenny Lau]

bienvenu

[Pablo Le Hénaff]

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]

Should I ask this on the other #general stream?

[Sean Leather]

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

[Rob Lewis]

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

[Scott Morrison]

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

[Rob Lewis]

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

[Pablo Le Hénaff]

I didn't know about data.buffer.parser

[Rob Lewis]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Scott Morrison]

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

[Scott Morrison]

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

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

[Rob Lewis]

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

[Johan Commelin]

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

[Scott Morrison]

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.