src/hub/get.bend
ezx@1.7.0.0 · 59 lines · 0 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.10.0.0/main.bend as Http
8import emerging-ezhttp@0.10.0.0/src/client.bend as Client
9import emerging-ezhttp@0.10.0.0/src/url.bend as Url
10import snap@1.3.0.0/main.bend as R
11import ezx@1.7.0.0/src/io/file.bend as F
12import ezx@1.7.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))