Melhores pontuações

Instruções

Gere a lista de pontuações altas de um jogador.

A tua tarefa é criar o component de pontuação alta do clássico jogo Frogger, um dos jogos mais vendidos e mais viciantes de todos os tempos e um clássico da era dos jogos de arcada. A tua tarefa é escrever métodos que devolvem a pontuação mais alta da lista, a última pontuação adicionada e as três pontuações mais altas.

Neste exercício, vais trabalhar com listas e arrays. Ambos são estruturas de dados muito importantes em Lean.

Listas

Como na maioria das linguagens funcionais, as listas são uma estrutura de dados fundamental em Lean.

Uma lista tem dois construtores: um para a lista vazia ([]) e outro para uma lista que contém um elemento (o head) e outra lista (o tail). É possível acrescentar elementos ao início de uma lista com ::, criando assim uma nova lista:

let list := x :: xs -- prepending x to xs creates a new list where x is the head and xs is the tail

As listas são intrinsecamente recursivas, o que as torna muito adequadas ao raciocínio indutivo. Também suportam partilha estrutural: podes acrescentar um novo elemento ao início de uma lista sem copiar a lista existente:

let list1 := [1, 2]
let list2 := 0 :: list1
-- now both list1 and list2 share [1, 2]

No entanto, a maioria das operações sobre listas leva um tempo proporcional ao seu comprimento, uma vez que é preciso percorrer cada elemento para chegar ao seguinte.

Arrays

Um array é um bloco de memória contíguo de tamanho dinâmico.

Para muitas operações, os arrays podem ser muito mais eficientes do que as listas:

1. Aceder a qualquer elemento de um array é rápido e corre em tempo constante.
2. Os arrays são modelados a partir de arrays dinâmicos, que tendem a ser particularmente eficientes nos sistemas modernos devido à localidade de cache.

Os arrays, no entanto, não se dão muito bem com a partilha estrutural. Em geral, atualizar um array num contexto funcional exige copiar todo o array existente.

Lean usa contagem de referências para mitigar esta desvantagem. Desde que nunca haja mais do que uma referência a um array (ou seja, que este seja usado de forma linear), não é feita nenhuma cópia e as atualizações podem ser feitas de forma destrutiva.

Muitas funções da API de Array fazem atualizações destrutivas quando os dados não são partilhados, por exemplo, set e push.

Notação do

Lean suporta a notação do, uma linguagem incorporada para escrever código num estilo imperativo.

Dentro de um bloco do, é possível declarar variáveis locais mutáveis, que podem ser reatribuídas, com a palavra-chave mut. Quando usada com estruturas de dados como os arrays, isto permite que o sistema de execução do Lean faça atualizações destrutivas no local, sempre que for seguro fazê-lo.

A notação do só pode ser usada dentro de uma mónada. Uma forma prática de escrever código de estilo imperativo que se mantém puro e não tem efeitos secundários observáveis é usar a mónada Identity:

def sumArray (array : Array Nat) := Id.run do
    let mut sum := 0
    for element in array do
        sum := sum + element
    return sum