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

A narrowed name keeps its assignability, a local whose address is taken or that a fn assigns is not narrowed, a trailing ? tests a whole chain, and the optional refusals name the test to write.

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-26 16:08:16 +07:00
parent 8afa054349
commit adfab2d482
7 changed files with 189 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

114
lib/check.ml
View File

@ -3165,6 +3165,25 @@ let mk loc ty e : Tast.expr = { Tast.e; ty; loc }
(* A local narrowed by [if x?]: the same slot, read as its payload. *)
let narrowed_tag = "~narrowed"
(* The locals of the function being checked that [if x?] must not narrow:
one whose address is taken, which a pointer could clear behind the
block's back, and one a fn assigns (decision 133, Kotlin's rule). *)
let unnarrowable : string list ref = ref []
let unnarrowable_in (body : Ast.expr list) =
let out = ref [] in
let rec walk ~in_fn (e : Ast.expr) =
(match e.Ast.e with
| Ast.Call ({ Ast.e = Ast.Var ("addr" | "addr-of"); _ }, [ { Ast.e = Ast.Var x; _ } ]) ->
out := x :: !out
| Ast.Set (Ast.Pvar x, _) when in_fn -> out := x :: !out
| _ -> ());
let in_fn = in_fn || (match e.Ast.e with Ast.Fn _ -> true | _ -> false) in
ignore (Ast.map_children (fun x -> walk ~in_fn x; x) e)
in
List.iter (walk ~in_fn:false) body;
!out
let local_of loc (b : binding) =
if b.bwhat = Some narrowed_tag then
mk loc b.bty (Tast.Field (mk loc (Types.Option b.bty) (Tast.Local b.slot), 1))
@ -6451,11 +6470,10 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
| Ast.Set (Ast.Pvar n, v)
when (match lookup ctx n with Some b -> b.bwhat = Some narrowed_tag | None -> false) ->
let b = Option.get (lookup ctx n) in
(* A parameter or a captured copy is refused as it is outside the block. *)
let place, _ = check_place ctx loc (Ast.Pvar n) in
(match trial ctx (fun () -> check ctx ~want:b.bty v) with
| Ok vv ->
expect ctx loc ~want
(mk loc Types.Unit
(Tast.Set (Tast.Pfield (mk loc (Types.Option b.bty) (Tast.Local b.slot), 1), vv)))
| Ok vv -> expect ctx loc ~want (mk loc Types.Unit (Tast.Set (place, vv)))
| Error d ->
(match trial ctx (fun () -> check ctx ~want:(Types.Option b.bty) v) with
| Ok { Tast.ty = Types.Option _; _ } ->
@ -10665,16 +10683,59 @@ and narrows (c : Ast.expr) =
and with_narrowed : 'a. ctx -> string list -> (unit -> 'a) -> 'a = fun ctx names f ->
if names = [] then f ()
else
scoped ctx (fun () ->
List.iter
(fun n ->
match lookup ctx n with
| Some ({ bty = Types.Option t; _ } as b) when b.bwhat <> Some narrowed_tag ->
ctx.scope <- (n, { b with bty = t; bwhat = Some narrowed_tag; blit = None })
:: ctx.scope
| _ -> ())
names;
f ())
let held = ref [] in
let r =
scoped ctx (fun () ->
List.iter
(fun n ->
match lookup ctx n with
| Some { bty = Types.Option _; _ } when List.mem n !unnarrowable ->
held := n :: !held
| Some ({ bty = Types.Option t; _ } as b) when b.bwhat <> Some narrowed_tag ->
ctx.scope <- (n, { b with bty = t; bwhat = Some narrowed_tag; blit = None })
:: ctx.scope
| _ -> ())
names;
(* A name something else can clear stays an Option; a refusal in
the block about it says why, and how to copy what it holds. *)
if !held = [] then f ()
else
let note (d : Loc.diag) =
let has s sub =
let ls = String.length s and lb = String.length sub in
let rec go i = i + lb <= ls && (String.sub s i lb = sub || go (i + 1)) in
go 0
in
let about = if has d.Loc.dmsg "Option" then !held else [] in
match about with
| [] -> d
| n :: _ ->
{ d with
Loc.notes =
d.Loc.notes
@ [ Loc.note d.Loc.dloc
(Printf.sprintf
"%s? does not make %s its payload here: %s's address \
is taken, or a fn assigns it, in this function, so \
something else could clear it. Write if %s? as g, \
which copies what it holds into g"
n n n n) ] }
in
(* Raised, or recorded while recovering: noted either way. *)
let before = ctx.env.recovered in
let r =
try f () with
| Loc.Error d -> raise (Loc.Error (note d))
| Loc.Errors ds -> raise (Loc.Errors (List.map note ds))
in
let rec fresh l =
if l == before then l
else match l with d :: t -> note d :: fresh t | [] -> []
in
ctx.env.recovered <- fresh ctx.env.recovered;
r)
in
r
(* [x?]: whether x holds a value — an Option that is Some, a dyn that is not
nil. *)
@ -11066,6 +11127,11 @@ and struct_of ctx (target : Ast.expr) (t : Tast.expr) : Tast.expr * string =
(match target.Ast.e with
| Ast.Var n ->
(match lookup ctx n with
| Some { bwhat = Some w; _ } when w = narrowed_tag ->
fail target.Ast.loc
"%s is tested with %s? above, so here it is what the Option \
holds, %s, and %s has no fields"
n n (tyname target.Ast.loc other) (tyname target.Ast.loc other)
| Some { bwhat = Some w; _ } ->
fail target.Ast.loc
"%s is %s — the pattern bound it to %s, so the value is already \
@ -11347,6 +11413,15 @@ and check_call ctx ~want loc (head : Ast.expr) (args : Ast.expr list) =
[ mk loc Types.String (Tast.Str owner) ])
| _ -> fail loc "internal: %%res-done takes a name — a compiler bug")
(* [i32?] where a value goes: the type, not a value. *)
| Ast.Var "Option" when fln_source loc
&& (match args with
| [ { Ast.e = Ast.Var n; _ } ] -> lookup ctx n <> None
| _ -> false) ->
let n = match args with [ { Ast.e = Ast.Var n; _ } ] -> n | _ -> "" in
fail loc
"%s? reads as the type Option(%s), because a capitalised name before ? \
is taken for a type. To test the local %s, give it a lowercase name, \
as in %s?" n n n (String.uncapitalize_ascii n)
| Ast.Var "Option" when fln_source loc ->
fail loc
"%s is an Option type, and a value is wanted here. On a value that may \
@ -12252,6 +12327,14 @@ and shadowed_type_arg ctx loc what args =
fail loc
"%s here is the value named %s and not the type, so nothing says what \
(%s) makes — rename that binding to write the type" n n what
(* [vec-new(grain?)] for a lowercase type: where a value is written, ? after
anything but a capitalised or primitive name is the test [x?]. *)
| { Ast.e = Ast.Call ({ Ast.e = Ast.Var "?"; _ }, [ { Ast.e = Ast.Var n; _ } ]); _ } :: _
when type_named ctx n && lookup ctx n = None && not (global_value ctx n) ->
fail loc
"%s? here is the test that a value is present, and %s is a type. Where a \
value is written, the Option of a type is Option(%s): %s(Option(%s))"
n n n what n
| _ -> ()
(* The element type for [vec-new]: a leading bare symbol naming a type, a
@ -18414,6 +18497,9 @@ let rec check_fn ?sign env (fn : Ast.fn) : Tast.fn =
| _ -> ret
in
let ctx = { (invented_ctx env ret) with owner = fn.Ast.name } in
let was_unnarrowable = !unnarrowable in
unnarrowable := unnarrowable_in fn.Ast.fbody;
Fun.protect ~finally:(fun () -> unnarrowable := was_unnarrowable) @@ fun () ->
List.iter2
(fun (p : Ast.field) ty ->
if List.mem_assoc p.Ast.fname ctx.scope then begin

50
lib/indent_reader.ml
View File

@ -989,17 +989,19 @@ let text_of (f : Form.t) =
names storage, and the forms they read to would show the reader's names. *)
let no_place (e : Form.t) =
match e.v with
| Form.List ({ v = Form.Sym "?."; _ } :: _) ->
| Form.List ({ v = Form.Sym "?."; _ } :: { v = Form.Vec [ _; root ]; _ } :: _) ->
let r = text_of root in
failk "chain-assign" e.loc
"%s is an optional chain, and a chain cannot be assigned to: when it \
holds nothing there is no place to write. Unwrap it first with if let, \
then assign through the name it binds"
(text_of e)
| Form.List [ { v = Form.Sym "!!"; _ }; _ ] ->
holds nothing there is no place to write. Test it first: if %s?, and \
in the block %s is what it holds, or if %s? as g, then assign through g"
(text_of e) r r r
| Form.List [ { v = Form.Sym "!!"; _ }; x ] ->
let r = text_of x in
failk "chain-assign" e.loc
"%s unwraps a value, and a value cannot be assigned to. Unwrap it with \
if let, then assign through the name it binds"
(text_of e)
"%s unwraps a value, and a value cannot be assigned to. Test it first: \
if %s?, and in the block %s is what it holds, then assign %s"
(text_of e) r r r
| _ -> ()
let unclosed p c l0 =
@ -1195,7 +1197,9 @@ and unary p =
and postfix p =
let l0 = (peek p).loc in
let rec loop ((f, _) as fp) =
(* [in_chain]: reading the rest of an optional chain, which a [?] that
starts no further chain ends — [o?.i?] tests the whole chain. *)
let rec loop ?(in_chain = false) ((f, _) as fp) =
let t = peek p in
if t.sp then fp
else
@ -1203,18 +1207,18 @@ and postfix p =
| LP ->
ignore (advance p);
let args = items p RP t.loc ~what:"arguments" in
loop (mk p l0 (Form.List (f :: args)), 12)
loop ~in_chain (mk p l0 (Form.List (f :: args)), 12)
| LB ->
ignore (advance p);
let idx = index_items p t.loc ~head:(text_of f) in
loop (mk p l0 (Form.List (sym t.loc "at" :: f :: idx)), 12)
loop ~in_chain (mk p l0 (Form.List (sym t.loc "at" :: f :: idx)), 12)
| NAME s when String.length s > 1 && s.[0] = '.' ->
ignore (advance p);
loop (mk p l0 (Form.List [ sym t.loc s; f ]), 12)
loop ~in_chain (mk p l0 (Form.List [ sym t.loc s; f ]), 12)
| LC ->
ignore (advance p);
let m = map_items p t.loc in
loop (mk p l0 (Form.List [ f; Form.make (Form.Map m) (span p t.loc) ]), 12)
loop ~in_chain (mk p l0 (Form.List [ f; Form.make (Form.Map m) (span p t.loc) ]), 12)
(* [a?.b.c(x)] and [a?[i]]: the rest of the chain is read over a fresh
name, [~o1], bound to what [a] holds — [(?. [~o1 a] (.c ...))]. No
reader can produce a [~] name, so it shadows nothing. A [?.] later
@ -1229,15 +1233,17 @@ and postfix p =
ignore (advance p);
incr opt_n;
let h = Printf.sprintf "~o%d" !opt_n in
let rest, _ = loop (sym t.loc h, 12) in
(mk p l0
(Form.List
[ sym t.loc "?.";
Form.make (Form.Vec [ sym t.loc h; f ]) f.loc;
rest ]), 12)
let rest, _ = loop ~in_chain:true (sym t.loc h, 12) in
loop ~in_chain
(mk p l0
(Form.List
[ sym t.loc "?.";
Form.make (Form.Vec [ sym t.loc h; f ]) f.loc;
rest ]), 12)
(* [T?] where a type is read, and after what can only be a type
where a value is, [vec-new(i32?)]. On a value, [x?] tests that it
holds one (decision 133): [(? x)]. *)
| QUEST when in_chain -> fp
| QUEST ->
let typish =
match f.v with
@ -1249,11 +1255,11 @@ and postfix p =
in
ignore (advance p);
if !in_type || typish then
loop (mk p l0 (Form.List [ sym l0 "Option"; f ]), 12)
else loop (mk p l0 (Form.List [ sym t.loc "?"; f ]), 12)
loop ~in_chain (mk p l0 (Form.List [ sym l0 "Option"; f ]), 12)
else loop ~in_chain (mk p l0 (Form.List [ sym t.loc "?"; f ]), 12)
| BANG ->
ignore (advance p);
loop (mk p l0 (Form.List [ sym t.loc "!!"; f ]), 12)
loop ~in_chain (mk p l0 (Form.List [ sym t.loc "!!"; f ]), 12)
| _ -> fp
in
loop (primary p)

8
spec-syntax.md
View File

@ -296,7 +296,13 @@ Each item: the proposal, then the reason in one line.
the same storage, so `x.count += 1` there changes the Option's payload. Not
in the `else`, not after the block, and not through `or` or `not`. In the
block `x` may be given a value of the payload's type, which keeps it
present; giving it an Option is refused. **Built.**
present; giving it an Option is refused, and a parameter or a captured copy
is no more assignable than outside it. A local whose address is taken, or
that a `fn` assigns, anywhere in the function is not narrowed (something
else could clear it); `if x? as g` copies what it holds instead. A `?` after
a chain tests the whole chain: `o?.i?`. A capitalised name before `?` is
read as a type, so a local tested this way needs a lowercase name.
**Built.**
- **`e? as g`** names what a test found, for an `e` that is not a plain name:
`if get(grid, r, c)? as cell` reads `(if-let [cell (get grid r c)] …)`, an
`if-let` over a plain name, which binds what an Option holds or a dyn that

5
test/programs/presence.fln
View File

@ -62,6 +62,11 @@ fn main()
total += nodes[i].v
cur = nodes[i].next
println(total)
;; A trailing ? tests the whole chain.
let nd: Node? = Some(nodes[2])
println(nd?.next?, nd?.v?)
if nd?.v? as v
println(v)
;; while x? narrows the body.
let k: i32? = Some(3)
let steps = 0

2
test/test_acceptance.ml
View File

@ -2275,7 +2275,7 @@ let () =
outputs ~x86:true (path ^ ", --x86") ("programs/" ^ path) want)
[ ("optionals.fln", optionals_out); ("optionals-dyn.fln", optionals_dyn_out);
(* x? tests and narrows, e? as g names what it found (decision 133). *)
("presence.fln", "true false true\n6\n-1\n3\n101 209 0\n11\n42\n2\nabsent\n6\n6\n15\n"); ("presence-dyn.fln", "true false\n103 209 0\nno pet\nann\n3 2\n") ];
("presence.fln", "true false true\n6\n-1\n3\n101 209 0\n11\n42\n2\nabsent\n6\nfalse true\n3\n6\n15\n"); ("presence-dyn.fln", "true false\n103 209 0\nno pet\nann\n3 2\n") ];
(* x! over nothing traps at its site and names the expression. *)
List.iter
(fun (x86, arg, want) ->

11
test/test_flan.ml
View File

@ -6933,11 +6933,10 @@ let () =
~needle:"nothing declares $t integer (is-integer)"
"(defn dbl [x $t] $t {:where (is-numeric $t)} (<< x 1))";
(* A caller bounded by is-integer satisfies a callee bounded by is-numeric: the
entailment carries across generic calls exactly as is-ordered-over-equal?
does. *)
entailment carries across generic calls exactly as is-ordered carries is-equal. *)
accepts "is-integer carries an is-numeric callee"
"(defn z? [x $t] bool {:where (is-numeric $t)} (= x 0))\n\
(defn odd-z? [x $t] bool {:where (is-integer $t)} (z? (bit-and x 1)))";
"(defn is-z [x $t] bool {:where (is-numeric $t)} (= x 0))\n\
(defn is-odd-z [x $t] bool {:where (is-integer $t)} (is-z (bit-and x 1)))";
(* The integer literal is admitted at a bounded variable by the same arm
under both bounds — the bound promises the literal a meaning at every
type the variable can become, and is-integer's types are a subset of
@ -7333,11 +7332,11 @@ let () =
one definition — needs a written 0 to stand where $t stands. The bound
is what makes it sound: every type [is-numeric] admits is an integer or a
float, and an untyped integer constant is usable at all of them, so
there is no instantiation of a [is-numeric] variable at which the literal
there is no instantiation of an [is-numeric] variable at which the literal
has no meaning. That is the whole rule, and the four pins below are its
two halves and its one asymmetry. *)
accepts "an integer literal stands where an is-numeric type variable is wanted"
"(defn above-zero? [x $t] bool {:where (is-numeric $t)} (> x 0))";
"(defn is-above-zero [x $t] bool {:where (is-numeric $t)} (> x 0))";
accepts "and in arithmetic, answering the variable"
"(defn next [x $t] $t {:where (is-numeric $t)} (+ x 1))";
(* And the prelude's own three, which are that body under its real name at

44
test/test_syntax.ml
View File

@ -1437,7 +1437,7 @@ let () =
and a ? on a value say what to write, and a lowercase type takes ?. *)
reads "a line ending in ?? continues" "x = a ??\n 5" "(set x (?? a 5))";
reads "a line starting with ?? continues" "x = a\n ?? 5" "(set x (?? a 5))";
refuses "a chain is not a place" "q?.x = 5" "indent/chain-assign" "Unwrap it first with if let";
refuses "a chain is not a place" "q?.x = 5" "indent/chain-assign" "cannot be assigned to";
refuses "nor under +=" "q?.x += 5" "indent/chain-assign" "cannot be assigned to";
refuses "an unwrap is not a place" "x! = 5" "indent/chain-assign" "a value cannot be assigned to";
refuses "T?? is not read" "fn f(a: i32??) = a" "indent/nested-option" "Option(i32?)";
@ -1452,6 +1452,33 @@ let () =
refused "where-fln.fln"
"fn big(a: $t, b: $t) -> bool = a < b\n\nfn main()\n println(big(1, 2))\n"
[ "nothing declares $t ordered (is-ordered)"; "Write where is-ordered($t)" ];
(* The second review: assignability holds in a narrowed block, a trailing ?
tests a whole chain, and the messages name what to write. *)
reads "a trailing ? tests the whole chain" "y = o?.i?"
"(set y (? (?. [~o1 o] (.i ~o1))))";
reads "and ? then as binds the chain's result" "if d?.k? as k\n k"
"(if-let [k (?. [~o1 d] (.k ~o1))] k)";
refused "narrowed-param.fln"
"fn f(x: i32?)\n if x?\n x += 100\n\nfn main()\n f(Some(1))\n"
[ "x is a parameter, and a parameter is not assignable" ];
refused "narrowed-field.fln"
"fn main()\n let x: i32? = Some(1)\n if x?\n x.n = 1\n"
[ "so here it is what the Option holds, i32, and i32 has no fields" ];
refuses "a chain is no place, and the fix is a test" "q?.x = 5" "indent/chain-assign"
"Test it first: if q?, and in the block q is what it holds, or if q? as g";
refused "lowercase-type-arg.fln"
"struct grain\n w: i32\n\nfn main()\n let v = vec-new(grain?)\n"
[ "grain? here is the test that a value is present, and grain is a type";
"vec-new(Option(grain))" ];
refused "addr-taken.fln"
"fn clear(p: Ptr(i32?))\n deref(p) = None\n\nfn main()\n let x: i32? = Some(1)\n\
\ let p = addr(x)\n if x?\n clear(p)\n println(x + 1)\n"
[ "expected Option(i32)" ];
refused "capital-local.fln" "fn main()\n let X: i32? = Some(1)\n println(X?)\n"
[ "To test the local X, give it a lowercase name, as in x?" ];
checks "addr-taken-test.fln"
"fn main()\n let x: i32? = Some(1)\n let p = addr(x)\n if x?\n println(x ?? 0)\n\
\ while x?\n x = None\n";
refused "chain-i32.fln"
"struct P\n x: i32\n\nfn main()\n let p = P{.x 1}\n println(p?.x)\n"
[ "?. has nothing to test. Write . instead" ]
@ -1789,4 +1816,19 @@ let () =
^ "(let [a Dir.north Dir (P {.north 5})] (println Dir.north (= a :north)) 0))\n") ]
else [])
(* A local whose address is taken is not narrowed by if x?: a pointer could
clear it inside the block. The refusal of a payload use says so. *)
let () =
let f = Filename.concat scratch "addr-taken-note.fln" in
write f
"fn main()\n let x: i32? = Some(1)\n let p = addr(x)\n if x?\n println(x + 1)\n";
match Front.checked f with
| _ -> fail "addr-taken-note.fln checked"
| exception (Loc.Error d | Loc.Errors (d :: _)) ->
if not (List.exists
(fun (n : Loc.note) -> Test_support.contains n.Loc.nmsg "Write if x? as g")
d.Loc.notes)
then fail "addr-taken-note.fln: no note naming if x? as g on: %s" d.Loc.dmsg
| exception e -> fail "addr-taken-note.fln: %s" (diag_text e)
let () = Test_support.report ~label:"syntax" ()