Zulip Chat Archive

Stream: general

Topic: has_reflect in interactive.parse


Keeley Hoek (Apr 20 2019 at 05:48):

@Sebastian Ullrich (and anyone else who might know!), why does the definition

@[reducible] meta def parse {α : Type} [has_reflect α] (p : parser α) : Type := α

need the [has_reflect α]?

Mario Carneiro (Apr 20 2019 at 07:03):

Because the parser needs to know what type to produce

Keeley Hoek (Apr 20 2019 at 07:31):

oh, ok, I understand

Keeley Hoek (Apr 20 2019 at 07:34):

So if I have a user-defined parserof a type \alpha I must have an instance of has_reflect \alpha in order to interactive.parse that parser.

On the other hand, a parser implemented in core lean doesn't need a has_reflect instance, so in terms of parsing a tactic unit I suppose we have some wiggle-room here.

Keeley Hoek (Apr 20 2019 at 07:39):

So I suppose [has_reflect \alpha] is unnecessarily strong---really we just need a way to reflect the result of p whenever it runs. I'll build an instance of reflectable_parser which encodes this and weaken the typeclass argument of parse.

Mario Carneiro (Apr 20 2019 at 07:46):

Oh, I looked into the code and now I see why it has to reflect stuff:

open interactive lean lean.parser
meta def tactic.interactive.foo
  (l : parse (list.reverse <$> many ident)) : tactic unit :=
return ()

#check `[foo a b]
-- has_bind.seq (tactic.save_info {line := 6, column := 9})
--   (tactic.step (tactic.interactive.foo [name.mk_string "b" name.anonymous, name.mk_string "a" name.anonymous])) :
--   tactic unit

Mario Carneiro (Apr 20 2019 at 07:47):

it has to build the expression corresponding to the tactic to be run before actually running it. The parser gets run long before the tactic starts execution

Mario Carneiro (Apr 20 2019 at 07:50):

Actually, looking at your comment again I don't see where the problem is... regardless of whether a parser is implemented in core lean or user defined, what matters is the type of the parser passed to parse. The core parsers don't need reflect instances, just the final result going to parse

Mario Carneiro (Apr 20 2019 at 07:52):

for example:

open interactive lean lean.parser

meta def xyzzy : parser (nat  nat) := return nat.succ

meta def tactic.interactive.foo
  (l : parse ((λ f : nat  nat, f 1) <$> xyzzy)) : tactic unit :=
return ()

#check `[foo]

the xyzzy parser doesn't need to provide a has_reflect instance for nat -> nat because the end result passed to parse is a nat

Keeley Hoek (Apr 20 2019 at 08:03):

I believe I understand your last comment, but I think there still is a distinction. Because the parser works as you describe, it should be impossible for a user defined parser to parse a tactic unit, since once constructed it is too late for a tactic unit to be turned back into an expr, required for emitting by the parser. On the other hand, a "parser" written in core lean could happily parse a tactic unit but keep it in expr form (as essentially happens when a nested tactic block parsed in the current parser), and then emit the expr form directly so that we really can just read a tactic unit block from interactive mode.

Do you think what I'm say makes sense, or am I still confused?

Mario Carneiro (Apr 20 2019 at 08:06):

What we can do is rather than parse a tactic unit we have a parser expr that produces an expr representing a tactic

Mario Carneiro (Apr 20 2019 at 08:06):

Obviously expr has a reflect instance

Keeley Hoek (Apr 20 2019 at 08:11):

Sure, that absolutely makes sense. There is also some scope for a generalisation

meta structure reflected_value (α : Type u) :=
(val : α)
[reflect : reflected val]

meta class reflectable_parser {α : Type} (p : parser α) :=
(full : parser (reflected_value α))
(valid : p = reflected_value.val <$> full)

@[reducible] meta def parse {α : Type} (p : parser α) [reflectable_parser p] : Type := α

What do you think about that? I guess one interpretation is that I'm type-safing your plain parser expr construction.

Keeley Hoek (Apr 20 2019 at 08:11):

Of course there is an instance

meta instance {α : Type} (p : parser α) [r : has_reflect α] : reflectable_parser p :=
(do v  p, return v), _⟩

Keeley Hoek (Apr 20 2019 at 08:11):

(I'm trying to write this in a way which wouldn't break code which compiles against vanilla lean.)

Mario Carneiro (Apr 20 2019 at 08:19):

so what's the new power with this? Are you going to add itactic as a parser and give it a reflectable_parser instance?

Keeley Hoek (Apr 20 2019 at 08:20):

That's what I was thinking. I could just do the parser expr thing if you want. :)

Mario Carneiro (Apr 20 2019 at 08:21):

Here's the parser expr approach with itactic:

meta constant itactic' : parser expr

meta def run_itactic (e : expr) : tactic unit :=
monad.join $ tactic.eval_expr (tactic unit) e

meta def tactic.interactive.repeat'
  (e : parse itactic') : tactic unit :=
tactic.repeat (run_itactic e)

there is an obvious ergonomic loss with this, but I'm not a fan of lean magic

Keeley Hoek (Apr 20 2019 at 08:21):

(I would really implement itactic as a parser (reflected_value (tactic unit)), and then make the normal parser (tactic unit) and instance in lean from it.)

Sure.

Keeley Hoek (Apr 20 2019 at 08:25):

One thing with this approach actually is that we still have to leave tactic.interative.itactic implemented the same way in lean, instead of being able to define def tactic.interative.itactic := interactive.parse lean.parser.itactic, and eliminate the need for how it was hard-implemented the old way.

Mario Carneiro (Apr 20 2019 at 08:26):

well you can still replace uses of itactic with the parser, but the interface is different

Mario Carneiro (Apr 20 2019 at 08:26):

also you can't define things to be parse bla because parse is lean magic

Mario Carneiro (Apr 20 2019 at 08:27):

If itactic stops being magic then it will have to be changed in uses anyway

Mario Carneiro (Apr 20 2019 at 08:32):

Actually I think I like reflectable_parser better than my idea

Mario Carneiro (Apr 20 2019 at 08:33):

It will cause some unnecessary expr quoting and interpretation inside tactic scripts

Mario Carneiro (Apr 20 2019 at 08:34):

I would drop the valid field of reflectable parser though

Keeley Hoek (Apr 20 2019 at 08:36):

Ok, and ok cool


Last updated: Dec 20 2023 at 11:08 UTC