The provider, checked against the reader that was written by hand

edn-provide.flan reads assets/edn/tileset.edn through a struct derived from it,
and its first five lines are edn-read.flan's first five character for character.
Two readers over one file agreeing is what says the derived one is right; either
alone could be self-consistently wrong. The pair memberships are the derivation
deciding in public: the set became a (Map [2 i64] bool), so [3 4] is a key and
[9 9] is not, where a version that made it 108 loose integers would have
compiled and answered differently on all four.

A tuning file beside it covers the rest of the matrix — a string, an integer, a
float, a boolean, a vector summed rather than counted, and a map inside a map
read two field loads deep — and then drift: the struct was derived from a file
with :speed and without :level, and the bytes read carry the opposite. Both are
named, and the read carries on.

The refusals write their own data file, because the data file is the test. Each
is asserted on the position it names, not on the fact of failing, and one of
them checks a line and column into a file the compiler is not reading — which
is the whole of what compile-error was added for.

Two things the tests caught. Load extends the ambient macro set rather than
replacing it, so a package reached twice handed its declarations over twice and
the module refused them as a redefinition; Macro.compile dedupes by name, which
is the rule macro_union already applies a level up. And `where` held a line and
a column at once, which the prelude's note over append-i64 says cannot be done:
i64->bytes renders into one shared static buffer, and both numbers read as the
second one.
This commit is contained in:
Joseph Ferano 2026-09-19 06:00:54 +07:00
parent 1422d4faf3
commit a5a77867f9
5 changed files with 244 additions and 2 deletions

View File

@ -246,11 +246,22 @@ let compile (names : string list) (extra : Form.t list) : loaded =
support set is dropped rather than reaching the checker as a name defined
twice. Current matters: a session that has just re-evaluated a macro holds
the new body in [macros] and the old one in [decls]. *)
(* Deduped by name as well as filtered, and the dedupe is not belt and
braces. [Load.program] extends the ambient set rather than replacing it
a session has already set its own when it calls so a package reached
along two routes, or a file reloaded inside a session that already knows
it, arrives twice. Two declarations of one name reach [Check.program] as a
redefinition, refused with a sentence nobody would connect to this. It is
the rule [Load.macro_union] already applies a level up, applied to the
declarations that now travel with those macros. *)
let support =
let seen = Hashtbl.create 64 in
List.filter
(fun (d : Ast.decl) ->
match Ast.declared_name d with
| Some n -> not (List.mem n names)
| Some n when List.mem n names -> false
| Some n -> if Hashtbl.mem seen n then false
else (Hashtbl.add seen n (); true)
| None -> true)
(support (roots_of extra) !Parse.imported_decls)
in

View File

@ -0,0 +1,11 @@
;; A tuning file with one of each shape defedn derives, so that the struct it
;; produces exercises every arm: a string, an integer, a float, a boolean, a
;; homogeneous vector, a nested map, and a nested map inside that one.
{:name "goblin"
:hp 12
:speed 1.5
:boss? false
:drops [3 1 4 1 5]
:hitbox {:w 16
:h 24
:offset {:x -2 :y 0}}}

View File

