tur/sized
static sizes and size arithmetic for memory layout verification.
Foundational support for SZ0/SZ1 phases. Enables type-safe array shape annotations.
Since: Phase SZ0
StaticInt
(defdata StaticInt (SInt int))
a compile-time integer annotation.
Carries an integer value intended for use as a type-level literal. Constructed with SInt.
Since: Phase SZ0
static-int
(static-int [n :int] :StaticInt)
construct a StaticInt from a literal integer.
| n | the integer value |
A (StaticInt) wrapping n.
(static-int 10) ; => SInt(10)
Since: Phase SZ0
static-int-val
(static-int-val [si :StaticInt] :int)
extract the integer value from a StaticInt.
| si | a (StaticInt) value |
The wrapped integer.
(static-int-val (static-int 10)) ; => 10
Since: Phase SZ0
static-int-add
(static-int-add [a :StaticInt b :StaticInt] :StaticInt)
add two StaticInt values.
| a | first (StaticInt) | |
| b | second (StaticInt) |
A (StaticInt) representing a + b.
(static-int-val (static-int-add (static-int 3) (static-int 4))) ; => 7
Since: Phase SZ0
static-int-mul
(static-int-mul [a :StaticInt b :StaticInt] :StaticInt)
multiply two StaticInt values.
| a | first (StaticInt) | |
| b | second (StaticInt) |
A (StaticInt) representing a * b.
(static-int-val (static-int-mul (static-int 3) (static-int 4))) ; => 12
Since: Phase SZ0
Size
(defdata Size (Static int) (Add Size Size) (Mul Size Size))
arithmetic expressions over compile-time sizes.
Constructors:
Static n -- a literal size from an integer Add s1 s2 -- sum of two sizes Mul s1 s2 -- product of two sizes
Evaluate a Size expression to a runtime integer with size-eval.
Since: Phase SZ0
size-static
(size-static [n :int] :Size)
create a literal Size from an integer.
| n | the integer literal |
A (Size) representing the literal value n.
(size-eval (size-static 4)) ; => 4
Since: Phase SZ0
size-add
(size-add [s1 :Size s2 :Size] :Size)
create a Size representing the sum of two sizes.
| s1 | the first (Size) | |
| s2 | the second (Size) |
A (Size) representing s1 + s2.
(size-eval (size-add (size-static 3) (size-static 4))) ; => 7
Since: Phase SZ0
size-mul
(size-mul [s1 :Size s2 :Size] :Size)
create a Size representing the product of two sizes.
| s1 | the first (Size) | |
| s2 | the second (Size) |
A (Size) representing s1 * s2.
(size-eval (size-mul (size-static 3) (size-static 4))) ; => 12
Since: Phase SZ0
size-eval
(size-eval [s :Size] :int)
evaluate a Size expression to a runtime integer.
| s | the (Size) expression to evaluate |
The integer value of the size expression.
(size-eval (size-add (size-static 2) (size-mul (size-static 3) (size-static 4)))) ; => 14
Since: Phase SZ0
SizedVec
(defdata SizedVec [n a] (SVNil : (SizedVec Size int)) (SVCons int (SizedVec Size int) : (SizedVec Size int)))
a phantom-typed singly-linked list annotated with a size.
The type parameters n and a are phantom: n documents the intended size and a documents the element type, but neither is enforced at the value level in this phase. True enforcement requires dependent types.
Constructors:
SVNil -- the empty SizedVec SVCons x xs -- x prepended to xs
Since: Phase SZ0
sized-vec-nil
(sized-vec-nil :SizedVec)
construct an empty SizedVec.
An empty (SizedVec Size int).
(sized-vec-nil) ; => SVNil
Since: Phase SZ0
sized-vec-cons
(sized-vec-cons [x :int xs :SizedVec] :SizedVec)
prepend an integer element to a SizedVec.
| x | the integer element to prepend | |
| xs | the existing (SizedVec Size int) |
A new (SizedVec Size int) with x at the front.
(sized-vec-cons 1 (sized-vec-nil)) ; => SVCons(1, SVNil)
Since: Phase SZ0
sized-vec-len
(sized-vec-len [v :SizedVec] :int)
compute the runtime length of a SizedVec.
| v | the (SizedVec Size int) to measure |
The number of elements in v as an int.
(sized-vec-len (sized-vec-cons 1 (sized-vec-cons 2 (sized-vec-nil)))) ; => 2
Since: Phase SZ0
sized-vec-head-or
(sized-vec-head-or [dflt :int v :SizedVec] :int)
return the first element, or dflt if empty.
| dflt | value returned when v is empty | |
| v | the (SizedVec Size int) to inspect |
The first element of v, or dflt if v is empty.
(sized-vec-head-or 99 (sized-vec-nil)) ; => 99 (sized-vec-head-or 99 (sized-vec-cons 7 (sized-vec-nil))) ; => 7
Since: Phase SZ0
sized-vec-tail
(sized-vec-tail [v :SizedVec] :SizedVec)
return all elements after the first.
| v | the (SizedVec Size int) to take the tail of |
The tail (SizedVec Size int); SVNil if v is empty.
(sized-vec-len (sized-vec-tail (sized-vec-cons 1 (sized-vec-cons 2 (sized-vec-nil))))) ; => 1
Since: Phase SZ0
sized-vec-sum
(sized-vec-sum [v :SizedVec] :int)
sum all integer elements of a SizedVec.
| v | the (SizedVec Size int) to sum |
The integer sum of all elements; 0 for empty.
(sized-vec-sum (sized-vec-cons 1 (sized-vec-cons 2 (sized-vec-cons 3 (sized-vec-nil))))) ; => 6
Since: Phase SZ0
sized-vec-size
(sized-vec-size [v :SizedVec] :Size)
compute a Size expression for the runtime length.
| v | the (SizedVec Size int) to measure |
A (Static n) where n is the runtime length of v.
(size-eval (sized-vec-size (sized-vec-cons 1 (sized-vec-cons 2 (sized-vec-nil))))) ; => 2
Since: Phase SZ0
size-eq?
(size-eq? [s1 :Size s2 :Size] :bool)
check whether two Size expressions evaluate to equal integers.
| s1 | the first (Size) expression | |
| s2 | the second (Size) expression |
true if both evaluate to the same integer, false otherwise.
(size-eq? (size-static 4) (size-add (size-static 1) (size-static 3))) ; => true
Since: Phase SZ1
size-le?
(size-le? [s1 :Size s2 :Size] :bool)
check whether s1 evaluates to <= s2.
| s1 | the first (Size) expression | |
| s2 | the second (Size) expression |
true if s1 <= s2 as integers.
(size-le? (size-static 3) (size-static 4)) ; => true
Since: Phase SZ1
size-lt?
(size-lt? [s1 :Size s2 :Size] :bool)
check whether s1 evaluates to < s2.
| s1 | the first (Size) expression | |
| s2 | the second (Size) expression |
true if s1 < s2 as integers.
(size-lt? (size-static 3) (size-static 4)) ; => true
Since: Phase SZ1
size-ge?
(size-ge? [s1 :Size s2 :Size] :bool)
check whether s1 evaluates to >= s2.
| s1 | the first (Size) expression | |
| s2 | the second (Size) expression |
true if s1 >= s2 as integers.
(size-ge? (size-static 5) (size-static 5)) ; => true
Since: Phase SZ1
size-gt?
(size-gt? [s1 :Size s2 :Size] :bool)
check whether s1 evaluates to > s2.
| s1 | the first (Size) expression | |
| s2 | the second (Size) expression |
true if s1 > s2 as integers.
(size-gt? (size-static 5) (size-static 4)) ; => true
Since: Phase SZ1
size-normalize
(size-normalize [s :Size] :Size)
reduce a Size expression to its canonical (Static n) form.
| s | the (Size) expression to normalize |
A (Static n) where n is the evaluated integer of s.
(size-eval (size-normalize (size-add (size-static 2) (size-mul (size-static 3) (size-static 4))))) ; => 14
Since: Phase SZ1
size-simplify
(size-simplify [s :Size] :Size)
apply algebraic reduction rules to a Size expression.
Applies identity and zero laws without evaluating the full expression:
Add (Static 0) s = s (left identity) Add s (Static 0) = s (right identity) Mul (Static 0) _ = Static 0 (left zero) Mul _ (Static 0) = Static 0 (right zero) Mul (Static 1) s = s (left identity) Mul s (Static 1) = s (right identity)
All other cases are folded to (Static n) via evaluation.
| s | the (Size) expression to simplify |
A simplified (Size) expression.
(size-eval (size-simplify (size-add (size-static 0) (size-static 7)))) ; => 7 (size-eval (size-simplify (size-mul (size-static 1) (size-static 9)))) ; => 9
Since: Phase SZ1
size-assert-eq!
(size-assert-eq! [s1 :Size s2 :Size] :nil)
panic at runtime if two Size expressions evaluate differently.
Use this to enforce size compatibility at the call site; analogous to sized-type subtyping: a value with size s1 is compatible with an expected size s2 only when size-assert-eq! passes.
| s1 | the actual (Size) (e.g., from sized-vec-size) | |
| s2 | the expected (Size) |
nil on success; panics with "sized type mismatch" on failure.
(size-assert-eq! (size-static 4) (size-add (size-static 2) (size-static 2)))
Since: Phase SZ1
size-assert-le!
(size-assert-le! [s1 :Size s2 :Size] :nil)
panic at runtime if s1 evaluates to greater than s2.
Checks that s1 is within the upper bound set by s2. Useful for verifying that a sized value fits into a buffer or allocation of size s2.
| s1 | the actual (Size) to check | |
| s2 | the upper bound (Size) |
nil on success; panics with "sized type mismatch" on failure.
(size-assert-le! (size-static 3) (size-static 10))
Since: Phase SZ1
size-compat?
(size-compat? [s1 :Size s2 :Size] :bool)
check whether two Size expressions are compatible (equal).
In the current phantom-type encoding, two sizes are compatible when they evaluate to the same integer. This is the runtime analog of the subtyping rule: (SizedVec n int) is compatible with (SizedVec m int) iff n = m.
| s1 | the first (Size) | |
| s2 | the second (Size) |
true if both sizes evaluate to the same integer.
(size-compat? (size-static 4) (size-add (size-static 2) (size-static 2))) ; => true
Since: Phase SZ1
sized-vec-of-1
(sized-vec-of-1 [a :int] :SizedVec)
construct a 1-element SizedVec, size inferred as 1.
| a | the element |
A (SizedVec Size int) containing [a].
(sized-vec-len (sized-vec-of-1 42)) ; => 1
Since: Phase SZ1
sized-vec-of-2
(sized-vec-of-2 [a :int b :int] :SizedVec)
construct a 2-element SizedVec, size inferred as 2.
| a | the first element | |
| b | the second element |
A (SizedVec Size int) containing [a, b].
(sized-vec-len (sized-vec-of-2 1 2)) ; => 2
Since: Phase SZ1
sized-vec-of-3
(sized-vec-of-3 [a :int b :int c :int] :SizedVec)
construct a 3-element SizedVec, size inferred as 3.
| a | the first element | |
| b | the second element | |
| c | the third element |
A (SizedVec Size int) containing [a, b, c].
(sized-vec-len (sized-vec-of-3 1 2 3)) ; => 3
Since: Phase SZ1
sized-vec-of-4
(sized-vec-of-4 [a :int b :int c :int d :int] :SizedVec)
construct a 4-element SizedVec, size inferred as 4.
| a | the first element | |
| b | the second element | |
| c | the third element | |
| d | the fourth element |
A (SizedVec Size int) containing [a, b, c, d].
(sized-vec-len (sized-vec-of-4 1 2 3 4)) ; => 4
Since: Phase SZ1
sized-vec-from-list
(sized-vec-from-list [lst])
convert a cons list to a SizedVec, inferring the size at runtime.
Traverses the cons list and collects elements in order into a SizedVec. The resulting SizedVec's length is the length of the input list. Assumes the cons list uses the standard { int64_t value; int64_t next; } layout (as produced by stdlib/list.tur or any inline cons implementation).
| lst | a cons list (0 for empty, or pointer to cons cell) |
A (SizedVec Size int) with the same elements in the same order.
(sized-vec-len (sized-vec-from-list (cons 1 (cons 2 (cons 3 (nil-value)))))) ; => 3
Since: Phase SZ1