136 lines
5.4 KiB
Plaintext
136 lines
5.4 KiB
Plaintext
;;;; 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; dyn-view-any.flan covers
|
|
;;;; the other storage and element types.
|
|
;;;;
|
|
;;;; 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 [str]] 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 (length 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 (length (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))))
|