Legjobb pontszámok

Utasítások

Kezeld egy játékos csúcspontszám-listáját.

A feladatod, hogy elkészítsd a klasszikus Frogger játék csúcspontszám-komponensét. A Frogger minden idők egyik legkelendőbb és legaddiktívabb játéka, az árkádkorszak klasszikusa. A feladatod, hogy olyan metódusokat írj, amelyek visszaadják a lista legmagasabb pontszámát, a legutóbb hozzáadott pontszámot és a három legmagasabb pontszámot.

Ebben a feladatban listákkal és tömbökkel fogsz dolgozni. Mindkettő nagyon fontos adatszerkezet a Leanben.

Listák

A legtöbb funkcionális nyelvhez hasonlóan a listák alapvető adatszerkezetnek számítanak a Leanben.

A listának két konstruktora van: az egyik az üres lista ([]), a másik pedig egy olyan lista, amely egy elemet (a head-et) és egy másik listát (a tail-t) tartalmaz. A :: operátorral új elemeket fűzhetsz a lista elejére, így új lista jön létre:

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

A listák eredendően rekurzívak, ami alkalmassá teszi őket az induktív következtetésre. Emellett a strukturális megosztást is támogatják: új elemet fűzhetsz a lista elejére anélkül, hogy lemásolnád a meglévő listát:

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

A legtöbb listaművelet futásideje azonban arányos a lista hosszával, mivel a következő elem eléréséhez minden elemen végig kell haladni.

Tömbök

A tömb egy dinamikusan méretezett, összefüggő memóriaterület.

Sok műveletnél a tömbök sokkal hatékonyabbak lehetnek, mint a listák:

1. A tömbben bármelyik elemhez gyorsan hozzáférhetsz, méghozzá konstans időben.
2. A tömbök dinamikus tömbök mintájára készültek, amelyek a cache lokalitás miatt különösen hatékonyak a modern rendszereken.

A tömbök azonban nem igazán barátai a strukturális megosztásnak. Általában egy tömb frissítése funkcionális környezetben a teljes meglévő tömb lemásolását igényli.

A Lean referenciaszámlálással mérsékli ezt a hátrányt. Amíg egy tömbre soha nincs egynél több hivatkozás (azaz lineárisan használjuk), nem készül másolat, és a frissítések destruktívan hajthatók végre.

Az Array API számos függvénye destruktív frissítést végez, ha az adat nincs megosztva, például a set és a push.

Do-notáció

A Lean támogatja a do-notációt, egy beágyazott nyelvet, amellyel imperatív stílusban írhatsz kódot.

Egy do blokkon belül a mut kulcsszóval módosítható helyi változókat hozhatsz létre, amelyek értéke újra hozzárendelhető. Ha tömbökhöz hasonló adatszerkezetekkel használod, ez lehetővé teszi, hogy a Lean futásidejű rendszere a színfalak mögött helyben, destruktívan végezze el a frissítéseket, amikor az biztonságos.

A do-notációt csak monádon belül használhatod. Ha imperatív stílusú, mégis tiszta kódot szeretnél írni, amelynek nincsenek megfigyelhető mellékhatásai, kényelmes megoldás az Identity monád használata:

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