def dec_rt

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2253

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/aml_name.bend as N

2253def dec_rt(+n: N.AmlName, +R: List<&2, U32>, +ok: {N.AmlName.valid(n) == True{} : Bool}) -> {Done{N.AmlNameL{n, R}} == N.nm.dec(B.append(B.mask(N.nm.enc(n)), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
2254  match n:
2255    case N.AmlName{r, u, ss}:
2256      match r:
2257        case True{}:
2258          match u:
2259            case 0n:
2260              %mask_app([92], N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{True{}, 0n, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2261              %pth_dpath(ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok)) : {Done{N.AmlNameL{N.AmlName{True{}, 0n, ss}, R}} == N.nm.named(True{}, 0n, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2262              {==}
2263            case 1n+p:
2264              Empty.absurd({Done{N.AmlNameL{N.AmlName{True{}, 1n+p, ss}, R}} == N.nm.dec(B.append(B.mask(N.nm.enc(N.AmlName{True{}, 1n+p, ss})), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2265        case False{}:
2266          match u:
2267            case 0n:
2268              %mask_app(N.nm.carets(0n), N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2269              %mask_carets(0n) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(B.append(B.append(_, B.mask(N.nm.path(ss))), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2270              %app_assoc(N.nm.carets(0n), B.mask(N.nm.path(ss)), R) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(_) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2271              pth_dec(ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok))
2272            case 1n+p:
2273              %mask_app(N.nm.carets(1n+p), N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2274              %mask_carets(1n+p) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(B.append(B.append(_, B.mask(N.nm.path(ss))), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2275              %app_assoc(N.nm.carets(1n+p), B.mask(N.nm.path(ss)), R) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(_) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2276              ups_rt(1n+p, ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok))