tur/refined
refinement newtypes for total collection accessors.
Since: stdlib-refinement-collections-plan (R1, R2)
NonEmpty
(NonEmpty [A] :int))
a cons list of element type A, proven to contain at least one
Since: R1
ne-of
(ne-of [A])
build a NonEmpty by prepending a head to an existing list.
| x | the head element (carrier :int) | |
| xs | the rest of the list (a cons list; may be empty / tnil) |
A NonEmpty whose head is x and whose tail is xs.
(ne-head (ne-of 7 (tnil))) ; => 7
Since: R1
ne-singleton
(ne-singleton [A])
build a one-element NonEmpty.
| x | the sole element (carrier :int) |
A NonEmpty containing exactly x.
(ne-head (ne-singleton 42)) ; => 42
Since: R1
ne-head
(ne-head [A])
the first element of a NonEmpty (total).
| ne | the NonEmpty to inspect |
The first element (carrier :int).
(ne-head (ne-of 1 (tcons 2 (tnil)))) ; => 1
Since: R1
ne-tail
(ne-tail [A])
the elements after the head, as an ordinary (possibly empty) list.
| ne | the NonEmpty to inspect |
The tail as a cons list (tnil when ne has a single element).
(list-head (ne-tail (ne-of 1 (tcons 2 (tnil))))) ; => 2
Since: R1
ne->list
(ne->list [A])
view a NonEmpty as an ordinary cons list.
| ne | the NonEmpty to convert |
The underlying cons list (never empty).
(list-head (ne->list (ne-singleton 5))) ; => 5
Since: R1
ne-len
(ne-len [A])
the number of elements in a NonEmpty (always >= 1).
| ne | the NonEmpty to measure |
The element count as an :int.
(ne-len (ne-of 1 (tcons 2 (tnil)))) ; => 2
Since: R1
ne-from?
(ne-from? [A])
smart constructor: recover a NonEmpty from an arbitrary list.
| xs | an arbitrary typed list (may be empty) |
(some ne) when xs is non-empty, (none) when xs is empty. The payload is a (NonEmpty A) whose element type A is recovered from the (List A) arg; recover it with ne-unwrap.
(some? (ne-from? (list-of 1))) ; => true (some? (ne-from? (list-of))) ; => false
Since: R1
ne-unwrap
(ne-unwrap [A])
recover the NonEmpty payload from a non-none Option.
| o | a (Option (NonEmpty A)) as returned by ne-from? |
The wrapped (NonEmpty A).
(let [o (ne-from? (list-of 9))]
(if (some? o) (ne-head (ne-unwrap o)) -1)) ; => 9
Since: R1
BoundedIdx
(BoundedIdx)
an index proven to satisfy 0 <= i < n for some length n.
Since: R2
bidx->int
(bidx->int [b : BoundedIdx] :)
recover the raw :int index from a BoundedIdx.
| b | the BoundedIdx to unwrap |
The underlying index as a plain :int.
(bidx->int (bidx-unwrap (bidx-of? 5 3))) ; => 3
Since: R2
bidx-of?
(bidx-of? [n : int i : int] :)
smart constructor: prove an index lies within [0, n).
| n | the exclusive upper bound (e.g. a collection's length) | |
| i | the candidate index |
(some b) when 0 <= i < n, (none) otherwise. Recover the BoundedIdx payload with bidx-unwrap.
(some? (bidx-of? 5 3)) ; => true (some? (bidx-of? 5 9)) ; => false
Since: R2
bidx-unwrap
(bidx-unwrap [o : (Option BoundedIdx)] :)
recover the BoundedIdx payload from a non-none Option.
| o | a (Option BoundedIdx) as returned by bidx-of? |
The wrapped BoundedIdx.
(let [o (bidx-of? 4 2)]
(if (some? o) (bidx->int (bidx-unwrap o)) -1)) ; => 2
Since: R2
vec-get-checked
(vec-get-checked [A])
index a Vec with a proven-in-range BoundedIdx (total).
| v | the Vec[A] pointer to read | |
| b | a BoundedIdx proven against (vec-len v) |
The element at the index (carrier :int).
(let [o (bidx-of? (vec-len v) 1)]
(if (some? o) (vec-get-checked v (bidx-unwrap o)) -1))
Since: R2
slice-get-checked
(slice-get-checked [s : int b : BoundedIdx] :)
index a Slice with a proven-in-range BoundedIdx (total).
| s | the Slice pointer to read | |
| b | a BoundedIdx proven against (slice-len s) |
The element at the index (carrier :int).
(let [o (bidx-of? (slice-len s) 0)]
(if (some? o) (slice-get-checked s (bidx-unwrap o)) -1))
Since: R2
Internal definitions
__ne-len-acc-- tail-recursive length accumulator over a cons list.