A String compares equal to a String or a str by its bytes, and a prelude builder's String is checked at the caller's line.

This commit is contained in:
Joseph Ferano 2026-09-26 12:22:17 +07:00
parent 5cc661d6ab
commit bfdd971baa
8 changed files with 162 additions and 19 deletions

View File

@ -33,7 +33,8 @@ str. Waits on the dyn-unless-annotated design.
CLOSED: [2026-09-26] CLOSED: [2026-09-26]
Its field and constructor are refused outside the prelude; a str or a code point is checked at Its field and constructor are refused outside the prelude; a str or a code point is checked at
run time at the append that stores it (literals at compile time), a [const u8] is refused for run time at the append that stores it (literals at compile time), a [const u8] is refused for
(str b). Rules out a String type in the backends, s[i] = c, and a byte path that skips the check. (str b); a prelude builder's String is checked at the caller's call. = and != compare bytes.
Rules out a String type in the backends, s[i] = c, a String map key, and a byte path that skips the check.
** DONE Any typed container crosses into dyn as a view ** DONE Any typed container crosses into dyn as a view
CLOSED: [2026-09-26] CLOSED: [2026-09-26]

View File

@ -7536,8 +7536,12 @@ byte arrives through `string-new`, `append`, `insert` or `bytes->string`. Text
the checker cannot prove valid — any str, since `(str b)` does not check — is the checker cannot prove valid — any str, since `(str b)` does not check — is
checked by `flan_utf8_check` at the site that stores it; a code point by checked by `flan_utf8_check` at the site that stores it; a code point by
`flan_rune_check` inside `flan_string_put_rune`. Literals are checked at compile `flan_rune_check` inside `flan_string_put_rune`. Literals are checked at compile
time. The prelude's builders end in `(bytes->string b)`, so a builder given bytes time. The prelude's builders wrap their Vec unchecked, and `ordinary_call`
that are not UTF-8 stops at the prelude's line, not the caller's. checks any String a prelude function answers at the caller's call
(`checked_string`), so bytes that are not UTF-8 stop at the line that asked.
`=` and `!=` compare a String with a String or a str through their str views;
`peeks_string` decides that from the operands' declared types without checking
them twice. Ordering and map keys are refused with the fix named.
Positions are characters: `flan_string_index` walks to one and signals Positions are characters: `flan_string_index` walks to one and signals
BoundsError with the character count as the length, which is why it joins BoundsError with the character count as the length, which is why it joins

View File

