dns.bend
bend-kit-dns@0.4.0.1 · 700 lines · 0 definitions
1# DNS codec and host lookup. Source: https://github.com/paymog/bend-kit/tree/main/dns
2import Base
3# bend-kit-wire@0.4.0.3
4import bend-kit-wire@0.4.0.3/wire.bend as Wire
5
6# query, answer, and resolve.pure are pure; PROOF.bend covers them, not effs/.
7# resolve.all uses the OS resolver (IPv4 and IPv6); resolve keeps the first address.
8# import bend-kit-dns@0.4.0.0/dns.bend as Dns
9
10type Cur is Data:
11 Cur{v: U32, rest: String}
12
13type RR is Data:
14 RRBad{}
15 RRA{ip: String}
16 RRSkip{rest: String}
17
18def u8(s: String) -> Maybe<&2, Cur>:
19 match s:
20 case SNil{}:
21 None{}
22 case SCon{Chr{c}, t}:
23 Some{Cur{c, t}}
24
25def u16.lo(hi: U32, m: Maybe<&2, Cur>) -> Maybe<&2, Cur>:
26 match m:
27 case None{}:
28 None{}
29 case Some{Cur{lo, r}}:
30 Some{Cur{(hi * 256 + lo : U32), r}}
31
32def u16.go(m: Maybe<&2, Cur>) -> Maybe<&2, Cur>:
33 match m:
34 case None{}:
35 None{}
36 case Some{Cur{hi, r}}:
37 u16.lo(hi, u8(r))
38
39def u16(s: String) -> Maybe<&2, Cur>:
40 u16.go(u8(s))
41
42def skip.if(+s: String, +n: Nat, short: Bool) -> Maybe<&2, String>:
43 match short:
44 case True{}:
45 None{}
46 case False{}:
47 Some{String.drop(s, n)}
48
49def skip(+s: String, +n: Nat) -> Maybe<&2, String>:
50 skip.if(s, n, Nat.is_lt(String.length(s), n))
51
52def then(m: Maybe<&2, String>, n: Nat) -> Maybe<&2, String>:
53 match m:
54 case None{}:
55 None{}
56 case Some{r}:
57 skip(r, n)
58
59def push16(+n: U32, acc: String) -> String:
60 SCon{Chr{U32.and(n, 255)}, SCon{Chr{U32.shrn(n, 8n)}, acc}}
61
62# Query
63# -----
64
65def label.ok(+l: String) -> Bool:
66 +n = String.length(l)
67 Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 63n))
68
69def label.ascii(s: String) -> Bool:
70 match s:
71 case SNil{}:
72 True{}
73 case SCon{Chr{c}, t}:
74 Bool.and(U32.is_lt(c, 128), label.ascii(t))
75
76def labels.ok(xs: List<&2, String>) -> Bool:
77 match xs:
78 case Nil{}:
79 True{}
80 case Con{+l, t}:
81 Bool.and(Bool.and(label.ok(l), label.ascii(l)), labels.ok(t))
82
83def labels.put(xs: List<&2, String>, acc: String) -> String:
84 match xs:
85 case Nil{}:
86 acc
87 case Con{+l, t}:
88 labels.put(t, String.reverse(l) ++ SCon{Chr{U32.from_nat(String.length(l))}, acc})
89
90def query.if(+id: U32, xs: List<&2, String>, ok: Bool) -> Maybe<&2, String>:
91 match ok:
92 case False{}:
93 None{}
94 case True{}:
95 # header: id, RD, QDCOUNT 1; question: QNAME, QTYPE A, QCLASS IN
96 Some{String.reverse(push16(1, push16(1, SCon{Chr{0}, labels.put(xs, push16(0, push16(0, push16(0, push16(1, push16(256, push16(id, SNil{})))))))})))}
97
98def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&2, String>:
99 query.if(id, xs, labels.ok(xs))
100
101def strip_dot.if(+s: String, dot: Bool) -> String:
102 match dot:
103 case True{}:
104 String.reverse(String.drop(String.reverse(s), 1n))
105 case False{}:
106 s
107
108def strip_dot(+s: String) -> String:
109 strip_dot.if(s, String.ends_with(s, "."))
110
111# RFC 1035 §4.1: a standard query for the A record of name.
112def query(id: U32, name: String) -> Maybe<&2, String>:
113 query.labels(id, String.split(strip_dot(name), '.'))
114
115# Answer
116# ------
117
118# §4.1.4: a name is labels ending in a zero octet, or a two-octet pointer.
119def name.skip(fuel: Nat, s: String) -> Maybe<&2, String>:
120 match fuel:
121 case 0n:
122 None{}
123 case 1n+f:
124 match s:
125 case SNil{}:
126 None{}
127 case SCon{Chr{+l}, +t}:
128 Bool.pick(Maybe<&2, String>, U32.is_eq(l, 0), Some{t}, Bool.pick(Maybe<&2, String>, U32.is_le(192, l), skip(t, 1n), Bool.pick(Maybe<&2, String>, U32.is_le(64, l), None{}, name.skip(f, String.drop(t, U32.to_nat(l))))))
129
130def name.then(m: Maybe<&2, String>, n: Nat) -> Maybe<&2, String>:
131 match m:
132 case None{}:
133 None{}
134 case Some{+r}:
135 then(name.skip(String.length(r), r), n)
136
137def dotted(s: String) -> String:
138 match s:
139 case SNil{}:
140 ""
141 case SCon{Chr{c}, t}:
142 match t:
143 case SNil{}:
144 U32.show(c)
145 case SCon{_, _}:
146 U32.show(c) ++ "." ++ dotted(t)
147
148def rr.f(+r: String, +len: U32, a: Bool) -> RR:
149 match a:
150 case True{}:
151 RRA{dotted(String.take(r, 4n))}
152 case False{}:
153 RRSkip{String.drop(r, U32.to_nat(len))}
154
155def rr.data(+r: String, +len: U32, a: Bool, short: Bool) -> RR:
156 match short:
157 case True{}:
158 RRBad{}
159 case False{}:
160 rr.f(r, len, a)
161
162def rr.e(+ty: U32, +cl: U32, m: Maybe<&2, Cur>) -> RR:
163 match m:
164 case None{}:
165 RRBad{}
166 case Some{Cur{+len, +r}}:
167 rr.data(r, len, Bool.and(Bool.and(U32.is_eq(ty, 1), U32.is_eq(cl, 1)), U32.is_eq(len, 4)), Nat.is_lt(String.length(r), U32.to_nat(len)))
168
169def rr.d(ty: U32, cl: U32, m: Maybe<&2, String>) -> RR:
170 match m:
171 case None{}:
172 RRBad{}
173 case Some{r}:
174 rr.e(ty, cl, u16(r))
175
176def rr.c(ty: U32, m: Maybe<&2, Cur>) -> RR:
177 match m:
178 case None{}:
179 RRBad{}
180 case Some{Cur{cl, r}}:
181 rr.d(ty, cl, skip(r, 4n))
182
183def rr.b(m: Maybe<&2, Cur>) -> RR:
184 match m:
185 case None{}:
186 RRBad{}
187 case Some{Cur{ty, r}}:
188 rr.c(ty, u16(r))
189
190def rr.a(m: Maybe<&2, String>) -> RR:
191 match m:
192 case None{}:
193 RRBad{}
194 case Some{r}:
195 rr.b(u16(r))
196
197# §4.1.3: NAME, TYPE, CLASS, TTL, RDLENGTH, RDATA.
198def rr(+s: String) -> RR:
199 rr.a(name.skip(String.length(s), s))
200
201# fuel = records left. The first A record wins; CNAMEs before it are skipped.
202def answers.scan(fuel: Nat, r: RR) -> Maybe<&2, String>:
203 match fuel:
204 case 0n:
205 None{}
206 case 1n+f:
207 match r:
208 case RRBad{}:
209 None{}
210 case RRA{ip}:
211 Some{ip}
212 case RRSkip{s}:
213 answers.scan(f, rr(s))
214
215def questions(fuel: Nat, m: Maybe<&2, String>) -> Maybe<&2, String>:
216 match fuel:
217 case 0n:
218 m
219 case 1n+f:
220 questions(f, name.then(m, 4n))
221
222def body.go(an: U32, m: Maybe<&2, String>) -> Maybe<&2, String>:
223 match m:
224 case None{}:
225 None{}
226 case Some{s}:
227 answers.scan(U32.to_nat(an), rr(s))
228
229def body.an(qd: U32, m: Maybe<&2, Cur>) -> Maybe<&2, String>:
230 match m:
231 case None{}:
232 None{}
233 case Some{Cur{an, r}}:
234 body.go(an, questions(U32.to_nat(qd), skip(r, 4n)))
235
236def body.qd(m: Maybe<&2, Cur>) -> Maybe<&2, String>:
237 match m:
238 case None{}:
239 None{}
240 case Some{Cur{qd, r}}:
241 body.an(qd, u16(r))
242
243# §4.1.1: QR set, opcode QUERY, not truncated, RCODE 0.
244def flags.ok(+f: U32) -> Bool:
245 Bool.and(Bool.and(U32.is_eq(U32.and(f, 32768), 32768), U32.is_eq(U32.and(f, 30720), 0)), Bool.and(U32.is_eq(U32.and(f, 512), 0), U32.is_eq(U32.and(f, 15), 0)))
246
247def head.flags.if(r: String, ok: Bool) -> Maybe<&2, String>:
248 match ok:
249 case False{}:
250 None{}
251 case True{}:
252 body.qd(u16(r))
253
254def head.flags(m: Maybe<&2, Cur>) -> Maybe<&2, String>:
255 match m:
256 case None{}:
257 None{}
258 case Some{Cur{+f, r}}:
259 head.flags.if(r, flags.ok(f))
260
261def head.id.if(r: String, ok: Bool) -> Maybe<&2, String>:
262 match ok:
263 case False{}:
264 None{}
265 case True{}:
266 head.flags(u16(r))
267
268def head.id(id: U32, m: Maybe<&2, Cur>) -> Maybe<&2, String>:
269 match m:
270 case None{}:
271 None{}
272 case Some{Cur{got, r}}:
273 head.id.if(r, U32.is_eq(id, got))
274
275# The IPv4 address the response gives for the query with this id.
276def answer(id: U32, msg: String) -> Maybe<&2, String>:
277 head.id(id, u16(msg))
278
279# resolv.conf
280# -----------
281
282def nameservers.add(+line: String, rest: List<&2, String>, hit: Bool) -> List<&2, String>:
283 match hit:
284 case False{}:
285 rest
286 case True{}:
287 Con{String.trim(String.drop(line, 10n)), rest}
288
289def nameservers.go(xs: List<&2, String>) -> List<&2, String>:
290 match xs:
291 case Nil{}:
292 Nil{}
293 case Con{+line, t}:
294 nameservers.add(line, nameservers.go(t), String.starts_with(line, "nameserver"))
295
296# Every nameserver line, in file order.
297def nameservers(conf: String) -> List<&2, String>:
298 nameservers.go(String.lines(conf))
299
300def nameserver.first(xs: List<&2, String>) -> Maybe<&2, String>:
301 match xs:
302 case Nil{}:
303 None{}
304 case Con{n, t}:
305 Some{n}
306
307# The first nameserver line of a resolv.conf.
308def nameserver(conf: String) -> Maybe<&2, String>:
309 nameserver.first(nameservers(conf))
310
311# Resolve
312# -------
313
314def none() -> IO(Maybe<&2, String>):
315 IO.pure(Maybe<&2, String>, None{})
316
317def list.append(xs: List<&2, String>, ys: List<&2, String>) -> List<&2, String>:
318 match xs:
319 case Nil{}:
320 ys
321 case Con{+h, t}:
322 h <> list.append(t, ys)
323
324def list.one(+x: String) -> List<&2, String>:
325 x <> Nil{}
326
327def list.any(+xs: List<&2, String>) -> Bool:
328 match xs:
329 case Nil{}:
330 False{}
331 case Con{+_, +_}:
332 True{}
333
334def list.first(xs: List<&2, String>) -> Maybe<&2, String>:
335 match xs:
336 case Nil{}:
337 None{}
338 case Con{+h, t}:
339 Some{h}
340
341def ipv4.go(s: String) -> Bool:
342 match s:
343 case SNil{}:
344 True{}
345 case SCon{Chr{+c}, t}:
346 Bool.and(Bool.or(U32.is_eq(c, 46), Bool.and(U32.is_le(48, c), U32.is_le(c, 57))), ipv4.go(t))
347
348# Digits and dots; TCP.connect rejects anything else that is not an address.
349def ipv4(+s: String) -> Bool:
350 Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))
351
352def ipv6.ch(+c: U32) -> Bool:
353 Bool.or(
354 Bool.and(U32.is_le(48, c), U32.is_le(c, 57)),
355 Bool.or(
356 Bool.and(U32.is_le(97, c), U32.is_le(c, 102)),
357 Bool.and(U32.is_le(65, c), U32.is_le(c, 70))))
358
359def ipv6.go(s: String) -> Bool:
360 match s:
361 case SNil{}:
362 True{}
363 case SCon{Chr{+c}, t}:
364 Bool.and(Bool.or(U32.is_eq(c, 58), ipv6.ch(c)), ipv6.go(t))
365
366def ipv6.has(s: String) -> Bool:
367 match s:
368 case SNil{}:
369 False{}
370 case SCon{Chr{+c}, t}:
371 Bool.or(U32.is_eq(c, 58), ipv6.has(t))
372
373# Bracket-free IPv6 text; connect validates the address.
374def ipv6(+s: String) -> Bool:
375 Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))
376
377def ip(+s: String) -> Bool:
378 Bool.or(ipv4(s), ipv6(s))
379
380# One attempt's outcome: try again, or this answer (None: no address).
381type Try is Data:
382 Again{}
383 Got{ip: Maybe<&2, String>}
384
385def try.pure(s: Socket, t: Try) -> IO(Socket & Try):
386 IO.pure(Socket & Try, (s, t))
387
388# A datagram from anyone but the nameserver's port 53 is ignored (retried).
389def try.from(s: Socket, +ns: String, id: U32, hpd: String & U32 & String) -> IO(Socket & Try):
390 (h, +p, d) = hpd
391 try.pure(s, Bool.pick(Try, Bool.and(String.eq(h, ns), U32.is_eq(p, 53)), Got{answer(id, d)}, Again{}))
392
393def try.back(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, String & U32 & String>) -> IO(Socket & Try):
394 (s, r) = m
395 match r:
396 case Fail{e}:
397 try.pure(s, Again{})
398 case Done{hpd}:
399 try.from(s, ns, id, hpd)
400
401# §4.2.1 and resolv.conf defaults: 5 s per attempt.
402def try.sent(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Socket & Try):
403 (s, r) = m
404 match r:
405 case Fail{e}:
406 try.pure(s, Again{})
407 case Done{u}:
408 do IO<Socket & Try>:
409 back : Socket & Result<&1, &1, U32 & String, String & U32 & String> <- Wire.recv_from(s, 512, 5000)
410 try.back(ns, id, back)
411
412def try.once(s: Socket, +ns: String, id: U32, q: String) -> IO(Socket & Try):
413 do IO<Socket & Try>:
414 sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send_to(s, ns, 53, q)
415 try.sent(ns, id, sent)
416
417def try.close(s: Socket, r: Maybe<&2, String>) -> IO(Maybe<&2, String>):
418 do IO<Maybe<&2, String>>:
419 Socket.close(s)
420 return r
421
422def tries.end(st: Socket & Try) -> IO(Maybe<&2, String>):
423 (s, t) = st
424 match t:
425 case Got{ip}:
426 try.close(s, ip)
427 case Again{}:
428 try.close(s, None{})
429
430# fuel: attempts left (resolv.conf's default is 2).
431def tries(fuel: Nat, +ns: String, +id: U32, +q: String, st: Socket & Try) -> IO(Maybe<&2, String>):
432 match fuel:
433 case 0n:
434 tries.end(st)
435 case 1n+f:
436 (s, t) = st
437 match t:
438 case Got{ip}:
439 try.close(s, ip)
440 case Again{}:
441 do IO<Maybe<&2, String>>:
442 next : Socket & Try <- try.once(s, ns, id, q)
443 tries(f, ns, id, q, next)
444
445def resolve.sock(ns: String, id: U32, q: String, r: Result<&1, &1, U32 & String, Socket>) -> IO(Maybe<&2, String>):
446 match r:
447 case Fail{e}:
448 none()
449 case Done{s}:
450 tries(2n, ns, id, q, (s, Again{}))
451
452def resolve.q(ns: String, id: U32, q: Maybe<&2, String>) -> IO(Maybe<&2, String>):
453 match q:
454 case None{}:
455 none()
456 case Some{bytes}:
457 do IO<Maybe<&2, String>>:
458 u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0)
459 resolve.sock(ns, id, bytes, u)
460
461# §7.3: a random id makes forged answers harder to land.
462def resolve.id(name: String, ns: String, r: Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&2, String>):
463 match r:
464 case Fail{e}:
465 none()
466 case Done{x}:
467 +id = U32.and(x, 65535)
468 resolve.q(ns, id, query(id, name))
469
470def resolve.ns(name: String, ns: Maybe<&2, String>) -> IO(Maybe<&2, String>):
471 match ns:
472 case None{}:
473 none()
474 case Some{n}:
475 do IO<Maybe<&2, String>>:
476 r : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
477 resolve.id(name, n, r)
478
479# Ask one nameserver. Tests use this; resolve reads /etc/resolv.conf.
480def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>):
481 resolve.ns(host, Some{ns})
482
483def conf.text(r: Result<&1, &1, U32 & String, String>) -> String:
484 match r:
485 case Fail{e}:
486 ""
487 case Done{s}:
488 s
489
490# ponytail: 3 nameservers; a longer resolv.conf ignores the rest
491def resolve.n3(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
492 match xs:
493 case Nil{}:
494 none()
495 case Con{+ns, t}:
496 resolve.at(name, ns)
497
498def resolve.n2b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
499 match ip:
500 case Some{s}:
501 IO.pure(Maybe<&2, String>, Some{s})
502 case None{}:
503 resolve.n3(name, rest)
504
505def resolve.n2(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
506 match xs:
507 case Nil{}:
508 none()
509 case Con{+ns, t}:
510 do IO<Maybe<&2, String>>:
511 ip : Maybe<&2, String> <- resolve.at(name, ns)
512 resolve.n2b(name, t, ip)
513
514def resolve.n1b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
515 match ip:
516 case Some{s}:
517 IO.pure(Maybe<&2, String>, Some{s})
518 case None{}:
519 resolve.n2(name, rest)
520
521def resolve.list(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
522 match xs:
523 case Nil{}:
524 none()
525 case Con{+ns, t}:
526 do IO<Maybe<&2, String>>:
527 ip : Maybe<&2, String> <- resolve.at(name, ns)
528 resolve.n1b(name, t, ip)
529
530def resolve.read(name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
531 (f, r) = m
532 do IO<Maybe<&2, String>>:
533 File.close(f)
534 resolve.list(name, nameservers(conf.text(r)))
535
536def resolve.conf(name: String, r: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
537 match r:
538 case Fail{e}:
539 none()
540 case Done{f}:
541 do IO<Maybe<&2, String>>:
542 m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
543 resolve.read(name, m)
544
545def resolve.dns(name: String) -> IO(Maybe<&2, String>):
546 do IO<Maybe<&2, String>>:
547 f : Result<&1, &1, U32 & String, File> <- File.open("/etc/resolv.conf", "r")
548 resolve.conf(name, f)
549
550
551def hosts.on_line(+name: String, ns: List<&2, String>) -> Bool:
552 match ns:
553 case Nil{}:
554 False{}
555 case Con{+n, t}:
556 Bool.or(String.eq(String.to_lower(n), name), hosts.on_line(name, t))
557
558def hosts.line.all(+name: String, xs: List<&2, String>) -> List<&2, String>:
559 match xs:
560 case Nil{}:
561 Nil{}
562 case Con{+addr, ns}:
563 Bool.pick(List<&2, String>, Bool.and(ip(addr), hosts.on_line(name, ns)), list.one(addr), Nil{})
564
565def hosts.sp(+c: U32, tab: Bool) -> U32:
566 match tab:
567 case True{}:
568 32
569 case False{}:
570 c
571
572def hosts.flat(s: String) -> String:
573 match s:
574 case SNil{}:
575 ""
576 case SCon{Chr{+c}, t}:
577 SCon{Chr{hosts.sp(c, U32.is_eq(c, 9))}, hosts.flat(t)}
578
579def hosts.scan.all(xs: List<&2, String>, +name: String, acc: List<&2, String>) -> List<&2, String>:
580 match xs:
581 case Nil{}:
582 acc
583 case Con{+line, t}:
584 hosts.scan.all(t, name,
585 list.append(acc, hosts.line.all(name, String.split(hosts.flat(line), ' '))))
586
587# Every address for name in an /etc/hosts file. The name is already lowercase.
588def hosts.all(+name: String, text: String) -> List<&2, String>:
589 hosts.scan.all(String.lines(text), name, Nil{})
590
591# First address for name in an /etc/hosts file. The name is already lowercase.
592def hosts(+name: String, text: String) -> Maybe<&2, String>:
593 list.first(hosts.all(name, text))
594
595def lookup.split(+s: String) -> List<&2, String>:
596 List.filter(~String, ~(n => Bool.not(String.is_empty(n))), String.split(s, Chr{0}))
597
598# OS resolver: every address, NUL-separated in getaddrinfo order.
599def lookup.all(host: String) -> IO(Result<&1, &1, U32 & String, String>):
600 import "./effs/dns.c"
601 import "./effs/dns.js"
602
603# Literals and localhost without the OS (for laws and fast paths).
604def resolve.literal.all(+host: String) -> List<&2, String>:
605 Bool.pick(List<&2, String>, ip(host), list.one(host),
606 Bool.pick(List<&2, String>, String.eq(host, "localhost"),
607 ["::1", "127.0.0.1"], Nil{}))
608
609def resolve.literal(+host: String) -> Maybe<&2, String>:
610 list.first(resolve.literal.all(host))
611
612def resolve.all.got(r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
613 match r:
614 case Fail{e}:
615 IO.pure(List<&2, String>, Nil{})
616 case Done{s}:
617 IO.pure(List<&2, String>, lookup.split(s))
618
619def resolve.all.os(+name: String) -> IO(List<&2, String>):
620 do IO<List<&2, String>>:
621 r : Result<&1, &1, U32 & String, String> <- lookup.all(name)
622 resolve.all.got(r)
623
624def resolve.all.dns.one(m: Maybe<&2, String>) -> IO(List<&2, String>):
625 match m:
626 case Some{ip}:
627 IO.pure(List<&2, String>, list.one(ip))
628 case None{}:
629 IO.pure(List<&2, String>, Nil{})
630
631# ponytail: UDP path still asks for A records only
632def resolve.all.dns(+name: String) -> IO(List<&2, String>):
633 do IO<List<&2, String>>:
634 m : Maybe<&2, String> <- resolve.dns(name)
635 resolve.all.dns.one(m)
636
637def resolve.all.from(+name: String, +xs: List<&2, String>) -> IO(List<&2, String>):
638 match xs:
639 case Nil{}:
640 resolve.all.dns(name)
641 case Con{+_, +t}:
642 IO.pure(List<&2, String>, xs)
643
644def resolve.all.text(+name: String, r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
645 match r:
646 case Fail{e}:
647 resolve.all.dns(name)
648 case Done{s}:
649 resolve.all.from(name, hosts.all(name, s))
650
651def resolve.all.opened(+name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
652 (f, r) = m
653 do IO<List<&2, String>>:
654 File.close(f)
655 resolve.all.text(name, r)
656
657def resolve.all.hosts(+name: String, r: Result<&1, &1, U32 & String, File>) -> IO(List<&2, String>):
658 match r:
659 case Fail{e}:
660 resolve.all.dns(name)
661 case Done{f}:
662 do IO<List<&2, String>>:
663 m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
664 resolve.all.opened(name, m)
665
666def resolve.all.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
667 match xs:
668 case Nil{}:
669 resolve.all.os(String.to_lower(host))
670 case Con{+_, +t}:
671 IO.pure(List<&2, String>, xs)
672
673def resolve.all(+host: String) -> IO(List<&2, String>):
674 resolve.all.pick(host, resolve.literal.all(host))
675
676def resolve.all.ask(+name: String) -> IO(List<&2, String>):
677 do IO<List<&2, String>>:
678 f : Result<&1, &1, U32 & String, File> <- File.open("/etc/hosts", "r")
679 resolve.all.hosts(name, f)
680
681def resolve.all.pure.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
682 match xs:
683 case Nil{}:
684 resolve.all.ask(String.to_lower(host))
685 case Con{+_, +t}:
686 IO.pure(List<&2, String>, xs)
687
688def resolve.all.pure(+host: String) -> IO(List<&2, String>):
689 resolve.all.pure.pick(host, resolve.literal.all(host))
690
691def resolve.pure(+host: String) -> IO(Maybe<&2, String>):
692 do IO<Maybe<&2, String>>:
693 xs : List<&2, String> <- resolve.all.pure(host)
694 return list.first(xs)
695
696# First address from resolve.all (getaddrinfo order when the OS resolves).
697def resolve(+host: String) -> IO(Maybe<&2, String>):
698 do IO<Maybe<&2, String>>:
699 xs : List<&2, String> <- resolve.all(host)
700 return list.first(xs)