@ -0,0 +1,94 @@
;;;; defedn over two real files, and the condition a drifted one signals.
;;;;
;;;; The first half is the claim the feature is for: `(.texture-path t)` here
;;;; is a field load off a struct nobody declared, and the same numbers
;;;; edn-read.flan prints through the dynamic reader come out of it. Two
;;;; readers over one file agreeing is what says the derived one is right —
;;;; either alone could be self-consistently wrong.
;;;;
;;;; The second half is the shape matrix: a string, an integer, a float, a
;;;; boolean, a vector, and a map inside a map, each read back.
;;;;
;;;; The third is drift. The struct was derived from the file as it was when
;;;; this was compiled; the bytes read at run time are a later version of it,
;;;; with one key gone and one arrived. Both are named by SchemaDrift, which is
;;;; the whole reason the reader carries one: a missing key otherwise leaves a
;;;; field at zero and the program draws nothing for a reason nothing reports.
(import edn "vendor:edn")
;; Both derived at compile time, from the files as they sit beside this one.
;; The path is the (embed "...") path — relative to this file — and not the
;; path the run-time reads below use, which is relative to the process.
(edn/defedn Tileset "assets/edn/tileset.edn")
(edn/defedn Tuning "assets/edn/tuning.edn")
;; The same file the dynamic reader in edn-read.flan walks. Embedded rather
;; than read, so this half asserts the reader and not the filesystem.
(defconst tileset (embed "assets/edn/tileset.edn"))
(defconst tuning (embed "assets/edn/tuning.edn"))
(defn show-tileset [a Allocator] ()
(let [t (Tileset-of-bytes tileset a)]
;; The line edn-read.flan prints first, off a struct field this time.
(println (.texture-path t))
;; 54 pairs, and the same three memberships and one miss. A derivation
;; that flattened the pairs into 108 integers would have a different count
;; and would answer no to every one of these.
(println (len (.selected-cells t)))
(println (has-key? (.selected-cells t) [3 4]))
(println (has-key? (.selected-cells t) [0 0]))
(println (has-key? (.selected-cells t) [4 11]))
(println (has-key? (.selected-cells t) [9 9]))))
(defn show-tuning [a Allocator] ()
(let [t (Tuning-of-bytes tuning a)]
(println (.name t))
(println (.hp t))
(println (.speed t))
(println (if (.boss? t) "yes" "no"))
(println (len (.drops t)))
;; 3 + 1 + 4 + 1 + 5. A vector read that stopped at the first element would
;; still have a plausible length from a zeroed Vec, so the sum is the claim.
(let [total (i64 0)]
(dotimes [i (len (.drops t))]
(set total (+ total (at (.drops t) i))))
(println total))
;; The nested structs, by the names the paths give them: Tuning-hitbox and
;; Tuning-hitbox-offset. Both are ordinary field loads, two deep.
(println (.w (.hitbox t)))
(println (.h (.hitbox t)))
(println (.x (.offset (.hitbox t))))
(println (.y (.offset (.hitbox t))))))
;; ── Drift ───────────────────────────────────────────────────────────
;;
;; The struct says :name :hp :speed :boss? :drops :hitbox. These bytes have no
;; :speed and have a :level the struct has never heard of, which is what a
;; tuning file looks like a month after the program was built.
(defconst drifted string
"{:name \"imp\" :hp 3 :level 7 :boss? true :drops [1] :hitbox {:w 1 :h 1 :offset {:x 0 :y 0}}}")
(defn show-drift [a Allocator] ()
(handler-bind
[(edn/SchemaDrift [d]
(do (print (if (.extra? d) "extra " "missing "))
(print (.field d))
(print " in ")
(println (.struct d))))]
(let [t (Tuning-of-bytes (bytes drifted) a)]
;; The fields that were there are read, which is the other half of the
;; contract: a drifted file is reported, not refused. :speed is the one
;; that was missing and is zero.
(println (.name t))
(println (.hp t))
(println (.speed t)))))
(defn main [] i32
(let [a (heap-allocator)]
(show-tileset a)
(println "")
(show-tuning a)
(println "")
(show-drift a))
0)

View File