@ -4924,6 +4924,13 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
| Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str" | Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str"
| t when bytewise_key t -> | t when bytewise_key t ->
Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat" Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"
| t when is_string_ty t ->
fail loc
"a String owns its bytes, and a map would share them with it rather \
than copy them, so a String is not a map key. Key the map by str and \
put %s, which is the String's text for as long as the String is not \
changed"
(if fln_source loc then "str(s)" else "(str s)")
| Types.Named n when Hashtbl.mem env.structs n -> struct_key_pair env loc n | Types.Named n when Hashtbl.mem env.structs n -> struct_key_pair env loc n
(* A data type key would have to hash the tag and then only the bytes the (* A data type key would have to hash the tag and then only the bytes the
case in hand actually uses — the rest of the payload is indeterminate, case in hand actually uses — the rest of the payload is indeterminate,
@ -11131,6 +11138,97 @@ and prelude_fn ctx name =
let moved = "prelude~/" ^ name in let moved = "prelude~/" ^ name in
if Hashtbl.mem ctx.env.fns moved then moved else name if Hashtbl.mem ctx.env.fns moved then moved else name
(* Whether [name] is the prelude's own function. *)
and prelude_defined ctx name =
match Hashtbl.find_opt ctx.env.fn_locs name with
| Some at -> String.equal at.Loc.file Prelude.file
| None -> false
(* A String a prelude builder answered, checked here, at the call the program
wrote. The builders take bytes — (to-lower b), (join parts sep) — and wrap
what they built without a check of their own, because a check inside the
prelude would stop the program at the prelude's line rather than at the
caller's. A builder reached through a function value is not checked. *)
and checked_string ctx loc (call : Tast.expr) =
let sl = fresh_slot ctx string_ty in
let s = mk loc string_ty (Tast.Local sl) in
mk loc string_ty
(Tast.Let ([ (sl, call) ],
[ rt loc Types.Unit "flan_utf8_check" [ string_bytes ctx loc s; here loc ];
s ]))
(* Whether an operand is a String, read off what the operand is without
checking it: a local or a global of that type, a call to a function that
answers one, a field of that type, or one of the builtins that make one. A
comparison asks this of every operand, so it must not walk them. *)
and peeks_string ctx (a : Ast.expr) =
let rec ty (a : Ast.expr) =
match a.Ast.e with
| Ast.Var n ->
(match lookup ctx n with
| Some b -> Some b.bty
| None ->
(match Hashtbl.find_opt ctx.env.globals n with
| Some (t, _) -> Some t
| None -> None))
| Ast.Call ({ Ast.e = Ast.Var ("string-new" | "bytes->string"); _ }, _) ->
Some string_ty
| Ast.Call ({ Ast.e = Ast.Var "deref"; _ }, [ p ]) ->
(match ty p with Some (Types.Ptr (_, t)) -> Some t | _ -> None)
| Ast.Call ({ Ast.e = Ast.Var f; _ }, _) ->
(match Hashtbl.find_opt ctx.env.fns f with
| Some (_, ret) -> Some ret
| None -> None)
| Ast.Field (t, name) ->
(match ty t with
| Some (Types.Named n | Types.Ptr (_, Types.Named n)) ->
(match fields_named ctx.env n with
| Some st ->
(match Tast.field_index st name with
| Some i -> Some (List.nth st.Tast.fields i).Tast.fty
| None -> None)
| None -> None)
| _ -> None)
| _ -> None
in
match ty a with Some t -> string_or_ptr t | None -> false
(* = and != over a String and a String or a str: the texts' bytes compared,
through the str view each has, which is the comparison str already has.
The orderings are refused as they are on a str, naming bytes<?. *)
and string_compare ctx ~want loc name p args =
(match name with
| "=" | "!=" -> ()
| _ ->
fail loc
"%s orders machine numbers and enums, and a String is neither. Text is \
ordered by its bytes with %s"
name
(if fln_source loc then "bytes<?(bytes-view(a), bytes-view(b))"
else "(bytes<? (bytes-view a) (bytes-view b))"));
let as_str (x : Ast.expr) =
let e =
match x.Ast.e with
| Ast.Str _ -> check ctx ~want:Types.String x
| _ -> check ctx x
in
match e.Tast.ty with
| Types.String -> e
| t when string_or_ptr t ->
mk x.Ast.loc Types.String
(Tast.Prim (Tast.StrOfBytes, [ string_bytes ctx x.Ast.loc e ]))
| other ->
fail x.Ast.loc "%s compares a String with a String or a str, found %s"
name (tyname x.Ast.loc other)
in
let ops = List.map as_str args in
let link u v = mk loc Types.Bool (Tast.Prim (p, [ u; v ])) in
match ops with
| [ a; b ] -> expect ctx loc ~want (link a b)
| _ ->
let pairs = if String.equal name "!=" then all_pairs else adjacent_pairs in
expect ctx loc ~want (cmp_over ctx loc Types.String ~pairs ~link ops)
and string_call ctx ~want loc name args = and string_call ctx ~want loc name args =
let i64 n = mk loc (Types.Int Types.I64) (Tast.Int (n, Types.I64)) in let i64 n = mk loc (Types.Int Types.I64) (Tast.Int (n, Types.I64)) in
match name, args with match name, args with
@ -11366,6 +11464,9 @@ and named_call ?(qualified = false) ctx ~want loc name args =
let x, y, rest = let x, y, rest =
match args with x :: y :: rest -> x, y, rest | _ -> assert false match args with x :: y :: rest -> x, y, rest | _ -> assert false
in in
if List.exists (fun a -> peeks_string ctx a) args then
string_compare ctx ~want loc name p args
else
(* The first pair decides the type, and whether this is a dyn comparison (* The first pair decides the type, and whether this is a dyn comparison
at all, exactly as it does for the folding operators: [binary] joins at all, exactly as it does for the folding operators: [binary] joins
the two, and every operand after them is checked against the answer. the two, and every operand after them is checked against the answer.
@ -13892,7 +13993,13 @@ and ordinary_call ctx ~want loc name args =
(temps, (temps,
[ rt loc Types.Unit "flan_dyn_ctor_site" [ here loc ]; [ rt loc Types.Unit "flan_dyn_ctor_site" [ here loc ];
mk loc ret (Tast.Call (name, uses)) ]))) mk loc ret (Tast.Call (name, uses)) ])))
| None -> expect ctx loc ~want (mk loc ret (Tast.Call (name, args)))) | None ->
let call = mk loc ret (Tast.Call (name, args)) in
expect ctx loc ~want
(if is_string_ty ret && prelude_defined ctx name
&& not (String.equal loc.Loc.file Prelude.file)
then checked_string ctx loc call
else call))
| None -> | None ->
if Hashtbl.mem ctx.env.datas name then if Hashtbl.mem ctx.env.datas name then
fail loc fail loc

