Puntajes altos

Instrucciones

Administra la lista de puntajes altos de un jugador.

Tu tarea es crear el componente de puntajes altos del clásico juego Frogger, uno de los juegos más vendidos y más adictivos de todos los tiempos, y un clásico de la era de los arcades. Tu tarea es escribir métodos que devuelvan el puntaje más alto de la lista, el último puntaje agregado y los tres puntajes más altos.

En este ejercicio vas a trabajar con listas y arrays. Se trata de dos estructuras de datos muy importantes en Lean.

Listas

Como en la mayoría de los lenguajes funcionales, las listas son una estructura de datos fundamental en Lean.

Una lista tiene dos constructores: uno para la lista vacía ([]) y otro para una lista que contiene un elemento (el head) y otra lista (el tail). Es posible anteponer elementos a una lista con ::, creando así una nueva lista:

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

Las listas son intrínsecamente recursivas, lo que las hace muy adecuadas para el razonamiento inductivo. También admiten el uso compartido de estructuras: puedes anteponer un nuevo elemento a una lista sin copiar la lista existente:

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

Sin embargo, la mayoría de las operaciones sobre listas tardan un tiempo proporcional a su longitud, ya que hay que recorrer cada elemento para llegar al siguiente.

Arrays

Un array es un bloque de memoria contiguo de tamaño dinámico.

Para muchas operaciones, los arrays pueden ser mucho más eficientes que las listas:

1. Acceder a cualquier elemento de un array es rápido y se ejecuta en tiempo constante.
2. Los arrays siguen el modelo de los arrays dinámicos, que suelen ser especialmente eficientes en los sistemas modernos gracias a la localidad de caché.

Sin embargo, los arrays no se llevan muy bien con el uso compartido de estructuras. En general, actualizar un array en un contexto funcional exige copiar todo el array existente.

Lean usa conteo de referencias para mitigar este inconveniente. Mientras nunca haya más de una referencia a un array (es decir, se use de forma lineal), no se hace ninguna copia y las actualizaciones se pueden realizar de forma destructiva.

Muchas funciones de la API de Array realizan actualizaciones destructivas cuando los datos no se comparten; por ejemplo, set y push.

Notación do

Lean admite la notación do, un lenguaje embebido para escribir código con un estilo imperativo.

Dentro de un bloque do, es posible declarar variables locales mutables, que se pueden reasignar, usando la palabra clave mut. Cuando se usa con estructuras de datos como los arrays, esto permite que el sistema de ejecución de Lean realice actualizaciones destructivas en el mismo lugar, siempre que sea seguro hacerlo.

La notación do solo se puede usar dentro de una mónada. Una forma cómoda de escribir código de estilo imperativo que siga siendo puro y no tenga efectos secundarios observables es usar la 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