# DNS codec and host lookup. Source: https://github.com/paymog/bend-kit/tree/main/dns
import Base
import ./wire.bend as Wire
import ./deps/bytes.bend as Bytes

# query, answer, and resolve.pure are pure; PROOF.bend covers them, not effs/.
# resolve.all uses the OS resolver (IPv4 and IPv6); resolve keeps the first address.
#   import bend-kit-dns@0.5.0.0/dns.bend as Dns

# Query
# -----

def label.ok(+l: String) -> Bool:
    +n = String.length(l)
    Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 63n))

def label.ascii(s: String) -> Bool:
    match s:
        case SNil{}:
            True{}
        case SCon{Chr{c}, t}:
            Bool.and(U32.is_lt(c, 128), label.ascii(t))

def labels.ok(xs: List<&2, String>) -> Bool:
    match xs:
        case Nil{}:
            True{}
        case Con{+l, t}:
            Bool.and(Bool.and(label.ok(l), label.ascii(l)), labels.ok(t))

# QNAME's length without its final zero octet.
def labels.len(xs: List<&2, String>, +n: U32) -> U32:
    match xs:
        case Nil{}:
            n
        case Con{+l, t}:
            labels.len(t, (n + 1 + U32.from_nat(String.length(l)) : U32))

def label.put(s: String, b: Bytes.Bytes, +i: U32) -> Bytes.Bytes:
    match s:
        case SNil{}:
            b
        case SCon{Chr{c}, t}:
            label.put(t, Bytes.set(b, i, c), (i + 1 : U32))

# Each label as its length octet, then its octets. The zero octet that ends QNAME is already there.
def labels.put(xs: List<&2, String>, b: Bytes.Bytes, +i: U32) -> Bytes.Bytes:
    match xs:
        case Nil{}:
            b
        case Con{+l, t}:
            +n = U32.from_nat(String.length(l))
            labels.put(t, label.put(l, Bytes.set(b, i, n), (i + 1 : U32)), (i + 1 + n : U32))

def query.if(+id: U32, +xs: List<&2, String>, ok: Bool) -> Maybe<&1, Bytes.Bytes>:
    match ok:
        case False{}:
            None{}
        case True{}:
            # header: id, RD, QDCOUNT 1; question: QNAME, QTYPE A, QCLASS IN. Other fields stay zero.
            +n = (labels.len(xs, 0) + 17 : U32)
            Some{Bytes.set.u16be(Bytes.set.u16be(labels.put(xs, Bytes.set.u16be(Bytes.set.u16be(Bytes.set.u16be(Bytes.new(n), 0, id), 2, 256), 4, 1), 12), (n - 4 : U32), 1), (n - 2 : U32), 1)}

def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&1, Bytes.Bytes>:
    query.if(id, xs, labels.ok(xs))

def strip_dot.if(+s: String, dot: Bool) -> String:
    match dot:
        case True{}:
            String.reverse(String.drop(String.reverse(s), 1n))
        case False{}:
            s

def strip_dot(+s: String) -> String:
    strip_dot.if(s, String.ends_with(s, "."))

# RFC 1035 §4.1: a standard query for the A record of name.
def query(id: U32, name: String) -> Maybe<&1, Bytes.Bytes>:
    query.labels(id, String.split(strip_dot(name), '.'))

# Answer
# ------

# One step through a name: go on at the next label, or stop with the offset past the name.
type Step is Data:
    Go{at: U32}
    Stop{end: Maybe<&2, U32>}

# §4.1.4: l, the octet at i, is 0 at the end, 192..255 for a two-octet pointer, 64..191 reserved.
def name.step.of(+i: U32, +l: U32) -> Step:
    Bool.pick(Step, U32.is_eq(l, 0), Stop{Some{(i + 1 : U32)}}, Bool.pick(Step, U32.is_le(192, l), Stop{Some{(i + 2 : U32)}}, Bool.pick(Step, U32.is_le(64, l), Stop{None{}}, Go{(i + 1 + l : U32)})))

