How to beta-reduce/simplify or reduce types in Infoview?

Stream: Is there code for X?

[Atticus Kuhn]

Is there a way to simplify or reduce types in the Lean infoview?

Here's the example: I am creating the embedded DSL for a language inside Lean, and I get complicated types like

rep✝ : SurfaceTy → Type
part : rep✝
  ((fun i ↦
      #[record
            [("n_comment", «int».dict «string»), ("n_name", «int».dict «string»), ("n_nationkey", «int».dict «int»),
              ("n_regionkey", «int».dict «int»), ("size", «int»)],
          record
            [("p_brand", «int».dict «string»), ("p_comment", «int».dict «string»), ("p_container", «int».dict «string»),
              ("p_mfgr", «int».dict «string»), ("p_name", «int».dict «string»), ("p_partkey", «int».dict «int»),
              ("p_retailprice", «int».dict «real»), ("p_size", «int».dict «int»), ("p_type", «int».dict «string»),
              ("size", «int»)],
          record
            [("ps_availqty", «int».dict «real»), ("ps_comment", «int».dict «string»), ("ps_partkey", «int».dict «int»),
              ("ps_suppkey", «int».dict «int»), ("ps_supplycost", «int».dict «real»), ("size", «int»)],
          record
            [("r_comment", «int».dict «string»), ("r_name", «int».dict «string»), ("r_regionkey", «int».dict «int»),
              ("size", «int»)],
          record
            [("s_acctbal", «int».dict «real»), ("s_address", «int».dict «string»), ("s_comment", «int».dict «string»),
              ("s_name", «int».dict «string»), ("s_nationkey", «int».dict «int»), ("s_phone", «int».dict «string»),
              ("s_suppkey", «int».dict «int»), ("size", «int»)]][↑i]!)
    1)

But, this should beta-reduce (i.e. fun is applied to 1), so really this should reduce to

 record
            [("p_brand", «int».dict «string»), ("p_comment", «int».dict «string»), ("p_container", «int».dict «string»),
              ("p_mfgr", «int».dict «string»), ("p_name", «int».dict «string»), ("p_partkey", «int».dict «int»),
              ("p_retailprice", «int».dict «real»), ("p_size", «int».dict «int»), ("p_type", «int».dict «string»),
              ("size", «int»)],

If this example is too complicated, I can try and reduce it to a simpler example.

[Notification Bot]

This topic was moved here from #Is there code for X? > How to beta-reduce/simplify or reduce types in Infoview by Atticus Kuhn.

[Aaron Liu]

maybe dsimp only at * is good enough for you?

[Atticus Kuhn]

Aaron Liu said:

maybe dsimp only at * is good enough for you?

How can I do that? I'm not in tactic mode, as I'm working inside an embedded DSL.

[Aaron Liu]

oh you're not in tactic mode

[Aaron Liu]

which part of the infoview is this then

[Atticus Kuhn]

image.png

I've created an embedded DSL in Lean using syntax macros, such that when I hover over an element of the DSL, the Lean infoview shows the type of that element of the AST. But, the types are not simplified and they are unwieldly large.

[Aaron Liu]

oh how does that work

[Aaron Liu]

where do you attach that information to the syntax

[Atticus Kuhn]

Let's ignore the syntax macros for a second, as that's kind of tangential/peripheral to the question I'm asking. In Lean, if you're in term mode, when you hover over a term, Lean will display the type of that term in the infoview. I'm asking if there is a way to simplify the displayed types in the infoview.

[Atticus Kuhn]

Aaron Liu said:

where do you attach that information to the syntax

Actually, it doesn't work very well right now (as I'm not sure how to attach the location of the original source to the location of the transformed code), but that's beside the point I'm making right now.

[Aaron Liu]

Atticus Kuhn said:

I'm asking if there is a way to simplify the displayed types in the infoview.

not without modifying whatever attaches that information to the syntax

[Aaron Liu]

at least I don't know of any way

[Aaron Liu]

I guess maybe you could go over the infotree any simplify it but

[Aaron Liu]

that feels sort of hacky

[Michael Rothgang]

If you were in tactic mode, you could use the beta_reduce tactic (or just call dsimp). That doesn't work in term mode, though.

[Kyle Miller]

There's set_option pp.beta true to have the pretty printer beta reduce terms. It can be a bit confusing though since tactics might not apply due to non-beta-reduced terms.

There's also trying to get your DSL to create beta reduced terms somehow. Lean itself attempts to do this when it elaborates terms, to avoid the unwieldy non-beta-reduced-types issue.