A function that can suspend execution and, when called again later, resume where it left off, in the middle of the function body. See the coroutines note for more details.

A type that depends on another value. For example, a variable `n`

‘s type might be “the length of `s`

”, for some other slice-typed variable `s`

. Dependent types are *a* way to implement bounds checking, but they’re not the only way. Wuffs does not use them.

An extension of the type system, applied to functions. Wuffs has three effect categories: pure, impure and coroutine. Pure means that the function has no side effects - it does not change any observable state. The other two categories may have side effects, with coroutines also being able to suspend and resume.

Impure functions are marked with a `!`

at their definition and at call sites. Coroutines are similarly marked, with a `?`

. Pure functions have no mark.

A boolean expression (e.g. `x > y`

) that happens to be true at a given point in a program. See the facts note for more details.

A unit of time. One flick (frame-tick) is `1 / 705_600_000`

of a second.

Arithmetic on numerical ranges. See the interval arithmetic note for more details.

Arithmetic that wraps around at a certain modulus, such as `256`

for the `base.u8`

type. For example, if `x`

is a `base.u8`

with value `200`

, then `(x + 70)`

has value `270`

and would overflow, but `(x ~mod+ 70)`

has value `14`

.

A ranking of arithmetic operators so that an expression like `a + b * c`

is unambiguous (for the computer), equivalent to exactly one of `(a + b) * c`

or, more conventionally, `a + (b * c)`

. While good for brevity, Wuffs does not have operator precedence: the bare `a + b * c`

is an invalid Wuffs expression and the parentheses must be explicit. The ambiguity (for the human) can be a source of bugs in other security-concious file format parsers.

Some binary operators (`+`

, `*`

, `&`

, `|`

, `^`

, `and`

, `or`

) are also associative: `(a + b) + c`

and `a + (b + c)`

are equivalent, and can be written in Wuffs as `a + b + c`

.

A basic type further constrained to a subset of its natural range. For example, if `x`

has type `base.u8[0 ..= 99]`

then it is an unsigned 8-bit integer whose value must be less than `100`

. Without the refinement, `x`

could be as high as `255`

.

`base.u8[0 ..= 99]`

and `base.u32[0 ..= 99]`

are two different types. They can have different run-time representations.

Non-nullable pointer types can be thought of as a refinement of regular pointer types, where the refined range excludes the `nullptr`

value.

Arithmetic that stops at certain bounds, such as `0`

and `255`

for the `base.u8`

type. For example, if `x`

is a `base.u8`

with value `200`

, then `(x + 70)`

has value `270`

and would overflow, but `(x ~sat+ 70)`

has value `255`

.

The set of facts at a given point in a program.