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 resolved against the current URL as RFC 3986 §5.2
8	# resolves a reference: an absolute http or https URL is taken as it is, a
9	# network-path (`//host/...`) takes the current scheme, an absolute path the
10	# current origin, a query the current path, and a relative path is merged
11	# with the current path's directory; dot segments are removed. An empty
12	# Location, a fragment, or another scheme stops. The client gives a chain at
13	# most `redirect.max()` hops.
14	import Base
15	import ./url.bend as Url
16	import ./http.bend as Http
17	
18	# what the client does after a response
19	type Hop is Data:
20	  Stop{}
21	  Go{url: String}
22	
23	# the most hops the client follows (httpx's default is 20)
24	def redirect.max() -> Nat:
25	  10n
26	
27	# whether a status asks the client to go elsewhere (RFC 9110 §15.4.2-9)
28	def redirect.is(+status: U32) -> Bool:
29	  Bool.or(U32.is_eq(status, 301), Bool.or(U32.is_eq(status, 302),
30	    Bool.or(U32.is_eq(status, 303), Bool.or(U32.is_eq(status, 307),
31	      U32.is_eq(status, 308)))))
32	
33	# whether a Location is an absolute http or https URL
34	def redirect.absolute(+loc: String) -> Bool:
35	  Bool.or(String.starts_with(loc, "http://"),
36	    String.starts_with(loc, "https://"))
37	
38	# --- dot segments (RFC 3986 §5.2.4) ---
39	
40	# the segments kept so far, last first, with the last one dropped
41	def redirect.pop(out: List<&2, String>) -> List<&2, String>:
42	  match out:
43	    case []:
44	      []
45	    case _ <> t:
46	      t
47	
48	# a path that ends in `.` or `..` keeps its trailing `/`: an empty last segment
49	def redirect.dots.end(last: Bool, out: List<&2, String>) -> List<&2, String>:
50	  match last:
51	    case True{}:
52	      "" <> out
53	    case False{}:
54	      out
55	
56	# a segment that is not `.`: `..` drops the last kept, any other is kept
57	def redirect.dots.up(up: Bool, last: Bool, s: String, out: List<&2, String>,
58	  rest: List<&2, String> -> List<&2, String>) -> List<&2, String>:
59	  match up:
60	    case True{}:
61	      rest(redirect.dots.end(last, redirect.pop(out)))
62	    case False{}:
63	      rest(s <> out)
64	
65	# one segment: `.` is dropped, `..` drops the last kept, any other is kept
66	def redirect.dots.one(dot: Bool, up: Bool, last: Bool, s: String,
67	  out: List<&2, String>, rest: List<&2, String> -> List<&2, String>)
68	  -> List<&2, String>:
69	  match dot:
70	    case True{}:
71	      rest(redirect.dots.end(last, out))
72	    case False{}:
73	      redirect.dots.up(up, last, s, out, rest)
74	
75	# a path's segments with dot segments removed, `out` holding those kept so
76	# far, last first
77	def redirect.dots(ss: List<&2, String>, out: List<&2, String>)
78	  -> List<&2, String>:
79	  match ss:
80	    case []:
81	      List.reverse(&2, String, out)
82	    case +s <> +t:
83	      redirect.dots.one(String.eq(s, "."), String.eq(s, ".."),
84	        List.is_empty(&2, String, t), s, out, o => redirect.dots(t, o))
85	
86	# the segments after a path's leading `/`, dot segments removed, as a path
87	def redirect.clean(ss: List<&2, String>) -> String:
88	  "/" ++ String.join(redirect.dots(ss, []), "/")
89	
90	# --- merging (RFC 3986 §5.2.3) ---
91	
92	# every segment but the last, after `s`
93	def redirect.init.of(t: List<&2, String>, s: String) -> List<&2, String>:
94	  match t:
95	    case []:
96	      []
97	    case u <> r:
98	      s <> redirect.init.of(r, u)
99	
100	# every segment but the last
101	def redirect.init(ss: List<&2, String>) -> List<&2, String>:
102	  match ss:
103	    case []:
104	      []
105	    case s <> t:
106	      redirect.init.of(t, s)
107	
108	# --- references ---
109	
110	# a Location's path and its query (with its `?`, "" when it has none)
111	type Ref is Data:
112	  Ref{path: String, query: String}
113	
114	# a Location divided at its first `?`
115	def redirect.split.of(c: Http.Cut, loc: String) -> Ref:
116	  match c:
117	    case Http.NoCut{}:
118	      Ref{loc, ""}
119	    case Http.Cut{before, after}:
120	      Ref{before, "?" ++ after}
121	
122	# a Location's path and query, its fragment dropped
123	def redirect.split(+loc: String) -> Ref:
124	  +bare = Url.frag.drop(loc)
125	  redirect.split.of(Http.divide(bare, "?"), bare)
126	
127	# an absolute-path reference's path, dot segments removed, then its query
128	def redirect.abs.of(r: Ref) -> String:
129	  match r:
130	    case Ref{path, query}:
131	      redirect.clean(List.tail(&2, String, String.split(path, '/'))) ++ query
132	
133	# a relative-path reference merged with the current path, dot segments
134	# removed, then its query
135	def redirect.rel.of(base: String, r: Ref) -> String:
136	  match r:
137	    case Ref{path, query}:
138	      redirect.clean(List.tail(&2, String,
139	        List.append(&2, String, redirect.init(String.split(base, '/')),
140	          String.split(path, '/')))) ++ query
141	
142	# a path without its query
143	def redirect.base(path: String) -> String:
144	  Url.query.hier(String.split(path, '?'))
145	
146	# --- which sort of reference a Location is ---
147	
148	# what sort of reference a Location that is not an absolute URL is
149	type Sort is Data:
150	  Net{}
151	  Abs{}
152	  Stay{}
153	  Query{}
154	  Rel{}
155	
156	# a character that ends a reference's first segment
157	def redirect.schemed.end(+c: Char) -> Bool:
158	  Bool.or(Char.is_eq(c, '/'), Bool.or(Char.is_eq(c, '?'), Char.is_eq(c, '#')))
159	
160	# a character that does not end the first segment: a `:` names a scheme
161	def redirect.schemed.colon(colon: Bool, rest: Unit -> Bool) -> Bool:
162	  match colon:
163	    case True{}:
164	      True{}
165	    case False{}:
166	      rest(Unit{})
167	
168	# one character of the scheme search
169	def redirect.schemed.at(stop: Bool, colon: Bool, rest: Unit -> Bool) -> Bool:
170	  match stop:
171	    case True{}:
172	      False{}
173	    case False{}:
174	      redirect.schemed.colon(colon, rest)
175	
176	# whether a reference names a scheme: a `:` before its first `/`, `?` or `#`
177	def redirect.schemed(s: String) -> Bool:
178	  match s:
179	    case SNil{}:
180	      False{}
181	    case SCon{+c, t}:
182	      redirect.schemed.at(redirect.schemed.end(c), Char.is_eq(c, ':'),
183	        _u => redirect.schemed(t))
184	
185	# a Location the client does not follow: empty, a fragment, another scheme
186	def redirect.stays(+loc: String) -> Bool:
187	  Bool.or(String.is_empty(loc), Bool.or(String.starts_with(loc, "#"),
188	    redirect.schemed(loc)))
189	
190	# a relative reference: a query, or a relative path
191	def redirect.sort.rel(query: Bool) -> Sort:
192	  match query:
193	    case True{}:
194	      Query{}
195	    case False{}:
196	      Rel{}
197	
198	# a reference that is not a path from the root: one the client stays on, or
199	# a relative one
200	def redirect.sort.stay(stay: Bool, query: Bool) -> Sort:
201	  match stay:
202	    case True{}:
203	      Stay{}
204	    case False{}:
205	      redirect.sort.rel(query)
206	
207	# a reference that is not a network path: an absolute path, or another
208	def redirect.sort.abs(abs: Bool, stay: Bool, query: Bool) -> Sort:
209	  match abs:
210	    case True{}:
211	      Abs{}
212	    case False{}:
213	      redirect.sort.stay(stay, query)
214	
215	# the sort, from what the Location starts with
216	def redirect.sort.of(net: Bool, abs: Bool, stay: Bool, query: Bool) -> Sort:
217	  match net:
218	    case True{}:
219	      Net{}
220	    case False{}:
221	      redirect.sort.abs(abs, stay, query)
222	
223	# what sort of reference a Location is
224	def redirect.sort(+loc: String) -> Sort:
225	  redirect.sort.of(String.starts_with(loc, "//"), String.starts_with(loc, "/"),
226	    redirect.stays(loc), String.starts_with(loc, "?"))
227	
228	# --- the target ---
229	
230	# a Location of a known sort against the current URL's parts
231	def redirect.against(scheme: String, host: String, port: U32, path: String,
232	  +loc: String, k: Sort) -> Maybe<&2, String>:
233	  match k:
234	    case Net{}:
235	      Some{scheme ++ ":" ++ loc}
236	    case Abs{}:
237	      Some{scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
238	        ++ redirect.abs.of(redirect.split(loc))}
239	    case Stay{}:
240	      None{}
241	    case Query{}:
242	      Some{scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
243	        ++ redirect.base(path) ++ loc}
244	    case Rel{}:
245	      Some{scheme ++ "://" ++ host ++ ":" ++ U32.show(port)
246	        ++ redirect.rel.of(redirect.base(path), redirect.split(loc))}
247	
248	# a Location against the current URL, once it is parsed
249	def redirect.at(l: Url.Loc, +loc: String) -> Maybe<&2, String>:
250	  match l:
251	    case Url.Bad{why}:
252	      None{}
253	    case Url.Loc{scheme, host, port, path}:
254	      redirect.against(scheme, host, port, path, loc, redirect.sort(loc))
255	
256	# a Location once it is known whether it is an absolute URL
257	def redirect.target.of(url: String, +loc: String, absolute: Bool)
258	  -> Maybe<&2, String>:
259	  match absolute:
260	    case True{}:
261	      Some{loc}
262	    case False{}:
263	      redirect.at(Url.parse(url), loc)
264	
265	# where a Location sends a client that is at `url`, or None when it is not
266	# one the client follows
267	def redirect.target(url: String, +loc: String) -> Maybe<&2, String>:
268	  redirect.target.of(url, loc, redirect.absolute(loc))
269	
270	# a resolved target as a hop
271	def redirect.hop(m: Maybe<&2, String>) -> Hop:
272	  match m:
273	    case None{}:
274	      Stop{}
275	    case Some{next}:
276	      Go{next}
277	
278	# a response once it is known whether its status redirects
279	def redirect.on(url: String, +loc: String, moved: Bool) -> Hop:
280	  match moved:
281	    case True{}:
282	      redirect.hop(redirect.target(url, loc))
283	    case False{}:
284	      Stop{}
285	
286	# the next hop from `url`, after a response with `status` and Location `loc`
287	# ("" when it had none), with `left` hops still allowed
288	def redirect.next(left: Nat, url: String, +status: U32, +loc: String) -> Hop:
289	  match left:
290	    case 0n:
291	      Stop{}
292	    case 1n+p:
293	      redirect.on(url, loc, redirect.is(status))
294	
295	# the next hop after a response's status and headers
296	def redirect.plan(left: Nat, url: String, +status: U32,
297	  headers: List<&2, Http.Header>) -> Hop:
298	  redirect.next(left, url, status, Http.headers.find(headers, "location"))
299	
300	# whether a request with this method follows redirects when asked to: only a
301	# GET does (method names are case-sensitive, RFC 9110 §9.1)
302	def redirect.follows(+method: String, follow: Bool) -> Bool:
303	  Bool.and(follow, String.eq(method, "GET"))