Add grep (#51)

Author: oxe-i

config.json

@@ -368,6 +368,14 @@
         "practices": [],
         "prerequisites": [],
         "difficulty": 8
+      },
+      {
+        "slug": "grep",
+        "name": "Grep",
+        "uuid": "f5f84a44-4e65-4598-811a-31766f68567c",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 8
       }
     ]
   },

exercises/practice/grep/.docs/instructions.append.md

@@ -0,0 +1,44 @@
+# Instructions append
+
+## IO process
+
+Unlike other exercises, `grep` requires interacting with the "external world": reading files, handling system errors and printing to `stdout`.
+
+In Lean, interacting with the system is usually done in the [IO][io] monad, which allows for side effects to occur in a contained environment without affecting the pure state of most other functions.
+
+## Reading arguments
+
+Lean allows for a file to be called as a script, either directly as a standalone script via `lean --run` or with the use of `lake`.
+
+A lean project has one point of entry, a function called `main`, that takes a `List String` with all arguments passed to it.
+In order to simulate running `Grep.lean` as an executable, arguments are passed in the same way in this exercise.
+
+## Reading files
+
+Lean offers [functions][files] to manipulate files in the `IO.FS` monad.
+For example, `IO.FS.readFile` may be used to read the contents of a file in a given path, as a `String`.
+
+## Writing output
+
+Instead of returning a value, this exercise requires results are written to standard output or standard error.
+There are [functions][console] in Lean for this purpose.
+
+## Handling system errors
+
+Unlike errors in `Except`, `IO` exceptions are actually runtime exceptions.
+You may use `try`/`catch` to handle them:
+
+```
+try
+    /- 
+        code that may possibly raise an exception 
+    -/
+catch msg =>
+    /-
+        code that is executed only if an exception was thrown
+    -/
+```
+
+[io]: https://lean-lang.org/doc/reference/latest/IO/#io
+[files]: https://lean-lang.org/doc/reference/latest/IO/Files___-File-Handles___-and-Streams/#The-Lean-Language-Reference--IO--Files___-File-Handles___-and-Streams
+[console]: https://lean-lang.org/doc/reference/latest/IO/Console-Output/#The-Lean-Language-Reference--IO--Console-Output

exercises/practice/grep/.docs/instructions.md

@@ -0,0 +1,27 @@
+# Instructions
+
+Search files for lines matching a search string and return all matching lines.
+
+The Unix [`grep`][grep] command searches files for lines that match a regular expression.
+Your task is to implement a simplified `grep` command, which supports searching for fixed strings.
+
+The `grep` command takes three arguments:
+
+1. The string to search for.
+2. Zero or more flags for customizing the command's behavior.
+3. One or more files to search in.
+
+It then reads the contents of the specified files (in the order specified), finds the lines that contain the search string, and finally returns those lines in the order in which they were found.
+When searching in multiple files, each matching line is prepended by the file name and a colon (':').
+
+## Flags
+
+The `grep` command supports the following flags:
+
+- `-n` Prepend the line number and a colon (':') to each line in the output, placing the number after the filename (if present).
+- `-l` Output only the names of the files that contain at least one matching line.
+- `-i` Match using a case-insensitive comparison.
+- `-v` Invert the program -- collect all lines that fail to match.
+- `-x` Search only for lines where the search string matches the entire line.
+
+[grep]: https://pubs.opengroup.org/onlinepubs/9699919799/utilities/grep.html

exercises/practice/grep/.meta/Example.lean

