JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

A defconst is a compiler const, on both backends and dyn is not one

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-20 14:50:01 +07:00
commit b2558f04de
6 changed files with 258 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

70
FIX.org
View File

@ -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,70 @@ 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. Both are the checker's now. The data
type case one is word for word what it was. The general one gained what the
checker knows and the emitter did not: it names the constant — "the constant
c is computed" rather than "this one is computed" — and it spells the way
through, =(defvar c ...)= or a literal, with the integer arithmetic the
folding pass accepts named beside it. Both are located at the declaration
now rather than at the expression inside it, which is where every other
refusal about a global points and what [next-error] jumps to. What is left
in the emitter 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.
- The case is searched for through the aggregates, which is what [Emit.const]
did by recursing: =(defconst g S (S {.u (U.B {.x 1})}))= is a case the image
cannot hold just as much as a bare one, and "this is computed" would be
advice nobody could act on. Left to right and first offender wins, so a
computed field written before a case field still gets the general message —
the emitter's own order, since it spelled the fields in order and failed at
the first one it could not spell.
- [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 <expr>)=, 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.

70
lib/check.ml
View File

@ -7481,6 +7481,73 @@ 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. It is searched for the way [Emit.const] used to find it
— down through the aggregates, because a case inside a struct literal is the
same unwritable value as a case on its own, and [(defconst g S (S {.u (U.B
{.x 1})}))] told about "computed" would be advice nobody could follow.
Left to right and stopping at the first value the image cannot hold, which
is [Emit.const]'s own order: it spelled the fields in order and failed at
the one it could not spell. So a computed field written before a case field
is still the general message, because that is the field a reader meets
first. *)
(* The first subexpression a constant image has no value for, descending
through the aggregates whose parts are themselves constants. [None] is a
value the linker can write, which is [Tast.const_init] arrived at from the
other side — the two walk the same nodes, and this one keeps the offender
rather than the verdict. *)
let rec unwritable (e : Tast.expr) =
match e.Tast.e with
| Tast.Int _ | Tast.Float _ | Tast.Bool _ | Tast.Str _ | Tast.Unit
| Tast.Zero _ | Tast.Uninit _ | Tast.None_ -> None
| Tast.Make (_, es) | Tast.Arr es -> List.find_map unwritable es
| Tast.Some_ v -> unwritable v
| _ -> Some e
let const_defconst_init env loc n (v : Tast.expr) =
match unwritable v with
| None -> ()
| Some { Tast.e = 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")
| Some _ ->
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 +7717,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;

68
lib/emit.ml
View File

@ -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:

8
test/programs/dev-rerun.flan
View File

@ -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

14
test/test_acceptance.ml
View File

@ -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)"

80
test/test_flan.ml
View File

@ -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 <src>)], 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
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
| None -> incr failures; Printf.printf "FAIL %s: no probe\n" name)
| 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,57 @@ 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 ...)";
(* The search for a case goes down through the aggregates, because a case
inside a struct literal is the same value the image cannot hold and the
general message's advice — make it a defvar, or write a literal — is not
followable for one. [Emit.const] recursed for the same reason. *)
rejects_check "a data type case nested in a constant struct"
"(defdata U [A (B [x i32])]) (defstruct S [u U]) \
(defconst g S (S {.u (U.B {.x 1})}))"
~needle:"needs a byte-level encoder that does not exist";
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"