The Hive TourContents
ENPT
Slide 18 of 74

Bounds, proved at compile time

What proves an index
proc main(): void {
	v := ["a", "b", "c"]
	echo v[2]                          // a literal into a known length

	last := len(v) - 1
	if v bounds last {
		echo v[last]                   // the guard covers it
	}
	if v bounds last && v[last] == "c" {
		echo "and the rest of its own condition"
	}

	for i := 0; i < len(v); i++ {
		echo v[i]                      // the loop's own condition is the guard
	}

	if indexOf(v, "b") is Result.Ok(at) {
		echo v[at]                     // a position indexOf answered with
	}
}
Binding the row a moving index picks
func cell(t: Str[dyn][dyn], r: Int, c: Int): Str {
	// `if t bounds r { if t[r] bounds c { echo t[r][c] } }` is refused:
	// t[r] is a different row each time r moves, so it is bound first.
	if t bounds r {
		row := t[r]
		if row bounds c {
			return row[c]
		}
	}
	return ""
}

proc main(): void {
	Str[dyn][dyn] t = [["a", "b"], ["c", "d"]]
	echo cell(t, 1, 0)
}

Every index and slice is proved in range before the program runs, so none can fail when it does; one the compiler cannot prove is a compile error. What proves one:

  • A literal index into a vector whose length is known: v[2] on a Str[3].
  • A guard, if v bounds i { … }, which is i >= 0 && i < len(v). It covers the branch under it and the rest of its own && condition, so if v bounds i && v[i] > 0 is proved; it proves nothing past an ||.
  • A counting loop whose counter starts at zero or above and counts up while below len(v).
  • A position indexOf answered with — but only for the vector it searched.

What proves nothing: an index worked out on the spot, like v[len(v) - 1], which has to be bound to a name and guarded; an early return, since a guard proves only the branch it opens; and a cell of a row picked by a moving index, t[r][c], where the row has to be bound first — row := t[r] — and the cell guarded against it. A slice's two bounds are proved one at a time.

A proof lasts until something could change what it was about: assigning to the vector or the index, declaring either again or binding its name in a pattern, drop (the one builtin that shortens a vector), or handing the vector to a mut parameter. Inside a loop, what the body does counts against every turn.

← PrevNext →