has_reflect in interactive.parse

Stream: general

[Keeley Hoek]

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

Because the parser needs to know what type to produce

[Keeley Hoek]

oh, ok, I understand

[Keeley Hoek]

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]

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]

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]

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]

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]

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]

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]

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]

Obviously expr has a reflect instance

[Keeley Hoek]

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]

Of course there is an instance

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

[Keeley Hoek]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

Actually I think I like reflectable_parser better than my idea

[Mario Carneiro]

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

[Mario Carneiro]

I would drop the valid field of reflectable parser though

[Keeley Hoek]

Ok, and ok cool