Puntuaciones máximas

Instrucciones

Gestiona la lista de puntuaciones altas de un jugador.

Tu tarea es construir un componente de puntuación alta del clásico juego Frogger, uno de los juegos más vendidos y más adictivos de todos los tiempos, y todo un clásico de la era de los salones recreativos. Tu tarea es escribir métodos que devuelvan la puntuación más alta de la lista, la última puntuación añadida y las tres puntuaciones más altas.

En este ejercicio vas a trabajar con listas y arrays. Ambos son 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 lista nueva:

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 compartición estructural: puedes anteponer un elemento nuevo 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 contiguo de memoria 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 están inspirados en 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 la compartición estructural. En general, actualizar un array en un contexto funcional requiere copiar todo el array existente.

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

Muchas funciones de la API Array realizan actualizaciones destructivas cuando los datos no están compartidos; 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, con 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 in situ, 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 con 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