From d006a8b4807b3236907cc0b9fd0ceb41457af224 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 10:14:24 +0700 Subject: [PATCH] An array literal's first element types the rest, constant arithmetic folds at a bounded type variable, and a pointer or a plain union takes a byte fill --- TODO.org | 38 +++++----- lib/check.ml | 100 ++++++++++++++++++------- test/programs/array-first-element.flan | 14 ++++ test/programs/fill-ptr-union.flan | 18 +++++ test/programs/generic-fold.flan | 11 +++ test/test_acceptance.ml | 20 +++++ test/test_flan.ml | 33 +++++--- 7 files changed, 179 insertions(+), 55 deletions(-) create mode 100644 test/programs/array-first-element.flan create mode 100644 test/programs/fill-ptr-union.flan create mode 100644 test/programs/generic-fold.flan diff --git a/TODO.org b/TODO.org index 779108ac..a9614cdd 100644 --- a/TODO.org +++ b/TODO.org @@ -659,19 +659,20 @@ it would entail =ordered?= and =equal?= and not =numeric?=, so the cast rule becomes a disjunction and the refusal has to name whichever the reader meant. Each part of that is a decision and the author has not been asked. -** NEXT The Ptr and union arms of the fill boundary are relaxable -Decided 2026-09-25: relax both. A =Ptr= may be byte-filled, a poisoned pointer being the useful case, and an untagged union is filled over its whole size. -What may be byte-filled is numbers, and structs and fixed arrays of numbers. -A =Ptr= is refused so the rule stays one sentence, and an untagged union -because the walk goes over a struct's fields rather than a union's members. -Both are named in the decision as the arms to relax first if it is reopened, -and a poisoned pointer is arguably the useful case. +** DONE The Ptr and union arms of the fill boundary are relaxable +CLOSED: [2026-09-25] +A =Ptr= may be byte-filled, and an untagged union is filled over its whole +size when every member may be, its members walked as a struct's fields are; a +union with a =dyn= member is refused naming the =dyn=. Everything else the rule +refused it still refuses. -** NEXT A compound constant expression at a bounded type variable -Decided 2026-09-25: fold constant integer arithmetic before the bounded-variable literal check, so =(+ x (+ 1 2))= is accepted where =(+ x 3)= is. -=(+ x (+ 1 2))= at a bounded variable is refused where =(+ x 3)= works — the -literal arm admits a bare constant and nothing folds the compound first. -Walk-backable, so it waits until a body actually wants it. +** DONE A compound constant expression at a bounded type variable +CLOSED: [2026-09-25] +Integer arithmetic over literals alone (=Check.literal_arith=) is folded to the +literal it computes wherever a type variable is wanted, so =(+ x (+ 1 2))= is +admitted exactly where =(+ x 3)= is. A defconst's name does not fold, since it +has a type of its own. The instantiation checks the form unfolded, at its +concrete type. ** DONE Generics by monomorphisation, checked abstractly, with where predicates CLOSED: [2026-09-13] @@ -896,13 +897,12 @@ ordinary expressions and the builtin reads the type back out of one type an expression cannot hold, such as =(Fn [i32] ())=, is parsed as =Ast.TypeArg=. Rules out a type expression anywhere else in expression position. -** NEXT An array literal cannot say it is [f32] -Decided 2026-09-25: the first element's type carries to the rest, so =[(f32 1.0) 2.5]= is an =[f32]=; that is refused today and is a bug. No =1.0f= suffix for now. -A float literal defaults to =f64=, an array literal has no context, and a =let= -has no annotation. Same shape as =(vec-new [u8])= and probably the same fix. -Not the same fix: a bracket literal has no argument to put a type in. Decision: -how a literal names its element type — a spelling of its own, or a =let= -annotation. +** DONE An array literal cannot say it is [f32] +CLOSED: [2026-09-25] +With nothing outside an array literal naming its element type, the first +element's type is the want for the rest, so =[(f32 1.0) 2.5]= is a =[2 f32]=. A +refusal of a later element carries a note at the first saying it set the type. +Rules out a =1.0f= suffix for now. ** NEXT A let binding takes no type annotation Decided 2026-09-25: =(the T expr)=, Common Lisp's special operator, gives any expression its want; checked at compile time like any other want, and it compiles to nothing. =let= is unchanged. On a =dyn= operand it is refused, naming the cast. The refusals that say "annotate the binding" — =None=, an empty =[]=, and =(zeroed)=/=(filled)=/=(dead-beef)= with no want — suggest it instead, because today their suggestion cannot compile. diff --git a/lib/check.ml b/lib/check.ml index a54b3ad6..678c19db 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1082,29 +1082,30 @@ let rec no_zeroed_fn loc what (t : Types.t) = - [string] and a slice. Two words, the second of which is a length every bounds check believes. A filled length is a bounds check that passes and an access that does not. - - [Ptr]. Not walked by the collector, and a poisoned pointer is arguably - the useful case — but it is still a value every [deref] in the language - trusts, and admitting it would make the rule "plain data, except one - kind of address". Kept out so the rule is one sentence. This is the arm - to relax first if the question is reopened. - [bool]. The one refusal that is about the backends rather than the runtime: a bool is a byte here and an [i1] to LLVM, which reads the low bit, where x86 compares the whole byte against zero. 0xDE is false on one and true on the other, and byte-identical behaviour across the two backends is the property this feature is pinned on. - - an enum, a data type, a union, an [(Option T)], a function value. Each + - an enum, a data type, an [(Option T)], a function value. Each carries a tag or a case index that something later reads as a small number with a meaning, and a filled one names a case that does not exist. Floats are in: every bit pattern is a float, NaNs included, and both - backends move one as bytes. *) + backends move one as bytes. So is a [Ptr], which the collector does not + walk and whose poisoned value is the useful case, and an untagged union + whose members are all admitted, filled over its whole size. *) let rec unfillable env seen (t : Types.t) : Types.t option = match t with - | Types.Int _ | Types.Float _ -> None + | Types.Int _ | Types.Float _ | Types.Ptr _ -> None | Types.Array (_, e) -> unfillable env seen e | Types.Named n when not (List.mem n seen) -> - (match Hashtbl.find_opt env.structs n with + (match + match Hashtbl.find_opt env.structs n with + | Some s -> Some s + | None -> Hashtbl.find_opt env.unions n + with | Some s -> List.fold_left (fun acc (fl : Tast.field) -> @@ -1112,9 +1113,8 @@ let rec unfillable env seen (t : Types.t) : Types.t option = | Some _ -> acc | None -> unfillable env (n :: seen) fl.Tast.fty) None s.Tast.fields - (* A data type or a union, which are the two [Named] things that are not - in [structs]. Both overlay their members, so the type itself is what - the refusal names. *) + (* A data type, the one [Named] thing in neither table: its tag names a + case, so the type itself is what the refusal names. *) | None -> Some t) | _ -> Some t @@ -1995,6 +1995,30 @@ let mk loc ty e : Tast.expr = { Tast.e; ty; loc } let unit_at loc = mk loc Types.Unit Tast.Unit +(* Integer arithmetic over literals alone, folded. Unlike [const_int] no name + is read: a defconst has a type of its own, and only an untyped constant may + stand at a type variable. *) +let rec literal_arith (e : Ast.expr) : int64 option = + match e.Ast.e with + | Ast.Int n -> Some n + | Ast.Call ({ Ast.e = Ast.Var op; _ }, x :: y :: rest) -> + let step a b = + match op with + | "+" -> Some (Int64.add a b) + | "-" -> Some (Int64.sub a b) + | "*" -> Some (Int64.mul a b) + | "/" when b <> 0L -> Some (Int64.div a b) + | "%" when b <> 0L && rest = [] -> Some (Int64.rem a b) + | _ -> None + in + List.fold_left + (fun acc e -> + match acc, literal_arith e with + | Some a, Some b -> step a b + | _ -> None) + (literal_arith x) (y :: rest) + | _ -> None + (* The environment for a lifted body, built once its own body has been checked and [caught] is therefore final. spec-memory.md's case 2, and the whole of @@ -3597,6 +3621,14 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = | Ast.ArrayFill (dims, v) -> check_array_fill ctx ~want loc dims v | Ast.ArrayGen (dims, f) -> check_array_gen ctx ~want loc dims f | Ast.Match (scrutinee, arms) -> check_match ctx ~tail ?want loc scrutinee arms + (* Constant integer arithmetic where a type variable is wanted is folded to + the literal it computes first, so [(+ x (+ 1 2))] is admitted wherever + [(+ x 3)] is. The instantiation re-checks the form unfolded, at a concrete + type, where the ordinary arithmetic is fine. *) + | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%"); _ }, _) + when (match want with Some (Types.Var _) -> true | _ -> false) + && literal_arith e <> None -> + int_literal loc ~want ~preds:ctx.env.tvpreds (Option.get (literal_arith e)) | Ast.Call (head, args) -> check_call ctx ~want loc head args | Ast.Unwrap (Ast.Usome, v) -> (* Unwrap Some, else early-return None from the enclosing function, so the @@ -5426,7 +5458,34 @@ and check_arr ctx ~want loc items = | Some (Types.Slice t) -> Some t | _ -> None in - let items = map_lr (fun i -> check ctx ?want:elem_want i) items in + (* With nothing outside saying what the elements are, the first one says: + [[(f32 1.0) 2.5]] is an [[2 f32]], its [2.5] checked at [f32] the way it + would be at an [f32] parameter. *) + let items = + match elem_want, items with + | Some _, _ | None, [] -> map_lr (fun i -> check ctx ?want:elem_want i) items + | None, first :: rest -> + let first = check ctx first in + let want = + match first.Tast.ty with Types.Never -> None | t -> Some t + in + (* A refusal of the element itself says where its type came from. *) + let one (i : Ast.expr) = + try check ctx ?want i with + | Loc.Error d when d.Loc.dloc = i.Ast.loc && want <> None -> + raise + (Loc.Error + { d with + Loc.notes = + d.Loc.notes + @ [ Loc.note first.Tast.loc + (Printf.sprintf + "this array's first element is %s, so every \ + element is" + (Types.to_string first.Tast.ty)) ] }) + in + first :: map_lr one rest + in let n = Int64.of_int (List.length items) in let elem = match elem_want, items with @@ -7160,8 +7219,8 @@ and named_call ?(qualified = false) ctx ~want loc name args = | Some bad -> Loc.failk "check/fill-not-plain-data" loc "%s writes raw bytes over %s, and %s is not plain data — %s. \ - Fill only numbers, and structs and fixed arrays built out of \ - them" + Fill only numbers and pointers, and structs, unions and fixed \ + arrays built out of them" name (Types.to_string ty) (if Types.equal bad ty then "it" else Types.to_string bad) (match bad with @@ -7173,8 +7232,6 @@ and named_call ?(qualified = false) ctx ~want loc name args = a filled header frees a wild address" | Types.String | Types.Slice _ -> "it is a pointer and a length every bounds check believes" - | Types.Ptr _ -> - "it is an address every deref trusts" | Types.Bool -> "a bool is an i1 to LLVM and a whole byte to the x86 backend, \ so a filled one would not even agree with itself across the \ @@ -7188,15 +7245,6 @@ and named_call ?(qualified = false) ctx ~want loc name args = | Types.Named n when Hashtbl.mem ctx.env.datas n -> "it carries a tag that names a case, and no byte pattern \ names a real one" - | Types.Named n when Hashtbl.mem ctx.env.unions n -> - (* Untagged, per [env.unions]'s own note — so the reason is - not a tag. It is that a union's members overlay, and this - rule walks a struct's fields rather than a union's members: - nothing here has shown they are all plain data, and a - member that is not would be filled through the one that - is. *) - "a union's members overlay, and this rule does not walk them \ - — so nothing here has shown that every member is plain data" | Types.Enum _ -> "an enum's values are the members it declared, and no byte \ pattern is one of them" diff --git a/test/programs/array-first-element.flan b/test/programs/array-first-element.flan new file mode 100644 index 00000000..a667a60a --- /dev/null +++ b/test/programs/array-first-element.flan @@ -0,0 +1,14 @@ +;;;; An array literal with nothing outside it saying what its elements are +;;;; takes that from its first element: [(f32 1.0) 2.5] is a [2 f32], and the +;;;; 2.5 is an f32 literal rather than an f64 refused for not being one. +(defn sum3 [a [3 f32]] f32 (+ (at a 0) (at a 1) (at a 2))) + +(defn main [] i32 + (let [a [(f32 1.0) 2.5 3.25] + b [(i64 1) 2 3] + c [(u8 1) 255]] + (println (length a)) + (println (sum3 a)) + (println (+ (at b 1) (i64 9000000000))) + (println (at c 1))) + 0) diff --git a/test/programs/fill-ptr-union.flan b/test/programs/fill-ptr-union.flan new file mode 100644 index 00000000..5e9d2d73 --- /dev/null +++ b/test/programs/fill-ptr-union.flan @@ -0,0 +1,18 @@ +;;;; A pointer and an untagged union take a byte fill. The union is filled +;;;; over its whole size, so its widest member reads back every byte; the +;;;; pointer is read back through a union that overlays it with a u64, since +;;;; there is no other way to see an address as a number. +(defunion U [a u32 b [8 u8]]) +(defunion W [p (Ptr i32) n u64]) + +(defn main [] i32 + (let [u (array 1 U)] + (set u (filled 0xAB)) + (println (.a (at u 0))) ; 2880154539 + (println (at (.b (at u 0)) 7))) ; 171 + (let [w (array 1 W)] + (set (.p (at w 0)) (dead-beef)) + (println (.n (at w 0))) ; 17275436393656397278 + (set (at w 0) (filled 0x01)) + (println (.n (at w 0)))) ; 72340172838076673 + 0) diff --git a/test/programs/generic-fold.flan b/test/programs/generic-fold.flan new file mode 100644 index 00000000..cddcedb9 --- /dev/null +++ b/test/programs/generic-fold.flan @@ -0,0 +1,11 @@ +;;;; Constant integer arithmetic stands where a bounded type variable is +;;;; wanted, as the single literal it folds to would. +(defn f [x $t] t {:where (numeric? $t)} (+ x (* 2 (+ 1 2)))) +(defn g [x $t] t {:where (integer? $t)} (- x (% 7 4))) + +(defn main [] i32 + (println (f 4)) ; 10 + (println (f (u8 250))) ; 0, u8 arithmetic wrapping + (println (f 1.5)) ; 7.5 + (println (g (i64 10))) ; 7 + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 92894d95..45947b76 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -529,6 +529,26 @@ let () = outputs "a u64 constant in decimal" "programs/u64-decimal.flan" u64_out; outputs ~x86:true "a u64 constant in decimal, x86" "programs/u64-decimal.flan" u64_out; + (* Constant arithmetic folds before a bounded variable checks it. *) + let fold_out = "10\n0\n7.5\n7\n" in + outputs "constant arithmetic at a bounded variable" + "programs/generic-fold.flan" fold_out; + outputs ~x86:true "constant arithmetic at a bounded variable, x86" + "programs/generic-fold.flan" fold_out; + (* A pointer and an untagged union take a byte fill. *) + let fpu_out = + "2880154539\n171\n17275436393656397278\n72340172838076673\n" in + outputs "a pointer and a union filled" "programs/fill-ptr-union.flan" + fpu_out; + outputs ~x86:true "a pointer and a union filled, x86" + "programs/fill-ptr-union.flan" fpu_out; + (* An array literal takes its element type from its first element when + nothing outside it names one. *) + let first_out = "3\n6.75\n9000000002\n255\n" in + outputs "an array literal's first element types the rest" + "programs/array-first-element.flan" first_out; + outputs ~x86:true "an array literal's first element types the rest, x86" + "programs/array-first-element.flan" first_out; (* into. The count of pulls is the assertion a unit test cannot make: one pass, one call per element per stage it reaches, and no intermediate collection anywhere. The two show lines either side of it are the same diff --git a/test/test_flan.ml b/test/test_flan.ml index 26ef0703..6da7418c 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2852,10 +2852,9 @@ let () = rejects_check "a string cannot be filled" "(defn f [] () (let [s \"hi\"] (set s (filled 0xFF))))" ~needle:"a length every bounds check believes"; - rejects_check "a pointer field cannot be filled" + accepts "a pointer field may be filled" "(defstruct S [p (Ptr i32)]) \ - (defn f [] () (let [s (S {})] (set s (filled 0xFF))))" - ~needle:"an address every deref trusts"; + (defn f [] () (let [s (S {})] (set s (filled 0xFF))))"; (* The one refusal that is about the two backends rather than the runtime: LLVM reads a bool's low bit and x86 compares the whole byte, so 0xDE is false on one and true on the other. Byte-identical behaviour across the @@ -2864,15 +2863,17 @@ let () = rejects_check "a bool cannot be filled" "(defn f [] () (let [b false] (set b (filled 0xFF))))" ~needle:"would not even agree with itself"; - (* Each of the tagged and address-carrying types names its own reason. They - shared one "it carries a tag that names a case" line until review caught - that it was false for two of them — a union is untagged (env.unions is - "the untagged unions") and a function value is a code pointer, not a - tag. Pinned per type so the reasons cannot quietly re-merge. *) - rejects_check "a union cannot be filled, and not because of a tag" + (* An untagged union is filled over its whole size when every member may be + filled, and refused for the member that may not. *) + accepts "a union of numbers may be filled" "(defunion U [a i32 b f64]) \ + (defn f [] () (let [u (U {})] (set u (dead-beef))))"; + rejects_check "a union with a dyn member cannot be filled" + "(defunion U [a i32 d dyn]) \ (defn f [] () (let [u (U {})] (set u (dead-beef))))" - ~needle:"a union's members overlay"; + ~needle:"a root pointing at nothing"; + (* Each of the tagged and address-carrying types names its own reason, so + the reasons cannot quietly merge into one that is false for some. *) rejects_check "a function value cannot be filled" "(defn g [] ()) (defn f [] () (let [h g] (set h (dead-beef))))" ~needle:"it is a code address"; @@ -6343,6 +6344,18 @@ let () = parse_rejects "the $ refusal names the bare spelling" "(defn $foo [x i32] i32 x)" ~needle:"Name it foo"; + (* ── An array literal's first element types the rest ───────────── *) + accepts "an f32 array literal from its first element" + "(defn main [] i32 (let [a [(f32 1.0) 2.5]] (i32 (length a))))"; + (match checked "(defn main [] i32 (let [a [(u8 1) 256]] 0))" with + | _ -> check "an element that does not fit the first element's type" false + | exception Loc.Error d -> + check "the refusal says the first element set the type" + (List.exists + (fun (n : Loc.note) -> + contains n.Loc.nmsg "this array's first element is u8") + d.Loc.notes)); + (* ── The acceptance program checks end to end ──────────────────── *) accepts "calc-me.flan type checks" (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all);