Tools for exploring data structures?

Stream: new members

[Eduardo Ochs]

Hi all! I was trying to understand the data structures that are accessible inside a run_cmd, but this example - from this thread -

import Lean
namespace Foo
run_cmd Lean.logInfo (← Lean.getCurrNamespace)

turned out to be too complex... so I took this one,

open Lean
#eval Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]
#eval mkNode `«term_+_» #[Syntax.mkNumLit "1", mkAtom "+", Syntax.mkNumLit "1"]

from the section "Constructing new Syntax" of the metaprogramming book, and expanded it into:

open Lean

def my1      := Syntax.mkNumLit "1"
def myadd    := mkIdent `Nat.add
def myplus   := `«term_+_»
def myadd11  := Syntax.mkApp myadd #[my1, my1]
def myplus11 := mkNode myplus #[my1, mkAtom "+", my1]

-- Compare:
#eval Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]
#eval myadd11
#eval mkNode `«term_+_» #[Syntax.mkNumLit "1", mkAtom "+", Syntax.mkNumLit "1"]
#eval myplus11

-- Primitive tools for exploring myadd11 and myplus11:
class Foo (α : Type) where foo : α → String

def Syntax.foo : Syntax → String
  | .missing              => "(missing)"
  | .node  info kind args => "(node)"
  | .atom  info val       => "(atom)"
  | .ident info rawVal val preresolved => "(ident)"

def Name.foo : Name → String
  | .anonymous   => "(anonymous)"
--| .str pre str => "(str)"
  | .str pre str => "(str: "++ str ++ ")"
  | .num pre i   => "(num)"

instance : Foo Syntax where foo := Syntax.foo
instance : Foo Name   where foo := Name.foo

#eval Syntax.foo myplus11
#eval Syntax.foo myadd11
#eval Name.foo   myplus

With that I can see that myplus11 is an object of the class Syntax that is of the form "node info kind args", and by changing my definitions of Syntax.foo and Name.foo I should be able to inspect to interesting subfields and subsubfields of myplus11 and myadd11... but that looks very clumsy.

How do non-newbies inspect particular cases data structures? For example, what are the better ways to discover that myplus11 above is of an object of the class Syntax, of the form "node info kind args", and how would non-newbies extract its "info" field?

[Chris Bailey]

Eduardo Ochs said:

For example, what are the better ways to discover that myplus11 above is of an object of the class Syntax, of the form "node info kind args", and how would non-newbies extract its "info" field?

You can use the #check <arg> command to get the type of <arg>. #check myplus11 should show myplus11: TSyntax myplus in the info window.

Most people are either going to search the docs, or use vscode's right-click menu options, like to go definition and go to type definition.

[Eduardo Ochs]

It's hard to extract the values of subfields from the info window! I was looking for something that would let me extract the values of subfields and subsubfields and put them into variables, like this -

open Lean
def my1      := Syntax.mkNumLit "1"
def myadd    := mkIdent `Nat.add
def myplus   := `«term_+_»
def myadd11  := Syntax.mkApp myadd #[my1, my1]
def myplus11 := mkNode myplus #[my1, mkAtom "+", my1]

macro "extractFrom " input:term " => " pat:term " => " result:term : term =>
  `(match ($input) with
     | some ($pat) => some ($result)
     | _ => none)

def a := some myadd11
#check a
#eval  a
#check Term

def b := extractFrom a => Syntax.node info kind args => info
#check b
#eval  b

Note that the macro "extractFrom" above is buggy! It worked for me in a simpler case (not shown), but it doesn't work in the code above. I'll try to fix that tomorrow - more later...