string replace

Stream: metaprogramming / tactics

[Joe Palermo]

Is there any nice way to do string replacement? i.e "xyz".replace("x", "a") => "ayz"? Seems there are no utilities for this.

Context:
I'm using metaprogramming to extract and process a dataset consisting of Lean proofs in raw text format. I'd like to do some cleanup like changing universe variables to a consistent set (u_1, u_2, etc...). I figure it'll be easiest to do this with string replacement, but if there's some easy way to replace universe variables in the underlying expr corresponding to each proof that would work too.

[Scott Morrison]

I think basically all string munging needs to be done as list-of-characters munging.

[Scott Morrison]

You can replace universe levels at the expr level too.

[Scott Morrison]

But I'm failing to immediately find clear examples of this being done. :-) I do remember seeing some functions for doing this at whole-expression level, but what I'm seeing now is traversing expressions and manually manipulating level terms.

[Joe Palermo]

Scott Morrison said:

I think basically all string munging needs to be done as list-of-characters munging.

That's good to know

[Joe Palermo]

Scott Morrison said:

But I'm failing to immediately find clear examples of this being done. :-) I do remember seeing some functions for doing this at whole-expression level, but what I'm seeing now is traversing expressions and manually manipulating level terms.

Wow I would love to have a function for doing that at whole-expression level. If anyone finds this please let me know :)

[Floris van Doorn]

Joe Palermo said:

Wow I would love to have a function for doing that at whole-expression level. If anyone finds this please let me know :)

I think you want docs#expr.instantiate_univ_params?

[Jason Rute]

Joe, (based on my understanding of your project), is this on the data gathering side or on the putting the expression back into Lean side? If on the data gathering side, you could also use docs#expr.collect_univ_params I think to find the universe params in your expression and print them. If it is on the putting the expression into Lean side, you can't modify the expression, because you haven't parsed your string into an expression. And you can't parse your string into an expression until you handle the missing universes. I suggest in that case, you may want to do the string processing in Python (or whatever language you are using to generate your expressions). Lean 3 doesn't have good string editing.

Now, if on the data gathering side you want to standardize the universes in the expressions before dumping them to output, then I think a combination of docs#expr.collect_univ_params to find the universe names and docs#expr.instantiate_univ_params to replace them, could work.

[Joe Palermo]

@Floris van Doorn Thanks for pointing it out!

@Jason Rute It's on the data gathering side. Like you pointed out, it will make things easier to standardize universes before dumping to output. In the interim I wrote up a Python script to do it but it's ugly and could lead to bugs, so I'd rather do it in Lean if I can. I'll try expr.instantiate_univ_params