59 lines
2.3 KiB
Plaintext
59 lines
2.3 KiB
Plaintext
;;;; 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.
|
|
(defonce the-data (Vec u8))
|
|
(defonce 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 is-loaded [] bool (> (length the-data) 0))
|
|
|
|
(defn load [] ()
|
|
(when (not (is-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 (length 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 (length 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 (length (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 (length c))
|
|
(free c))
|
|
(println (length the-data))
|
|
0)
|