How do you print object that you don't know fully?

Stream: general

[lunuy]

I'm studying LEAN4 internals and I want to see the result of Lean.readModuleData function, however, I cannot print it (its type is ModuleData × CompactedRegion) and I cannot derive ToString for it also. In situation like this, how do you print objects? I think implementing printing function for every types is really painful.

[Eric Taucher]

lunuy said:

I think implementing printing function for every types is really painful.

In the same boat at present.

What is somewhat helpful but only for the simpler types is using an LLM. Currently find some success with simpler types using Claude and/or Mistral but have not tried all LLMs, e.g.

Create Lean 4 toString and toJson for this type

<type definition>

Also consider using Lean toJson.

One caveat I found with toJson is that a Lean list, ( ['a','b','c'] ) and a Lean array ( #['a','b','c']) will both be converted to a JSON array as there is no JSON list. (JSON syntax)

My lean file for experimenting with toString and toJson.
Had to cut off much of it to meet the posting length. :frown:

example.lean

import Lean.Data.Json    -- ToJson

-- https://github.com/teorth/equational_theories/blob/main/equational_theories/ParseImplications.lean#L12-L20
structure Implication where
  lhs : String
  rhs : String
  finite : Bool
deriving Lean.ToJson

#print Implication
/-
structure Implication : Type
number of parameters: 0
fields:
  Implication.lhs : String
  Implication.rhs : String
  Implication.finite : Bool
constructor:
  Implication.mk (lhs rhs : String) (finite : Bool) : Implication
-/

-- Define the ToString instance for Implication
instance : ToString Implication where
  toString imp :=
    "Implication { lhs := " ++ imp.lhs ++
    ", rhs := " ++ imp.rhs ++
    ", finite := " ++ toString imp.finite ++ " }"

#check { lhs := "a", rhs := "b", finite := true : Implication }
-- { lhs := "a", rhs := "b", finite := true } : Implication
#check Implication.mk "A" "B" true
-- { lhs := "A", rhs := "B", finite := true } : Implication
#eval Implication.mk "A" "B" true
-- Implication { lhs := A, rhs := B, finite := true }
#eval IO.println (Lean.toJson { lhs := "a", rhs := "b", finite := true : Implication } ).pretty
-- {"rhs": "b", "lhs": "a", "finite": true}
#eval toString { lhs := "a", rhs := "b", finite := true : Implication }
-- "Implication { lhs := a, rhs := b, finite := true }"
def Implication_01 := Implication.mk "A" "B" true
#check Implication_01
-- Implication_01 : Implication
#eval Implication_01
-- Implication { lhs := A, rhs := B, finite := true }
#eval toString Implication_01
-- "Implication { lhs := A, rhs := B, finite := true }"
#eval IO.println (Lean.toJson (Implication.mk "a" "b" true)).pretty
-- {"rhs": "b", "lhs": "a", "finite": true}
#eval IO.println (Lean.toJson Implication_01 ).pretty
-- {"rhs": "B", "lhs": "A", "finite": true}

-- ----------------------------------------------------------------------------

-- Define an list of strings
def listOfStrings : List String := ["a", "b", "1", "Hello, World"]
#check listOfStrings
-- listOfStrings : List String
#eval listOfStrings
-- ["a", "b", "1", "Hello, World"]
#eval toString listOfStrings
-- "[a, b, 1, Hello, World]"
#eval IO.println (Lean.toJson listOfStrings).pretty
-- ["a", "b", "1", "Hello, World"]

-- Define an array of strings
def arrayOfStrings : Array String := #["a","b","1","Hello, World"]
#check arrayOfStrings
-- arrayOfStrings : Array String
#eval arrayOfStrings
-- #["a", "b", "1", "Hello, World"]
#eval toString arrayOfStrings
-- "#[a, b, 1, Hello, World]"
#eval IO.println (Lean.toJson arrayOfStrings).pretty
-- ["a", "b", "1", "Hello, World"]

instance : ToString (Array String) where
  toString arr :=
    let items := arr.map (fun s => "\"" ++ s ++ "\"")
    let joined := String.intercalate ", " items.toList
    s!"[{joined}]"

#eval toString (#["hello", "world"])
-- "[\"hello\", \"world\"]"
#eval toString (#["hello world"])
-- "[\"hello world\"]"
#eval toString (#["hello, world"])
-- "[\"hello, world\"]"
#eval toString listOfStrings
-- "[a, b, 1, Hello, World]"
#eval toString arrayOfStrings
-- "[\"a\", \"b\", \"1\", \"Hello, World\"]"  -- NB This changed with the addition of `instance : ToString (Array String) where`

[Kevin Buzzard]

You can enclose code in quadruple backticks to display it properly in spoilers.

[Eric Taucher]

Kevin Buzzard said:

You can enclose code in quadruple backticks to display it properly in spoilers.

Did not know that trick for Zulip markdown. To many variations for Markdown and too many forums to learn, oh my!

[Yaël Dillies]

That's a standard markdown feature I believe. When you want to enclose something that contains n consecutive backticks, you can use n + 1 consecutive backticks

[Ruben Van de Velde]

The use of "standard" when referring to markdown is somewhat risky :)

[Mario Carneiro]

@lunuy There are objects of unknown (to lean) type stored inside ModuleData. CompactedRegion you can ignore, it's not really a piece of data itself but rather a handle to the region which stores the ModuleData, and which can be used (unsafely) to deallocate it. You can view arbitrary lean objects using the structure that the garbage collector uses to do its job; this is implemented in the oleandump library, invented precisely for being able to inspect the module data in .olean files