diff --git a/lib/check.ml b/lib/check.ml index d25ed1f7..9bb94eb6 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -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 diff --git a/lib/indent_reader.ml b/lib/indent_reader.ml index d3b6f6b6..3898b753 100644 --- a/lib/indent_reader.ml +++ b/lib/indent_reader.ml @@ -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) diff --git a/spec-syntax.md b/spec-syntax.md index 3a3e2546..d6b13f7d 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -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 diff --git a/test/programs/presence.fln b/test/programs/presence.fln index 2e412f90..c2f01e22 100644 --- a/test/programs/presence.fln +++ b/test/programs/presence.fln @@ -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 diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index fc28a613..4f986296 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -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) -> diff --git a/test/test_flan.ml b/test/test_flan.ml index 7f4309ec..59b8221e 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -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 diff --git a/test/test_syntax.ml b/test/test_syntax.ml index bffae0d4..d64e413d 100644 --- a/test/test_syntax.ml +++ b/test/test_syntax.ml @@ -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" ()