Punteggi migliori

Istruzioni

Gestisci l'array dei punteggi più alti di un giocatore.

Il tuo compito è costruire un componente per i punteggi più alti del classico gioco Frogger, uno dei giochi più venduti e più avvincenti di tutti i tempi, nonché un classico dell'epoca delle sale giochi. Il tuo compito è scrivere dei metodi che restituiscono il punteggio più alto dell'array, l'ultimo punteggio aggiunto e i tre punteggi più alti.

In questo esercizio, lavorerai con le liste e gli array. Entrambi sono strutture dati molto importanti in Lean.

Liste

Come nella maggior parte dei linguaggi funzionali, le liste sono una struttura dati fondamentale in Lean.

Una lista ha due costruttori: uno per la lista vuota ([]) e un altro per una lista che contiene un elemento (head) e un'altra lista (tail). È possibile anteporre elementi ad una lista usando ::, creando così una nuova lista:

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

Le liste sono intrinsecamente ricorsive, il che le rende adatte al ragionamento induttivo. Supportano anche la condivisione strutturale: puoi anteporre un nuovo elemento ad una lista senza copiare quella esistente:

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

Tuttavia, la maggior parte delle operazioni sulle liste richiede un tempo proporzionale alla loro lunghezza, dato che ogni elemento dev'essere attraversato per raggiungere il successivo.

Array

Un array è un blocco contiguo di memoria a dimensione dinamica.

Per molte operazioni, gli array possono essere molto più efficienti delle liste:

1. Accedere a un elemento qualsiasi di un array è veloce e avviene in tempo costante.
2. Gli array sono modellati sugli array dinamici, che tendono a essere particolarmente efficienti sui sistemi moderni grazie alla località della cache.

Gli array, però, non si prestano bene alla condivisione strutturale. In generale, aggiornare un array in un contesto funzionale richiede di copiare l'intero array esistente.

Lean usa il conteggio dei riferimenti per attenuare questo svantaggio. Finché non esiste mai più di un riferimento ad un array (cioè, viene usato linearmente), non viene fatta alcuna copia e gli aggiornamenti possono essere eseguiti in modo distruttivo.

Molte funzioni nell'API Array eseguono aggiornamenti distruttivi in caso di dati non condivisi, per esempio set e push.

Notazione do

Lean supporta la notazione do, un linguaggio incorporato per scrivere codice in stile imperativo.

All'interno di un blocco do, è possibile dichiarare variabili locali mutabili, che possono essere riassegnate, usando la parola chiave mut. Se usata con strutture dati come gli array, questa permette al sistema di runtime di Lean di eseguire aggiornamenti distruttivi sul posto dietro le quinte, ogni volta che è sicuro farlo.

La notazione do può essere usata solo all'interno di una monade. Un modo comodo per scrivere codice in stile imperativo che resta puro e non ha effetti collaterali osservabili è usare la monade Identity:

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