امتیازهای برتر

دستورالعمل‌ها

فهرست امتیازهای برتر یک بازیکن بازی را مدیریت کنید.

وظیفه‌ی شما این است که مؤلفه‌ی امتیازهای برترِ بازی کلاسیک 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