;;;; A global of move-only type, which is allowed, and the one rule that makes
;;;; it allowed: reading a global Vec is always a borrow and never a move. The
;;;; lifetime question ownership tracking exists to answer has a constant
;;;; answer here — the process's — so nothing may take the global and nothing
;;;; may free it, and with no owner to hand over there is no double free to
;;;; catch. The refusals that enforce that are in test_flan.ml.
;;;;
;;;; A zeroed Vec is a real empty Vec, so the global starts as one and is
;;;; loaded by whoever loads it. What this program pins is that the loading
;;;; happens once and survives: [entry] is called twice, the way a re-entered
;;;; main would be, and the second call finds the data the first one left.
(defvar the-data (Vec u8))
(defvar counts (Map u8 i64))

;; Reading it here is a borrow. So is reading it in [total] below, which is the
;; case the old rule could not express: two functions holding the same global
;; at once is fine exactly because neither of them can free it.
(defn loaded? [] bool (> (len the-data) 0))

(defn load [] ()
  (when (not (loaded?))
    (set the-data (vec-new u8))
    (dotimes [i 5] (push the-data (u8 (* i 3))))))

(defn total [] i64
  (let [s (i64 0)]
    (dotimes [i (len the-data)] (set s (+ s (i64 (at the-data i)))))
    s))

;; Mutating in place, through the global rather than through a copy of it. The
;; aliasing contract is the one every Vec has (spec-memory.md, "Borrowing"): a
;; push may reallocate and invalidate a slice taken before it, and that is the
;; programmer's, here as much as for a local.
(defn bump [] ()
  (set (at the-data 0) (+ (at the-data 0) 1))
  (push the-data 100))

(defn entry [] ()
  (load)
  (bump)
  (put counts 1 (total))
  (println (len the-data))
  (println (total))
  (match (get counts 1) (Some v) (println v) None (println "?")))

(defn main [] i32
  (entry)
  ;; The second run. Nothing re-initialises the global between them, so the
  ;; length keeps climbing and the loaded data is the same block it was.
  (entry)
  (println (len (as-slice the-data)))
  ;; A copy is the one thing something else may own, and freeing that copy
  ;; leaves the global untouched.
  (let [c (clone the-data)]
    (println (len c))
    (free c))
  (println (len the-data))
  0)