View File

@ -1719,6 +1719,11 @@ let source = {flan|
;; writes (with-allocator a (join parts sep)) and the Vec records the arena, so ;; writes (with-allocator a (join parts sep)) and the Vec records the arena, so
;; the free and the clone never need it named again. ;; the free and the clone never need it named again.
;; ;;
;; **The text builders answer a String without checking it.** Each takes
;; bytes, and a check here would stop the program at this file's line; the
;; checker checks the String at the caller's call instead (check.ml,
;; [checked_string]).
;;
;; **No Result, anywhere.** Running out of storage signals StorageExhausted ;; **No Result, anywhere.** Running out of storage signals StorageExhausted
;; under a `retry` restart and no allocating operation returns an error ;; under a `retry` restart and no allocating operation returns an error
;; (spec-memory.md, "Allocation failure"), so these signatures say what they ;; (spec-memory.md, "Allocation failure"), so these signatures say what they
@ -1777,7 +1782,7 @@ let source = {flan|
(let [b (vec-new u8)] (let [b (vec-new u8)]
(dotimes [i (length parts)] (dotimes [i (length parts)]
(append (addr b) (at parts i))) (append (addr b) (at parts i)))
(bytes->string b))) (String {.bytes b})))
;; n parts yield n-1 separators, and the empty slice of parts yields the empty ;; n parts yield n-1 separators, and the empty slice of parts yields the empty
;; result rather than a leading separator — which is the off-by-one a join ;; result rather than a leading separator — which is the off-by-one a join
@ -1789,13 +1794,13 @@ let source = {flan|
(when (> i 0) (when (> i 0)
(append (addr b) sep)) (append (addr b) sep))
(append (addr b) (at parts i))) (append (addr b) (at parts i)))
(bytes->string b))) (String {.bytes b})))
(defn repeat-bytes [s [const u8] n i32] String (defn repeat-bytes [s [const u8] n i32] String
(let [b (vec-new u8)] (let [b (vec-new u8)]
(dotimes [i n] (dotimes [i n]
(append (addr b) s)) (append (addr b) s))
(bytes->string b))) (String {.bytes b})))
;; The allocating halves of the ASCII case pair. The note above lower-ascii ;; The allocating halves of the ASCII case pair. The note above lower-ascii
;; says why there is no in-place one; these write only bytes of their own. ;; says why there is no in-place one; these write only bytes of their own.
@ -1803,13 +1808,13 @@ let source = {flan|
(let [b (vec-new u8)] (let [b (vec-new u8)]
(dotimes [i (length s)] (dotimes [i (length s)]
(push b (lower-ascii (at s i)))) (push b (lower-ascii (at s i))))
(bytes->string b))) (String {.bytes b})))
(defn to-upper [s [const u8]] String (defn to-upper [s [const u8]] String
(let [b (vec-new u8)] (let [b (vec-new u8)]
(dotimes [i (length s)] (dotimes [i (length s)]
(push b (upper-ascii (at s i)))) (push b (upper-ascii (at s i))))
(bytes->string b))) (String {.bytes b})))
;; Every non-overlapping occurrence, left to right, which is the rule that ;; Every non-overlapping occurrence, left to right, which is the rule that
;; makes (replace-bytes (bytes-view "aaa") (bytes-view "aa") (bytes-view "b")) answer "ba" and ;; makes (replace-bytes (bytes-view "aaa") (bytes-view "aa") (bytes-view "b")) answer "ba" and
@ -1840,7 +1845,7 @@ let source = {flan|
(do (do
(append (addr b) (slice s i (length s))) (append (addr b) (slice s i (length s)))
(set i (length s)))))) (set i (length s))))))
(bytes->string b))) (String {.bytes b})))
;; A (Vec [u8]) cannot be written at a let, and this one-line function is where ;; A (Vec [u8]) cannot be written at a let, and this one-line function is where
;; the type is said instead. (vec-new) takes its element type as a *bare ;; the type is said instead. (vec-new) takes its element type as a *bare
@ -1960,7 +1965,7 @@ let source = {flan|
(dotimes [i (- p (length d))] (dotimes [i (- p (length d))]
(push b \0)) (push b \0))
(append (addr b) d)))))))) (append (addr b) d))))))))
(bytes->string b))) (String {.bytes b})))
;; ── Still refused, and what the reason is now ───────────────────────── ;; ── Still refused, and what the reason is now ─────────────────────────
;; ;;