@@ -0,0 +1,93 @@
+import Std
+
+namespace Grep
+
+def aggregateResults (results : List String) (prepend : String := "") : String :=
+  results.foldl (fun acc x => (prepend ++ x ++ "\n" ++ acc).trim) ""
+
+def processFile
+  (check : String -> Bool)
+  (getResult : Nat -> String -> String -> String)
+  (file : String) : IO (Except String (List String)) := do
+    try
+      let fileContent ← IO.FS.readFile file
+      let mut results := []
+      let lines := fileContent.splitOn "\n" |> (·.toArray)
+      for idx in [:lines.size] do
+        let line := lines[idx]!
+        if check line then
+          results := (getResult (idx + 1) line file) :: results
+      return (.ok results)
+    catch e =>
+      return (.error e.toString)
+
+def processGrep
+  (pattern : String)
+  (flags : List String)
+  (files : List String) : IO Unit := do
+    let flagsSet := Std.HashSet.ofList flags
+    let adjustedPattern :=
+      if flagsSet.contains "-i" then
+        pattern.toLower
+      else
+        pattern
+    let formatLine :=
+      if flagsSet.contains "-i" then
+        fun line => String.toLower line
+      else
+        fun line => line
+    let getResult :=
+      if flagsSet.contains "-n" then
+        fun (idx : Nat) (line : String) _ => s!"{idx}:{line}"
+      else
+        fun _ line _ => line
+    let compare :=
+      if flagsSet.contains "-x" then
+        fun (line : String) => s!"{formatLine line}" == adjustedPattern
+      else
+        fun (line : String) => formatLine line |> (·.toSlice.contains adjustedPattern)
+    let check :=
+      if flagsSet.contains "-v" then
+        fun line => !(compare line)
+      else
+        compare
+    match files with
+    | [] => return
+    | file :: [] =>
+      let maybeResults <- processFile check getResult file
+      match maybeResults with
+      | .error _ =>
+        IO.eprintln "File not found"
+      | .ok results =>
+        let validResults := results.filter (·!="")
+        if validResults.isEmpty then
+          return
+        else if flagsSet.contains "-l" then
+          IO.println file
+        else
+          IO.println (aggregateResults validResults)
+    | _ =>
+      for file in files do
+        let maybeResults <- processFile check getResult file
+        match maybeResults with
+        | .error _ =>
+          IO.eprintln "File not found"
+        | .ok results =>
+          let validResults := results.filter (·!="")
+          if validResults.isEmpty then
+            continue
+          else if flagsSet.contains "-l" then
+            IO.println file
+          else
+            IO.println (aggregateResults validResults s!"{file}:")
+
+def grep (args : List String) : IO Unit := do
+  match args with
+  | [] => IO.eprintln "Called without arguments"
+  | _ :: [] => IO.eprintln "Called without a file name"
+  | pattern :: xs =>
+    let flags := xs.takeWhile (fun flag => flag.startsWith "-")
+    let files := xs.dropWhile (fun flag => flag.startsWith "-")
+    processGrep pattern flags files
+
+end Grep

exercises/practice/grep/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "Grep.lean"
+    ],
+    "test": [
+      "GrepTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Search a file for lines matching a regular expression pattern. Return the line number and contents of each matching line.",
+  "source": "Conversation with Nate Foster.",
+  "source_url": "https://www.cs.cornell.edu/Courses/cs3110/2014sp/hw/0/ps0.pdf"
+}

exercises/practice/grep/.meta/extra.json

@@ -0,0 +1,38 @@
+[
+  {
+    "description": "Test error -> Called without arguments",
+    "property": "grep",
+    "input": {
+    "pattern": "",
+    "flags": [],
+    "files": []
+    },
+    "expected": {
+      "error": "Called without arguments"
+    }
+  },
+  {
+    "description": "Test error -> Called without a file",
+    "property": "grep",
+    "input": {
+    "pattern": "who",
+    "flags": [],
+    "files": []
+    },
+    "expected": {
+      "error": "Called without a file name"
+    }
+  },
+  {
+    "description": "Test error -> File not found",
+    "property": "grep",
+    "input": {
+    "pattern": "Agamemnon",
+    "flags": [],
+    "files": ["odyssey.txt"]
+    },
+    "expected": {
+      "error": "File not found"
+    }
+  }
+]

exercises/practice/grep/.meta/tests.toml

