What parsers parses the "(ab : α×β)" in a "fun ... => ..."?

Stream: new members

[Eduardo Ochs]

Hi all,

sorry if this looks like a question that is being asked too early... I was checking how much, or how little, I know about how Lean parsers certain expressions, and I saw that in

#check fun {α β} (ab : α×β) => let (a,_) := ab; a

the {α β} is parsed by funImplicitBinder, but I couldn't find the name of the (sub)parser that funBinder uses to parse the (ab : α×β)... hints, please?

[Eduardo Ochs]

Here's some more context. I'm writing my (guess for a) parse tree in this format,

import Lean
open   Lean Elab Command Meta Term

#check fun {α β}         (ab : α×β) => let (a,_) := ab; a
#check fun {α β} [BEq α] (ab : α×β) => let (a,_) := ab; a==a

-- #check fun   {α           β          } (ab : α×β) =>   let (a,_) := ab ;            a
--        -----  ----------- -----------  ---------- ----     ----------- ------------ ----------
--        "fun"  binderIdent binderIdent      ?      "=>"     letDecl?    optSemicolon termParser
--              ------------------------- ----------      ---------------------------------------
--              funImplicitBinder         funBinder?      termParser?
--              -------------------------
--              funBinder
--              ---------------------------------------------------------------------------------
--              basicFun

-- Hyperlinks to the parsers:
#check Lean.Parser.Term.basicFun
#check Lean.Parser.Term.binderIdent
#check Lean.Parser.Term.funBinder
#check Lean.Parser.Term.funImplicitBinder
#check Lean.Parser.Term.funStrictImplicitBinder
#check Lean.Parser.Term.letDecl
#check Lean.Parser.Term.letPatDecl
#check Lean.Parser.Term.matchAlts
#check Lean.Parser.Term.«fun»
#check Lean.Parser.Term.«let»
#check Lean.Parser.termParser

[Eduardo Ochs]

...and I'm working on a program that processes the tree in ASCII art and LaTeXes it as a diagram with underbraces that looks like this:

[Eduardo Ochs]

sshot-cropped.png

[Eduardo Ochs]

I still have lots of doubts about how to complete that parse tree, but most of these doubts are about parsing combinators... and I hope that understanding funBinder will help me with the rest.

[Eric Wieser]

If you use

#check `(fun {α β} [BEq α] (ab : α×β) => let (a,_) := ab; a==a)

then the names of all most of the parsers are embedded in the output

[Eduardo Ochs]

Thanks!!!
New diagram:

[Eduardo Ochs]

sshot.png

[Eduardo Ochs]

Is there an easy way to extract the expression inside the raw := ... from a syntax quotation? How? Let's consider this smaller example:

import Lean
open   Lean.Elab.Term.Quotation
#check mkSyntaxQuotation
#check  `(42 + "foo")
#check (`(42 + "foo") : Lean.MacroM (Lean.TSyntax `term))

[Eric Wieser]

You probably want to parse it inside run_cmd do

[Eric Wieser]

That is, something like

run_cmd do
  let stx <- `(fun {α β} [BEq α] (ab : α×β) => let (a,_) := ab; a==a)
  -- process stx
  Lean.logInfo m!"{stx}"

[Eduardo Ochs]

Perfect! Thanks! :smile:
For the sake of completeness, here's what I've got...
It's just a prototype, but I think it's nice anyway.

[Eduardo Ochs]

sshot.png

[Eduardo Ochs]

import Lean
import Init.Data.Format
open   Lean SourceInfo Parser
open   Std Format

def pile : (List Format) → Format
  | []           => ""
  | [item]       => item
  | item :: rest => item ++ line ++ pile rest

def zpile (head : String) (fmts : List Format) :=
  nest (1 + String.length head) <| head ++ align true ++ (pile fmts)

class  ToPrettier (α : Type) where toPrettier : α → Format
export ToPrettier (toPrettier)

def    toPrettier_Nat (n : Nat) : Format := toString n
def    toPrettier_Int (n : Int) : Format := toString n
def    toPrettier_List  [ToPrettier α] (as : List α)  : Format :=
  zpile "[]"  (List.map  toPrettier as)
def    toPrettier_Array [ToPrettier α] (as : Array α) : Format :=
  zpile "#[]" (List.map toPrettier (as.toList))
def    toPrettier_SourceInfo (_ : Sourceinfo) : Format := ".sourceinfo"
def    toPrettier_Name : Name → Format
  | .anonymous .. => ".anonymous"
  | .num name i   => toPrettier_Name name ++ " " ++ toString i
  | .str _ str    => "name: " ++ str

instance : ToPrettier Nat        where toPrettier := toPrettier_Nat
instance : ToPrettier Int        where toPrettier := toPrettier_Int
instance : ToPrettier Name       where toPrettier := toPrettier_Name
instance : ToPrettier SourceInfo where toPrettier := toPrettier_SourceInfo
instance {α} [ToPrettier α] : ToPrettier (List α)  where toPrettier := toPrettier_List
instance {α} [ToPrettier α] : ToPrettier (Array α) where toPrettier := toPrettier_Array

def toPrettier_SyntaxNodeKind  : SyntaxNodeKind  → Format := toPrettier_Name
def toPrettier_SyntaxNodeKinds : SyntaxNodeKinds → Format := toPrettier_List
instance : ToPrettier SyntaxNodeKind  where toPrettier := toPrettier_SyntaxNodeKind
instance : ToPrettier SyntaxNodeKinds where toPrettier := toPrettier_SyntaxNodeKinds

partial def toPrettier_Syntax : Syntax → Format
  | .missing          => ".missing"
  | .atom _ str       => ".atom: " ++ str
  | .ident _ _ name _ => ".ident: " ++ toPrettier_Name name
  | .node _ kind args =>
       let k     := toPrettier_SyntaxNodeKind kind
       let sargs := List.map toPrettier_Syntax (args.toList)
       zpile ".node" (k :: sargs)

instance : ToPrettier Syntax where toPrettier := toPrettier_Syntax

partial def toPrettier_TSyntax {ks : SyntaxNodeKinds} (ts : TSyntax ks) : Format :=
  zpile "TSyntax" [toPrettier ks, toPrettier ts.raw]

instance : ToPrettier (TSyntax ks) where toPrettier := toPrettier_TSyntax

run_cmd do
  let stx <- `(fun {α β} [BEq α] (ab : α×β) => let (a,_) := ab; a==a)
  -- let stx <- `(fun (x : Nat) => x*x)
  -- process stx
  Lean.logInfo m!"{stx}"
  -- Lean.logInfo s!"{repr stx}"
  Lean.logInfo s!"{toPrettier stx}"

[Eric Wieser]

Eduardo Ochs said:

sshot.png

Note that in some sense here you are reinventing the UX of the infoview; it would be possible to have a command that displays syntax in the infoview, and lets you hover over its pieces to see which parser they are (instead of the usual behavior of hovering over an expression and seeing the types of the subexpressions)

[Sebastian Ullrich]

trace.Elab.command does similar non interactive output