def name.step(+i: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & Step:
    (b, m) = r
    match m:
        case None{}:
            (b, Stop{None{}})
        case Some{l}:
            (b, name.step.of(i, l))

def name.walk(fuel: Nat, r: Bytes.Bytes & Step) -> Bytes.Bytes & Maybe<&2, U32>:
    match fuel:
        case 0n:
            (b, s) = r
            (b, None{})
        case 1n+f:
            (b, s) = r
            match s:
                case Stop{end}:
                    (b, end)
                case Go{+at}:
                    name.walk(f, name.step(at, Bytes.get(b, at)))

# The offset past the name at i. §2.3.4: a name is at most 255 octets, so 128 steps are enough.
def name.skip(b: Bytes.Bytes, +i: U32) -> Bytes.Bytes & Maybe<&2, U32>:
    name.walk(128n, name.step(i, Bytes.get(b, i)))

type RR is Data:
    RRBad{}
    RRA{ip: String}
    RRSkip{at: U32}

def dotted(+ip: U32) -> String:
    U32.show(U32.shrn(ip, 24n)) ++ "." ++ U32.show(Bytes.b8(U32.shrn(ip, 16n))) ++ "." ++ U32.show(Bytes.b8(U32.shrn(ip, 8n))) ++ "." ++ U32.show(Bytes.b8(ip))

def rr.a(r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
    (b, m) = r
    match m:
        case None{}:
            (b, RRBad{})
        case Some{ip}:
            (b, RRA{dotted(ip)})

# RDATA at i holds len octets. A skipped record past the end fails at the next read.
def rr.data(a: Bool, b: Bytes.Bytes, +i: U32, +len: U32) -> Bytes.Bytes & RR:
    match a:
        case True{}:
            rr.a(Bytes.get.u32be(b, i))
        case False{}:
            (b, RRSkip{(i + len : U32)})

def rr.len(+o: U32, +ty: U32, +cl: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
    (b, m) = r
    match m:
        case None{}:
            (b, RRBad{})
        case Some{+len}:
            rr.data(Bool.and(Bool.and(U32.is_eq(ty, 1), U32.is_eq(cl, 1)), U32.is_eq(len, 4)), b, (o + 10 : U32), len)

def rr.cl(+o: U32, +ty: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
    (b, m) = r
    match m:
        case None{}:
            (b, RRBad{})
        case Some{cl}:
            rr.len(o, ty, cl, Bytes.get.u16be(b, (o + 8 : U32)))

def rr.ty(+o: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
    (b, m) = r
    match m:
        case None{}:
            (b, RRBad{})
        case Some{ty}:
            rr.cl(o, ty, Bytes.get.u16be(b, (o + 2 : U32)))

def rr.name(r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
    (b, m) = r
    match m:
        case None{}:
            (b, RRBad{})
        case Some{+o}:
            rr.ty(o, Bytes.get.u16be(b, o))

# §4.1.3: NAME, TYPE, CLASS, TTL, RDLENGTH, RDATA.
def rr(b: Bytes.Bytes, +i: U32) -> Bytes.Bytes & RR:
    rr.name(name.skip(b, i))

# fuel = records left. The first A record wins; CNAMEs before it are skipped.
def answers.scan(fuel: Nat, r: Bytes.Bytes & RR) -> Maybe<&2, String>:
    match fuel:
        case 0n:
            None{}
        case 1n+f:
            (b, x) = r
            match x:
                case RRBad{}:
                    None{}
                case RRA{ip}:
                    Some{ip}
                case RRSkip{+at}:
                    answers.scan(f, rr(b, at))

# QTYPE and QCLASS follow the name.
def question.end(r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & Maybe<&2, U32>:
    (b, m) = r
    match m:
        case None{}:
            (b, None{})
        case Some{e}:
            (b, Some{(e + 4 : U32)})

def questions(fuel: Nat, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & Maybe<&2, U32>:
    match fuel:
        case 0n:
            (b, m) = r
            (b, m)
        case 1n+f:
            (b, m) = r
            match m:
                case None{}:
                    (b, None{})
                case Some{+at}:
                    questions(f, question.end(name.skip(b, at)))

def body.go(+an: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
    (b, m) = r
    match m:
        case None{}:
            None{}
        case Some{+at}:
            answers.scan(U32.to_nat(an), rr(b, at))

# The 12-octet header ends with NSCOUNT and ARCOUNT; the questions follow.
def body.an(+qd: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
    (b, m) = r
    match m:
        case None{}:
            None{}
        case Some{an}:
            body.go(an, questions(U32.to_nat(qd), (b, Some{12})))

def body.qd(r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
    (b, m) = r
    match m:
        case None{}:
            None{}
        case Some{qd}:
            body.an(qd, Bytes.get.u16be(b, 6))

# §4.1.1: QR set, opcode QUERY, not truncated, RCODE 0.
def flags.ok(+f: U32) -> Bool:
    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)))

def head.flags.if(ok: Bool, b: Bytes.Bytes) -> Maybe<&2, String>:
    match ok:
        case False{}:
            None{}
        case True{}:
            body.qd(Bytes.get.u16be(b, 4))

def head.flags(r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
    (b, m) = r
    match m:
        case None{}:
            None{}
        case Some{f}:
            head.flags.if(flags.ok(f), b)

def head.id.if(ok: Bool, b: Bytes.Bytes) -> Maybe<&2, String>:
    match ok:
        case False{}:
            None{}
        case True{}:
            head.flags(Bytes.get.u16be(b, 2))

def head.id(+id: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
    (b, m) = r
    match m:
        case None{}:
            None{}
        case Some{got}:
            head.id.if(U32.is_eq(id, got), b)

# The IPv4 address the response gives for the query with this id.
def answer(id: U32, msg: Bytes.Bytes) -> Maybe<&2, String>:
    head.id(id, Bytes.get.u16be(msg, 0))

# resolv.conf
# -----------

def nameservers.add(+line: String, rest: List<&2, String>, hit: Bool) -> List<&2, String>:
    match hit:
        case False{}:
            rest
        case True{}:
            Con{String.trim(String.drop(line, 10n)), rest}

def nameservers.go(xs: List<&2, String>) -> List<&2, String>:
    match xs:
        case Nil{}:
            Nil{}
        case Con{+line, t}:
            nameservers.add(line, nameservers.go(t), String.starts_with(line, "nameserver"))

# Every nameserver line, in file order.
def nameservers(conf: String) -> List<&2, String>:
    nameservers.go(String.lines(conf))

def nameserver.first(xs: List<&2, String>) -> Maybe<&2, String>:
    match xs:
        case Nil{}:
            None{}
        case Con{n, t}:
            Some{n}

# The first nameserver line of a resolv.conf.
def nameserver(conf: String) -> Maybe<&2, String>:
    nameserver.first(nameservers(conf))

# Resolve
# -------

def none() -> IO(Maybe<&2, String>):
    IO.pure(Maybe<&2, String>, None{})

def list.append(xs: List<&2, String>, ys: List<&2, String>) -> List<&2, String>:
    match xs:
        case Nil{}:
            ys
        case Con{+h, t}:
            h <> list.append(t, ys)

def list.one(+x: String) -> List<&2, String>:
    x <> Nil{}

def list.any(+xs: List<&2, String>) -> Bool:
    match xs:
        case Nil{}:
            False{}
        case Con{+_, +_}:
            True{}

def list.first(xs: List<&2, String>) -> Maybe<&2, String>:
    match xs:
        case Nil{}:
            None{}
        case Con{+h, t}:
            Some{h}

def ipv4.go(s: String) -> Bool:
    match s:
        case SNil{}:
            True{}
        case SCon{Chr{+c}, t}:
            Bool.and(Bool.or(U32.is_eq(c, 46), Bool.and(U32.is_le(48, c), U32.is_le(c, 57))), ipv4.go(t))

# Digits and dots; TCP.connect rejects anything else that is not an address.
def ipv4(+s: String) -> Bool:
    Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))

def ipv6.ch(+c: U32) -> Bool:
    Bool.or(
        Bool.and(U32.is_le(48, c), U32.is_le(c, 57)),
        Bool.or(
            Bool.and(U32.is_le(97, c), U32.is_le(c, 102)),
            Bool.and(U32.is_le(65, c), U32.is_le(c, 70))))

def ipv6.go(s: String) -> Bool:
    match s:
        case SNil{}:
            True{}
        case SCon{Chr{+c}, t}:
            Bool.and(Bool.or(U32.is_eq(c, 58), ipv6.ch(c)), ipv6.go(t))

def ipv6.has(s: String) -> Bool:
    match s:
        case SNil{}:
            False{}
        case SCon{Chr{+c}, t}:
            Bool.or(U32.is_eq(c, 58), ipv6.has(t))

# Bracket-free IPv6 text; connect validates the address.
def ipv6(+s: String) -> Bool:
    Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))

def ip(+s: String) -> Bool:
    Bool.or(ipv4(s), ipv6(s))

# One attempt's outcome: try again, or this answer (None: no address).
type Try is Data:
    Again{}
    Got{ip: Maybe<&2, String>}

def try.pure(s: Socket, t: Try) -> IO(Socket & Try):
    IO.pure(Socket & Try, (s, t))

# A datagram from anyone but the nameserver's port 53 is ignored (retried).
def try.from(s: Socket,
             +ns: String,
             id: U32,
             hpd: String & U32 & (U32 & Array<U32>)) -> IO(Socket & Try):
    (h, +p, d) = hpd
    (n, w) = d
    try.pure(s, Bool.pick(Try, Bool.and(String.eq(h, ns), U32.is_eq(p, 53)), Got{answer(id, Bytes.Bytes{n, w})}, Again{}))

def try.back(ns: String,
             id: U32,
             m: Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)>) -> IO(Socket & Try):
    (s, r) = m
    match r:
        case Fail{e}:
            try.pure(s, Again{})
        case Done{hpd}:
            try.from(s, ns, id, hpd)

# §4.2.1 and resolv.conf defaults: 5 s per attempt.
def try.sent(ns: String,
             id: U32,
             m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Socket & Try):
    (s, r) = m
    match r:
        case Fail{e}:
            try.pure(s, Again{})
        case Done{u}:
            do IO<Socket & Try>:
                back : Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)>
                    <- Wire.recv_from.words(s, 512, 5000)
                try.back(ns, id, back)

# Bytes cannot be copied, so each attempt builds its own query. A name that query rejects ends the tries.
def try.send(s: Socket, +ns: String, id: U32, q: Maybe<&1, Bytes.Bytes>) -> IO(Socket & Try):
    match q:
        case None{}:
            try.pure(s, Got{None{}})
        case Some{Bytes.Bytes{n, w}}:
            do IO<Socket & Try>:
                sent : Socket & Result<&1, &1, U32 & String, Unit>
                    <- Wire.send_to.words(s, ns, 53, n, w)
                try.sent(ns, id, sent)

def try.once(s: Socket, +ns: String, +id: U32, name: String) -> IO(Socket & Try):
    try.send(s, ns, id, query(id, name))

def try.close(s: Socket, r: Maybe<&2, String>) -> IO(Maybe<&2, String>):
    do IO<Maybe<&2, String>>:
        Socket.close(s)
        return r

def tries.end(st: Socket & Try) -> IO(Maybe<&2, String>):
    (s, t) = st
    match t:
        case Got{ip}:
            try.close(s, ip)
        case Again{}:
            try.close(s, None{})

# fuel: attempts left (resolv.conf's default is 2).
def tries(fuel: Nat,
          +ns: String,
          +id: U32,
          +name: String,
          st: Socket & Try) -> IO(Maybe<&2, String>):
    match fuel:
        case 0n:
            tries.end(st)
        case 1n+f:
            (s, t) = st
            match t:
                case Got{ip}:
                    try.close(s, ip)
                case Again{}:
                    do IO<Maybe<&2, String>>:
                        next : Socket & Try <- try.once(s, ns, id, name)
                        tries(f, ns, id, name, next)

def resolve.sock(ns: String,
                 id: U32,
                 name: String,
                 r: Result<&1, &1, U32 & String, Socket>) -> IO(Maybe<&2, String>):
    match r:
        case Fail{e}:
            none()
        case Done{s}:
            tries(2n, ns, id, name, (s, Again{}))

# §7.3: a random id makes forged answers harder to land.
def resolve.id(name: String,
               ns: String,
               r: Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&2, String>):
    match r:
        case Fail{e}:
            none()
        case Done{x}:
            do IO<Maybe<&2, String>>:
                u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0)
                resolve.sock(ns, U32.and(x, 65535), name, u)

def resolve.ns(name: String, ns: Maybe<&2, String>) -> IO(Maybe<&2, String>):
    match ns:
        case None{}:
            none()
        case Some{n}:
            do IO<Maybe<&2, String>>:
                r : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
                resolve.id(name, n, r)

# Ask one nameserver. Tests use this; resolve reads /etc/resolv.conf.
def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>):
    resolve.ns(host, Some{ns})

# HTTP adapter path: one DNS attempt with a caller-provided receive deadline.
def try.sent.timeout(ns: String,
                     id: U32,
                     ms: U32,
                     result: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Socket & Try):
    (sock, sent) = result
    match sent:
        case Fail{error}:
            try.pure(sock, Again{})
        case Done{unit}:
            do IO<Socket & Try>:
                reply : Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)>
                    <- Wire.recv_from.words(sock, 512, ms)
                try.back(ns, id, reply)

def try.send.timeout(sock: Socket,
                     +ns: String,
                     id: U32,
                     ms: U32,
                     query_bytes: Maybe<&1, Bytes.Bytes>) -> IO(Socket & Try):
    match query_bytes:
        case None{}: try.pure(sock, Got{None{}})
        case Some{Bytes.Bytes{n, w}}:
            do IO<Socket & Try>:
                result : Socket & Result<&1, &1, U32 & String, Unit>
                    <- Wire.send_to.words(sock, ns, 53, n, w)
                try.sent.timeout(ns, id, ms, result)

def try.once.timeout(sock: Socket,
                     +ns: String,
                     +id: U32,
                     +name: String,
                     ms: U32) -> IO(Socket & Try):
    try.send.timeout(sock, ns, id, ms, query(id, name))

def resolve.sock.timeout.end(result: Socket & Try) -> IO(Maybe<&2, String>):
    (sock, outcome) = result
    match outcome:
        case Got{ip}:
            try.close(sock, ip)
        case Again{}:
            try.close(sock, None{})

def resolve.sock.timeout(ns: String,
                         id: U32,
                         name: String,
                         ms: U32,
                         result: Result<&1, &1, U32 & String, Socket>) -> IO(Maybe<&2, String>):
    match result:
        case Fail{error}: none()
        case Done{sock}:
            do IO<Maybe<&2, String>>:
                attempt : Socket & Try <- try.once.timeout(sock, ns, id, name, ms)
                resolve.sock.timeout.end(attempt)

def resolve.id.timeout(name: String,
                       ns: String,
                       ms: U32,
                       result: Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&2, String>):
    match result:
        case Fail{error}: none()
        case Done{random}:
            do IO<Maybe<&2, String>>:
                bound : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0)
                resolve.sock.timeout(ns, U32.and(random, 65535), name, ms, bound)

