gralha-http-core

Releases (1):
  0.1.0.0  0x59279b68893c8c86cbcf854fcfc9db2f  indexed  https://jend.leeeet.dev/files.txt?path=gralha-http-core@0.1.0.0

Definitions (61):
  Http.when (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=when)
   # One of two computations, run on c; only the chosen one runs.
   def when(-A: Type, c: Bool, yes: Unit -> A, no: Unit -> A) -> A:
  Http.cut.go (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=cut.go)
   # The text before the first sep and the text after it, or None without sep.
   def cut.go(s: String, +sep: String, +acc: String) -> Maybe<&1, String & String>:
  Http.cut (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=cut)
   def cut(s: String, +sep: String) -> Maybe<&1, String & String>:
  Http.before.cut (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=before.cut)
   def before.cut(c: Maybe<&1, String & String>, whole: String) -> String:
  Http.before (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=before)
   # The text before sep, or all of it without sep.
   def before(+s: String, +sep: String) -> String:
  Http.after.cut (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=after.cut)
   def after.cut(c: Maybe<&1, String & String>) -> String:
  Http.after (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=after)
   # The text after sep, or "" without sep.
   def after(s: String, +sep: String) -> String:
  Http.utf8.width (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.width)
   def utf8.width(+c: U32) -> U32:
  Http.utf8.count (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.count)
   def utf8.count(s: String, acc: U32) -> U32:
  Http.utf8.length (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.length)
   # The bytes a text takes in UTF-8, as Content-Length counts them.
   def utf8.length(s: String) -> U32:
  Http.utf8.push (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.push)
   # A character's UTF-8 bytes, prepended to acc in reverse.
   def utf8.push(+c: U32, +acc: List<&2, U32>) -> List<&2, U32>:
  Http.utf8.need (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.need)
   # Decoding reads a byte at a time: need is the continuation bytes still
   # owed and code the bits so far. A byte out of place is U+FFFD.
   def utf8.need(+b: U32, +need: U32) -> U32:
  Http.utf8.code (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.code)
   def utf8.code(+b: U32, +need: U32, +code: U32) -> U32:
  Http.utf8.emit (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.emit)
   def utf8.emit(+b: U32, +need: U32, +code: U32, +acc: String) -> String:
  Http.utf8.decode.go (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.decode.go)
   def utf8.decode.go(bytes: List<&2, U32>, +need: U32, +code: U32, acc: String) -> String:
  Http.utf8.decode (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=utf8.decode)
   def utf8.decode(bytes: List<&2, U32>) -> String:
  Http.hex.digit (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=hex.digit)
   def hex.digit(+c: U32) -> U32:
  Http.hex.is_digit (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=hex.is_digit)
   def hex.is_digit(+c: U32) -> Bool:
  Http.url.bytes (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=url.bytes)
   def url.bytes(s: String, +acc: List<&2, U32>) -> List<&2, U32>:
  Http.url.decode (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=url.decode)
   # A url component with %XX escapes and + (a space, as forms send it)
   # decoded; the bytes read as UTF-8.
   def url.decode(s: String) -> String:
  Http.target.path (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=target.path)
   # A target's path: the part before ?.
   def target.path(+target: String) -> String:
  Http.target.query (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=target.query)
   # A target's query: the part after ?, or "".
   def target.query(target: String) -> String:
  Http.query.find (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=query.find)
   def query.find(pairs: List<&2, String>, +name: String) -> Maybe<&2, String>:
  Http.query.get (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=query.get)
   # The first value of a query parameter, decoded, e.g. query.get("a=1&b=x%20y", "b").
   def query.get(query: String, +name: String) -> Maybe<&2, String>:
  Http.Header (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=Header)
   type Header is Data:
     Header{name: String, value: String}
  Http.header.find (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=header.find)
   # The value of the first header named name, any case.
   def header.find(headers: List<&2, Header>, +name: String) -> Maybe<&2, String>:
  Http.header.get (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=header.get)
   def header.get(headers: List<&2, Header>, name: String) -> Maybe<&2, String>:
  Http.header.has (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=header.has)
   def header.has(headers: List<&2, Header>, name: String) -> Bool:
  Http.header.line (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=header.line)
   def header.line(c: Maybe<&1, String & String>, rest: List<&2, Header>) -> List<&2, Header>:
  Http.header.parse (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=header.parse)
   # Header lines, "Name: value" each; a line with no colon is skipped.
   def header.parse(lines: List<&2, String>) -> List<&2, Header>:
  Http.header.text (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=header.text)
   def header.text(headers: List<&2, Header>) -> String:
  Http.digits (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=digits)
   def digits(s: String) -> Bool:
  Http.number (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=number)
   # A decimal number made of digits only, as Content-Length is.
   def number(+s: String) -> Maybe<&2, U32>:
  Http.number.or_zero (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=number.or_zero)
   def number.or_zero(m: Maybe<&2, String>) -> U32:
  Http.content.length (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=content.length)
   # The Content-Length a header list declares, or 0.
   def content.length(headers: List<&2, Header>) -> U32:
  Http.Request (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=Request)
   type Request is Data:
     Request{method: String, target: String, version: String, headers: List<&2, Header>, body: String}
  Http.request.line (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.line)
   def request.line(parts: List<&2, String>, headers: List<&2, Header>, body: String) -> Maybe<&2, Request>:
  Http.request.head (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.head)
   def request.head(lines: List<&2, String>, body: String) -> Maybe<&2, Request>:
  Http.request.cut (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.cut)
   def request.cut(c: Maybe<&1, String & String>) -> Maybe<&2, Request>:
  Http.request.parse (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.parse)
   # A request: "METHOD target HTTP/x.y", header lines, a blank line, the body
   # (all that follows it). None when the head is unfinished or malformed.
   def request.parse(text: String) -> Maybe<&2, Request>:
  Http.request.complete.cut (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.complete.cut)
   def request.complete.cut(c: Maybe<&1, String & String>) -> Bool:
  Http.request.complete (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.complete)
   # Whether text holds a whole request: its head ended, and as many body bytes
   # as its Content-Length (none without one).
   def request.complete(text: String) -> Bool:
  Http.request.method (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.method)
   def request.method(r: Request) -> String:
  Http.request.target (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.target)
   def request.target(r: Request) -> String:
  Http.request.path (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.path)
   def request.path(r: Request) -> String:
  Http.request.body (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.body)
   def request.body(r: Request) -> String:
  Http.request.header (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.header)
   # A header of the request, any case.
   def request.header(r: Request, name: String) -> Maybe<&2, String>:
  Http.request.query (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.query)
   # A query parameter of the request's target, decoded.
   def request.query(r: Request, +name: String) -> Maybe<&2, String>:
  Http.request.is (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=request.is)
   # Whether the request is method on path, e.g. request.is(r, "GET", "/").
   def request.is(+r: Request, method: String, path: String) -> Bool:
  Http.Response (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=Response)
   type Response is Data:
     Response{status: U32, headers: List<&2, Header>, body: String}
  Http.reason (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=reason)
   # The reason phrase of a status code, or "" for one not listed.
   def reason(+code: U32) -> String:
  Http.response (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=response)
   # A response with a status, a Content-Type and a body.
   def response(+status: U32, content_type: String, body: String) -> Response:
  Http.ok (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=ok)
   # A 200 response with a Content-Type and a body.
   def ok(content_type: String, body: String) -> Response:
  Http.status (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=status)
   # A plain-text response with the status's reason phrase as its body.
   def status(+code: U32) -> Response:
  Http.response.with (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=response.with)
   # The response with one more header, after the ones it has.
   def response.with(r: Response, name: String, value: String) -> Response:
  Http.response.status (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=response.status)
   def response.status(r: Response) -> U32:
  Http.head (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=head)
   # The status line and the header lines, up to the blank line: what a server
   # sends before a body it writes itself.
   def head(+status: U32, headers: List<&2, Header>) -> String:
  Http.length.with (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=length.with)
   def length.with(+headers: List<&2, Header>, +body: String) -> List<&2, Header>:
  Http.response.text (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=response.text)
   # The response as sent: its head, with a Content-Length counted in UTF-8
   # bytes after its own headers (unless it has one), then its body.
   def response.text(r: Response) -> String:
  Http.ok_is_200 (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=ok_is_200)
   law ok_is_200:
     for t: String
     for b: String
     {response.status(ok(t, b)) == 200 : U32}
  Http.with_keeps_status (https://jend.leeeet.dev/definition.txt?path=gralha-http-core@0.1.0.0/http.bend&name=with_keeps_status)
   law with_keeps_status:
     for r: Response
     for n: String
     for v: String
     {response.status(response.with(r, n, v)) == response.status(r) : U32}