diff --git a/lib/check.ml b/lib/check.ml index e01bca51..c6acece6 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -4986,6 +4986,56 @@ let const_note ?(fln = false) env ~(want : Types.t) ~(got : Types.t) = (Types.spell ~indented:fln want) (Types.spell ~indented:fln got) | _ -> "" +let nil_has_no_none loc w = + fail loc + "nil has no None to become at %s — nil only converts to (Option T) \ + or to dyn itself; wrap the type in Option, or keep the value dyn" + (tyname loc w) + +(* A literal boxed where a dyn was wanted, and the literal. It brings no dyn + of its own to an operator: (+ nil 1) over a literal 1 checked at dyn is as + typed as (+ nil x) over an i32 x. *) +let boxed_literal (e : Tast.expr) = + match e.Tast.e with + | Tast.Prim (Tast.Rt ("flan_dyn_from_i64" | "flan_dyn_from_f64" + | "flan_dyn_from_char" | "flan_dyn_from_bool"), [ x ]) -> + let x = match x.Tast.e with Tast.Prim (Tast.Cast _, [ y ]) -> y | _ -> x in + (match x.Tast.e with + | Tast.Int (n, _) when x.Tast.ty <> Types.Char -> + (* The type the literal takes where nothing is wanted. *) + let k = + if Int64.compare n (Int64.of_int32 Int32.max_int) > 0 + || Int64.compare n (Int64.of_int32 Int32.min_int) < 0 + then Types.I64 else Types.I32 + in + Some (Types.Int k) + | Tast.Int _ | Tast.Float _ | Tast.Bool _ -> Some x.Tast.ty + | _ -> None) + | _ -> None + +(* The operands of an arithmetic, bitwise or ordering operator gone dyn, + before they are boxed: a literal [nil] among them with nothing else dyn is + refused as [expect] refuses it at a typed want, whichever position it is + in and whether or not the form has a want. A dyn that holds nil is the + run-time trap's, so (+ 1 2 nil) is refused and (+ 1 2 (the dyn nil)) + traps. [=] and [!=] ask no such question: nil is unequal to a number. *) +let no_bare_nil (ops : Tast.expr list) = + match List.find_opt is_nil_lit ops with + | None -> () + | Some nil -> + let makes_dyn (e : Tast.expr) = + e.Tast.ty = Types.Dyn && not (is_nil_lit e) && boxed_literal e = None + in + if not (List.exists makes_dyn ops) then + match + List.find_map + (fun (e : Tast.expr) -> + if e.Tast.ty <> Types.Dyn then Some e.Tast.ty else boxed_literal e) + ops + with + | Some t -> nil_has_no_none nil.Tast.loc t + | None -> () + let expect ctx loc ~want (got : Tast.expr) = match want with | None -> got @@ -5009,11 +5059,7 @@ let expect ctx loc ~want (got : Tast.expr) = actually see — the literal, written right where the mismatch is. Refused here, at the offending line, instead of waiting for the runtime trap [unbox] would otherwise reach for two arms down. *) - | w, Types.Dyn when is_nil_lit got -> - fail loc - "nil has no None to become at %s — nil only converts to (Option T) \ - or to dyn itself; wrap the type in Option, or keep the value dyn" - (tyname loc w) + | w, Types.Dyn when is_nil_lit got -> nil_has_no_none loc w | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got | (Types.String | Types.Slice _ | Types.Array _), Types.Dyn -> let opened = into_typed ctx loc w got in @@ -6817,6 +6863,13 @@ and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n = (tyname loc other) n | _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default)) +(* A wide literal where a dyn is wanted. A global's initialiser adds the fix + (its type); anywhere else there is nothing to retype. *) +and wide_at_dyn s = + Printf.sprintf + "expected dyn, found the integer literal %s, which is above the largest \ + dyn int (9223372036854775807), so it has no dyn value" s + (* An integer written at or above 2^63, in decimal or in hex. Only a u64 holds one, so it is accepted there and refused everywhere else, in the spelling it was written in — its pattern read as an i64 is a different number. *) @@ -6835,12 +6888,7 @@ and wide_literal loc ~want n s = "%s does not fit in i32, the type an integer literal takes when nothing \ says otherwise — write (u64 %s) for a u64" s s - | Some Types.Dyn -> - Loc.failk literal_at_want loc - "expected dyn, found the integer literal %s, which only a u64 holds — a \ - dyn integer is an i64, and no i64 is this large. Give what holds it \ - the type u64" - s + | Some Types.Dyn -> Loc.failk literal_at_want loc "%s" (wide_at_dyn s) | Some other -> Loc.failk literal_at_want loc "expected %s, found the integer literal %s, which only a u64 holds" @@ -9806,6 +9854,10 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) = v.Ast.loc items | _ -> expect ctx v.Ast.loc ~want:(Some ty) (check ctx ~want:ty v) in + (* (the dyn nil) is a dyn value that holds nil, not the literal: at a typed + want it traps at run time as any dyn holding nil does, where a bare nil + is refused ([is_nil_lit] sees through nothing, so the [Do] hides it). *) + let r = if is_nil_lit r && ty = Types.Dyn then mk loc Types.Dyn (Tast.Do [ r ]) else r in expect ctx loc ~want r (* [f] run for its answer alone: whatever it wrote into the context is put @@ -11903,13 +11955,24 @@ and fold_arg ctx ty (arg : Ast.expr) = match trial_at ctx arg ty with | Ok v -> fold_operand ctx ty v | Error _ -> - let own () = - let v = check ctx arg in - if v.Tast.ty = Types.Dyn then v else fail arg.Ast.loc "not a dyn" + (* Only asked, and asked with the literal locals' uses unrecorded: a + [trial] does not take back what the session recorded, and the operand + on its own terms is not how the program reads it unless it is a dyn — + (+ x y) over an int x and a float y would merge the two and move the + refusal onto x. A dyn is then checked again, recorded. *) + let unrecorded f = + match ctx.lits with + | Some s when s.recording -> + s.recording <- false; + Fun.protect ~finally:(fun () -> s.recording <- true) f + | _ -> f () in - match trial ctx own with - | Ok v -> `Dyn v - | Error _ -> fold_operand ctx ty (check ctx ~want:ty arg) + let is_dyn = + probe ctx arg.Ast.loc (fun () -> unrecorded (fun () -> (check ctx arg).Tast.ty)) + = Some Types.Dyn + in + if is_dyn then `Dyn (to_dyn ctx (check ctx arg)) + else fold_operand ctx ty (check ctx ~want:ty arg) (* A pair an arithmetic operator refused, when one operand is a char: that is the refusal to give, rather than the mismatch between the two. Asked @@ -12023,11 +12086,6 @@ and dyn_fold ctx ~want loc name first rest = no column — [here loc] is the same string literal [cast_dyn] hands the runtime, and the runtime prints it as a GNU prefix. *) let apply acc b = rt loc Types.Dyn sym [ acc; box ~ctx loc b; here loc ] in - let acc = - match first with - | [ a; b ] -> apply (box ~ctx loc a) b - | _ -> assert false - in let operand arg = if bitwise then begin let v = check ctx arg in @@ -12036,7 +12094,14 @@ and dyn_fold ctx ~want loc name first rest = end else check ctx ~want:Types.Dyn arg in - let acc = List.fold_left (fun acc arg -> apply acc (operand arg)) acc rest in + let rest = map_lr operand rest in + no_bare_nil (first @ rest); + let acc = + match first with + | [ a; b ] -> apply (box ~ctx loc a) b + | _ -> assert false + in + let acc = List.fold_left apply acc rest in expect ctx loc ~want acc (* The runtime's entry point for each bit operation on a dyn int. *) @@ -13483,7 +13548,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = two things being unalike is the answer to "are these equal", not an error. The orderings do trap, and rightly — there is no true answer to whether a string is less than a vector. *) - (* [ops] are every operand, boxed. *) + (* [ops] are every operand, not yet boxed. *) let dyn_chain ops = let sym = match name with @@ -13508,17 +13573,22 @@ and named_call ?(qualified = false) ctx ~want loc name args = mk loc Types.Bool (Tast.Prim (Tast.Not, [ cmp ])) else cmp in - let r = + let ops = match rest with - | [] -> link (box ~ctx loc a) (box ~ctx loc b) - | _ -> cmp_over ctx loc Types.Dyn ~pairs ~link (ops ()) + | [] -> [ a; b ] + | _ -> ops () + in + if not (String.equal sym "flan_dyn_eq") then no_bare_nil ops; + let r = + match List.map (box ~ctx loc) ops with + | [ a; b ] -> link a b + | ops -> cmp_over ctx loc Types.Dyn ~pairs ~link ops in expect ctx loc ~want r in if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then dyn_chain (fun () -> - box ~ctx loc a :: box ~ctx loc b - :: map_lr (fun e -> box ~ctx loc (check ctx ~want:Types.Dyn e)) rest) + a :: b :: map_lr (fun e -> check ctx ~want:Types.Dyn e) rest) else begin (* [=] and [!=] admit types [<] does not. A handle is one: a pair of numbers in one word and where being the same entity is the question the @@ -13560,8 +13630,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = dyn in it is a dyn comparison. *) if List.exists (function `Dyn _ -> true | `Typed _ -> false) rest then dyn_chain (fun () -> - box ~ctx loc a :: box ~ctx loc b - :: List.map (function `Dyn d -> d | `Typed v -> box ~ctx loc v) rest) + a :: b :: List.map (function `Dyn d -> d | `Typed v -> v) rest) else let ops = a :: b :: List.map (function `Typed v -> v | `Dyn d -> d) rest in @@ -13643,6 +13712,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = (fun (v : Tast.expr) -> if v.Tast.ty <> Types.Dyn then bits_operand ctx v.Tast.loc name v) [ a; b ]; + no_bare_nil [ a; b ]; expect ctx loc ~want (rt loc Types.Dyn (dyn_bits_sym name) [ box ~ctx loc a; box ~ctx loc b; here loc ]) end else begin @@ -19471,6 +19541,11 @@ let check_global env (d : Ast.decl) : Tast.global option = { Tast.e = Tast.Uninit ty; ty; loc = d.Ast.dloc } | Ast.Init v -> let c = ctx () in + (match v.Ast.e with + | Ast.UInt (_, s) when ty = Types.Dyn -> + Loc.failk literal_at_want v.Ast.loc "%s. Give %s the type u64" + (wide_at_dyn s) n + | _ -> ()); let v = view_global_init := Some (n, kind); Fun.protect ~finally:(fun () -> view_global_init := None) diff --git a/test/programs/dyn-crossing.flan b/test/programs/dyn-crossing.flan index 41431fa0..4b80b47c 100644 --- a/test/programs/dyn-crossing.flan +++ b/test/programs/dyn-crossing.flan @@ -1,6 +1,6 @@ ;;;; Typed values crossing into dyn beside a dyn operand: a u64, a dyn nil past -;;;; a fold's first pair, and a $t bounded by is-numeric. With an argument, the -;;;; program runs the trap that argument names instead. +;;;; a fold's pair (a bare nil is refused, see test_flan), and an is-numeric $t. +;;;; With an argument, the program runs the trap that argument names instead. (defn add-dyn [x $t] dyn {:where (is-numeric $t)} @@ -54,6 +54,11 @@ (when (= a "nil-first") (println (+ (the dyn nil) 1 2))) (when (= a "nil-last") (println (+ 1 2 (the dyn nil)))) (when (= a "nil-less") (println (< 1 2 (the dyn nil)))) - (when (= a "nil-min") (println (min 1 2 nil))) - (when (= a "nil-bits") (println (bit-or 1 2 nothing)))))) + (when (= a "nil-min") (println (min 1 2 nothing))) + (when (= a "nil-bits") (println (bit-or 1 2 nothing))) + ;; At a typed want too: the dyn nil traps in any position. + (let [r (the i32 0)] + (when (= a "nil-want-first") (set r (+ (the dyn nil) 1 2))) + (when (= a "nil-want-last") (set r (+ 1 2 (the dyn nil)))) + (println r))))) 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 4c35b408..c75a53ff 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -5688,7 +5688,9 @@ level "1" "nil-last", "55:41", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)"; "nil-less", "56:41", "dyn <: int and nil"; "nil-min", "57:40", "dyn min: int and nil"; - "nil-bits", "58:41", "dyn bit-or: int and nil" ] + "nil-bits", "58:41", "dyn bit-or: int and nil"; + "nil-want-first", "61:50", "dyn: an i32 is wanted here, and this is nil"; + "nil-want-last", "62:46", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)" ] in List.iter (fun x86 -> diff --git a/test/test_flan.ml b/test/test_flan.ml index 0c7fa3e0..836e7433 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2066,6 +2066,70 @@ let () = rejects_check "nil at a bare T is refused at compile time" "(defn take [n i32] i32 n)\n(defn main [] i32 (take nil))" ~needle:"nil has no None to become"; + (* A bare nil in an arithmetic, bitwise or ordering operator with nothing + else dyn is refused in every position, with or without a want; a dyn that + holds nil is left to trap at run time (dyn-crossing.flan). *) + (* The 1-based column of [sub] in [form], placed at column [base]. *) + let col_of base form sub = + let n = String.length sub in + let rec at i = if String.sub form i n = sub then i else at (i + 1) in + base + at 0 + in + List.iter + (fun form -> + List.iter + (fun (what, base, src) -> + let col = col_of base form "nil" in + match + (try ignore (checked src); None with Loc.Error d -> Some d) + with + | Some d when contains d.Loc.dmsg "nil has no None to become at i32" + && d.Loc.dloc.Loc.col = col -> () + | Some d -> + incr failures; + Printf.printf "FAIL a bare nil in %s, %s: got %d: %s\n" form what + d.Loc.dloc.Loc.col d.Loc.dmsg + | None -> + incr failures; + Printf.printf "FAIL a bare nil in %s, %s: accepted\n" form what) + [ "at a want", 16, + Printf.sprintf "(defn f [] i32 %s)\n(defn main [] i32 (f))" form; + "with none", 25, + Printf.sprintf "(defn f [] i32 (println %s) 0)\n(defn main [] i32 (f))" form ]) + [ "(+ nil 1 2)"; "(+ 1 nil 2)"; "(+ 1 2 nil)"; "(+ 1 nil)"; + "(< nil 1 2)"; "(< 1 2 nil)"; "(min 1 2 nil)"; "(bit-or nil 1 2)"; + "(bit-or 1 2 nil)" ]; + accepts "a dyn holding nil in a fold is left to the run time" + "(defn f [p dyn] i32 (+ 1 2 p (the dyn nil)))\n\ + (defn g [] i32 (let [r (the i32 0)] (set r (+ (the dyn nil) 1 2)) r))\n\ + (defn main [] i32 (println (< 1 2 (the dyn nil))) 0)"; + accepts "nil beside a real dyn in a fold is left to the run time" + "(defn f [p dyn] dyn (+ 1 2 p nil))\n(defn main [] i32 0)"; + (* An operand past the pair asked on its own terms records nothing: the + float y is blamed, not the int x it would have merged with. *) + List.iter + (fun form -> + let col = col_of 45 form "y)" in + match + (try ignore (checked ("(defn main [] i32 (let [x 5 y 2.5] (println " + ^ form ^ ")) 0)")); None + with Loc.Error d -> Some d) + with + | Some d when d.Loc.dloc.Loc.col = col -> () + | Some d -> + incr failures; + Printf.printf "FAIL %s blames col %d, not y at %d: %s\n" form + d.Loc.dloc.Loc.col col d.Loc.dmsg + | None -> incr failures; Printf.printf "FAIL %s: accepted\n" form) + [ "(+ (the i64 1) 2 (+ x y))"; "(* (the i64 1) 2 (* x y))"; + "(max (the i64 1) 2 (max x y))"; "(< (the i64 1) 2 (+ x y))" ]; + rejects_check "a wide literal at dyn with nothing to retype" + "(defn main [] i32 (println (the dyn 0xFFFFFFFFFFFFFFFF)) 0)" + ~needle:"0xFFFFFFFFFFFFFFFF, which is above the largest dyn int \ + (9223372036854775807), so it has no dyn value"; + rejects_check "a wide literal beside a dyn" + "(defn main [] i32 (println (+ (the dyn 0) 0xFFFFFFFFFFFFFFFF)) 0)" + ~needle:"so it has no dyn value"; (* A $t crosses into dyn only under a bound every type of which has a dyn value; an unbounded one could be a pointer, refused at no call site. *) rejects_check "an unbounded $t does not cross into dyn" @@ -8032,7 +8096,7 @@ let () = ~needle:"the member A of E is 0xFFFFFFFFFFFFFFFF, which does not fit i32"; rejects_check "a wide literal in a dyn global names the type u64" "(defonce big 0xFFFFFFFFFFFFFFFF)" - ~needle:"no i64 is this large. Give what holds it the type u64"; + ~needle:"so it has no dyn value. Give big the type u64"; accepts "the type the dyn refusal names compiles" "(defonce big u64 0xFFFFFFFFFFFFFFFF)"; (* A macro's Form has one integer case; the literal comes back wide all the