O Tour do HiveSumário
ENPT
Slide 18 de 74

Limites, provados em tempo de compilação

O que prova um índice
proc main(): void {
	v := ["a", "b", "c"]
	echo v[2]                          // um literal em um tamanho conhecido

	last := len(v) - 1
	if v bounds last {
		echo v[last]                   // a guarda cobre
	}
	if v bounds last && v[last] == "c" {
		echo "e o resto da própria condição"
	}

	for i := 0; i < len(v); i++ {
		echo v[i]                      // a condição do laço é a guarda
	}

	if indexOf(v, "b") is Result.Ok(at) {
		echo v[at]                     // uma posição que indexOf respondeu
	}
}
Vinculando a linha que um índice variável escolhe
func cell(t: Str[dyn][dyn], r: Int, c: Int): Str {
	// `if t bounds r { if t[r] bounds c { echo t[r][c] } }` é recusado:
	// t[r] é uma linha diferente a cada vez que r muda, então ela é vinculada antes.
	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)
}

Todo índice e toda fatia são provados dentro dos limites antes de o programa rodar, então nenhum pode falhar quando ele roda; um que o compilador não consegue provar é um erro de compilação. O que prova um:

  • Um índice literal em um vetor de tamanho conhecido: v[2] em um Str[3].
  • Uma guarda, if v bounds i { … }, que é i >= 0 && i < len(v). Ela cobre o ramo abaixo dela e o resto da sua própria condição com &&, então if v bounds i && v[i] > 0 fica provado; ela não prova nada depois de um ||.
  • Um laço de contagem cujo contador começa em zero ou acima e sobe enquanto for menor que len(v).
  • Uma posição que indexOf respondeu — mas só para o vetor que ele procurou.

O que não prova nada: um índice calculado na hora, como v[len(v) - 1], que precisa ser vinculado a um nome e guardado; um return antecipado, já que uma guarda prova só o ramo que abre; e uma célula de uma linha escolhida por um índice que muda, t[r][c], em que a linha precisa ser vinculada antes — row := t[r] — e a célula guardada contra ela. Os dois limites de uma fatia são provados um de cada vez.

Uma prova dura até algo poder mudar aquilo de que ela trata: atribuir ao vetor ou ao índice, declarar qualquer um de novo ou vincular o nome dele em um padrão, drop (o único builtin que encurta um vetor), ou passar o vetor a um parâmetro mut. Dentro de um laço, o que o corpo faz conta para toda volta.

← AnteriorPróximo →