argumentcomputer / Megaparsec.lean

Lean 4 port of Megaparsec

MIT License

22 stars 4 forks source link

Enhancement: Infinite streams #20

Open cognivore opened 2 years ago

cognivore commented 2 years ago

Why?

In lazy languages, it's trivial to build infinite Streams. Lean would require plumbing around it to allow for infinite data structures. It's not acceptable, because we would like to parse stuff we get down the wire, signals coming from a signal generator, multipart form data.

The most practical use case is processing streams of data that are exceeding memory capabilities, such as huge JSON or XML files.

What?

[ ] Generate a large (1GiB+) CSV file
[ ] Spawn a VM with 512MiB RAM
[ ] Refactor Stream to be accommodating for a demo showing how to parse some bits out of that CSV without loading all of it into RAM
[ ] Test it on an actual computer
[ ] Demonstrate that it works in a small VM

cognivore commented 2 years ago

There's this one defined in Lean:

structure FS.Stream where
  isEof   : IO Bool
  flush   : IO Unit
  read    : USize → IO ByteArray
  write   : ByteArray → IO Unit
  getLine : IO String
  putStr  : String → IO Unit
  deriving Inhabited