View File

@ -57,6 +57,14 @@
(let [j (join (slice [(bytes-view "a") (bytes-view "b")]) (bytes-view "-"))] (let [j (join (slice [(bytes-view "a") (bytes-view "b")]) (bytes-view "-"))]
(println j) (println j)
(free j)) (free j))
;; = and != compare bytes, against a String or a str, either side first.
(let [a (string-new "日本")
b (string-new "日")]
(append b 0x672c)
(println (= a b) (!= a b) (= a "日本") (= "日本" a) (= a "日") (!= b "x"))
(println (= a b (to-upper (bytes-view "日本"))))
(free a)
(free b))
(let [e (string-new)] (let [e (string-new)]
(println (length e) (rune-count e)) (println (length e) (rune-count e))
(free e)) (free e))

View File

@ -1,8 +1,9 @@
;;;; What a String refuses at run time, one per run: the argument chooses. ;;;; What a String refuses at run time, one per run: the argument chooses.
;;;; Bytes that are not UTF-8, reached through a str, stop the program at the ;;;; Bytes that are not UTF-8, reached through a str, stop the program at the
;;;; append; so does a code point with no encoding; a character position past ;;;; append; so does a code point with no encoding; a character position past
;;;; the end signals BoundsError counted in characters. The test asserts the ;;;; the end signals BoundsError counted in characters; and a text builder
;;;; line and column of each. ;;;; given bytes that are not UTF-8 stops at the call that asked for it. The
;;;; test asserts the line and column of each.
(defonce bad [2 u8]) (defonce bad [2 u8])
(defn main [args [str]] i32 (defn main [args [str]] i32
@ -16,6 +17,7 @@
(= which 1) (append s (+ 0xd800 which -1)) (= which 1) (append s (+ 0xd800 which -1))
(= which 2) (insert s 3 "x") (= which 2) (insert s 3 "x")
(= which 3) (println (remove s 2)) (= which 3) (println (remove s 2))
(= which 5) (println (to-lower (slice bad)))
:else (append s (bytes->string (let [v (vec-new u8)] (push v 0xff) v)))) :else (append s (bytes->string (let [v (vec-new u8)] (push v 0xff) v))))
(println s)) (println s))
0) 0)

