;;;; 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. (Boxing a value AFTER passing it through an
;;;; ordinary by-value parameter would view that parameter's own copy instead
;;;; — value semantics, not a hole in this feature — so every view here is
;;;; taken where the container already lives.)
;;;;
;;;; 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
;;;; last one 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.
;;;;
;;;; 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)

(defn main [args [string]] i32
  (let [n (i32 (bytes->i64 (bytes (at args 1))))]
    (cond
      (= n 0)
      (do
        ;; A (Vec i64) view.
        (let [v (vec-new i64)]
          (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.
        (let [a (array 4 i64)]
          (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.
        (let [a2 (array 3 f64)]
          (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")))
        (let [bv (vec-new bool)]
          (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")))
        0)
      (= n 1)
      ;; Out of range. The runtime's own message names the length.
      (do (let [v (vec-new i64)]
            (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 (let [v (vec-new i64)]
            (push v 1)
            (let [dv (as-dyn v)]
              (set (at dv 0) "nope")))
          0)
      :else (do (println "?") 1))))