Request: Add string formatting operator

[jonesmartins]

String formatting overloads would make debugging easier when used in conjunction with PrintT(). I'm aware VSCode has a LLVM debugger, but the Toolbox does not... There might be other uses of which I'm not aware.

For example, we could have a TLCExt!Format(sequence) operator that converts any non-string element of a sequence to string and concatenates all of them. That might be possible in TLA⁺, but slow because the language lacks typing.

Any thoughts?

[jonesmartins]

Also, TLA+ doesn't allow indexing strings to check if it starts and ends with \", or checking whether STRING contains a non-character element.

[lemmy]

Strings are sequences in TLA+. Do any of the operators below help with your use case? https://github.com/tlaplus/CommunityModules/blob/626a6bdf03b841dc97a371bc8fe88f7d5992aa76/modules/SequencesExt.tla#L366-L432

By the way, does the TLA+ debugger (VSCode) address your underlying debugging need?

[jonesmartins]

Strings are sequences in TLA+. Do any of the operators below help with your use case?

They don't, unfortunately.

---

TLC isn't treating strings as sequences here:

\* ToString, PrintT from TLC module
\* Head from Sequences module
\* flatten and Last from SequencesExt module
 
Str(s) ==
  LET Result == ToString(s)
  IN IF Head(Result) = "\"" /\ Last(Result) = "\""
     THEN s
     ELSE Result

Format(seq) ==
  IF Len(seq) = 0 THEN seq
  ELSE
    LET flatten[i \in 1..Len(seq)] ==
        IF i = 1
        THEN Str(seq[i])
        ELSE flatten[i-1] \o Str(seq[i])
    IN flatten[Len(seq)]

...

ASSUME PrintT(Format(<<"Hello", 2>>))

It's interesting that the flatten function works fine with indexes, but Str does not

The example above generated the error: The argument of Head should be a sequence, but instead it is: "2"

Also, this doesn't work either:

Str(s) ==
  IF s \notin STRING
  THEN ToString(s)
  ELSE s

Generates Attempted to check if the value: 2 is an element of STRING.

Although I'm not so sure about the latter Str operator.

---

By the way, does the TLA+ debugger (VSCode) address your underlying debugging need?

It did! :)

[lemmy]

You've discovered a shortcoming of TLC, not of TLA+: TLC does not have characters, which is why, e.g., Head("abc") doesn't work (compare: https://github.com/tlaplus/tlaplus/issues/512#issuecomment-717602371).

[jonesmartins]

Given than many operators in the CommunityModules are overriden by Java implementations, would it be possible or, rather, useful to have a Format operator (or anything of the sort) anyway, since one can't be specified in TLA+?

[lemmy]

What would the definition of TLCExt!Format look like?

[jonesmartins]

My TLA+ definition of TLCExt!Format above failed, so I don't really know. But operator-wise, we have two options:

1. Format(formatString, parameters) like Format("[{}, {}, {}]", <<1, 2, 3>>);
2. Format(sequence) like Format(<<"[", 1, ",", 2, ",", 3, "]">>), which I tried to specify;

The first one reminds me of a few dynamically typed languages. It's easier to read and harder to implement. Also, it's depends on some arbitrary placeholder. In this case, "{}".

The second one is a little harder to read, but it only depends on string conversion and concatenation.

[lemmy]

Let's just expose Java's String#format as Format(formatString, sequenceOfParameters).

It is also consistent with: https://github.com/tlaplus/CommunityModules/blob/626a6bdf03b841dc97a371bc8fe88f7d5992aa76/modules/CSV.tla#L9-L14?

[jonesmartins]

So I assume the placeholders would be %1, %2, and so on? Looks good to me!

[lemmy]

https://docs.oracle.com/javase/7/docs/api/java/util/Formatter.html

[jonesmartins]

Perfect. I get it now. Thanks, Markus