@@ -0,0 +1,85 @@
+# This is an auto-generated file.
+#
+# Regenerating this file via `configlet sync` will:
+# - Recreate every `description` key/value pair
+# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
+# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
+# - Preserve any other key/value pair
+#
+# As user-added comments (using the # character) will be removed when this file
+# is regenerated, comments can be added via a `comment` key.
+
+[9049fdfd-53a7-4480-a390-375203837d09]
+description = "Test grepping a single file -> One file, one match, no flags"
+
+[76519cce-98e3-46cd-b287-aac31b1d77d6]
+description = "Test grepping a single file -> One file, one match, print line numbers flag"
+
+[af0b6d3c-e0e8-475e-a112-c0fc10a1eb30]
+description = "Test grepping a single file -> One file, one match, case-insensitive flag"
+
+[ff7af839-d1b8-4856-a53e-99283579b672]
+description = "Test grepping a single file -> One file, one match, print file names flag"
+
+[8625238a-720c-4a16-81f2-924ec8e222cb]
+description = "Test grepping a single file -> One file, one match, match entire lines flag"
+
+[2a6266b3-a60f-475c-a5f5-f5008a717d3e]
+description = "Test grepping a single file -> One file, one match, multiple flags"
+
+[842222da-32e8-4646-89df-0d38220f77a1]
+description = "Test grepping a single file -> One file, several matches, no flags"
+
+[4d84f45f-a1d8-4c2e-a00e-0b292233828c]
+description = "Test grepping a single file -> One file, several matches, print line numbers flag"
+
+[0a483b66-315b-45f5-bc85-3ce353a22539]
+description = "Test grepping a single file -> One file, several matches, match entire lines flag"
+
+[3d2ca86a-edd7-494c-8938-8eeed1c61cfa]
+description = "Test grepping a single file -> One file, several matches, case-insensitive flag"
+
+[1f52001f-f224-4521-9456-11120cad4432]
+description = "Test grepping a single file -> One file, several matches, inverted flag"
+
+[7a6ede7f-7dd5-4364-8bf8-0697c53a09fe]
+description = "Test grepping a single file -> One file, no matches, various flags"
+
+[3d3dfc23-8f2a-4e34-abd6-7b7d140291dc]
+description = "Test grepping a single file -> One file, one match, file flag takes precedence over line flag"
+
+[87b21b24-b788-4d6e-a68b-7afe9ca141fe]
+description = "Test grepping a single file -> One file, several matches, inverted and match entire lines flags"
+
+[ba496a23-6149-41c6-a027-28064ed533e5]
+description = "Test grepping multiples files at once -> Multiple files, one match, no flags"
+
+[4539bd36-6daa-4bc3-8e45-051f69f5aa95]
+description = "Test grepping multiples files at once -> Multiple files, several matches, no flags"
+
+[9fb4cc67-78e2-4761-8e6b-a4b57aba1938]
+description = "Test grepping multiples files at once -> Multiple files, several matches, print line numbers flag"
+
+[aeee1ef3-93c7-4cd5-af10-876f8c9ccc73]
+description = "Test grepping multiples files at once -> Multiple files, one match, print file names flag"
+
+[d69f3606-7d15-4ddf-89ae-01df198e6b6c]
+description = "Test grepping multiples files at once -> Multiple files, several matches, case-insensitive flag"
+
+[82ef739d-6701-4086-b911-007d1a3deb21]
+description = "Test grepping multiples files at once -> Multiple files, several matches, inverted flag"
+
+[77b2eb07-2921-4ea0-8971-7636b44f5d29]
+description = "Test grepping multiples files at once -> Multiple files, one match, match entire lines flag"
+
+[e53a2842-55bb-4078-9bb5-04ac38929989]
+description = "Test grepping multiples files at once -> Multiple files, one match, multiple flags"
+
+[9c4f7f9a-a555-4e32-bb06-4b8f8869b2cb]
+description = "Test grepping multiples files at once -> Multiple files, no matches, various flags"
+
+[ba5a540d-bffd-481b-bd0c-d9a30f225e01]
+description = "Test grepping multiples files at once -> Multiple files, several matches, file flag takes precedence over line number flag"
+
+[ff406330-2f0b-4b17-9ee4-4b71c31dd6d2]
+description = "Test grepping multiples files at once -> Multiple files, several matches, inverted and match entire lines flags"

exercises/practice/grep/Grep.lean

@@ -0,0 +1,6 @@
+namespace Grep
+
+def grep (args : List String) : IO Unit :=
+  sorry
+
+end Grep