;;;; spec-memory.md's arena rule, which is the run-time half of what replaced
;;;; the three type-level refusals a container of owning elements used to meet.
;;;;
;;;; "Constructing a container whose element type owns storage, against an
;;;; allocator that lacks can-free, is refused at the point of construction:
;;;; one branch per container, not per element." One branch and not a walk,
;;;; because the alternative is something that inspects the graph at release,
;;;; and that is the registry of destructors the frame tier's reset exists to
;;;; not have.
;;;;
;;;; It is a run-time branch and not a compile-time refusal because there is
;;;; nothing static to refuse against: with-allocator rebinds a dynamic
;;;; variable, so which tier a (vec-new) meets is not knowable where it is
;;;; written. The compiler decides only whether to *ask*.
;;;;
;;;; Argument 0 is everything that must work, argument 1 and argument 2 are the
;;;; two ways this dies. Each death is the whole test of its case, so they are
;;;; separate runs rather than one program that could pass by dying early.

(defvar frame Allocator)

(defalias Row (Vec i32))

(defdata Value [Nil (Int [n i64]) (List [items (Vec Value)])])

(defn main [args [string]] i32
  (set frame (arena-new 4096))
  (let [which (if (> (len args) 1) (i32 (bytes->i64 (bytes (at args 1)))) 0)]
    (cond
      (= which 1)
        ;; The refusal. The context here is the heap, which can free one
        ;; block, and a (Vec Value) against it is a free that would release
        ;; the slots and strand every inner Vec — so the construction dies
        ;; rather than the free three hundred lines later.
        (let [bad (vec-new Value)]
          (println (len bad)))

      (= which 2)
        ;; Use after free-all, which is a different mechanism and worth
        ;; pinning separately: the allocator's epoch moves on every free-all
        ;; and every container records the epoch it was made at. The header
        ;; below was copied *out* of the arena container into a local before
        ;; the release, which is the case the check has to cover and the
        ;; reason spec-memory.md makes an Allocator a pointer rather than a
        ;; copied value — a copied allocator would carry its own epoch and
        ;; the copy would never notice.
        (let [outer (vec-new Value frame)]
          (let [inner (vec-new Value frame)]
            (push inner (Value.Int {.n (i64 7)}))
            (push outer (Value.List {.items inner})))
          (match (at outer 0)
            (List items)
              (do (println (len items))
                  (free-all frame)
                  (println (len items)))
            _ (println 0)))

      (= which 3)
        ;; ZII, which is the hole a guard only at the construction would have
        ;; left. The items field is omitted from the literal, so it is a zeroed
        ;; Vec with no allocator at all — it never went near (vec-new) — and
        ;; the first push is what adopts the context. So the branch is emitted
        ;; at every growth too, and there it asks the container, which answers
        ;; from the allocator it will adopt when it has none of its own.
        (let [v (Value.List {})]
          (match v
            (List items)
              (do (push items (Value.Int {.n (i64 1)}))
                  (println (len items)))
            _ (println 0)))

      :else
        (do
          ;; The control, and it is the case the frame tier exists for: a
          ;; (Vec (Vec i32)) owns storage at two levels and is perfectly happy
          ;; in a region, because free-all releases every block the region
          ;; handed out and the inner ones are among them. The rule asks about
          ;; the *allocator*, never "does this element own anything", so this
          ;; must be built without complaint.
          (with-allocator frame
            (let [rows (vec-new Row)]
              (let [row (vec-new i32)]
                (push row 1)
                (push row 2)
                (push rows row))
              (println (len rows))
              (println (len (at rows 0)))))
          (free-all frame)
          ;; And the same container against the heap dies — asserted from the
          ;; other side in run 1 above; here the point is only that the region
          ;; run above got no complaint.
          (with-allocator frame
            (let [vs (vec-new Value)]
              (push vs (Value.Int {.n (i64 41)}))
              (println (len vs))))
          (free-all frame)
          ;; And the zeroed field of run 3, this time in the region: the growth
          ;; guard has to pass here as surely as it has to fail there, or every
          ;; ZII container in an arena would be unusable.
          (with-allocator frame
            (let [v (Value.List {})]
              (match v
                (List items)
                  (do (push items (Value.Int {.n (i64 1)}))
                      (println (len items)))
                _ (println 0))))
          (free-all frame))))
  (arena-destroy frame)
  0)