Getting the type of a theorem in Rust?

Stream: Is there code for X?

[Alessandra Simmons]

I'm working on a project where I need to be able to use the types of various theorems from Lean in Rust. For example, if I had

@[my_export_tag]
theorem zero_add_custom (a: ℚ) : (0: ℚ) + a = a := by
  exact Rat.zero_add a

I would want to receive some structured representation of 0 + a = a at compile-time in Rust. (For example, getting the data as something like LeanTree::Eq(LeanTree::Add(LeanTree::Rational(0, 1), LeanTree::Rational('a')), LeanTree::Rational('a'))). Does anything along those lines already exist?

If something like that doesn't exist, is there a way to en masse export that kind of data as JSON or some other portable format that I can parse into something similar?

[Eric Wieser]

Does this help?

import Mathlib

-- this probably doesn't produce the Json you want, but you can replace these with custom instances / functions
deriving instance Lean.ToJson for Lean.Syntax.Preresolved
deriving instance Lean.ToJson for String.Pos
deriving instance Lean.ToJson for Substring
deriving instance Lean.ToJson for Lean.SourceInfo
deriving instance Lean.ToJson for Lean.Syntax
deriving instance Lean.ToJson for Lean.DataValue
deriving instance Lean.ToJson for Lean.Literal
deriving instance Lean.ToJson for Lean.LevelMVarId
deriving instance Lean.ToJson for Lean.Level
deriving instance Lean.ToJson for Lean.BinderInfo
instance : Lean.ToJson Lean.MData where
  toJson d := Lean.ToJson.toJson d.entries
deriving instance Lean.ToJson for Lean.Expr

-- some really thin boilerplate around `inferType`
elab "#show_type_json " t:term : command => Lean.Elab.Command.runTermElabM fun vars => do
  let e ← Lean.Elab.Term.elabTerm t none
  let typ ← Lean.Meta.inferType e
  Lean.logInfo m!"{Lean.ToJson.toJson typ}"


-- your example
theorem zero_add_custom (a: ℚ) : (0: ℚ) + a = a := by
  exact Rat.zero_add a

#show_type_json zero_add_custom

[Kim Morrison]

I was about to post a slightly messier version of exactly the same approach. :-)

[Kim Morrison]

Likely Alessandra wants to drop a lot of this information, and maybe compress iterated Expr.app into an Array of arguments. But it may make sense to do these as JSON-to-JSON transformations, keeping the initial JSON output as faithful as possible to the Lean Expr structure.

[Kim Morrison]

(The "bigger picture" answer to Alessandra's question also being --- no, there isn't something off the shelf for this, but Lean's metaprogramming means that certainly anything in this direction is possible.)

[Kim Morrison]

I wonder if we should just turn on all those instances above by default, so that next time some asks for #synth Lean.ToJson Lean.Expr it just works.

[Eric Wieser]

Kim Morrison said:

But it may make sense to do these as JSON-to-JSON transformations, keeping the initial JSON output as faithful as possible to the Lean Expr structure.

On the other hand, the transformation might require writing inferType in rust to attach types to subexpressions, in which case doing the processing all on the Lean side is likely to work better

[Eric Wieser]

Kim Morrison said:

I wonder if we should just turn on all those instances above by default, so that next time some asks for #synth Lean.ToJson Lean.Expr it just works.

I think the Substring instance is likely dangerous; sometimes you want it to serialize as s.toString, other times you actually want the offset information

[Eric Wieser]

The Level instance probably would be more user-friendly if it sent .{37} to 37 rather than

{"succ":
 {"succ":
  {"succ":
   {"succ":
    {"succ":
     {"succ":
      {"succ":
       {"succ":
        {"succ":
         {"succ":
          {"succ":
           {"succ":
            {"succ":
             {"succ":
              {"succ":
               {"succ":
                {"succ":
                 {"succ":
                  {"succ":
                   {"succ":
                    {"succ":
                     {"succ":
                      {"succ":
                       {"succ":
                        {"succ":
                         {"succ":
                          {"succ":
                           {"succ":
                            {"succ":
                             {"succ":
                              {"succ":
                               {"succ":
                                {"succ":
                                 {"succ":
                                  {"succ":
                                   {"succ":
                                    {"succ":
                                     "zero"}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}

[Eric Wieser]

Similarly for Lean.Literal

[Alessandra Simmons]

Eric Wieser said:

Does this help?

Ah, that's really quite helpful! I'll probably do JSON-to-JSON transformations on something very similar to this, like Kim was recommending. Also, as a side note, "wow!" to instances as a language feature.