Grep

說明

在檔案中搜尋符合搜尋字串的行，並回傳所有符合的行。

Unix 的grep指令會在檔案中搜尋符合正規表示式的行。你的任務是實作一個簡化的 grep 指令，支援搜尋固定字串。

grep 指令接受 3 個引數：

1. 要搜尋的字串。
2. 零個或多個用來調整指令行為的旗標。
3. 一個或多個要搜尋的檔案。

接著它會讀取指定檔案的內容（依照指定的順序），找出包含搜尋字串的行，最後依照找到的順序回傳這些行。在多個檔案中搜尋時，每個符合的行前面會加上檔名和一個冒號（':'）。

旗標

grep 指令支援下列旗標：

• -n 在輸出的每一行前面加上行號和一個冒號（':'），行號放在檔名之後（如果有檔名的話）。
• -l 只輸出至少包含一行符合內容的檔案名稱。
• -i 使用不分大小寫的比較來比對。
• -v 反轉程式，收集所有不符合的行。
• -x 只搜尋整行都與搜尋字串完全相符的行。

IO 流程

與其他練習不同，grep需要與「外部世界」互動：讀取檔案、處理系統錯誤，以及輸出到stdout。

在 Lean 中，與系統互動通常是在 IO monad 裡進行，它讓副作用能在受控的環境中發生，而不影響大多數其他函式的純狀態。

讀取引數

Lean 允許將檔案當作腳本呼叫，可以直接透過lean --run當成獨立腳本執行，也可以使用lake。

一個 Lean 專案只有一個進入點，也就是名為main的函式，它會接收一個List String，裡面帶有傳入的所有引數。

為了模擬將Grep.lean當成執行檔執行，這個練習會以同樣的方式傳入引數。

讀取檔案

Lean 提供了在IO.FS monad 中操作檔案的函式。

例如，可以使用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
    -/

---

出處

與 Nate Foster 的對話。