How to use hand written parsers

Stream: lean4

[Mario Carneiro]

Could someone explain how I should finish this example? I get errors about missing formatters and pretty printers but I haven't figured out what to write to fix the error. I'm fine with stubbing that stuff out, I just want a custom parser for now.

import Lean

namespace Lean
namespace Parser

def evenNumLit : Parser where
  fn := fun c s =>
    let initStackSz := s.stackSize
    let iniPos := s.pos
    let s := numLitFn c s
    if s.hasError then s else
    let ok : Bool :=
      match s.stxStack.back.isNatLit? with
      | some n => n % 2 = 0
      | none => false
    if ok then s else s.mkErrorAt "even numeral" iniPos initStackSz
  info := numLit.info

syntax (name := evenTerm) "even " evenNumLit : term

#check even 6

[Wojciech Nawrocki]

The following between def and syntax should work:

open PrettyPrinter
-- fully qualified names because the attribute forgets to check namespaces I guess
@[combinatorFormatter Lean.Parser.evenNumLit] def evenNumLit.formatter : Formatter := pure ()
@[combinatorParenthesizer Lean.Parser.evenNumLit] def evenNumLit.parenthesizer : Parenthesizer := pure ()

[Mario Carneiro]

Yay, a calc parser:

import Lean
namespace Lean
namespace Parser

def calcLHS : Parser where
  fn c s :=
    let s := symbolFn "..." c s
    if s.hasError then s else
    let tables := (getCategory (parserExtension.getState c.env).categories `term).get!.tables
    trailingLoop tables c s
  info := ("..." >> termParser).info

open PrettyPrinter Elab.Term

@[combinatorFormatter Lean.Parser.calcLHS] def calcLHS.formatter : Formatter := pure ()
@[combinatorParenthesizer Lean.Parser.calcLHS] def calcLHS.parenthesizer : Parenthesizer := pure ()

syntax (name := calcTerm) "calc " term " : " term (calcLHS " : " term)* : term

@[macro Lean.Parser.calcTerm] def expandCalc : Macro := fun stx => `(sorry)

#check calc
  x ≤ y : _
  ... ≤ z : _

[Sebastian Ullrich]

Now I wonder if it would be more Lean 4-y to replace ... with whitespace sensitivity :blush: ...

[Mario Carneiro]

I thought about it but that is going to cause some strange indentation, I think

[Mario Carneiro]

calc blocks are hard to align because you usually want the binops to line up, which means you have to either indent a lot or put the first line LHS on another line

[Mac]

Mario Carneiro said:

put the first line LHS on another line

Yeah, my preferred style for this has always been

foo
  = bar : _
  = baz : _

i.e. indent the binops on the next line

[Mario Carneiro]

The use of colon here is also weird. Maybe => is more lean 4-ish?

[Mario Carneiro]

But I think that actually implementing this via whitespace sensitivity will hit the same issue that the - tac block notation had: binops currently don't check indentation, and this particular situation in calc is bad because we're putting a = term immediately after an ambiguously ended term \n

[Gabriel Ebner]

Mario Carneiro said:

The use of colon here is also weird. Maybe => is more lean 4-ish?

Other reasonable options would be := or from or by (in analogy to have).

[Patrick Massot]

I hope this was a joke by Mario. What's the issue with :?

[Patrick Massot]

By the way, didn't we have an agreement that the => was only for programming and we would replace it in the math parts of mathlib?

[Mario Carneiro]

Lean usually uses : to mean that the type of the left side is the right side, but in calc the meaning is flipped: the right side is a proof of the type which is written on the left

[Patrick Massot]

I don't think there is any risk of confusion here. But using by or from would be ok as well.

[Mario Carneiro]

Re: less =>, I still don't know what to do about the style guide for lambdas in proofs. λ x => pf just looks weird to me

[Patrick Massot]

I think almost everything would look good compared to using => to mean anything but implies.

[Mario Carneiro]

in mathlib4 I've been using fun x => pf but I'm not super happy about it

[Patrick Massot]

In the math part of mathlib I think there is a huge consensus that we simply don't want to use => at all.

[Mario Carneiro]

It also shows up in match, induction , cases, ...

[Patrick Massot]

We could use a weird symbol if computer scientists really can't stand seeing $\mapsto$, but not something that is clearly the ascii-art version of $\implies$.

[Mario Carneiro]

I can't imagine not seeing it on a majority of lines even in the math part of mathlib the way lean 4 syntax is currently designed

[Patrick Massot]

Mario Carneiro said:

It also shows up in match, induction , cases, ...

But this is core Lean. In mathlib 4 we can change that, right?

[Mario Carneiro]

sure, propose away

[Mario Carneiro]

I don't know what mathlib 4 style is yet

[Mario Carneiro]

Gabriel Ebner said:

Mario Carneiro said:

The use of colon here is also weird. Maybe => is more lean 4-ish?

Other reasonable options would be := or from or by (in analogy to have).

Does by actually work here? I would think that expr by expr would be parsed as an expression, an application expr (by expr)

[Patrick Massot]

Really, any weird symbol you can't recognize in the unicode table would be better than using a symbol which is well-known to have a different meaning. But of course the obvious candidate is $\mapsto$

[Mario Carneiro]

I considered using ⇒ as a unicode alternative for =>, but I think the category theory folks have that one reserved (and almost all other similar arrows as well)

[Mario Carneiro]

\mapsto could work, even without a leader, similar to the dependent arrow being used for pi now

[Patrick Massot]

@Mario Carneiro said:

I considered using ⇒ as a unicode alternative for =>, but I think the category theory folks have that one reserved (and almost all other similar arrows as well)

That would be even more confusing.

[Mario Carneiro]

but one thing I don't like about the dependent arrow is that you can't write (a : A) (b : B) -> C, you have to write (a : A) -> (b : B) -> C, and I would guess a similar restriction would appear for iterated lambda

[Patrick Massot]

That would be bad.

[Mario Carneiro]

we could just try to make a b c |-> d work, it would mean we don't get the nice no-paren syntax of fun a b c => d but that seems tolerable given that in lean 3 you need parens or $ before \lam if it is a function argument

[Gabriel Ebner]

Does by actually work here? I would think that expr by expr would be parsed as an expression, an application expr (by expr)

syntax (name := calcTerm) "calc" (term "by" tactic)+ : term

@[macro Lean.Parser.calcTerm] def expandCalc : Macro | stx => do
  dbg_trace stx
  `(sorry)

#check calc
  a ≤ b by skip
  _ ≤ c by { apply le_c; assumption }
  _ ≤ c by trivial
  _ ≤ c by trivial

The last one is parsed as [(«term_≤_» (Term.hole "_") "≤" `c) "by" (Tactic.tacticTrivial "trivial")].

[Sebastian Ullrich]

Yes, by's precedence is lower than e.g. fun's, otherwise show-by etc. wouldn't work either

[Mario Carneiro]

so I guess that's also why foo $ by ... needs the $ even though fun lost it?

[Sebastian Ullrich]

Note that we've recently unified have-from/by to a single, simpler syntax, though we still have it in other places because show ... := would look really weird (to me)...

[Mario Carneiro]

I could get used to show ty := expr, it would finally get rid of the useless from keyword

[Mario Carneiro]

also a big +1 on that new have syntax

[Patrick Massot]

I like the from keyword, it reads nicely.

[Mario Carneiro]

what about show ty; expr or show ty \n expr, similar to let parsing? That would line up more with the tactic

[Mario Carneiro]

That also means that you can use show ty; by tactic without needing show-by to be a special grammar production, which in turn means that by can get a higher precedence and foo $ by tactic can lose the $