Is there a variant of repr that "prints the type"?

Stream: new members

[Eduardo Ochs]

I wrote my first DSL a few days ago - here, screenshot - and I'm in a stage in which I still have to decompose each example in the Metaprogramming book into 10 smaller snippets to understand what is going on in it... and this looks like a good way to explore (specific) Syntax/TSyntax objects:

import Lean
open Lean Elab Command

elab "#withstring " x:str : command =>
  match x with
  | `("a") => logInfo x
  | `("b") => do { logInfo x; logInfo (repr x) }
  | `("c") => do { logInfo x; logInfo (repr x.raw) }
  | _ => Elab.throwUnsupportedSyntax

#withstring "a"
#withstring "b"
#withstring "c"

I know that repr o converts o to its repr as a string, and #check o prints o and its type - but #check is a command, so it has access to the current context...

Is there a function that receives an object o and returns its type converted to a string?

[Damiano Testa]

Could you give an example of an o and what you would like to obtain?

[Eduardo Ochs]

Oops, sorry!
In my example above the #withstring "b" displays repr x without saying that its type is TSyntax `str.

[Kyle Miller]

Do you need a string for your particular application? Or is this for use with logInfo?

[Eduardo Ochs]

It's for logInfo! I asked for the type "as a string" because that seemed to be general enough...

[Eduardo Ochs]

...in the sense of: "people that start from the code that returns the type as a string and then discover how that type was represented before being converted into a string".

[Eduardo Ochs]

I was planning to write a blog post, or something like that looks like one, to explain what I did to decypher some examples of the Metaprogramming book, and why I am still stuck at some other examples... would that be useful?

[Kyle Miller]

Few things use repr, as it turns out. It's mostly for the case where you have a runtime representation that you want to turn into a string representation, where in metaprogramming you already are working with an Expr representation of the object rather than a runtime representation, and the Expr representation is "richer" in a number of ways.

For example, with the Expr representation, you can compute the type of the term (as an Expr).

For repr, if you really want to work with it, you would have to make your own version that also includes a reprTypePrec field for creating a representation of the type.

Here's a simple #check command:

import Lean

open Lean Elab Command Meta

elab "#my_check " t:term : command => do
  runTermElabM fun _ => do -- go into term elaboration mode after processing any `variables` commands
    let e ← Term.elabTermAndSynthesize t none -- elaborate `t` and run all elaboration tasks to completion
    let eTy ← inferType e --  compute the type of `e`
    logInfo m!"{e} : {eTy}" -- log a MessageData with `e` and `eTy` embedded into it

#my_check "s"
-- "s" : String

The logInfo line is not using repr at all. Instead, e and eTy are both Exprs, they are being embedded into the MessageData, and then, eventually, they are pretty printed (not using repr) in such a way that you can hover over them in the InfoView and get informational popups.

[Eduardo Ochs]

Wow! That's exactly what I was looking for! Thanks! =)

[Eduardo Ochs]

...except for one thing: sometimes I need to inspect objects whose types have metavariables - like here, in which #my_check gives the error typeclass instance problem is stuck, it is often due to metavariables but #check handles that in a nice way...

#check    do logInfo "foo"
#my_check do logInfo "foo"

Is that trivial to fix? How?

[Kyle Miller]

The "typeclass instance problem is stuck" error comes from elabTermAndSynthesize. You can do some of it manually to adjust some configuration:

import Lean

open Lean Elab Command Meta

elab "#my_check " t:term : command => do
  runTermElabM fun _ => do -- go into term elaboration mode after processing any `variables` commands
    let e ← Term.elabTerm t none -- elaborate `t` and run all elaboration tasks to completion
    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
    let eTy ← inferType e --  compute the type of `e`
    logInfo m!"{e} : {eTy}" -- log a MessageData with `e` and `eTy` embedded into it

#my_check do logInfo "foo"
-- logInfo ((MessageData.ofFormat ∘ format) "foo") : ?m.983 Unit

[Kyle Miller]

If you right click on #check and "Go to Definition" you can see how #check does it.