src/hub/get.bend

ezx@1.11.0.0 · 59 lines · 7 definitions

1# hub/get: a file fetched from the hub over ezhttp, or read off the disk for a
2# `file:` url, and judged by hub/hub against the hash that names it. The GET
3# lives apart from the judging because ezhttp reaches foreign code, and bend
4# 2.0.32 fails a proof whose imports reach foreign code, so a law may import
5# hub/hub but never this.
6import Base
7import emerging-ezhttp@0.14.0.0/main.bend as Http
8import emerging-ezhttp@0.14.0.0/src/client.bend as Client
9import emerging-ezhttp@0.14.0.0/src/url.bend as Url
10import snap@1.4.0.0/main.bend as R
11import ezx@1.11.0.0/src/io/file.bend as F
12import ezx@1.11.0.0/src/hub/hub.bend as Hub
13
14# what ezhttp answered. It folds a socket that would not open and a reply that
15# came apart into one Err, so both are 6.
16def get.reply(response: Client.Response) -> String:
17  match response:
18    case Client.Err{why}:
19      "6\n" ++ why
20    case Client.Response{+status, _headers, body}:
21      Hub.get.status(U32.is_eq(status, 200), status, body)
22
23# a url fetched over a socket
24def get.http(url: String) -> IO(String):
25  do IO<String>:
26    r : Client.Response <- Http.http.get(url)
27    return get.reply(r)
28
29# a file url read off the disk
30def get.file(+path: String) -> IO(String):
31  do IO<String>:
32    m : Maybe<&2, String> <- F.read(path)
33    return Hub.get.file.got(m, path)
34
35# a url whose scheme decides where the body comes from
36def get.scheme(file: Bool, url: String, path: String) -> IO(String):
37  match file:
38    case True{}:
39      get.file(path)
40    case False{}:
41      get.http(url)
42
43# a url that came apart, or the reason it did not
44def get.loc(loc: Url.Loc, url: String) -> IO(String):
45  match loc:
46    case Url.Bad{why}:
47      IO.pure(String, "22\n" ++ why)
48    case Url.Loc{+scheme, _host, _port, path}:
49      get.scheme(String.eq(scheme, "file"), url, path)
50
51# the body at a url: "0" and the body, or a status and the reason
52def get(+url: String) -> IO(String):
53  get.loc(Http.parse_url(url), url)
54
55# the file at a url, accepted only when it hashes to `want`
56def fetch(+url: String, want: String) -> IO(Hub.Got):
57  do IO<Hub.Got>:
58    +out : String <- get(url)
59    return Hub.judge(R.ok(out), Hub.matches(want, R.text(out)), url, R.text(out))