Рекордні результати

Вказівки

Керуйте масивом рекордів гравця.

Ваше завдання - створити компонент для підрахунку рекордів класичної гри Frogger, однієї з найбільш продаваних і найбільш затягуючих ігор усіх часів та класики ери аркадних автоматів. Ваше завдання - написати методи, які повертають найвищий рекорд із масиву, останній доданий рекорд і три найвищі рекорди.

У цій вправі ми будемо працювати зі списками та масивами. Обидва є дуже важливими структурами даних у 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 використовує підрахунок посилань, щоб помʼякшити цю ваду. Поки на масив існує не більше ніж одне посилання (тобто він використовується лінійно), копіювання не відбувається, і оновлення можна виконувати деструктивно.

Багато функцій у Array API виконують деструктивні оновлення, коли дані не є спільними, наприклад set і push.

Do-нотація

Lean підтримує do-нотацію, вбудовану мову для написання коду в імперативному стилі.

Усередині блоку do за допомогою ключового слова mut можна оголошувати локальні змінні, яким можна повторно присвоювати значення. Коли ми використовуємо його з такими структурами даних, як масиви, це дозволяє системі виконання Lean виконувати деструктивні оновлення на місці, коли це безпечно.

Do-нотацію можна використовувати лише всередині монади. Зручний спосіб писати код в імперативному стилі, який залишається чистим і не має спостережуваних побічних ефектів, - це скористатися монадою Identity:

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