From ce93ac7622ff9c749683ada6292faa895cf8a12e Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 14:31:32 +0700 Subject: [PATCH] A defconst's value is what the linker writes, on both backends The refusal moves to the checker: Emit.const refused a computed defconst by name while the x86 backend ran it through the startup function behind an .init~once. flag, like a defvar, so the two backends disagreed about the same program. One refusal in Check.const_defconst_init ends that, and it is the only place that can name the way through. The accepted set is unchanged: Tast.const_init's, which is Emit.const's and the x86 data_sym path's, plus the integer arithmetic collect's folding pass has already turned into an Int before the initialiser is looked at. Emit.const's two refusals become a failwith no program reaches; emit_global's gconst || const_init loses its left half; x86 needed no edit, since it never classified by the form. test_flan's infers probe asks Check.expression now that a defconst can no longer wrap an arbitrary expression. --- FIX.org | 57 +++++++++++++++++++++++++ lib/check.ml | 48 +++++++++++++++++++++ lib/emit.ml | 68 ++++++++++++------------------ test/programs/dev-rerun.flan | 8 ++-- test/test_acceptance.ml | 14 ++++-- test/test_flan.ml | 82 +++++++++++++++++++++++++++++------- 6 files changed, 215 insertions(+), 62 deletions(-) diff --git a/FIX.org b/FIX.org index 17f6851..fc13d3f 100644 --- a/FIX.org +++ b/FIX.org @@ -832,6 +832,9 @@ globals at all. program instead, because [Emit.const] has nowhere to run a computed value. That divergence predates the re-run rule — the refusal landed in 495629f and the flags in 931cf86 — and is noted here rather than fixed. + Resolved 2026-09-20: there is no computed [defconst] any more, so the + paragraph above describes a program the checker no longer accepts. See "A + defconst is a compiler const" below. - If the language grows a [def]-style form that re-evaluates, that form recomputes on every run. None exists today and none was invented for this; the rule is written so that adding one is a new case and not a revision. @@ -1217,3 +1220,57 @@ function dyn_ops.c *calls*, the call is compiled against the header and the symbol has to resolve against flan_dyn.o, so a rename, a removal or a changed argument list is a compile or link error in =dune test=. A function nothing here calls gets neither. Both comments now say that instead. + +* A defconst is a compiler const, decided 2026-09-20 +The author's words: "defconst should not be computed, it's the equivalent to a +compiler const." So a defconst's initialiser has to be a compile-time constant, +and the refusal is the checker's — [Check.const_defconst_init], called from +[check_global] right after the union refusal it sits beside. + +It had to move because the two backends were not refusing the same program. +[Emit.const] refused a computed defconst by name, late and on its way to LLVM +IR; the x86 backend classified globals by [Tast.const_init] alone, so the same +defconst fell into the computed set, was stored by the startup function and was +guarded by an [.init~once.] flag exactly like a defvar. The same split let x86 +accept =(defconst g U (U.B {.x 1}))=, a data type case in a constant, which +LLVM refused with the byte-level-encoder message. One refusal in the checker +ends both, and it is the only place that can name the way through. + +** The boundary, derived rather than chosen +What a defconst may be is exactly what [Emit.const] can write and what the x86 +backend's [data_sym] path lowers, which is [Tast.const_init]'s set: an integer, +float, bool or string literal; unit; a zeroed or uninit value; [None]; a [Some] +of one of these; and a struct literal or array of them. Nothing that compiled +on LLVM before stopped compiling. + +Integer arithmetic is in the set and is not an exception to it. [collect]'s +folding pass — [const_int], +, -, *, / and %, over literals and over other +folded constants, to a fixpoint — has already replaced =(/ screen-height +cell-size)= with its answer before [check_global] looks at the initialiser, so +what the refusal sees is an [Int]. That pass is integers only, which is why +=(defconst half f64 (/ 1.0 2.0))= is computed and refused. Widening it would be +a second folder and was not done; a test pins that there is not one. + +** What came out +- [Emit.const]'s two refusals are gone. The general one and the data type case + one are the checker's now, word for word, so the messages a program sees did + not change. What is left in their place is a [failwith] in the file's own + idiom: no program reaches it, and it fires only if the checker's accepted set + and [Tast.const_init] ever stop agreeing. +- [emit_global]'s =gconst || const_init ginit= lost its left half. The form no + longer decides anything there; the initialiser does, and a zeroinitializer is + now always a defvar waiting for the startup function. +- x86 needed no edit: it never had a defconst case to delete. It classifies by + [Tast.const_init], and the checker now guarantees a defconst passes it, so no + defconst reaches [Emit.startup_plan] and no [.init~once.] flag is made for + one. The flag machinery for defvar is untouched. + +** The test harness that depended on the old rule +test_flan.ml's [infers] read a type off =(defconst probe )=, which is how +it pinned literal defaulting and every primitive's result — and most of those +probes are calls. It asks [Check.expression] now, the way a session checks an +expression sent from the editor, which is the question the wrapper was only a +way of asking. A defvar could not stand in: only the defconst form takes no +type. The one corpus row that relied on an untyped computed defconst, +=(defconst k (g))= ordered before [g], is a typed defvar and still pins the +order-independence it was there for. diff --git a/lib/check.ml b/lib/check.ml index 0bd25c3..06889e4 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -7481,6 +7481,51 @@ let no_union_const env loc n (v : Tast.expr) = n un | _ -> () +(* A defconst's value is what the linker writes into the program's image, so it + has to be a value the linker can write: a literal, a zero, an aggregate of + those — [Tast.const_init]'s set, which is [Emit.const]'s accepted set asked + as a question. The integer arithmetic a defconst is allowed to be written as + is already gone by here: [collect]'s folding pass turned [(/ screen-height + cell-size)] into its answer before any type resolved, so what arrives here + is an [Int] and passes. + + The author's rule, 2026-09-20: "defconst should not be computed, it's the + equivalent to a compiler const." Refused here rather than in a backend + because a backend can only refuse the program it is asked to emit, and the + two were not asking the same question — [Emit.const] refused a computed + defconst by name while the x86 backend ran it through the startup function + behind an [.init~once.] flag, like a defvar. One refusal in the checker is + the same program refused the same way on both, and it is the only place + that can say what to do instead. + + A data type case says it with its own message, which is the one thing a + reader could not work out from "this is computed": the case would have to be + serialised into the payload blob, and that is an encoder rather than an + order of operations. *) +let const_defconst_init env loc n (v : Tast.expr) = + match v.Tast.e with + | Tast.MakeCase (dname, case, _) -> + fail loc + "a constant cannot be %s.%s — a data type's payload is a blob, and \ + writing a case into one at link time needs a byte-level encoder that \ + does not exist (a string field could not be encoded at all). Make it a \ + defvar, whose initialiser runs at startup and stores the case, or \ + declare it zeroed, which is %s.%s" + dname case dname + (match Hashtbl.find_opt env.datas dname with + | Some { Tast.cases = c :: _; _ } -> c.Tast.vname + | _ -> "its first case") + | _ when not (Tast.const_init v) -> + fail loc + "a constant's value must be a compile-time constant — the constant %s \ + is computed. A defvar may have a computed initialiser, because it runs \ + at startup and stores the result; a defconst is what the linker writes \ + into the image and has nowhere to run. Write (defvar %s ...), or give \ + the constant a literal — integer constants may also be written as \ + arithmetic over literals and other constants, which is folded here" + n n + | _ -> () + (* A global's initialiser runs at startup: from [main], after the runtime is up, before a line of the program's own code. Nothing has established a handler or a restart by then, and nothing outside the initialiser can — the @@ -7650,6 +7695,9 @@ let check_global env (d : Ast.decl) : Tast.global option = | _ -> check (ctx ()) ~want:ty v in no_union_const env d.Ast.dloc n ginit; + (* After the union's own refusal, so a computed union member keeps the + message that names its way through rather than the general one. *) + const_defconst_init env d.Ast.dloc n ginit; (* [env.consts] holds exactly the constants the folding pass consumed, so membership is the question "is this value in the program's shape?" *) Some { Tast.gname = n; gty = ty; ginit; gconst = true; diff --git a/lib/emit.ml b/lib/emit.ml index c76dbe4..3ba2f40 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -3313,8 +3313,9 @@ let emit_fn m ?(hidden = false) ?(pnames = []) (fn : Tast.fn) = [Check] lifts a computed initialiser into a function and [emit_startup] below stores its result before [main] runs. So what reaches here is what needs no code — every [defvar] whose initialiser [Tast.const_init] accepts, - and every [defconst], which is a different rule. A constant is what the - linker writes, and a value that has to be computed is not one. *) + and every [defconst], because a defconst's initialiser is one of those too: + the checker refuses a computed one outright (2026-09-20). A constant is what + the linker writes, and a value that has to be computed is not one. *) let rec const m (e : Tast.expr) = match e.Tast.e with | Tast.Int (n, _) -> Int64.to_string n @@ -3333,34 +3334,19 @@ let rec const m (e : Tast.expr) = | _ -> "{ " ^ String.concat ", " inner ^ " }") | Tast.Some_ v -> Printf.sprintf "{ i8 1, %s %s }" (ll v.Tast.ty) (const m v) - (* A data type's payload is declared as a blob of integers, so a constant of one - would have to be the case's fields *serialised into those integers* — - which is a byte-level encoder this compiler does not have, and which could - not express a string field at all, since that is a pointer the linker has - to relocate and a byte array has nowhere to put a relocation. - - Only a [defconst] reaches this now. The same case in a [defvar] is a - computed initialiser like any other: it is lifted into a function and the - case is written by the same store that writes one in a body, which needs - no encoder at all. That is the way through, and it is what the message - names. *) - | Tast.MakeCase (dname, case, _) -> - fail e.Tast.loc - "a constant cannot be %s.%s — a data type's payload is a blob, and \ - writing a case into one at link time needs a byte-level encoder that \ - does not exist (a string field could not be encoded at all). Make it a \ - defvar, whose initialiser runs at startup and stores the case, or \ - declare it zeroed, which is %s.%s" - dname case dname - (match Hashtbl.find_opt m.datas dname with - | Some { Tast.cases = c :: _; _ } -> c.Tast.vname - | _ -> "its first case") + (* No program reaches this. A [defvar] whose initialiser is computed never + asks — it was lifted into a function and this one is only called for the + constant ones — and a computed [defconst] is refused by + [Check.const_defconst_init], which is where the two messages that used to + be here now live: the one about a data type case needing a byte-level + encoder, and the general one about a constant having nowhere to run. So + this is an internal assertion in the file's own idiom rather than a + diagnostic, and it fires only if that refusal and [Tast.const_init] stop + agreeing about the same set. *) | _ -> - fail e.Tast.loc - "a constant's value must be a compile-time constant — this one is \ - computed. A defvar may have a computed initialiser, because it runs at \ - startup and stores the result; a defconst is what the linker writes \ - into the image and has nowhere to run" + failwith + ("no constant image for " ^ Types.to_string e.Tast.ty ^ " at " + ^ Loc.to_string e.Tast.loc) (* A dev build emits a [defconst] as a mutable [global]. Two things follow, and both are wanted: LLVM can no longer fold a read of it, and a redefinition @@ -3380,11 +3366,11 @@ let emit_global m ?(hidden = false) (g : Tast.global) = (if hidden then "hidden " else "") (if g.Tast.gconst && not m.dev then "constant" else "global") (ll g.Tast.gty) - (* A [defconst] goes through [const] whatever its initialiser is, so a - computed one is refused there by name rather than quietly zeroed - here: a constant has nowhere to run. *) - (if g.Tast.gconst || Tast.const_init g.Tast.ginit then - const m g.Tast.ginit + (* The initialiser decides, and the form no longer has to be asked: a + [defconst]'s initialiser is always one [const] can write, because the + checker refuses a computed one. So a zeroinitializer here is always a + [defvar] waiting for the startup function. *) + (if Tast.const_init g.Tast.ginit then const m g.Tast.ginit else "zeroinitializer")) (* ── Startup ───────────────────────────────────────────────────────── *) @@ -3424,12 +3410,14 @@ let startup_sym = fname ".init-globals" reaches neither. The split is [Tast.const_init]'s, and it is over the *initialiser* and not - over the form — nothing below asks [gconst]. A [defconst] with a computed - initialiser would therefore be guarded here like any [defvar], and on the - x86 backend it is. On this one it never arrives: [const] refuses a computed - [defconst] by name, because a constant has nowhere to run. So the two - backends disagree about that one program, and the disagreement is older - than this rule. + over the form — nothing below asks [gconst], and nothing has to: since + 2026-09-20 a [defconst]'s initialiser is always a compile-time constant, + because [Check.const_defconst_init] refuses a computed one on the way in. + The two therefore coincide for a constant and no [defconst] reaches the + plan below. Until then they did not, and the backends disagreed about that + one program: [const] refused a computed [defconst] by name while the x86 + backend guarded it here like any [defvar]. One refusal in the checker is + what ended it. So each computed initialiser guards itself with a flag of its own. Per global and not per startup function, because the rule belongs to the form: diff --git a/test/programs/dev-rerun.flan b/test/programs/dev-rerun.flan index 1e8fb59..c518f6a 100644 --- a/test/programs/dev-rerun.flan +++ b/test/programs/dev-rerun.flan @@ -8,9 +8,11 @@ ;;;; calls ran again from the top and stored the initial value back over ;;;; whatever the last run had left. A [defconst] whose initialiser is a ;;;; compile-time constant is written into the image and no startup code -;;;; reaches it at all, so the question does not arise for it. The split is -;;;; over the initialiser and not over the form — a computed [defconst] would -;;;; be guarded like a [defvar], and the LLVM backend refuses one outright. +;;;; reaches it at all, so the question does not arise for it. Since +;;;; 2026-09-20 there is no other kind: a defconst's initialiser has to be a +;;;; compile-time constant, refused in the checker so that both backends +;;;; refuse the same program. Before that the LLVM backend refused a computed +;;;; one while x86 guarded it at startup like a defvar. ;;;; ;;;; So each line printed below is a claim about one of those cases, and the ;;;; run number is the first of them: [runs] is computed, so before the fix it diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index b9fd9e6..cd2aa3f 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -4090,9 +4090,12 @@ level "1" "the payload past the case in hand is indeterminate"; (* A *constant* cannot hold a case, because writing one at link time means serialising the fields into the payload blob and a string field is a - relocation a byte array has nowhere to put. Refused in the emitter, - where the rest of the rule about what the image can hold lives, so the - assertion has to get that far rather than stopping at the checker. *) + relocation a byte array has nowhere to put. Refused in the checker since + 2026-09-20, with the same words it was refused with in the emitter: a + constant's initialiser has to be one the linker can write on *both* + backends, and a refusal reached only by emitting was a refusal only one + of them made. The pipeline below still runs the emitter, so the test + does not care which of the two stopped it. *) (let name = "a constant initialised with a data type case" in let src = "(defdata U [A (B [x i32])])\n(defconst g U (U.B {.x 1}))\n\ @@ -4130,7 +4133,10 @@ level "1" Printf.printf "FAIL %s\n refused: %S\n" name m); (* And a computed initialiser on a defconst is refused by name, because a constant is what the linker writes and there is nowhere for it to run. - The emitter again: the checker has no opinion about what folds. *) + The checker, so that the x86 backend refuses it too — it used to run one + through its startup function like a defvar. What folds is still not the + checker's opinion: the accepted set is [Tast.const_init]'s, plus the + integer arithmetic [collect] had already folded before this ran. *) (let name = "a defconst with a computed initialiser" in let src = "(defn two [] i64 2)\n(defconst c i64 (two))\n(defn main [] i32 0)" diff --git a/test/test_flan.ml b/test/test_flan.ml index 8c474ae..75e5a1e 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -735,20 +735,34 @@ let () = let checked src = program src |> Check.program -(* The type a defconst's value infers to, as the checker prints it. Enough to - pin down literal defaulting and every primitive's result. *) +(* The environment a bare expression is checked against: the prelude and + nothing else, built once because building it is the expensive half and no + probe below declares anything. *) +let probe_env = lazy (snd (Check.program_with_env [])) + +(* The type an expression infers to, as the checker prints it. Enough to pin + down literal defaulting and every primitive's result. + + Checked as an expression, the way a session checks one sent from the editor. + It used to be the type of [(defconst probe )], which stopped working on + 2026-09-20: a defconst's initialiser has to be a compile-time constant now + and most of the probes below are calls — (cast ...), (len ...), a + comparison. A defvar would not do either, since only the defconst form + takes no type. This asks [check] the question the wrapper was only ever a + way of asking. *) let infers name src expected = - match checked (Printf.sprintf "(defconst probe %s)" src) with - | p -> - (match List.find_opt (fun (g : Tast.global) -> g.gname = "probe") p.globals with - | Some g -> - let got = Types.to_string g.gty in - if got <> expected then begin - incr failures; - Printf.printf "FAIL %s\n src: %s\n got: %s\n wanted: %s\n" - name src got expected - end - | None -> incr failures; Printf.printf "FAIL %s: no probe\n" name) + match + let form = List.hd (read src) in + let e = Parse.with_imported [] (fun () -> Parse.expr form) in + let t, _, _ = Check.expression (Lazy.force probe_env) e in + Types.to_string t.Tast.ty + with + | got -> + if got <> expected then begin + incr failures; + Printf.printf "FAIL %s\n src: %s\n got: %s\n wanted: %s\n" + name src got expected + end | exception Loc.Error { Loc.dloc = loc; dmsg = msg; _ } -> incr failures; Printf.printf "FAIL %s\n src: %s\n error: %s: %s\n" @@ -2050,11 +2064,49 @@ let () = "(defvar grid [rows i32]) (defconst rows 8)"; accepts "constants defined out of order" "(defconst a (+ b 1)) (defconst b 1)"; - accepts "an untyped constant from a later function" - "(defconst k (g)) (defn g [] u8 1)"; + (* A typed [defvar] here and not an untyped [defconst], which it was until + 2026-09-20: a computed initialiser belongs to a defvar now, and only the + defconst form takes no type. The order-independence being pinned is the + same one either way — [g] is resolved from a declaration further down the + file. *) + accepts "a global initialised from a later function" + "(defvar k u8 (g)) (defn g [] u8 1)"; rejects_check "a genuinely unknown constant still reports itself" "(defconst a (+ nope 1))" ~needle:"unknown name nope"; + (* ── What a defconst's value may be, decided 2026-09-20 ─────────── *) + + (* The author's rule: a defconst is the equivalent of a compiler const, so + its value is what the linker writes and never something that runs. The + accepted set is [Tast.const_init]'s, which is [Emit.const]'s — and the + integer arithmetic below is in it because [collect]'s folding pass has + already turned it into its answer by the time the initialiser is looked + at, which is the same pass that makes (/ w cell) usable as an array + length. Both backends refuse the computed one here now, at the checker, + rather than one of them refusing and the other running it at startup. *) + rejects_check "a computed defconst" + "(defn seed [] i64 7) (defconst c i64 (seed))" + ~needle:"a constant's value must be a compile-time constant"; + rejects_check "a computed defconst names the way through" + "(defn seed [] i64 7) (defconst c i64 (seed))" + ~needle:"Write (defvar c ...)"; + accepts "a constant written as a literal" + "(defconst x u64 0xcbf29ce484222325)"; + accepts "a constant written as arithmetic over other constants" + "(defconst w i64 640) (defconst cell i64 16) (defconst cols i64 (/ w cell))"; + accepts "a constant aggregate of literals" + "(defstruct P [x i32 y i32]) (defconst origin P (P {.x 1 .y 2}))"; + accepts "a constant array of literals" + "(defconst xs [3 i32] [1 2 3])"; + accepts "a zeroed constant" + "(defstruct P [x i32 y i32]) (defconst origin P (P {}))"; + (* The fold is over integers only, so the same shape in floats is computed + and refused — deliberately, because widening it would be a second folder + and this pins that there is not one. *) + rejects_check "float arithmetic is not folded into a constant" + "(defconst half f64 (/ 1.0 2.0))" + ~needle:"a constant's value must be a compile-time constant"; + (* ── Conditions, spec-conditions.md §1 and §2 ──────────────────── *) accepts "handler-bind over a struct condition"