Meilleurs scores

Instructions

Gère le tableau des meilleurs scores d'un joueur.

Ta tâche consiste à construire le composant de gestion des meilleurs scores du classique Frogger, l'un des jeux les plus vendus et les plus addictifs de tous les temps, et un classique de l'ère des salles d'arcade. Ta tâche consiste à écrire des méthodes qui renvoient le meilleur score du tableau, le dernier score ajouté et les trois meilleurs scores.

Dans cet exercice, tu vas travailler avec des listes et des tableaux. Ce sont deux structures de données très importantes en Lean.

Listes

Comme dans la plupart des langages fonctionnels, les listes sont une structure de données fondamentale en Lean.

Une liste prend deux constructeurs : un pour la liste vide ([]) et un autre pour une liste contenant un élément (le head) et une autre liste (le tail). Il est possible d'ajouter des éléments en tête d'une liste avec ::, ce qui crée une nouvelle liste :

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

Les listes sont intrinsèquement récursives, ce qui les rend particulièrement adaptées au raisonnement par induction. Elles autorisent aussi le partage structurel, ce qui permet d'ajouter un nouvel élément en tête d'une liste sans copier la liste existante :

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

Cependant, la plupart des opérations sur les listes prennent un temps proportionnel à leur longueur, puisqu'il faut parcourir chaque élément pour atteindre le suivant.

Tableaux

Un tableau est un bloc de mémoire contigu de taille dynamique.

Pour de nombreuses opérations, les tableaux peuvent être bien plus efficaces que les listes :

1. Accéder à n'importe quel élément d'un tableau est rapide et se fait en temps constant.
2. Les tableaux sont inspirés des tableaux dynamiques, qui ont tendance à être particulièrement efficaces sur les systèmes modernes grâce à la localité de cache.

Les tableaux, en revanche, se prêtent mal au partage structurel. En général, mettre à jour un tableau dans un contexte fonctionnel oblige à copier tout le tableau existant.

Lean utilise le comptage de références pour atténuer cet inconvénient. Tant qu'il n'existe jamais plus d'une référence vers un tableau (autrement dit, tant qu'il est utilisé linéairement), aucune copie n'est faite et les mises à jour peuvent être effectuées de façon destructive.

De nombreuses fonctions de l'API Array effectuent des mises à jour destructives lorsque les données ne sont pas partagées, par exemple set et push.

Notation do

Lean prend en charge la notation do, un langage embarqué pour écrire du code dans un style impératif.

À l'intérieur d'un bloc do, il est possible de déclarer des variables locales mutables, que l'on peut réaffecter, à l'aide du mot-clé mut. Lorsqu'on l'utilise avec des structures de données comme les tableaux, cela permet au système d'exécution de Lean d'effectuer des mises à jour destructives sur place, en coulisses, dès que c'est sans danger.

La notation do ne peut s'utiliser qu'à l'intérieur d'une monade. Une façon pratique d'écrire du code de style impératif qui reste pur et sans effets de bord observables consiste à utiliser 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