Zulip Chat Archive

Stream: general

Topic: string -> tactic?


Scott Morrison (Apr 05 2018 at 23:20):

Is there a good way to take a string (e.g. "simp, exact p") and return the tactic that executes it in interactive mode?

Scott Morrison (Apr 05 2018 at 23:21):

(I have some "self-describing tactics", which can print as a message "what they did" in terms of built-in tactics, and I would like to automatic verify they are producing correct output.)

Simon Hudon (Apr 06 2018 at 00:11):

I think the best I could do is something of type string -> parser (tactic unit)

Simon Hudon (Apr 06 2018 at 00:13):

I don't know how to run that in a tactic though ... unless we're parsing the parameters to the tactic. Is that good enough?

Scott Morrison (Apr 06 2018 at 00:13):

Unfortunately not. I'm deep inside a tactic by now.

Simon Hudon (Apr 06 2018 at 00:15):

I think we'd need to plead with the developers to give us a parser_state.mk function

Scott Morrison (Apr 06 2018 at 00:34):

If I want to parse a rw_rule, followed by a nat (e.g. so I can write some_tactic foo 1, or some_tactic ← foo 3), what am I meant to do?

Scott Morrison (Apr 06 2018 at 00:34):

I've worked out that (q : parse (rw_rule_p (parser.pexpr 0))) will parse a single rw_rule.

Simon Hudon (Apr 06 2018 at 00:43):

Is the rw_rule fed by the user through a begin ... end block?

Scott Morrison (Apr 06 2018 at 00:44):

yes

Scott Morrison (Apr 06 2018 at 00:44):

I've decided that it's just as good to parse a list of rw_rules, and this seems to work out of the box.

Scott Morrison (Apr 06 2018 at 00:45):

(q : parse rw_rules) (n : ℕ)

Simon Hudon (Apr 06 2018 at 00:45):

Oh good then

Simon Hudon (Apr 06 2018 at 00:46):

I don't know if n : ℕ will work but if it doesn't, you can use n : parse small_nat

Scott Morrison (Apr 06 2018 at 00:47):

Ah, I see, I just found parse small_nat in conv. Not bothering to use the parser for the nat seems okay.

Simon Hudon (Apr 06 2018 at 00:49):

Alright then :)

Mario Carneiro (Apr 06 2018 at 01:10):

@Sebastian Ullrich knows the answer to this one. My first thought was either a parser A -> tactic A lift, or the with_input function which is used to implement format!, but the first doesn't exist (you can make a parser from a tactic but not vice versa) and the second only works in the parser monad. There is no way to create a parser_state in lean that I can see (which corresponds to creating a C++ parser object), so I think parsing can only be done at parse time, not at tactic running time. (One suuper hacky way to maybe get this to work is to call lean using the io monad with a file that you create.)

Sebastian Ullrich (Apr 06 2018 at 06:49):

What Mario said


Last updated: Dec 20 2023 at 11:08 UTC