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.
6	import Base
7	import 0x49ec536f1d3da4f76d78aaece3ccda7a/main.bend as Http
8	import 0x49ec536f1d3da4f76d78aaece3ccda7a/src/client.bend as Client
9	import 0x49ec536f1d3da4f76d78aaece3ccda7a/src/url.bend as Url
10	import 0xead4c7939c9eaca8d47da53b4496b731/main.bend as R
11	import ../io/file.bend as F
12	import ./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.
16	def 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
24	def 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
30	def 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
36	def 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
44	def 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
52	def 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`
56	def 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))