def tb.bg_vals

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:185

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
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/header.bend as H
import bend-osdev-acpi@0.1.1.0/fields.bend as F
import bend-osdev-acpi@0.1.1.0/bgrt.bend as Bg

185def tb.bg_vals(+h: H.AcpiHeader, +v: U32, +st: U32, +it: U32, +ah: U32, +al: U32, +x: U32, +y: U32) -> {Done{Bg.AcpiBgrt{h, F.AcpiF.u16(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 0n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 2n), F.AcpiF.u8(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 3n), F.AcpiF.u64(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 4n), F.AcpiF.u32(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 12n), F.AcpiF.u32(B.Octets.concat([B.Octets.le16(v), B.Octets.of_list([st, it]), B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le32(x), B.Octets.le32(y)]), 16n)}} == Done{Bg.AcpiBgrt{h, B.low16(v), B.byte(st), B.byte(it), W.W64.from_parts(ah, al), x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}:
186  match v ah al x y:
187    case U32{WCon{v0, WCon{v1, WCon{v2, WCon{v3, WCon{v4, WCon{v5, WCon{v6, WCon{v7, WCon{v8, WCon{v9, WCon{v10, WCon{v11, WCon{v12, WCon{v13, WCon{v14, WCon{v15, WCon{v16, WCon{v17, WCon{v18, WCon{v19, WCon{v20, WCon{v21, WCon{v22, WCon{v23, WCon{v24, WCon{v25, WCon{v26, WCon{v27, WCon{v28, WCon{v29, WCon{v30, WCon{v31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, WCon{x16, WCon{x17, WCon{x18, WCon{x19, WCon{x20, WCon{x21, WCon{x22, WCon{x23, WCon{x24, WCon{x25, WCon{x26, WCon{x27, WCon{x28, WCon{x29, WCon{x30, WCon{x31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
188      {==}