flan/test/programs/slice-from-ptr.flan
Joseph Ferano 57fe91f303 Five records become one, and every citation lands somewhere
FIX.org, NEXT.md, DISCUSS.org, docs/DISCUSS.md and the session handoff at the
root are one TODO.org now: 293 entries under seven subsystem headings, each
carrying an org keyword that says where it stands. A DONE entry is a few lines
saying what was decided and what that rules out; the reasoning that would not
compress — the embedding spike and the four reports the hand-written x86
backend was built from — moved into docs/BUILT.md instead, and its entries
point there in one line.

Every entry was checked against the tree before it got a keyword, and the
prose was wrong in both directions. Things the deleted files called open were
built: the first-evaluation stall, main being redefinable, macro parameter
lists, the type-limit constants, the array constructors, the byte fills,
inc/dec, the discard's fontification, the Emacs buffers, rt_die's _exit, the
backtrace surface, and the acceptance failure that could print and still exit
zero. Things they called done were not: the backend reports' no-plan buckets
had gone stale in the other direction, the value-dependent defvar was
superseded rather than built, and macro-expansion source locations are on an
unmerged lane, so that entry is NEXT and names the branch.

Every comment that cited one of the five by name now cites a heading that
exists, in TODO.org or in docs/BUILT.md. The session reports under
docs/handoffs/ keep naming the files they worked on, because rewriting them
would falsify what those sessions did; each carries a note saying where the
content went.
2026-09-21 21:05:48 +07:00

62 lines
2.6 KiB
Plaintext

;;;; (slice-from-ptr p n) — TODO.org, "A pointer from C needs a length before
;;;; it can be indexed". The motivating pointers come from C, but nothing about
;;;; the form does: a (Ptr T) is a (Ptr T) whoever made it, so this case makes
;;;; its own with (addr (at a 0)) and needs no library and no window.
;;;;
;;;; What is asserted, line by line:
;;;;
;;;; - the length is the one the caller stated, and (length s) answers it;
;;;; - the elements read through are the same storage, not a copy — the last
;;;; two lines write through the slice and read the array back, which is
;;;; the whole ptr+len claim;
;;;; - a shorter promise than the truth is legal and is what indexing then
;;;; believes, because the caller's number is the only length there is;
;;;; - the result is an ordinary [T]: it slices, it is passed to a function
;;;; that takes a slice, and the prelude's algorithms work on it.
;;;;
;;;; What is NOT here, and is in test_flan.ml's refusal table instead: a
;;;; negative literal length, a first argument that is not a pointer, and
;;;; (free (slice-from-ptr ...)) — a slice owns nothing, so free refuses it by
;;;; the rule it already had.
(defonce a [5 i32])
(defn total [s [i32]] i32
(let [acc 0]
(dotimes [i (length s)]
(set acc (+ acc (at s i))))
acc))
(defn main [] ()
(dotimes [i 5]
(set (at a i) (* (+ i 1) 10)))
;; The whole array, as the caller promises it: five elements behind the
;; address of the first.
(let [s (slice-from-ptr (addr (at a 0)) 5)]
(println (length s)) ; 5
(println (at s 0)) ; 10
(println (at s 4)) ; 50
(println (total s)) ; 150
;; An ordinary [i32] from here on: slice it, and the sub-view still points
;; into the same storage.
(println (total (slice s 1 3)))) ; 50
;; A promise shorter than the truth. Nothing complains — there is nothing to
;; complain with — and the length the caller gave is the length indexing and
;; the bounds check both use.
(let [s (slice-from-ptr (addr (at a 1)) 2)]
(println (length s)) ; 2
(println (total s))) ; 50
;; Zero is a length like any other. An empty slice is not a null pointer and
;; is not an error.
(println (length (slice-from-ptr (addr (at a 0)) 0))) ; 0
;; It is a view, not a copy: a write through the slice is a write to the
;; array, and this is what would fail if the form ever grew a memcpy.
(let [s (slice-from-ptr (addr (at a 0)) 5)]
(set (at s 2) 7)
(println (at a 2)) ; 7
(println (total s)))) ; 127