Reservoir

Parse.lean

It"s a protocol parser generator for Lean4 based on https://github.com/nodejs/llparse. It currently generates parsers in Lean and C. The Lean version is in most cases 2 times slower than the C version right now.

parser Http in Lean where
    def method : Nat
    def url : Nat × Nat

    node method where
        switch (store method beforeUrl)
            | "HEAD" => 0
            | "GET" => 1
            | "POST" => 2
            | "PUT" => 3
            | "DELETE" => 4
            | "OPTIONS" => 5
            | "CONNECT" => 6
            | "TRACE" => 7
            | "PATCH" => 8
        otherwise (error 0)

    node beforeUrl where
        is " " beforeUrl
        goto (start url url)

    node url where
        peek ' ' (end url http)
        otherwise url

    node http where
        is " HTTP/1.1\r\n\r\n" http
        otherwise (error 1)