The batch from two reviews plus the acceptance exit code, item by item
Constraints parsing peeled a body-leading map only when its first key was
literally :where; any other keyword fell through to the body, so a typo'd
key surfaced as a baffling error from inside what was meant as a predicate
and a stray map at body start compiled away silently. Any keyword-first map
is read as a constraint map now, but only when something follows it in the
body — a single-form map body is a real dyn value and not a discarded
statement, so that case is left alone.
An empty map literal still parses as a struct literal, (P {}) still meaning
the zero struct for a real struct name — the parser has no symbol table to
tell (take {}) apart from it at that point. check.ml now catches the case
where the name turns out to be a known function instead and says so, rather
than "unknown struct take".
flan_dyn.c's tag comment still said 6 and 7 were free; keywords and maps
took 4 and a kind field under BOX_OBJ, not new top-level tags, so 5, 6 and 7
are what is actually open for the interop handle. NEXT.md and json.flan both
still pointed at test/programs/arena-edn.flan, gone since edn/read stopped
taking an allocator; both now point at what replaced it.
flan_rt.c's flan_str_eq comment claimed the empty string literal was a
hypothetical null-pointer string; it isn't, its address is an interned
symbol's. The real case the zero-length guard exists for is a zero-length
container converted to a string. check.ml's ordering refusal said a string
has no comparison at all, which stopped being true when typed = and !=
grew strings in daed039 — split the message so an equality refusal and an
ordering refusal say the right noun, and updated the pinned rejects_check
rows to match. string-eq.flan gained the row the fast path most wants
tested, a slice against the prefix it was cut from sharing a base pointer at
different lengths, plus a != row at equal length with differing bytes;
acceptance now carries the real output, captured by running the program on
all three lanes. x86.ml's xor-1 comment now names the 0/1 return contract as
a requirement flan_str_eq must hold, not an incidental fact. SPIKE-DUPLICITY
now says plainly that its equality-and-ordering argument landed in daed039
and marks its transcript as the historical state that argument was made
against. FIX.org ticks M2 queue item 5.
And the acceptance runner: the tail check that turns a nonzero failure count
into exit 1 was already there and already fired — a fresh build with one row
broken already exited 1 before anything here changed. What wasn't proven is
that every path through the file's clang/wasmtime/raylib/lldb probes still
reaches that tail rather than skipping past rows that already failed. An
at_exit guard now closes that class regardless of which path the process
leaves by, flushing stdout first so a failing run's FAIL lines survive
Unix._exit rather than being dropped from the buffer. Verified both
directions with a deliberately broken row: dune test exits nonzero and the
log still carries the FAIL line and the failure count; restored, the same
run is exit 0 with nothing printed but green summaries. The other test
binaries were checked for the same gap and none have it — each gates its
own exit on a single failures ref that the tail already reads.
This commit is contained in:
parent
f360531918
commit
c76a507d3b
16
FIX.org
16
FIX.org
@ -424,7 +424,7 @@ rename. typed-flan branch freezes the static language pre-dyn.
|
||||
4. nil: arrives with maps. nil <-> None at (Option T) boundaries, trap at
|
||||
bare T, (Some nil) unconstructible.
|
||||
5. Typed = and != grow strings: bytewise, length + same-pointer fast paths,
|
||||
both backends, one survey program. Ordering stays refused.
|
||||
both backends, one survey program. Ordering stays refused. — LANDED, daed039
|
||||
6. defclass = named dyn map + shape tag; CLOS class dispatch AND
|
||||
Clojure-style arbitrary dispatch functions. After 1.
|
||||
7. dyn if: truthiness (nil/false are false, all else true). Typed stays
|
||||
@ -505,11 +505,15 @@ instead of saying something false.
|
||||
|
||||
** Sweep policy, decided 2026-09-19
|
||||
A lane runs the fast check and nothing more. `dune test` is the whole of a
|
||||
lane's obligation, and it is judged by reading the printed output rather than
|
||||
by the exit status, which stays 0 even when the acceptance runner prints
|
||||
failures. Running one program directly to capture its real output for an
|
||||
acceptance row is still expected; that is cheap. What a lane may no longer do
|
||||
is sweep.
|
||||
lane's obligation. It used to be judged by reading the printed output rather
|
||||
than by trusting the exit status, on the theory that some path through the
|
||||
acceptance runner could print a FAIL and still exit 0 — the tail check itself
|
||||
already exited 1, but nothing proved every skip path (no clang, no wasmtime,
|
||||
no raylib, no lldb) still reached it. test_acceptance.ml now closes that class
|
||||
with an `at_exit` handler that holds regardless of which path the process
|
||||
leaves by, so the exit status can be trusted again and either check does.
|
||||
Running one program directly to capture its real output for an acceptance row
|
||||
is still expected; that is cheap. What a lane may no longer do is sweep.
|
||||
|
||||
The x86 survey and the sanitizer sweep run once, after several lanes have
|
||||
landed, and whatever they turn up is dispatched as fixes in a single batch.
|
||||
|
||||
4
NEXT.md
4
NEXT.md
@ -1648,7 +1648,9 @@ and the refusals' own words say so: each of them named *teardown* as the problem
|
||||
on `can-free` at construction and at every growth — rather than being answered with a hook. This is Odin's position in
|
||||
full: `core:encoding/json` ships a hand-written recursive `destroy_value` in the *library* and names parsing against
|
||||
`temp_allocator` plus `free_all` as the idiomatic alternative, and neither is a language feature. See spec-memory.md,
|
||||
"A container of owning elements lives in a region", and `test/programs/arena-edn.flan`.
|
||||
"A container of owning elements lives in a region". `test/programs/arena-edn.flan` was that case's acceptance program;
|
||||
it is gone now that `edn/read` answers plain dyn rather than an arena-allocated `(Vec Value)`, and `test/programs/edn-read.flan` is
|
||||
where the recursive document is exercised today.
|
||||
|
||||
**The safety net, and the better use of effort: a debug tracking allocator.** ASan's leak detection covers memory
|
||||
*instrumented* code allocated — the Flan allocator, and it is already wired up and clean. It does **not** cover a leaked
|
||||
|
||||
@ -105,7 +105,16 @@ that fell out rather than the one that was chosen.
|
||||
|
||||
## 2. Equality and ordering — not two meanings, one side missing a case
|
||||
|
||||
Typed `=` is numbers and enums and nothing else. `lib/types.ml:166-168`:
|
||||
**Landed in `daed039`** (M2 queue item 5): typed `=` and `!=` now grow the `string` case this section argues
|
||||
for, bytewise, with the fast paths `runtime/flan_rt.c`'s `flan_str_eq` carries. `is_equatable` is no longer a
|
||||
bare alias for `is_comparable` — `lib/types.ml` now reads `let is_equatable = function String -> true | t ->
|
||||
is_comparable t` — and the transcript below, quoted as this section found it, now accepts `(= "hi" "hi")`.
|
||||
Ordering was deliberately left alone: `<` and friends still refuse a string, on the same "no collation this
|
||||
language has picked" grounds §2 raises, and that half of the verdict did not land. What follows is kept as
|
||||
the historical argument that got the equality half moving; read the two paragraphs above as its outcome, not
|
||||
as a correction of anything past this point.
|
||||
|
||||
Typed `=` is numbers and enums and nothing else, as this was written. `lib/types.ml:166-168` then read:
|
||||
|
||||
```ocaml
|
||||
let is_comparable = function Enum _ -> true | t -> is_numeric t
|
||||
@ -116,13 +125,13 @@ let is_equatable = is_comparable
|
||||
dyn operation that never traps (`SPIKE-DYNAMIC.md:285-287`), and dyn `<` orders text bytewise by `memcmp`
|
||||
(`SPIKE-DYNAMIC.md:273-275`).
|
||||
|
||||
One probe, both operators, one line apart:
|
||||
One probe, both operators, one line apart — as run before `daed039`; the second `println` now accepts too:
|
||||
|
||||
```
|
||||
$ flan check b3.flan
|
||||
(defn f [x] dyn x)
|
||||
(defn main [] i32 (do (println (= (f "hi") (f "hi"))) ; accepted
|
||||
(println (= "hi" "hi")) ; refused
|
||||
(println (= "hi" "hi")) ; refused, at the time
|
||||
0))
|
||||
b3.flan:2:64: = compares machine numbers; string has no built-in comparison (plan.org, Types)
|
||||
```
|
||||
|
||||
25
lib/check.ml
25
lib/check.ml
@ -3056,6 +3056,19 @@ and check_struct ctx ~want loc name kvs =
|
||||
"%s is a data type, and a data type value names the case as well as the \
|
||||
type — write (%s.%s {.field value ...}) for one of %s"
|
||||
name name (first_case_name ctx.env name) (case_list ctx.env name)
|
||||
(* [kvs = []] is the parser's one blind spot here: a symbol applied to
|
||||
an empty map literal, [(name {})], parses as a struct literal with
|
||||
no fields regardless of what [name] turns out to be, because the
|
||||
parser has no table to tell a struct name from a function name. If
|
||||
[name] is a known function, the empty map was meant as an argument
|
||||
— and there is no syntax to pass a map literal straight into a call
|
||||
that way, empty or not; every real function argument is a bound
|
||||
name. Naming that is more useful than "unknown struct". *)
|
||||
else if kvs = [] && Hashtbl.mem ctx.env.fns name then
|
||||
fail loc
|
||||
"%s is a function, not a struct — a map literal cannot be passed \
|
||||
directly as an argument; bind it first, as (let [m {}] (%s m))"
|
||||
name name
|
||||
else
|
||||
Loc.failk "check/unknown-struct" loc ~notes:(declared_note ctx.env name)
|
||||
"unknown struct %s" name)
|
||||
@ -3989,9 +4002,15 @@ and named_call ctx ~want loc name args =
|
||||
~needs:(match name with "=" | "!=" -> "equal?" | _ -> "ordered?")
|
||||
a.Tast.ty;
|
||||
if not (ok || generic_ty a.Tast.ty) then
|
||||
fail loc
|
||||
"%s compares machine numbers; %s has no built-in comparison \
|
||||
(plan.org, Types)" name (Types.to_string a.Tast.ty);
|
||||
(match name with
|
||||
| "=" | "!=" ->
|
||||
fail loc
|
||||
"%s compares machine numbers, enums and strings; %s has no \
|
||||
built-in equality (plan.org, Types)" name (Types.to_string a.Tast.ty)
|
||||
| _ ->
|
||||
fail loc
|
||||
"%s orders machine numbers; %s has no built-in ordering \
|
||||
(plan.org, Types)" name (Types.to_string a.Tast.ty));
|
||||
prim p Types.Bool [ a; b ]
|
||||
end
|
||||
| "not" ->
|
||||
|
||||
19
lib/parse.ml
19
lib/parse.ml
@ -154,11 +154,20 @@ and pitems (items : Form.t list) : Ast.pitem list =
|
||||
is what braces mean in the position a body starts in. *)
|
||||
let constraints (body : Form.t list) : Ast.pred list * Form.t list =
|
||||
match body with
|
||||
(* Only when the first key is [:where] — the one key the map takes. Braces
|
||||
opening on any other keyword are a dyn map literal standing as the body's
|
||||
first form, and belong to the body. *)
|
||||
| ({ Form.v = Form.Map (({ Form.v = Form.Kw "where"; _ } :: _ as kvs)); _ } as m)
|
||||
:: rest ->
|
||||
(* Any map literal whose first key is a keyword is read as a constraint
|
||||
map when something follows it, not just one that opens on [:where]: a
|
||||
keyword-first map is never a struct literal ([is_struct_map] wants a
|
||||
[.field] symbol or [Map []]), and one sitting where the body starts with
|
||||
more body after it is discarded on evaluation — a map literal has no
|
||||
side effects, so that spot is always a mistake and not a case a real
|
||||
program uses. Reading a typo'd key, like [:wheer], as ordinary body code
|
||||
used to print a baffling "unknown function ordered?" from inside what
|
||||
the user meant as a predicate; reading it here instead lets [keys] below
|
||||
say which key it does not recognise. The single-form body, [rest = []],
|
||||
is left alone: there the map is not discarded, it IS the answer — a
|
||||
[(defn f [] dyn {:a 1})] whose whole body is the dyn value to build. *)
|
||||
| ({ Form.v = Form.Map (({ Form.v = Form.Kw _; _ } :: _ as kvs)); _ } as m)
|
||||
:: (_ :: _ as rest) ->
|
||||
let pred (p : Form.t) =
|
||||
match p.Form.v with
|
||||
(* [$t] at a predicate, not bare [t]: the clause talks about the
|
||||
|
||||
@ -2764,7 +2764,14 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) dst =
|
||||
[call_native]; only the sense of the answer needs flipping for [!=],
|
||||
the same [xor 1] the [Tast.Not] arm below uses on a bool. [check.ml]
|
||||
never builds [<] and friends on a string (Types.is_comparable says no),
|
||||
so this arm only ever sees [Eq] or [Ne]. *)
|
||||
so this arm only ever sees [Eq] or [Ne].
|
||||
|
||||
[xor 1] is only correct because [flan_str_eq] is REQUIRED to return
|
||||
exactly 0 or 1 — an int8_t cast from a C [==] expression, not from a
|
||||
truncated wider comparison — and this arm may not be changed to call a
|
||||
function with a looser contract without also widening this to a proper
|
||||
zero-test. The LLVM side (emit.ml) does not share this requirement: its
|
||||
[icmp ne i8 r, 0] tolerates any nonzero byte as true. *)
|
||||
| (Tast.Eq | Tast.Ne), [ a; b ] when a.Tast.ty = Types.String ->
|
||||
call_native f ~sym:"flan_str_eq" ~args:[ a; b ] ~rty:(Types.Int Types.I8) dst;
|
||||
if p = Tast.Ne then begin
|
||||
|
||||
@ -86,9 +86,10 @@ _Noreturn void flan_trap(const uint8_t *name, int64_t namelen);
|
||||
* milliseconds until the year 6429; the box is what keeps the other end of the
|
||||
* type honest rather than quietly wrapping. See the doc.
|
||||
*
|
||||
* Tags 6 and 7 are unspoken for, and that is where a typed handle goes when
|
||||
* interop arrives — a (Vec i64) crossing into dyn without being copied. Again,
|
||||
* the doc. */
|
||||
* Tags 5, 6 and 7 are unspoken for — keywords and maps took 4 and BOX_OBJ's
|
||||
* [kind] field, not new top-level tags — and that is where a typed handle
|
||||
* goes when interop arrives — a (Vec i64) crossing into dyn without being
|
||||
* copied. Again, the doc. */
|
||||
|
||||
typedef uint64_t flan_dyn;
|
||||
|
||||
|
||||
@ -1961,8 +1961,9 @@ int8_t flan_eq_str(const void *a, const void *b, int64_t size, void *xfer) {
|
||||
* after the lengths have already been found equal. The zero-length return
|
||||
* guards the [memcmp] below: [memcmp(NULL, NULL, 0)] is technically undefined
|
||||
* even though every real implementation treats it as a no-op, and a 0-length
|
||||
* string built from a null pointer is not a hypothetical here — the empty
|
||||
* string literal is one. */
|
||||
* string built from a null pointer is not a hypothetical here — an empty
|
||||
* string literal is not one, its address is an interned symbol's and is never
|
||||
* null, but a zero-length container converted to a string is. */
|
||||
int8_t flan_str_eq(const uint8_t *ap, int64_t alen,
|
||||
const uint8_t *bp, int64_t blen) {
|
||||
if (alen != blen) return 0;
|
||||
|
||||
@ -30,6 +30,7 @@
|
||||
;; A one-byte difference at the end, so the length check cannot rule it
|
||||
;; out and the byte loop has to run to the last byte before it can answer.
|
||||
(println (= "abd" "abc")) ; false
|
||||
(println (!= "abd" "abc")) ; true
|
||||
|
||||
;; Empty strings: the length check's zero case, which the runtime helper
|
||||
;; also uses to skip a memcmp that would otherwise read through a null
|
||||
@ -37,4 +38,10 @@
|
||||
(println (= "" "")) ; true
|
||||
(println (= "" "a")) ; false
|
||||
(println (= "a" "")) ; false
|
||||
|
||||
;; A slice and the prefix it was cut from: same base pointer, different
|
||||
;; lengths -- the one pair the same-pointer fast path would answer wrong on
|
||||
;; if it ran before the length check instead of after.
|
||||
(let [s "abcd"]
|
||||
(println (= s (string (slice (bytes s) 0 2))))) ; false
|
||||
0)
|
||||
|
||||
@ -12,6 +12,25 @@ let () = Watchdog.arm ~seconds:1200 "test_acceptance"
|
||||
|
||||
let failures = ref 0
|
||||
|
||||
(* The tail of this file exits 1 when [failures] is nonzero, but that check
|
||||
is one path among several a run can take: a probe for clang, wasmtime,
|
||||
raylib or lldb can skip a whole section and jump past rows that already
|
||||
failed. Reading through the file to prove every path still reaches the
|
||||
tail check is exactly the kind of proof that quietly stops being true the
|
||||
next time a case is added. An [at_exit] guard makes the invariant hold no
|
||||
matter which path the process leaves by: however this binary exits, if it
|
||||
printed a FAIL it exits nonzero. [Unix._exit] and not [exit] — calling
|
||||
[exit] from inside an [at_exit] handler recurses through [do_at_exit] —
|
||||
but [_exit] skips the channel flush stdlib's own [at_exit] handler does,
|
||||
and handlers run LIFO, so this one would fire first and throw away every
|
||||
row that already printed FAIL, buffered in stdout, before it ever reached
|
||||
the pipe. [flush_all] first is what [watchdog.ml]'s [dying] does for the
|
||||
same reason: a report that eats the rows that failed is worse than the
|
||||
hang it is there to catch. *)
|
||||
let () =
|
||||
at_exit (fun () ->
|
||||
if !failures > 0 then begin flush_all (); Unix._exit 1 end)
|
||||
|
||||
let scratch = Filename.get_temp_dir_name ()
|
||||
|
||||
let run exe arg =
|
||||
@ -965,7 +984,7 @@ let () =
|
||||
not a row here: a program that ordered two string literals would not
|
||||
compile. *)
|
||||
let string_eq_out =
|
||||
"true\nfalse\nfalse\ntrue\ntrue\nfalse\nfalse\ntrue\nfalse\nfalse\n"
|
||||
"true\nfalse\nfalse\ntrue\ntrue\nfalse\nfalse\ntrue\ntrue\nfalse\nfalse\nfalse\n"
|
||||
in
|
||||
outputs "string equality" "programs/string-eq.flan" string_eq_out;
|
||||
outputs ~opt:"-O0" "string equality, -O0" "programs/string-eq.flan"
|
||||
|
||||
@ -1186,17 +1186,17 @@ let () =
|
||||
(* ── Unconstrained operators, and everything past milestone 2 ──── *)
|
||||
(* M2 queue item 5: typed = and != grow strings, bytewise. Ordering does
|
||||
not — there is no collation the language has picked, so < stays
|
||||
refused with the message it already had. *)
|
||||
refused, on the grounds that a string is equatable but not ordered. *)
|
||||
accepts "typed = on strings" "(defn f [] bool (= \"a\" \"b\"))";
|
||||
accepts "typed != on strings" "(defn f [] bool (!= \"a\" \"b\"))";
|
||||
rejects_check "no built-in < on strings"
|
||||
"(defn f [] bool (< \"a\" \"b\"))" ~needle:"no built-in comparison";
|
||||
"(defn f [] bool (< \"a\" \"b\"))" ~needle:"no built-in ordering";
|
||||
rejects_check "no built-in <= on strings"
|
||||
"(defn f [] bool (<= \"a\" \"b\"))" ~needle:"no built-in comparison";
|
||||
"(defn f [] bool (<= \"a\" \"b\"))" ~needle:"no built-in ordering";
|
||||
rejects_check "no built-in > on strings"
|
||||
"(defn f [] bool (> \"a\" \"b\"))" ~needle:"no built-in comparison";
|
||||
"(defn f [] bool (> \"a\" \"b\"))" ~needle:"no built-in ordering";
|
||||
rejects_check "no built-in >= on strings"
|
||||
"(defn f [] bool (>= \"a\" \"b\"))" ~needle:"no built-in comparison";
|
||||
"(defn f [] bool (>= \"a\" \"b\"))" ~needle:"no built-in ordering";
|
||||
(* (Vec T) is built. What is still refused is the arity: one element type,
|
||||
and a near-miss there would otherwise resolve to a type variable and come
|
||||
back as generics. *)
|
||||
|
||||
13
vendor/json/json.flan
vendored
13
vendor/json/json.flan
vendored
@ -40,10 +40,15 @@
|
||||
;;;; survive the free-all in the cases that had no escapes and not in the
|
||||
;;;; others, which is the kind of contract nobody can hold in their head.
|
||||
;;;;
|
||||
;;;; Note what that buys against test/programs/arena-edn.flan, whose header has
|
||||
;;;; a section called "One lifetime that is not the region's" for exactly this:
|
||||
;;;; its Values point back at `src` and outlive the arena. A Value built out of
|
||||
;;;; string-of does not. The source buffer is dead the moment the read returns.
|
||||
;;;; Note what that buys against vendor/edn/read.flan's dyn reader, which
|
||||
;;;; settled the same question a different way: it takes no allocator at all,
|
||||
;;;; because every string it produces is boxed onto the collector's heap on
|
||||
;;;; the spot — read-value's "a document owns its strings" rule. This
|
||||
;;;; package's split is the one to take when there is a context allocator to
|
||||
;;;; put the copy in and a caller who may not want one for every string in the
|
||||
;;;; document; the dyn reader's is the one to take when there is no allocator
|
||||
;;;; in the picture at all. Either way, a Token's raw `text` is never what
|
||||
;;;; outlives the read — only what string-of or the box copies out of it does.
|
||||
;;;;
|
||||
;;;; ── The allocator ───────────────────────────────────────────────────
|
||||
;;;;
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user