View File

@ -2024,7 +2024,8 @@ let () =
let owned_out = let owned_out =
"héllo wörld日!\n17 13\n😀h→éllo wörld日!\n8594\n128512\n\ "héllo wörld日!\n17 13\n😀h→éllo wörld日!\n8594\n128512\n\
héllo wörld日!\nabababab 8\n233 246 26085 13\n17 18\ntrue\n17\n\ héllo wörld日!\nabababab 8\n233 246 26085 13\n17 18\ntrue\n17\n\
(Named {.label \"x\" .n 3})\nhéllo wörld日!\n:text\na-b\n0 0\n" (Named {.label \"x\" .n 3})\nhéllo wörld日!\n:text\na-b\n\
true false true true false true\ntrue\n0 0\n"
in in
outputs "an owned String" "programs/string-owned.flan" owned_out; outputs "an owned String" "programs/string-owned.flan" owned_out;
outputs ~opt:"-O0" "an owned String, -O0" "programs/string-owned.flan" outputs ~opt:"-O0" "an owned String, -O0" "programs/string-owned.flan"
@ -2050,12 +2051,16 @@ let () =
arg (match x86 with Some true -> ", --x86" | _ -> "") arg (match x86 with Some true -> ", --x86" | _ -> "")
text code want text code want
end) end)
[ ("0", "string-traps.flan:15:19: this text is not valid UTF-8 — byte 0 \ [ ("0", "string-traps.flan:16:19: this text is not valid UTF-8 — byte 0 \
is 0xc3"); is 0xc3");
("1", "string-traps.flan:16:19: 55296 is not a Unicode scalar value"); ("1", "string-traps.flan:17:19: 55296 is not a Unicode scalar value");
("2", "string-traps.flan:17:19: index 3 is out of bounds for length 2"); ("2", "string-traps.flan:18:19: index 3 is out of bounds for length 2");
("3", "string-traps.flan:18:28: index 2 is out of bounds for length 2"); ("3", "string-traps.flan:19:28: index 2 is out of bounds for length 2");
("4", "string-traps.flan:19:23: this text is not valid UTF-8 — byte 0 \ (* The builder's own check is made at the call, not inside the
prelude. *)
("5", "string-traps.flan:20:28: this text is not valid UTF-8 — byte 0 \
is 0xc3");
("4", "string-traps.flan:21:23: this text is not valid UTF-8 — byte 0 \
is 0xff") ]; is 0xff") ];
(try Sys.remove exe with Sys_error _ -> ()) (try Sys.remove exe with Sys_error _ -> ())
in in

View File

@ -2354,6 +2354,17 @@ let () =
rejects_check "a String through a const pointer is not changed" rejects_check "a String through a const pointer is not changed"
"(defn f [s (Ptr const String)] () (append s \"x\"))" "(defn f [s (Ptr const String)] () (append s \"x\"))"
~needle:"can only be read"; ~needle:"can only be read";
rejects_check "a String is not ordered"
"(defn f [a String b String] bool (< a b))"
~needle:"(bytes<? (bytes-view a) (bytes-view b))";
rejects_check "a String is not a map key"
"(defn f [s String] () (let [m (map-new String i32)] (put m s 1)))"
~needle:"Key the map by str and put (str s)";
rejects_check "a String compares only with text"
"(defn f [s String] bool (= s 3))"
~needle:"= compares a String with a String or a str, found";
accepts "a String equals a String or a str, either side first"
"(defn f [a String b String] bool (and (= a b) (!= \"x\" a) (= a \"y\")))";
accepts "a String through a pointer is changed" accepts "a String through a pointer is changed"
"(defn f [s (Ptr String)] () (append s \"x\") (insert s 0 \\a))"; "(defn f [s (Ptr String)] () (append s \"x\") (insert s 0 \\a))";