@ -643,6 +643,125 @@ let () =
outputs ~opt:"-O0" "edn/read over the tileset, -O0"
"programs/edn-read.flan" edn_read_out;
(* The same file again, through a struct derived from it at compile time.
The first five lines are the first five above, character for character,
and that is the claim: two readers over one file agreeing is what says
the derived one is right, where either alone could be self-consistently
wrong. Nothing in the program declares a type and nothing in it matches
on a tag (.texture-path t) is a field load.
The pair memberships are the derivation's own decision showing: the set
became a (Map [2 i64] bool), so [3 4] is a key and [9 9] is not. A
version that made it a (Vec i64) of 108 numbers would have compiled and
would answer differently on every one of these four lines.
Then the shape matrix a string, an integer, a float, a boolean, a
vector summed, and a map inside a map read two field loads deep, by the
names the paths give them. 14 is 3+1+4+1+5, and it is there because a
length alone would pass on a Vec that was allocated and never filled.
Last, drift: the struct was derived from a file with :speed and without
:level, and the bytes read carry the opposite. Both conditions are
named, in the order the reader meets them the unknown key as it
arrives, the missing field when the map closes and the read carries
on, which is the other half of the contract. :speed reads 0. *)
let edn_provide_out =
"./source-assets/Sprout Lands Premium/Objects/Mushrooms, Flowers, \
Stones.png\n\
54\ntrue\ntrue\ntrue\nfalse\n\n\
goblin\n12\n1.5\nno\n5\n14\n16\n24\n-2\n0\n\n\
extra level in Tuning\nmissing speed in Tuning\nimp\n3\n0\n"
in
outputs "defedn over the tileset and a tuning file"
"programs/edn-provide.flan" edn_provide_out;
outputs ~opt:"-O0" "defedn over the tileset and a tuning file, -O0"
"programs/edn-provide.flan" edn_provide_out;
(* What a provider refuses, and where it says the trouble is.
A data file the compiler could not make sense of is one the program
would have read wrongly, so each of these is a compile that stops rather
than a struct with a field of some guessed type.
Both halves of the pair are written here rather than committed, because
the data file *is* the test: a fixture .edn sitting in the corpus would
be read by nothing else and would look like an asset. They go beside the
other programs so that the two things a provider resolves the vendor:
collection, and the data path relative to the source file resolve the
way they do for a real one.
Each is asserted on the position it names and not only on the fact of
failing. A version that refused everything with one sentence would pass
a test that checked the refusal alone, and a line and column into a file
the compiler is not reading is the whole of what the refusal had to be
given a facility for. *)
let provider_refusal name edn needle =
let base = "programs/refuse-" ^ name in
let ednp = base ^ ".edn" and flanp = base ^ ".flan" in
Out_channel.with_open_bin ednp (fun ch -> Out_channel.output_string ch edn);
Out_channel.with_open_bin flanp (fun ch ->
Out_channel.output_string ch
(Printf.sprintf
"(import edn \"vendor:edn\")\n(edn/defedn T \"refuse-%s.edn\")\n\
(defn main [] i32 0)\n" name));
(match
let l = Load.program ~file:flanp (Reader.read_file flanp) in
Check.program l.Load.decls
with
| _ ->
incr failures;
Printf.printf "FAIL %s\n it was accepted\n" name
| exception Loc.Error { Loc.dmsg = m; _ } ->
if not (contains m needle) then begin
incr failures;
Printf.printf "FAIL %s\n said: %S\n wanted: %S in it\n"
name m needle
end);
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ()) [ ednp; flanp ]
in
(* The element positions are named, both of them, because "heterogeneous"
on its own sends someone to read the whole file. *)
provider_refusal "mixed-vector" "{:xs [1 2 \"three\"]}" "element 2 is string";
(* A map whose keys are not all keywords is not a struct: a field is named,
and "name" in quotes is a value. *)
provider_refusal "mixed-keys" "{:a 1 \"b\" 2}" "that is not a keyword";
(* An empty collection carries no element to derive an element type from,
which is the one thing a shape read out of data cannot guess. *)
provider_refusal "empty-vector" "{:xs []}"
"has no element to derive an element type from";
(* nil has no type. A field that is sometimes absent is not something a
struct holds, and guessing would put a zero where a decision belongs. *)
provider_refusal "nil-value" "{:a nil}" "has no type to derive";
(* The line and column are into the *data* file and are the point of the
whole error facility: this one is on the third line. *)
provider_refusal "position" "{:a 1\n :b 2\n :c [1 \"x\"]}" "line 3 column";
(* A set becomes a (Map T bool), so its elements are map keys. A set of
maps is refused by name here rather than at the (Map ...) it would build,
whose message names a type nobody wrote. *)
provider_refusal "set-of-maps" "{:s #{{:a 1}}}"
"is not something this builds";
(* And the file that is not there, which is the case the path rule is for:
it says where it looked. *)
(let flanp = "programs/refuse-missing.flan" in
Out_channel.with_open_bin flanp (fun ch ->
Out_channel.output_string ch
"(import edn \"vendor:edn\")\n\
(edn/defedn T \"no-such-file.edn\")\n(defn main [] i32 0)\n");
(match
let l = Load.program ~file:flanp (Reader.read_file flanp) in
Check.program l.Load.decls
with
| _ ->
incr failures;
Printf.printf "FAIL a defedn over a file that is not there\n\
\ it was accepted\n"
| exception Loc.Error { Loc.dmsg = m; _ } ->
if not (contains m "there is no file at no-such-file.edn") then begin
incr failures;
Printf.printf "FAIL a defedn over a file that is not there\n\
\ said: %S\n" m
end);
(try Sys.remove flanp with Sys_error _ -> ()));
(* And the branch that makes it safe, which needs a program that dies to
say anything the shape bounds.flan uses, and for the same reason.
Run 0 is the control and must not trap: a (Vec (Vec i32)) in the region

View File

@ -66,8 +66,15 @@
(defn joined3 [a string b string c string] string
(joined a (joined b c)))
;; Copied out, and not `(string (i64->bytes n))`. The prelude's note over
;; append-i64 is the reason: i64->bytes renders into one shared static buffer
;; in the runtime, so two of its results cannot be held at once — and `where`
;; below holds a line and a column at the same time, which read as the same
;; number until this copied.
(defn i64->string [n i64] string
(string (i64->bytes n)))
(let [v (vec-new u8)]
(append-i64 (addr v) n)
(string (as-slice v))))
;; The tokenizer answers byte offsets, because that is what a slice into the
;; buffer costs nothing to produce. A person reading a refusal wants a line and