source
def Lake.hexEncodeByte (b : UInt8) :
Char
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lake.uriEscapeByte (b : UInt8) (s : String := "") :
String

Encode a byte as a URI escape code (e.g., `%20`).

Equations

- Lake.uriEscapeByte b s = ((s.push '%').push (Lake.hexEncodeByte (b >>> 4))).push (Lake.hexEncodeByte (b &&& 15))

Instances For

source
@[specialize #[]]
def Lake.foldlUtf8M {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) :
m σ

Folds a monadic function over the UTF-8 bytes of `Char` from most significant to least significant.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
abbrev Lake.foldlUtf8 {σ : Type u_1} (c : Char) (f : σ → UInt8 → σ) (init : σ) :
σ
Equations

- Lake.foldlUtf8 c f init = (Lake.foldlUtf8M c (fun (x1 : σ) (x2 : UInt8) => pure (f x1 x2)) init).run

Instances For

source
def Lake.uriEscapeChar (c : Char) (s : String := "") :
String

Encode a character as a sequence of URI escape codes representing its UTF8 encoding.

Equations

- Lake.uriEscapeChar c s = Lake.foldlUtf8 c (fun (s : String) (b : UInt8) => Lake.uriEscapeByte b s) s

Instances For

source
def Lake.isUriUnreservedMark (c : Char) :
Bool

A URI unreserved mark as specified in RFC3986. Unlike the older RFC2396, RFC2396 also reserves `!`, `*`, `'`, `(`, and `)`.

Lake uses RFC3986 here because the `curl` implementation of AWS Sigv4 that Lake uses to upload artifacts requires these additional characters to be escaped.

Equations

- Lake.isUriUnreservedMark '-' = true
- Lake.isUriUnreservedMark '_' = true
- Lake.isUriUnreservedMark '.' = true
- Lake.isUriUnreservedMark '~' = true
- Lake.isUriUnreservedMark c = false

Instances For

source
def Lake.uriEncodeChar (c : Char) (s : String := "") :
String

Encodes anything but a URI unreserved character as a URI escape sequences.

Equations

- Lake.uriEncodeChar c s = if (c.isAlphanum || Lake.isUriUnreservedMark c) = true then s.push c else Lake.uriEscapeChar c s

Instances For

source
def Lake.uriEncode (s : String) (init : String := "") :
String

Encodes a string as an ASCII URI component, escaping special characters (and unicode).

Equations

- Lake.uriEncode s init = String.foldl (fun (s : String) (c : Char) => Lake.uriEncodeChar c s) init s

Instances For

source
def Lake.getUrl? (url : String) (headers : Array String := #[]) :
LogIO (Option String)

Performs a HTTP `GET` request of a URL (using `curl` with JSON output) and, if successful, return the body. Otherwise, returns `none` on a 404 and errors on anything else.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lake.getUrl (url : String) (headers : Array String := #[]) :
LogIO String

Perform a HTTP `GET` request of a URL (using `curl`) and return the body.

Equations

- One or more equations did not get rendered due to their size.

Instances For