;;;; M2 item 3: a typed container crossing into dyn is a VIEW, not a copy. ;;;; ;;;; [as-dyn]'s parameter is unannotated dyn and its argument is a typed ;;;; (Vec i64), a fixed array or a slice — the box happens at the call, on the ;;;; caller's own value, which is what makes [dv] below the SAME storage [v] ;;;; is and not a copy of it. ;;;; ;;;; Every container viewed below is a GLOBAL, and that is not incidental to ;;;; this program — it is the lifetime guard review added after the first ;;;; landing: a view's descriptor chases the container's own address on every ;;;; operation, which is what makes a Vec's growth safe, but it is also what ;;;; makes a DANGLING container's address a live hazard. box refuses a Vec, a ;;;; slice or a fixed array whose storage is not known to outlive the view — ;;;; a local's, a parameter's, a temporary's — and a global's is the one ;;;; storage this milestone can prove permanent: fixed in .data for the ;;;; process — as is a field of one, and an ELEMENT of one when the global ;;;; is an array, whose elements sit inside its own storage. An element of a ;;;; global SLICE is not: the slice is ptr+len and says nothing about where ;;;; the data is — and that holds at every index of a multi-index (at g i j), ;;;; not just the first, so one slice level anywhere in the walk refuses. ;;;; test_flan.ml's checker tests carry the refusal side of this (a local ;;;; Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound to a local, an ;;;; element of a global slice, and an element reached through a slice at a ;;;; later index level); this program is the acceptance side, over storage ;;;; the guard allows. ;;;; ;;;; Mode 0 is the survey: a read through the view boxes the element ;;;; correctly, a write through either side is seen through the other, and a ;;;; push through the view — which can only mean the Vec case, since neither ;;;; a slice nor a fixed array can grow — moves the Vec's backing storage and ;;;; the typed side still sees the grown length and the new element. That is ;;;; the design's central claim: the view's descriptor points AT the Vec's ;;;; own header rather than snapshotting its pointer and length, so there is ;;;; no snapshot for the growth to invalidate — and the header itself is the ;;;; global's, which never moves even though the buffer behind it does. ;;;; ;;;; Modes 1 and 2 are the two traps a view can throw: an index outside its ;;;; length, and a write whose dyn tag does not match the element type the ;;;; view was built over. Both come from the runtime, by name, and both end ;;;; the process — a survey program can show at most one trap, so each gets ;;;; its own mode the way test/programs/bounds.flan's do. (defn as-dyn [d dyn] dyn d) (defonce v (Vec i64) (vec-new i64)) (defonce a [4 i64]) (defonce a2 [3 f64]) (defonce bv (Vec bool) (vec-new bool)) ;; A global ARRAY of Vecs. An element of this is permanent — it sits inside ;; the global's own storage at a fixed offset — and a view over it is the ;; acceptance half of the [At] arm's guard. The refusal half is the same ;; program with [[(Vec i64)]] (a global SLICE) instead, which holds only ;; ptr+len and so says nothing about where the Vecs live; test_flan.ml ;; carries that pair, because a refusal cannot run. (defonce rows [2 (Vec i64)]) (defn main [args [string]] i32 (let [n (i32 (bytes->i64 (bytes-view (at args 1))))] (cond (= n 0) (do ;; A (Vec i64) view, over the global. (push v 10) (push v 20) (push v 30) (let [dv (as-dyn v)] (print dv) (print "\n") ;; Write through the view, read through the typed side. (set (at dv 1) 999) (print (at v 1)) (print "\n") ;; Write through the typed side, read through the view. (set (at v 2) 777) (print (at dv 2)) (print "\n") ;; Grow through the view. flan_vec_grow reallocates v's backing ;; storage and overwrites v's own header in place, which is the ;; same header the view points at — so the typed side, asked ;; afterwards, already agrees with the push it never made itself. (push dv 40) (print (len v)) (print "\n") (print (at v 3)) (print "\n")) ;; A fixed array's view: nothing here can grow, so a snapshot taken ;; once at the crossing is sound — there is no move to go stale over. (set (at a 0) 1) (set (at a 1) 2) (set (at a 2) 3) (set (at a 3) 4) (let [da (as-dyn a)] (print da) (print "\n") (set (at da 0) 100) (print (at a 0)) (print "\n") (set (at a 3) 400) (print (at da 3)) (print "\n")) ;; A slice's view, over f64 elements, and a bool Vec's view — the ;; other two of the three element kinds a view can hold. The slice ;; is cut directly from the global at the call, which is what keeps ;; its trace back to permanent storage visible to the checker. (set (at a2 0) 1.5) (set (at a2 1) 2.5) (set (at a2 2) 3.5) (let [ds (as-dyn (slice a2 0 3))] (print ds) (print "\n") (set (at ds 0) 9.5) (print (at a2 0)) (print "\n")) (push bv true) (push bv false) (let [db (as-dyn bv)] (print db) (print "\n") (set (at db 1) true) (print (at bv 1)) (print "\n")) ;; An element of the global array: a (Vec i64) living inside the ;; global's own storage, viewed from there. A push through the view ;; grows that element's buffer and the typed side sees it, exactly ;; as for the plain global Vec above — the element's header never ;; moves, because the array it sits in never does. (push (at rows 0) 111) (push (at rows 0) 222) (let [dr (as-dyn (at rows 0))] (print dr) (print "\n") (push dr 333) (print (len (at rows 0))) (print "\n") (print (at (at rows 0) 2)) (print "\n")) 0) (= n 1) ;; Out of range. The runtime's own message names the length. (do (push v 1) (let [dv (as-dyn v)] (print (at dv 5))) 0) (= n 2) ;; Wrong type on write: a text where the view holds i64. Tag-checked ;; and refused, never coerced and never silently stored. (do (push v 1) (let [dv (as-dyn v)] (set (at dv 0) "nope")) 0) :else (do (println "?") 1))))