src/hub/get.bend source

src/hub/get.bend on the hub · documented module

# hub/get: a file fetched from the hub over ezhttp, or read off the disk for a# `file:` url, and judged by hub/hub against the hash that names it. The GET# lives apart from the judging because ezhttp reaches foreign code, and bend# 2.0.32 fails a proof whose imports reach foreign code, so a law may import# hub/hub but never this.import Baseimport 0xf1c957a470368870a6d1d62a8c0cbe32/main.bend as Httpimport 0xf1c957a470368870a6d1d62a8c0cbe32/src/client.bend as Clientimport 0xf1c957a470368870a6d1d62a8c0cbe32/src/url.bend as Urlimport 0xabe575924687afad4cee1a2c1194d639/main.bend as Rimport ../io/file.bend as Fimport ./hub.bend as Hub# what ezhttp answered. It folds a socket that would not open and a reply that# came apart into one Err, so both are 6.def get.reply(response: Client.Response) -> String:  match response:    case Client.Err{why}:      "6\n" ++ why    case Client.Response{+status, _headers, body}:      Hub.get.status(U32.is_eq(status, 200), status, body)# a url fetched over a socketdef get.http(url: String) -> IO(String):  do IO<String>:    r : Client.Response <- Http.http.get(url)    return get.reply(r)# a file url read off the diskdef get.file(+path: String) -> IO(String):  do IO<String>:    m : Maybe<&2, String> <- F.read(path)    return Hub.get.file.got(m, path)# a url whose scheme decides where the body comes fromdef get.scheme(file: Bool, url: String, path: String) -> IO(String):  match file:    case True{}:      get.file(path)    case False{}:      get.http(url)# a url that came apart, or the reason it did notdef get.loc(loc: Url.Loc, url: String) -> IO(String):  match loc:    case Url.Bad{why}:      IO.pure(String, "22\n" ++ why)    case Url.Loc{+scheme, _host, _port, path}:      get.scheme(String.eq(scheme, "file"), url, path)# the body at a url: "0" and the body, or a status and the reasondef get(+url: String) -> IO(String):  get.loc(Http.parse_url(url), url)# the file at a url, accepted only when it hashes to `want`def fetch(+url: String, want: String) -> IO(Hub.Got):  do IO<Hub.Got>:    +out : String <- get(url)    return Hub.judge(R.ok(out), Hub.matches(want, R.text(out)), url, R.text(out))