leading_parser?

Stream: new members

[Eduardo Ochs]

People, where can I find more about leading_parser? It appears many times in the source but I couldn't find mentions to it in any of the books, and its definition (???) in Lean/Elab/BuiltinNotation.lean is too difficult to read (IMO) and doesn't have comments...

Thanks in advance! :oh_no:

[Eduardo Ochs]

Aha, I just found this message by @Kyle Miller! Let me change my question...

Where can I find examples of how to translate calls to "leading_parser" to calls to "syntax"?

[Kyle Miller]

Usually it's ">> becomes space and f x y z becomes f(x, y, z)" though sometimes the parser name for syntax can be a little different.

There are also transformations like many p becomes p* and many1 p becomes p+, among some others.

[Eduardo Ochs]

Hi, another question...

I decided to inspect the objects created by leading_parser, and I got this, after a lot of trial and error:

import Lean.Parser.Types
namespace Lean
namespace Parser
def foo := leading_parser "bar "
#check foo
#check foo.info
#check foo.info.firstTokens

def a := foo.info.firstTokens
def b := Lean.Parser.FirstTokens.tokens ["$", "bar"]
#eval a
#eval b

Here a and b are "equal" but not "eq".

Is there an easy way to print the structure of a? My guess - as a newbie - is: "no because FirstTokens doesn't derive Repr, but there are workarounds using instances".

Is that right? Is it possible to make FirstTokens an instance of Repr? If yes, how?

Thanks in advance!

[Kyle Miller]

What's the question about a and b not being "eq"? They're equal according to

example : a = b := rfl

[Kyle Miller]

(With import Lean imported, #eval a prints [$, bar]. I'm not sure what you're seeing, since your mwe fails on leading_parser for me on a version near Lean 4.8.0-rc1)

[Kyle Miller]

no because FirstTokens doesn't derive Repr, but there are workarounds using instances

Note that "deriving Repr" means "try to automatically create a Repr instance". Mentioning that in case you think instances are some sort of workaround.

[Kyle Miller]

This is the easiest way to see what leading_parser is doing:

def foo := leading_parser "bar "

#print foo
/-
def Lean.Parser.foo : Parser :=
withCache `Lean.Parser.foo
  (withAntiquot (mkAntiquot "foo" `Lean.Parser.foo true) (leadingNode `Lean.Parser.foo 1024 (symbol "bar ")))
-/

It's a macro that expands to that. The key thing it does is embed the declaration name for foo into itself, in the leadingNode parser combinator. That's what creates a Syntax.node with Lean.Parser.foo as the kind.

[Kyle Miller]

The antiquote business is for parsing `(... $x:foo ...) in syntax quotations in syntactically correct locations.

[Eduardo Ochs]

About "eq" and "equal", I was thinking about this:

(eq    '(a b) '(a b))  ;-> nil
(equal '(a b) '(a b))  ;-> t

It didn't occur to me that we could test "equal"ity in Lean using "example : a = b := rfl"... neat!

[Eduardo Ochs]

Now about the output of "#print foo": wow and thanks! It works here, but I think that I need to understand other things before understanding that... and my guess is that would be a good idea to start by understand how "deriving Repr" works in a simple case. I tried this,

inductive myNat where
  | zero             : myNat
  | succ (n : myNat) : myNat
  deriving Repr

def my1 := myNat.succ myNat.zero
#check my1
#eval  my1
#print my1
#check repr my1
#eval  repr my1
#print repr my1
#check Std.Format

and then:

1) the method "repr" for the type myNat is not in a super-obvious place, like in myNat.repr,

2) the output of "#check repr my1" is "repr my1 : Std.Format", and I don't have test snippets (yet) for the class Std.Format,

3) but I read some parts of the source starting by "mkReprInstanceHandler" and I found references to "isInductive" and "getStructureFields" - they look very useful, can we start by them? If yes, question: how do I call "isInductive" and "getStructureFields" on the "myNat" or on the "my1" of the example above?

Thanks in advance!

[Kyle Miller]

Here's how you can get the name of the instance:

#synth Repr myNat
-- instReprMyNat

[Kyle Miller]

Unfortunately you reach a dead end quick because the deriving handler defines a constant with an inaccessible name:

#print instReprMyNat
/-
def instReprMyNat : Repr myNat :=
{ reprPrec := reprmyNat✝ }
-/

[Kyle Miller]

Though if you set set_option trace.Elab.command true you can see what deriving constructs.

[Kyle Miller]

Here, if you want to see:

open Lean

def reprmyNat (n : myNat) (prec : Nat) : Format :=
  match n with
  | myNat.zero =>
    Repr.addAppParen
      (Format.group (Format.nest (if prec >= max_prec then 1 else 2) (Std.Format.text "myNat.zero"))) prec
  | @myNat.succ a =>
    Repr.addAppParen
      (Format.group
        (Format.nest (if prec >= max_prec then 1 else 2)
          (Std.Format.text "myNat.succ" ++ Format.line ++ reprmyNat a max_prec)))
      prec

instance : Repr myNat where
  reprPrec := reprmyNat

[Kyle Miller]

Repr instances aren't so interesting. They're just code to turn data into some string representation (using Format so that indentation is taken care of). I would not suggest going deep into the derive handler unless you're willing to venture forth into the less-documented parts of Lean. (You might look at the Lean 4 Metaprogramming Book to get an idea of how some of the system works, but it's not comprehensive yet.)

Repr doesn't have anything to do with #print. What #print does is pretty print a declaration, whose value is an Expr.

[Kyle Miller]

Re Lisp-like eq vs equal, in Lean the main equality type Eq is more like equal, and there's no such thing as eq unless you are willing to do unsafe things. The Eq is true mathematical equality. There's also BEq for user-defined equality operations.