;;;; Allocators — spec-memory.md, "Allocators". No container here: this is the
;;;; tier on its own, so that a failure in it is not read as a Vec bug.
;;;;
;;;; What is asserted: the capability set is readable at run time and differs
;;;; per allocator; with-allocator rebinds for its dynamic extent and restores
;;;; afterwards, including out of a call and out of a transfer; free-all is
;;;; retain-capacity and bumps the epoch anyway; and nothing is released at
;;;; scope exit, which is the point the spec is most emphatic about.

;; A zeroed Allocator. A global rather than a local because the arena has to
;; outlive the frame that makes it, and because a handler cannot see a local
;; (check.ml's `captured` says so by name).
(defvar frame Allocator)

;;; The context is a dynamic variable, so a function called from inside a
;;; with-allocator body sees the rebinding without anything being passed.
(defn who-am-i [] bool
  (can-free? context/allocator))

(defn main [] i32
  ;; The heap allocator frees one block; an arena does not. That is Odin's
  ;; answer too — its arena returns Mode_Not_Implemented for .Free — and it is
  ;; the capability spec-memory.md calls load-bearing.
  (set frame (arena-new 1024))
  (println (can-free? (heap-allocator)))       ; true
  (println (can-free? frame))                  ; false
  (println (can-free-all? (heap-allocator)))   ; false
  (println (can-free-all? frame))              ; true

  ;; The default context is the heap allocator, and context/temp is its own
  ;; arena — the per-frame tier, distinct from it.
  (println (can-free? context/allocator))      ; true
  (println (can-free? context/temp))           ; false

  ;; with-allocator rebinds for the dynamic extent, so a call made from inside
  ;; the body sees the arena, and the binding is gone after the body.
  (println (with-allocator frame (who-am-i)))  ; false
  (println (who-am-i))                         ; true

  ;; ... and it is an expression: the body's last value is the form's value.
  (println (with-allocator frame 41))          ; 41

  ;; free-all is retain-capacity: the pages stay, the epoch moves. Both halves
  ;; matter — the first is what makes a per-frame reset free, and the second is
  ;; what a container's dev trap reads.
  (println (alloc-epoch frame))                ; 0
  (free-all frame)
  (println (alloc-epoch frame))                ; 1
  (free-all frame)
  (println (alloc-epoch frame))                ; 2

  ;; Nothing is released at scope exit — not at the end of a let, not at the
  ;; end of a with-allocator body. The epoch is the observable proof: leaving
  ;; the body did not release the region it named.
  (let [before (alloc-epoch frame)]
    (with-allocator frame (println (alloc-epoch frame)))  ; 2
    (println (= before (alloc-epoch frame))))             ; true

  ;; And out of a transfer. The restart-case's clause runs after the body has
  ;; left through the pad, so the context allocator here is the one the
  ;; with-allocator displaced, not the arena.
  (println
    (restart-case
      (with-allocator frame (invoke-restart 'resync))
      (resync [] (can-free? context/allocator))))         ; true

  (arena-destroy frame)
  0)