Recordes

Instruções

Gerencie a lista de maiores pontuações de um jogador.

Sua tarefa é construir um component de pontuação do clássico Frogger, um dos jogos mais vendidos e mais viciantes de todos os tempos, e um clássico da era dos fliperamas. Você vai escrever métodos que retornem a maior pontuação da lista, a última pontuação adicionada e as três maiores pontuações.

Neste exercício, você vai trabalhar com listas e arrays. Ambas 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 adicionar 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 inerentemente recursivas, o que as torna muito adequadas ao raciocínio indutivo. Elas também dão suporte a compartilhamento estrutural: você pode adicionar 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 em listas leva um tempo proporcional ao comprimento delas, já que cada elemento precisa ser percorrido para se chegar ao próximo.

Arrays

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

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

1. Acessar qualquer elemento de um array é rápido e leva tempo constante.
2. Os arrays são modelados a partir de arrays dinâmicos, que costumam ser especialmente eficientes em sistemas modernos por causa da localidade de cache.

Os arrays, porém, não são muito amigáveis ao compartilhamento estrutural. Em geral, atualizar um array em um contexto funcional exige copiar todo o array existente.

Lean usa contagem de referências para amenizar essa desvantagem. Enquanto nunca houver mais de uma referência a um array (ou seja, se ele for usado linearmente), nenhuma cópia é feita e as atualizações podem ser feitas de forma destrutiva.

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

Notação do

Lean dá suporte à notação do, uma linguagem embutida para escrever código em estilo imperativo.

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

Essa notação só pode ser usada dentro de uma mônada. Uma forma prática de escrever código em estilo imperativo que continua puro e não tem efeitos colaterais 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