string.replace

Stream: general

[Johan Commelin]

Currently, to_additive can replace substrings that don't contain _ to guess the additive version of the name.
So mul becomes add, and one becomes zero.
I would like to add support for mapping one_le to nonneg and one_lt to pos, etc...

/-- Dictionary of words used by `to_additive.guess_name` to autogenerate
names. -/
meta def tokens_dict : native.rb_map string string :=
native.rb_map.of_list $
[("one_le", "nonneg"), -- this doesn't work
  ("mul", "add"), ("one", "zero"), ("inv", "neg"), ("prod", "sum")]

/-- Autogenerate target name for `to_additive`. -/
meta def guess_name : string → string :=
string.map_tokens '_' $
string.map_tokens ''' $
λ s, (tokens_dict.find s).get_or_else s

[Johan Commelin]

Is there some sort of string.replace or anything I could use for this?

[Yury G. Kudryashov]

As you can see, guess_name splits the name on _ and ', maps subwords using tokens_dict, then joins the results.

[Johan Commelin]

Yes... that's why I'm asking here...

[Johan Commelin]

I would like to have a fancier guess_name, but since lean isn't python, I don't know how to do this.

[Johan Commelin]

import data.string.regex didn't work :sad:

[Johan Commelin]

We need someone to formalise Chomsky's formal languages etc...

[Johan Commelin]

Should I write a string.replace or is that something that typically needs VM support?

[Gabriel Ebner]

Look at data.string.defs and data.string.basic. If you can find nothing there, you can always convert the string to a list of characters and back.

[Johan Commelin]

Hmmm... it's not there

[Johan Commelin]

I'll see if I get get something working

[Mario Carneiro]

Why not use a function that processes the list after splitting so that tr ("one" :: "le" :: s) = "nonneg" :: tr s

[Mario Carneiro]

that way you don't have to do any string manipulation, and you also don't introduce false matches like zone_le ~> znonneg

[Johan Commelin]

Yup, that's what I'm trying now

[Johan Commelin]

/-- Dictionary used by `to_additive.guess_name` to autogenerate names. -/
meta def tr : list string → list string
| ("one" :: "le" :: s) := "nonneg" :: tr s
| ("one" :: "lt" :: s) := "pos"    :: tr s
| ("le" :: "one" :: s) := "nonpos" :: tr s
| ("lt" :: "one" :: s) := "neg"    :: tr s
| ("mul" :: s)         := "add"    :: tr s
| ("inv" :: s)         := "neg"    :: tr s
| ("div" :: s)         := "sub"    :: tr s
| ("one" :: s)         := "zero"   :: tr s
| ("prod" :: s)        := "sum"    :: tr s
| (x :: s)             := (x :: tr s)
| []                   := []

/-- Autogenerate target name for `to_additive`. -/
meta def guess_name : string → string :=
string.map_tokens ''' $
λ s, string.intercalate (string.singleton '_') $
tr (s.split_on '_')

[Johan Commelin]

Nope, I see what I need to fix

[Gabriel Ebner]

tr ["foo", "one"]?

[Johan Commelin]

Exactly

[Johan Commelin]

Fixed

[Johan Commelin]

#eval guess_name "le_mul_of_one_le_right'" -- "le_add_of_nonneg_right'"