Grep

说明

在文件中搜索与搜索字符串匹配的行，并返回所有匹配的行。

Unix 的grep命令会在文件中搜索匹配正则表达式的行。你的任务是实现一个简化版的grep命令，它支持搜索固定字符串。

grep命令接受三个参数：

1. 要搜索的字符串。
2. 零个或多个用于自定义命令行为的标志。
3. 一个或多个要搜索的文件。

然后它会按指定的顺序读取这些文件的内容，找出包含搜索字符串的行，最后按找到它们的顺序返回这些行。在多个文件中搜索时，每条匹配的行前面都会加上文件名和一个冒号（':'）。

标志

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
    -/

---

来源

与 Nate Foster 的一次对话。