Delaborator for String.mk

Stream: lean4

[Yann Herklotz]

I was wondering if there was a delaborator for String.mk, or a way to go from a String.mk application back into a Expr.lit (.strLit string), because I believe that is what gets pretty-printed properly.

An example is the following:

example y : "hello" ++ "a" = y := by
  conv => left; reduce

which results in:

{ data := ['h', 'e', 'l', 'l', 'o', 'a'] } = y

whereas I would hope for: "helloa" = y, which is what is produced by dsimp:

example y : "hello" ++ "a" = y := by dsimp

[Kyle Miller]

Writing that delaborator is doable. I wonder whether it is useful to know that you have a non-literal String though? The literal string case is more optimized.

[Kyle Miller]

I'm seeing an even worse term on the master branch after reduce:

{
    data :=
      [{ val := { toBitVec := { toFin := ⟨104, ⋯⟩ } }, valid := ⋯ },
        { val := { toBitVec := { toFin := ⟨101, ⋯⟩ } }, valid := ⋯ },
        { val := { toBitVec := { toFin := ⟨108, ⋯⟩ } }, valid := ⋯ },
        { val := { toBitVec := { toFin := ⟨108, ⋯⟩ } }, valid := ⋯ },
        { val := { toBitVec := { toFin := ⟨111, ⋯⟩ } }, valid := ⋯ },
        { val := { toBitVec := { toFin := ⟨97, ⋯⟩ } }, valid := ⋯ }] }

[Eric Wieser]

Should { toFin := f} delaborate as BitVec.ofFin f?

[Eric Wieser]

The above looks like it's working as intended though; ⟨104, ⋯⟩ : Fin UMax shouldn't delaborate as 104 : Fin UMax

[Yann Herklotz]

Hmm yeah it's definitely useful to know that you aren't dealing with a string literal, but it would be great if it was still readable. Actually, alternatively could we just traverse the expression and turn applications of String.mk into literal Strings? I'll have a look, maybe there are some helper functions for that already, dsimp seems to do something similar (being able to essentially apply ++ on the string literal), but I guess it only operates on string literals.

[Eric Wieser]

Arguably the mistake here is reduce which instructs Lean to ignore any preferred spellings and aggressively unfold everything

[Eric Wieser]

Using simp which runs docs#String.reduceAppend results in much better behavior

[Yann Herklotz]

Yeah I definitely agree, the main issue is we haven’t figured out how to make simp unfold/compute our definition efficiently yet, so have been resorting to reduce which works in most cases.

Thank you for the reference to the simproc! I was trying to find it.