Created
July 17, 2024 22:02
-
-
Save david415/f1fe01da5a409be9c852b0e7557bde60 to your computer and use it in GitHub Desktop.
grep written in Lean 4
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| partial def grep (stream : IO.FS.Stream) (expected : String) : IO Unit := do | |
| let line ← stream.getLine | |
| if line.isEmpty then | |
| pure () | |
| else | |
| let words := line.splitOn " " | |
| if words.contains expected then | |
| IO.print line | |
| grep stream expected | |
| def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do | |
| let fileExists ← filename.pathExists | |
| if not fileExists then | |
| let stderr ← IO.getStderr | |
| stderr.putStrLn s!"File not found: {filename}" | |
| pure none | |
| else | |
| let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read | |
| pure (some (IO.FS.Stream.ofHandle handle)) | |
| def processFiles (expected : String) (files : List String) : IO UInt32 := do | |
| match files with | |
| | [] => | |
| pure 0 | |
| | filename :: rest => | |
| let streamOpt ← fileStream filename | |
| match streamOpt with | |
| | none => | |
| let code ← processFiles expected rest | |
| pure (code+1) | |
| | some stream => | |
| grep stream expected | |
| processFiles expected rest | |
| def process (expected : String) (files : List String) : IO UInt32 := do | |
| match files with | |
| | [] => | |
| let stdin ← IO.getStdin | |
| grep stdin expected | |
| pure 0 | |
| | _ => | |
| processFiles expected files | |
| def printUsage : IO UInt32 := do | |
| let stdout ← IO.getStdout | |
| stdout.putStrLn "grep [--help] expected_word [files]" | |
| pure (1) | |
| def main (args : List String) : IO UInt32 := | |
| match args with | |
| | [] => printUsage | |
| | [x] => process x [] | |
| | x :: xs => process x xs |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment