Joseph Ferano
3c1fb1b31e
Both directions of the boundary go through expect, the way every other dyn crossing does. A dyn's tag decides which case an (Option T) becomes on the way in; an Option's own tag decides nil or a boxed payload on the way out. box_option/unbox_option build the same If-over-a-tag shape get and map-remove already build for the same reason, reading an Option's tag and payload with the raw Field access Render's structural printer already uses — nothing new for either backend to lower. A literal Some/None skips the runtime check entirely, since the checker already knows which case it is. A bare T has no None to become. The literal nil the checker can see is refused right there, at compile time, in expect itself — the author's decision to do both halves rather than settle for the runtime trap alone. Everything one step removed from the syntax — a dyn that only turns out to be nil once the program runs — reaches flan_dyn_need_i64's existing DynType trap, unchanged; there is no dataflow in this checker for it to be otherwise (see "Ownership tracking repealed"). (Some nil) is refused the same way: the literal at compile time, with a message saying why nil and None would collide; a dyn that turns out to be nil only at run time through the new flan_dyn_need_not_nil, which traps by the same route flan_dyn_need_i64 does. (Option (Option T)) does not cross either direction — boxing Some of an inner None would box it as nil, indistinguishable from the outer None, the same ambiguity (Some nil) is refused for. The type itself stays legal on the typed side; only the crossing does not exist for it. (Option dyn) needs no case of its own in the boundary code — the payload is already dyn, so box_option/unbox_option treat it as the identity — but it is not yet a value a program can hold anywhere. The per-type-descriptor pass (M2 item 2) refuses it at every storage site today, the same way it refuses (Vec dyn), because a struct's dyn fields are marked by byte offsets and (Option dyn)'s payload has none. Item 4 does not lift that gate; it only makes the boundary already correct for the day items 2/3 do. expect grew a ctx parameter to build the fresh slot the two new crossings need — every call site threaded through, one context mismatch caught and fixed in check_fn's tail-expression case along the way. var's None case grew a direct Dyn arm: None at a dyn want is nil outright, with nothing to build. nil-option.flan carries the crossings that succeed and ends on the bare-T trap; some-nil.flan is (Some nil)'s run-time half, kept in its own file the way dyn-boundary.flan is one trap per program. Both are in no_fallback_slots and test_sanitize.ml: the new dyn temporary unbox_option's tag test mints is rooted, and reads its Option's tag and payload through ASan clean, --sanitize matching the unsanitized run byte for byte.
15 lines
622 B
Plaintext
15 lines
622 B
Plaintext
;;;; (Some nil), the run-time half -- M2 queue item 4.
|
|
;;;;
|
|
;;;; The literal (Some nil) is refused at compile time (test_flan.ml). This is
|
|
;;;; the other half: a dyn value the checker cannot see is nil until the
|
|
;;;; program runs, reaching Some anyway. flan_dyn_need_not_nil owns the
|
|
;;;; wording, the same way flan_dyn_need_i64 owns dyn-boundary.flan's.
|
|
|
|
(defn maybe-nil [flag bool] dyn (if flag 5 nil))
|
|
|
|
(defn main [] ()
|
|
(print (match (Some (maybe-nil true)) (Some x) x None -1))
|
|
(println "") ; 5
|
|
(print (match (Some (maybe-nil false)) (Some x) x None -1))
|
|
(println ""))
|