Вступ
Ми влаштувалися на роботу до місцевої бібліотеки, де допомагаємо впорядковувати колекцію старих книжок. Студенти, які приходять до бібліотеки, часто шукають цитати, які памʼятають лише наполовину, щоб процитувати їх у своїх курсових роботах. Замість того щоб вручну читати кожну книжку від першої до останньої сторінки, ми вирішуємо створити невеликий інструмент, який буде сканувати їх, шукаючи ці уривки цитат.
Вказівки
Знайти у файлах рядки, що містять рядок пошуку, і повернути всі знайдені рядки.
Команда Unix grep шукає у файлах рядки, що відповідають регулярному виразу.
Наше завдання - реалізувати спрощену команду grep, яка підтримує пошук фіксованих рядків тексту (англ. string).
Команда grep приймає три аргументи:
- Рядок пошуку.
- Нуль або більше прапорців, які налаштовують поведінку команди.
- Один або більше файлів, у яких виконувати пошук.
Далі вона читає вміст указаних файлів (у вказаному порядку), знаходить рядки, що містять рядок пошуку, і нарешті повертає ці рядки в порядку, у якому їх було знайдено.
Під час пошуку в кількох файлах перед кожним знайденим рядком додається імʼя файлу та двокрапка (':').
Прапорці
Команда grep підтримує такі прапорці:
-
-n Додає номер рядка та двокрапку (':') перед кожним рядком у вихідних даних, розміщуючи номер після імені файлу (якщо воно є).
-
-l Виводить лише імена файлів, які містять принаймні один знайдений рядок.
-
-i Шукає з порівнянням без урахування регістру.
-
-v Інвертує роботу програми: збирає всі рядки, що не відповідають умові пошуку.
-
-x Шукає лише ті рядки, які повністю збігаються з рядком пошуку.
Процес IO
На відміну від інших вправ, grep потребує взаємодії із «зовнішнім світом»: читання файлів, обробки системних помилок і виведення в stdout.
У Lean взаємодія із системою зазвичай відбувається в монаді IO, яка дозволяє побічним ефектам виникати в ізольованому середовищі, не впливаючи на чистий стан більшості інших функцій.
Читання аргументів
Lean дозволяє викликати файл як скрипт: або безпосередньо як окремий скрипт через lean --run, або з використанням lake.
Проєкт Lean має одну точку входу, функцію з назвою main, яка приймає List String з усіма переданими їй аргументами.
Щоб змоделювати запуск Grep.lean як виконуваного файлу, у цій вправі аргументи передаються так само.
Читання файлів
Lean пропонує функції для роботи з файлами в монаді IO.FS.
Наприклад, IO.FS.readFile можна використати, щоб прочитати вміст файлу за заданим шляхом як String.
Запис вихідних даних
Замість повернення значення ця вправа вимагає, щоб результати записувалися до стандартного виводу або стандартного потоку помилок.
Для цього в Lean є функції.
Обробка системних помилок
На відміну від помилок у Except, винятки IO насправді є винятками часу виконання.
Щоб їх обробити, можна використати try/catch:
try
/-
code that may possibly raise an exception
-/
catch msg =>
/-
code that is executed only if an exception was thrown
-/
