1	# ezhttp/src/redirect: where a GET goes after a response, pure. The client's
2	# follow loop (client.bend) sends the next GET where this module says and
3	# decides nothing itself. SPEC.md HTTP-REDIR lists what is guaranteed.
4	#
5	# Policy: the client follows redirects for GET only, so every hop is a GET.
6	# 301, 302, 303, 307 and 308 with a Location are followed; any other status
7	# stops. A Location is either an absolute http or https URL, taken as it is,
8	# or an absolute path, resolved against the current URL's scheme, host and
9	# port. Any other Location (a relative path, `//host/...`, empty) stops. The
10	# client gives a chain at most `redirect.max()` hops.
11	import Base
12	import ./url.bend as Url
13	import ./http.bend as Http
14	
15	# what the client does after a response
16	type Hop is Data:
17	  Stop{}
18	  Go{url: String}
19	
20	# the most hops the client follows (httpx's default is 20)
21	def redirect.max() -> Nat:
22	  10n
23	
24	# whether a status asks the client to go elsewhere (RFC 9110 §15.4.2-9)
25	def redirect.is(+status: U32) -> Bool:
26	  Bool.or(U32.is_eq(status, 301), Bool.or(U32.is_eq(status, 302),
27	    Bool.or(U32.is_eq(status, 303), Bool.or(U32.is_eq(status, 307),
28	      U32.is_eq(status, 308)))))
29	
30	# whether a Location is an absolute http or https URL
31	def redirect.absolute(+loc: String) -> Bool:
32	  Bool.or(String.starts_with(loc, "http://"),
33	    String.starts_with(loc, "https://"))
34	
35	# whether a Location is an absolute path: one `/`, not two
36	def redirect.path(+loc: String) -> Bool:
37	  Bool.and(String.starts_with(loc, "/"),
38	    Bool.not(String.starts_with(loc, "//")))
39	
40	# the origin of a URL that came apart, with an absolute path after it
41	def redirect.join(l: Url.Loc, loc: String) -> Maybe<&2, String>:
42	  match l:
43	    case Url.Bad{why}:
44	      None{}
45	    case Url.Loc{scheme, host, port, path}:
46	      Some{scheme ++ "://" ++ host ++ ":" ++ U32.show(port) ++ loc}
47	
48	# a Location once it is known whether it is an absolute path
49	def redirect.target.path(url: String, loc: String, path: Bool)
50	  -> Maybe<&2, String>:
51	  match path:
52	    case True{}:
53	      redirect.join(Url.parse(url), loc)
54	    case False{}:
55	      None{}
56	
57	# a Location once it is known whether it is an absolute URL
58	def redirect.target.of(url: String, +loc: String, absolute: Bool)
59	  -> Maybe<&2, String>:
60	  match absolute:
61	    case True{}:
62	      Some{loc}
63	    case False{}:
64	      redirect.target.path(url, loc, redirect.path(loc))
65	
66	# where a Location sends a client that is at `url`, or None when it is not
67	# one the client follows
68	def redirect.target(url: String, +loc: String) -> Maybe<&2, String>:
69	  redirect.target.of(url, loc, redirect.absolute(loc))
70	
71	# a resolved target as a hop
72	def redirect.hop(m: Maybe<&2, String>) -> Hop:
73	  match m:
74	    case None{}:
75	      Stop{}
76	    case Some{next}:
77	      Go{next}
78	
79	# a response once it is known whether its status redirects
80	def redirect.on(url: String, +loc: String, moved: Bool) -> Hop:
81	  match moved:
82	    case True{}:
83	      redirect.hop(redirect.target(url, loc))
84	    case False{}:
85	      Stop{}
86	
87	# the next hop from `url`, after a response with `status` and Location `loc`
88	# ("" when it had none), with `left` hops still allowed
89	def redirect.next(left: Nat, url: String, +status: U32, +loc: String) -> Hop:
90	  match left:
91	    case 0n:
92	      Stop{}
93	    case 1n+p:
94	      redirect.on(url, loc, redirect.is(status))
95	
96	# the next hop after a response's status and headers
97	def redirect.plan(left: Nat, url: String, +status: U32,
98	  headers: List<&2, Http.Header>) -> Hop:
99	  redirect.next(left, url, status, Http.headers.find(headers, "location"))