def resolve.ns.timeout(name: String, ns: String, ms: U32) -> IO(Maybe<&2, String>):
    do IO<Maybe<&2, String>>:
        random : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
        resolve.id.timeout(name, ns, ms, random)

def resolve.at.timeout(+host: String, ns: String, ms: U32) -> IO(Maybe<&2, String>):
    resolve.ns.timeout(host, ns, ms)

def resolve.conf.server(name: String, ms: U32, server: Maybe<&2, String>) -> IO(Maybe<&2, String>):
    match server:
        case None{}: none()
        case Some{address}: resolve.at.timeout(name, address, ms)

def resolve.conf.contents(name: String,
                          ms: U32,
                          contents: Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
    match contents:
        case Fail{error}: none()
        case Done{text}:
            resolve.conf.server(name, ms, nameserver(text))

def resolve.conf.read(name: String,
                      ms: U32,
                      result: File & Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
    (file, contents) = result
    do IO<Maybe<&2, String>>:
        File.close(file)
        resolve.conf.contents(name, ms, contents)

def resolve.conf.timeout(name: String,
                         result: Result<&1, &1, U32 & String, File>,
                         ms: U32) -> IO(Maybe<&2, String>):
    match result:
        case Fail{error}: none()
        case Done{file}:
            do IO<Maybe<&2, String>>:
                conf : File & Result<&1, &1, U32 & String, String> <- File.read(file, 65536)
                resolve.conf.read(name, ms, conf)

def resolve.timeout(+name: String, ms: U32) -> IO(Maybe<&2, String>):
    do IO<Maybe<&2, String>>:
        file : Result<&1, &1, U32 & String, File> <- File.open("/etc/resolv.conf", "r")
        resolve.conf.timeout(name, file, ms)

def conf.text(r: Result<&1, &1, U32 & String, String>) -> String:
    match r:
        case Fail{e}:
            ""
        case Done{s}:
            s

# ponytail: 3 nameservers; a longer resolv.conf ignores the rest
def resolve.n3(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
    match xs:
        case Nil{}:
            none()
        case Con{+ns, t}:
            resolve.at(name, ns)

def resolve.n2b(+name: String,
                rest: List<&2, String>,
                ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
    match ip:
        case Some{s}:
            IO.pure(Maybe<&2, String>, Some{s})
        case None{}:
            resolve.n3(name, rest)

def resolve.n2(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
    match xs:
        case Nil{}:
            none()
        case Con{+ns, t}:
            do IO<Maybe<&2, String>>:
                ip : Maybe<&2, String> <- resolve.at(name, ns)
                resolve.n2b(name, t, ip)

def resolve.n1b(+name: String,
                rest: List<&2, String>,
                ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
    match ip:
        case Some{s}:
            IO.pure(Maybe<&2, String>, Some{s})
        case None{}:
            resolve.n2(name, rest)

def resolve.list(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
    match xs:
        case Nil{}:
            none()
        case Con{+ns, t}:
            do IO<Maybe<&2, String>>:
                ip : Maybe<&2, String> <- resolve.at(name, ns)
                resolve.n1b(name, t, ip)

def resolve.read(name: String,
                 m: File & Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
    (f, r) = m
    do IO<Maybe<&2, String>>:
        File.close(f)
        resolve.list(name, nameservers(conf.text(r)))

def resolve.conf(name: String, r: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
    match r:
        case Fail{e}:
            none()
        case Done{f}:
            do IO<Maybe<&2, String>>:
                m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
                resolve.read(name, m)

def resolve.dns(name: String) -> IO(Maybe<&2, String>):
    do IO<Maybe<&2, String>>:
        f : Result<&1, &1, U32 & String, File> <- File.open("/etc/resolv.conf", "r")
        resolve.conf(name, f)


def hosts.on_line(+name: String, ns: List<&2, String>) -> Bool:
    match ns:
        case Nil{}:
            False{}
        case Con{+n, t}:
            Bool.or(String.eq(String.to_lower(n), name), hosts.on_line(name, t))

def hosts.line.all(+name: String, xs: List<&2, String>) -> List<&2, String>:
    match xs:
        case Nil{}:
            Nil{}
        case Con{+addr, ns}:
            Bool.pick(List<&2, String>, Bool.and(ip(addr), hosts.on_line(name, ns)), list.one(addr), Nil{})

def hosts.sp(+c: U32, tab: Bool) -> U32:
    match tab:
        case True{}:
            32
        case False{}:
            c

def hosts.flat(s: String) -> String:
    match s:
        case SNil{}:
            ""
        case SCon{Chr{+c}, t}:
            SCon{Chr{hosts.sp(c, U32.is_eq(c, 9))}, hosts.flat(t)}

def hosts.scan.all(xs: List<&2, String>, +name: String, acc: List<&2, String>) -> List<&2, String>:
    match xs:
        case Nil{}:
            acc
        case Con{+line, t}:
            hosts.scan.all(t, name,
                list.append(acc, hosts.line.all(name, String.split(hosts.flat(line), ' '))))

# Every address for name in an /etc/hosts file. The name is already lowercase.
def hosts.all(+name: String, text: String) -> List<&2, String>:
    hosts.scan.all(String.lines(text), name, Nil{})

# First address for name in an /etc/hosts file. The name is already lowercase.
def hosts(+name: String, text: String) -> Maybe<&2, String>:
    list.first(hosts.all(name, text))

def lookup.split(+s: String) -> List<&2, String>:
    List.filter(~String, ~(n => Bool.not(String.is_empty(n))), String.split(s, Chr{0}))

# OS resolver: every address, NUL-separated in getaddrinfo order.
def lookup.all(host: String) -> IO(Result<&1, &1, U32 & String, String>):
    import "./dns_eff/dns.c"
    import "./dns_eff/dns.js"

# Literals and localhost without the OS (for laws and fast paths).
def resolve.literal.all(+host: String) -> List<&2, String>:
    Bool.pick(List<&2, String>, ip(host), list.one(host),
        Bool.pick(List<&2, String>, String.eq(host, "localhost"),
            ["::1", "127.0.0.1"], Nil{}))

def resolve.literal(+host: String) -> Maybe<&2, String>:
    list.first(resolve.literal.all(host))

def resolve.all.got(r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
    match r:
        case Fail{e}:
            IO.pure(List<&2, String>, Nil{})
        case Done{s}:
            IO.pure(List<&2, String>, lookup.split(s))

def resolve.all.os(+name: String) -> IO(List<&2, String>):
    do IO<List<&2, String>>:
        r : Result<&1, &1, U32 & String, String> <- lookup.all(name)
        resolve.all.got(r)

def resolve.all.dns.one(m: Maybe<&2, String>) -> IO(List<&2, String>):
    match m:
        case Some{ip}:
            IO.pure(List<&2, String>, list.one(ip))
        case None{}:
            IO.pure(List<&2, String>, Nil{})

# ponytail: UDP path still asks for A records only
def resolve.all.dns(+name: String) -> IO(List<&2, String>):
    do IO<List<&2, String>>:
        m : Maybe<&2, String> <- resolve.dns(name)
        resolve.all.dns.one(m)

def resolve.all.from(+name: String, +xs: List<&2, String>) -> IO(List<&2, String>):
    match xs:
        case Nil{}:
            resolve.all.dns(name)
        case Con{+_, +t}:
            IO.pure(List<&2, String>, xs)

def resolve.all.text(+name: String,
                     r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
    match r:
        case Fail{e}:
            resolve.all.dns(name)
        case Done{s}:
            resolve.all.from(name, hosts.all(name, s))

def resolve.all.opened(+name: String,
                       m: File & Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
    (f, r) = m
    do IO<List<&2, String>>:
        File.close(f)
        resolve.all.text(name, r)

def resolve.all.hosts(+name: String, r: Result<&1, &1, U32 & String, File>) -> IO(List<&2, String>):
    match r:
        case Fail{e}:
            resolve.all.dns(name)
        case Done{f}:
            do IO<List<&2, String>>:
                m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
                resolve.all.opened(name, m)

def resolve.all.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
    match xs:
        case Nil{}:
            resolve.all.os(String.to_lower(host))
        case Con{+_, +t}:
            IO.pure(List<&2, String>, xs)

def resolve.all(+host: String) -> IO(List<&2, String>):
    resolve.all.pick(host, resolve.literal.all(host))

def resolve.all.ask(+name: String) -> IO(List<&2, String>):
    do IO<List<&2, String>>:
        f : Result<&1, &1, U32 & String, File> <- File.open("/etc/hosts", "r")
        resolve.all.hosts(name, f)

def resolve.all.pure.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
    match xs:
        case Nil{}:
            resolve.all.ask(String.to_lower(host))
        case Con{+_, +t}:
            IO.pure(List<&2, String>, xs)

def resolve.all.pure(+host: String) -> IO(List<&2, String>):
    resolve.all.pure.pick(host, resolve.literal.all(host))

def resolve.pure(+host: String) -> IO(Maybe<&2, String>):
    do IO<Maybe<&2, String>>:
        xs : List<&2, String> <- resolve.all.pure(host)
        return list.first(xs)

# First address from resolve.all (getaddrinfo order when the OS resolves).
def resolve(+host: String) -> IO(Maybe<&2, String>):
    do IO<Maybe<&2, String>>:
        xs : List<&2, String> <- resolve.all(host)
        return list.first(xs)