Narrowing › string. The names in the examples are those of section 2.
A string alternative is the bare kind, every string, or {:string, set}: a Feel.Type.StringSet (D-39). A set is one of three things, and the analyzer keeps the simplest:
| Written | Is |
|---|---|
string = "a", string in {"a", "b"} | exactly those strings (up to 64) |
string in ["a".."m"], string in (.."m"), string in ("m"..) | an interval of strings, in the order of the run; .. is "no bound" |
string except "a", string in (.."a"], ["m"..) except "a", "m" | every string (or those of the intervals) but the ones left out |
Within the representation budget, string comparisons can keep intervals and excluded points, including ties. Oversized finite sets lose precision. See the common correctness obligations before treating composed facts as proofs.
Comparisons with a string
| Condition | s when true | s when not true |
|---|---|---|
s = "a" | string = "a" | string except "a" | Null |
s != "a" | string except "a" | Null | string = "a" |
s < "m" | string in (.."m") | string in ["m"..) | Null |
s <= "m" | string in (.."m"] | string in ["m"..) except "m" | Null |
s > "m" | string in ("m"..) | string in (.."m"] | Null |
s >= "m" | string in ["m"..) | string in (.."m"] except "m" | Null |
The null rules are those of the other kinds: an ordering of null is null, so a true ordering excludes it and a not-true one keeps Null; s != "a" is true for null (null.md).
Why <= and >= have an except
The order of the run (Feel.Runtime.Compare) is by code point, a prefix first, with a trailing U+0000 left out of the comparison. That order is not total: "m" and "m\u0000" are neither below nor above one another, and they are not equal. The strings with the same key, "m", "m\u0000", "m\u0000\u0000", are a class, and an interval consists of whole classes. So s <= "m" is true for the strings below the class of "m", and for "m" itself, but not for the other strings of its class. When it is not true, the values left are the whole class and above, without "m": string in ["m"..) except "m". The same holds, mirrored, for >=. For almost every use you can read an interval as an interval and an except as "and not that one".
in, and and or
A list of values or ranges is joined in then and met in else, as for numbers (number).
| Condition | s when true | s when not true |
|---|---|---|
s in ("a", "b") | string in {"a", "b"} | string except "a", "b" | Null |
s in ["a".."m"] | string in ["a".."m"] | string in (.."a"], ["m"..) except "a", "m" | Null |
s = "a" or s = "b" | string in {"a", "b"} | string except "a", "b" | Null |
s in ("a", "b", "c") and s != "b" | string in {"a", "c"} | string except "a", "c" | Null |
s > "a" and s < "m" | string in ("a".."m") | string in (.."a"], ["m"..) | Null |
The other side is not a constant
The other side is read as the set of strings it can be. A name, whose set is not known, gives nothing for equality and little for an ordering. As for numbers, when the other side can be null or its kind is not known, else learns nothing.
| Condition | s when true | s when not true |
|---|---|---|
s = s2 | string | Null | string | Null |
s < s2 | string | string | Null |
s = v | string | Null | string | Null |
s = s2 can be true when both are null. s < s2 is not true for a null, so s is a string.
A function of the string
A comparison of a call of a function of strings with a value is not true of a null, so in then the arguments are of the kinds for which the call gives a value of the kind the other side has (D-170; Feel.Analysis.Images says what a call gives). string length(s) > 3 is not true of a null, so s is a string. For the length of a string the comparison says more: it is true of the empty string (a length of 0) or of the others, and the others are one set (StringSet has no set of the strings of a length), so string length(s) > 0 leaves every string except "", and string length(s) = 0 leaves "".
| Condition | s when true | s when not true |
|---|---|---|
string length(s) > 0 | string except "" | string = "" | Null |
string length(s) >= 1 | string except "" | string = "" | Null |
string length(s) != 0 | string except "" | Null | string = "" |
string length(s) = 0 | string = "" | string except "" | Null |
string length(s) < 1 | string = "" | string except "" | Null |
string length(s) > 3 | string except "" | string | Null |
string length(s) < 3 | string | string except "" | Null |
upper case(s) = "ABC" | string | string | Null |
contains(s, "a") = true | string | string | Null |
string length(s) > -1 | string | string | Null |
The function gives a value for the strings and for a list of one string. s here is a string: for a name that is Any, string length(v) > 0 leaves the strings except "", and the lists.
| Condition | v when true | v when not true |
|---|---|---|
string length(v) > 0 | string except "" | list<Any | Null> | Any | Null |
string length(v) = 0 | string = "" | list<Any | Null> | Any | Null |
instance of
| Condition | s when true | s when not true |
|---|---|---|
s instance of string | string | Null |
s instance of number | — | string | Null |
Limits
- A set of more than 64 strings is every string:
s = "a1" or s = "a2" or … or s = "a64"keeps the 64, and a 65th makes itstring. - A set of strings with intervals keeps its single strings next to the intervals and the ones left out of them; there is no cap on those.
- A concatenation of sets that have intervals or exceptions (
s + "!") is not kept: the result is the bare kind. todo.md lists it as still open.
See also: number, null, Any; Feel.Type.StringSet has the algebra (type-system.md, 3.3).