أعلى النتائج

التعليمات

أدر قائمة أعلى النقاط لدى أحد اللاعبين.

مهمتك هي بناء مكوّن أعلى النقاط للعبة 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