Converting from doSeq to doSeqItem

Stream: lean4

[Eric Wieser]

Is there a better way to write the following?

def doSeqToItem {m: Type → Type} [Monad m] [MonadRef m] [MonadQuotation m]
    (t : TSyntax ``doSeq) : m (TSyntax ``doSeqItem) :=
  `(doSeqItem| if h : True then $t else (h trivial).elim)

[Mario Carneiro]

import Lean
open Lean Parser Term

def doSeqToItem {m: Type → Type} [Monad m] [MonadRef m] [MonadQuotation m]
    (t : TSyntax ``doSeq) : m (TSyntax ``doSeqItem) :=
  `(doSeqItem| do $t)

[Mario Carneiro]

you'd think this starts a new do scope, but it doesn't

[Mario Carneiro]

example :
  (Id.run do
    if true then
      do
        return 1
    else
      pure 0
    pure 10
  ) = 1 := rfl

example :
  (Id.run do
    if true then
      (do
        return 1)
    else
      pure 0
    pure 10
  ) = 10 := rfl

[Eric Wieser]

And a follow up question, how do I go from a TSyntax `doElem to a TSyntax `Lean.Parser.Term.doSeq : Type?

[Eric Wieser]

(and why is it a fake `doElem name and not a real declaration unlike doSeq?)

[Mario Carneiro]

doElem and a few others like term use unqualified names for the syntax kind, I think this is an outdated style and we would prefer they are all declarations but for now there are fake declarations like src#Lean.Parser.Category.term for hanging the docs for these

[Mario Carneiro]

what they have in common is these are all extensible syntax categories, not individual definitions

[Mario Carneiro]

def doElemToSeq {m: Type → Type} [Monad m] [MonadRef m] [MonadQuotation m]
    (t : TSyntax `doElem) : m (TSyntax ``doSeq) :=
  `(doSeq| $t:doElem)

[Eric Wieser]

It's not entirely clear to me what the difference between doSeqItem and doElem is

[Mario Carneiro]

not much:

def doSeqItem      := leading_parser
  ppLine >> doElemParser >> optional "; "

[Eric Wieser]

Thanks! The context here is https://github.com/leanprover-community/quote4/pull/27, where return is misbehaving

[Mario Carneiro]

oh that's right, quote4 had this horrible hack with comefrom being laundered through assert! to work around the fact that do elaboration is not extensible

[Eric Wieser]

To me it looks like comefrom is just an optimization

[Eric Wieser]

(in order to avoid duplicating a match alternative

[Mario Carneiro]

this line

  elabTerm (← `(have $n:ident : ?m := (do $b:doSeq); $body)) expectedType

is adding a new do scope

[Mario Carneiro]

possibly on purpose?

[Mario Carneiro]

no that's definitely the bug, although maybe it's not clear how to elaborate that in the context of the outer do block

[Eric Wieser]

I assume you saw that my PR deleted those lines already?

[Mario Carneiro]

can you explain what the new version is doing by example?

[Eric Wieser]

Its directly substituting the alternations as syntax, rather than trying to declare them as lets and resume them

[Eric Wieser]

I think the problem is that _qq_match is handling the alternation itsel

[Mario Carneiro]

does this involve duplicating syntax?

[Eric Wieser]

Yes, it does. Is that bad for other reasons?

[Mario Carneiro]

it involves duplicating it in a loop, no less

[Eric Wieser]

I think I understand a way to avoid doing that (build an Option of a sigma type, and ultimately do the final match on that), but it might be a larger refactor than I have time for today

[Mario Carneiro]

this seems like it would explode exponentially

[Mario Carneiro]

The usual technique used for the do elaborator is to capture the remainder of the block into a closure and jump to it under certain circumstances

[Mario Carneiro]

I think that's what the comefrom stuff was about

[Eric Wieser]

But that's not an option because it interferes with the real do notation

[Eric Wieser]

I think the solution here is that

let ~q(f $x $y) := e | alt

should be a macro for

let some ⟨x, y, match_eq⟩ := (←do_q_match ~q(f $x $y) e) | alt

[Mario Carneiro]

what's the match_eq part about?

[Mario Carneiro]

Well, actually rather than doing two macro expansions I would just suggest building both the ⟨x, y⟩ pattern and the expression to go in for do_q_match ~q(f $x $y) e in a single go

[Eric Wieser]

Mario Carneiro said:

what's the match_eq part about?

It contains the $e =Q f $x $y term