Υψηλές Βαθμολογίες

Οδηγίες

Διαχειρίσου τη λίστα υψηλών σκορ ενός παίκτη.

Η αποστολή σου είναι να φτιάξεις ένα component υψηλών σκορ για το κλασικό παιχνίδι Frogger, ένα από τα παιχνίδια με τις περισσότερες πωλήσεις και τα πιο εθιστικά όλων των εποχών, καθώς και ένα κλασικό της εποχής των arcade. Η αποστολή σου είναι να γράψεις μεθόδους που επιστρέφουν το υψηλότερο σκορ από τη λίστα, το τελευταίο σκορ που προστέθηκε και τα τρία υψηλότερα σκορ.

Σε αυτή την άσκηση, θα δουλέψεις με λίστες και πίνακες. Και τα δύο είναι πολύ σημαντικές δομές δεδομένων στο Lean.

Λίστες

Όπως στις περισσότερες συναρτησιακές γλώσσες, οι λίστες είναι μια θεμελιώδης δομή δεδομένων στο Lean.

Μια λίστα έχει δύο κατασκευαστές: έναν για την κενή λίστα ([]) και έναν για μια λίστα που περιέχει ένα στοιχείο (το head) και μια άλλη λίστα (το tail). Μπορείς να προσθέσεις στοιχεία στην αρχή μιας λίστας χρησιμοποιώντας το ::, δημιουργώντας έτσι μια νέα λίστα:

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

Οι λίστες είναι εγγενώς αναδρομικές, κάτι που τις κάνει κατάλληλες για επαγωγικό συλλογισμό. Υποστηρίζουν επίσης δομικό διαμοιρασμό: μπορείς να προσθέσεις ένα νέο στοιχείο στην αρχή μιας λίστας χωρίς να αντιγράψεις την υπάρχουσα λίστα:

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

Ωστόσο, οι περισσότερες πράξεις σε λίστες παίρνουν χρόνο ανάλογο με το μήκος τους, αφού πρέπει να διασχίσεις κάθε στοιχείο για να φτάσεις στο επόμενο.

Πίνακες

Ένας πίνακας είναι ένα συνεχές μπλοκ μνήμης δυναμικού μεγέθους.

Για πολλές πράξεις, οι πίνακες μπορούν να είναι πολύ πιο αποδοτικοί από τις λίστες:

1. Η πρόσβαση σε οποιοδήποτε στοιχείο ενός πίνακα είναι γρήγορη και γίνεται σε σταθερό χρόνο.
2. Οι πίνακες είναι σχεδιασμένοι κατά το πρότυπο των δυναμικών πινάκων, οι οποίοι τείνουν να είναι ιδιαίτερα αποδοτικοί στα σύγχρονα συστήματα χάρη στην τοπικότητα της κρυφής μνήμης.

Οι πίνακες, ωστόσο, δεν τα πάνε και πολύ καλά με τον δομικό διαμοιρασμό. Γενικά, η ενημέρωση ενός πίνακα σε συναρτησιακό περιβάλλον απαιτεί την αντιγραφή ολόκληρου του υπάρχοντος πίνακα.

Το Lean χρησιμοποιεί μέτρηση αναφορών για να μετριάσει αυτό το μειονέκτημα. Όσο δεν υπάρχει ποτέ περισσότερη από μία αναφορά σε έναν πίνακα (δηλαδή, χρησιμοποιείται γραμμικά), δε γίνεται κανένα αντίγραφο και οι ενημερώσεις μπορούν να γίνουν καταστροφικά.

Πολλές συναρτήσεις στο API του Array κάνουν καταστροφικές ενημερώσεις όταν τα δεδομένα δεν είναι διαμοιρασμένα, για παράδειγμα οι set και push.

Σημειογραφία do

Το Lean υποστηρίζει τη σημειογραφία do, μια ενσωματωμένη γλώσσα για να γράφεις κώδικα με προστακτικό στυλ.

Μέσα σε ένα μπλοκ do, μπορείς να δηλώσεις τοπικές μεταβλητές που μπορούν να τροποποιηθούν και να τους αναθέσεις ξανά τιμή, χρησιμοποιώντας τη λέξη-κλειδί mut. Όταν χρησιμοποιείται με δομές δεδομένων όπως οι πίνακες, αυτό επιτρέπει στο σύστημα χρόνου εκτέλεσης του Lean να κάνει καταστροφικές ενημερώσεις επί τόπου στο παρασκήνιο, όποτε είναι ασφαλές να το κάνει.

Η σημειογραφία do μπορεί να χρησιμοποιηθεί μόνο μέσα σε μια μονάδα. Ένας βολικός τρόπος για να γράψεις κώδικα προστακτικού στυλ που παραμένει καθαρός και δεν έχει παρατηρήσιμες παρενέργειες είναι να χρησιμοποιήσεις τη μονάδα ταυτότητας:

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