aml_interp.bend

bend-osdev-acpi@0.1.1.0 · 2,945 lines · 334 definitions

1# bend-osdev-acpi, aml_interp.bend: the AML interpreter (ACPI 6.5, chapter
2# 19, ASL Reference, for what each operator does; chapter 20, AML
3# Specification, for its encoding).
4#
5# The interpreter is a small-step machine over the AML bytes: a cursor (the
6# bytes left in the term list being run), a stack of frames (the operator
7# whose operands are being read, the If, While, method call or package
8# being run), and the world it changes (the method's Arg and Local values,
9# the namespace, the operation-region host, notifications and the Debug
10# log). Each step reads one opcode, or gives one value to the frame on top.
11# AmlM.run stops after its step bound whatever the AML does (LAWS.bend:
12# run_steps_bound), so a method that loops for ever ends with
13# AcpiAmlStepLimit.
14#
15# Operation regions are reached through the host, a template argument
16# (aml_host.bend): ~H: Data, ~io: H -> AmlHostOp -> Result<..., AmlHostAns<H>>.
17#
18# Method calls take their argument count from the namespace when they are
19# reached, which is how AML is meant to be read (a MethodInvocation is a
20# NameString followed by as many TermArgs as the method takes, 20.2.5.4).
21# What is not supported is listed in README.md.
22import Base
23import bend-osdev-word64@0.1.1.0/word64.bend as W
24import bend-osdev-bytes@0.1.1.0/bytes.bend as B
25import bend-osdev-acpi@0.1.1.0/error.bend as E
26import bend-osdev-acpi@0.1.1.0/aml_pkglength.bend as K
27import bend-osdev-acpi@0.1.1.0/aml_name.bend as N
28import bend-osdev-acpi@0.1.1.0/aml_value.bend as V
29import bend-osdev-acpi@0.1.1.0/aml_ns.bend as S
30import bend-osdev-acpi@0.1.1.0/aml_host.bend as Hs
31import bend-osdev-acpi@0.1.1.0/aml_field.bend as F
32
33# Options
34
35type AmlOptions is Data:
36  # the strings \_OSI answers True for; \_OS and \_REV
37  AmlOptions{osi: List<&2, String>, os: String, rev: U32}
38
39# \_OSI answers True for the Windows releases firmware tests for, as
40# operating systems commonly do, and for "Module Device" and "Processor
41# Device"; \_OS is "Microsoft Windows NT"; \_REV is 2 (ACPI 6.5, 5.7.2)
42def AmlOptions.default() -> AmlOptions:
43  AmlOptions{["Windows 2000", "Windows 2001", "Windows 2001 SP1", "Windows 2001 SP2", "Windows 2001.1", "Windows 2001.1 SP1", "Windows 2006", "Windows 2006 SP1", "Windows 2006.1", "Windows 2009", "Windows 2012", "Windows 2013", "Windows 2015", "Windows 2016", "Windows 2017", "Windows 2017.2", "Windows 2018", "Windows 2018.2", "Windows 2019", "Windows 2020", "Windows 2021", "Windows 2022", "Module Device", "Processor Device", "3.0 Thermal Model", "Extended Address Space Descriptor"], "Microsoft Windows NT", 2}
44
45# The machine
46
47# the bytes left in the current term list: the list from here, and how
48# many of its bytes belong to the list
49type AmlCur is Data:
50  AmlCur{code: List<&2, U32>, lim: Nat}
51
52# what an operand must be
53type AmlArgK is Data:
54  # a TermArg: a value
55  AmlKTerm{}
56  # a Target or SuperName: a location
57  AmlKTarget{}
58  # a source (Index, SizeOf, ObjectType, CreateField): its location if it
59  # has one, its value otherwise
60  AmlKBase{}
61  # CondRefOf's operand: a location, or nothing if the name is undefined
62  AmlKCond{}
63  # a package element: a value, or a name as a reference (not run)
64  AmlKElem{}
65  # immediate data
66  AmlKByte{}
67  AmlKWord{}
68  AmlKDWord{}
69  # a NameString, as the path it names from the current scope
70  AmlKName{}
71
72type AmlOp is Data:
73  # an operator, by opcode (an extended opcode 0x5B xx is 256 + xx)
74  AmlOpCode{code: U32}
75  AmlOpCall{path: String, nargs: Nat}
76  AmlOpOsi{}
77
78type AmlCtx is Data:
79  # the scope names resolve from; Arg0-6; Local0-7; the names this method
80  # call created (removed when it returns)
81  AmlCtx{scope: String, args: List<&2, V.AmlValue>, locals: List<&2, V.AmlValue>, temps: List<&2, String>}
82
83type AmlFrame is Data:
84  AmlFArgs{op: AmlOp, got: List<&2, V.AmlValue>, todo: List<&2, AmlArgK>}
85  # a nested term list (Scope, Device, Else, ...): where to resume, and the
86  # scope to restore
87  AmlFSeq{after: AmlCur, scope: String}
88  # an If whose predicate is being read
89  AmlFIf{after: AmlCur}
90  # an If whose body is running
91  AmlFIfBody{after: AmlCur}
92  # a While: its predicate's start, what follows it, and whether the body
93  # is running (else the predicate is being read)
94  AmlFWhile{start: AmlCur, after: AmlCur, body: Bool}
95  # a method call's return point
96  AmlFCall{ctx: AmlCtx, back: AmlCur}
97  # a Buffer whose size is being read; the rest of its package is its
98  # initializer
99  AmlFBuffer{after: AmlCur}
100  # a Package: its NumElements, the elements so far (last first)
101  AmlFPkg{count: Nat, got: List<&2, V.AmlValue>, after: AmlCur}
102  # a VarPackage whose count is being read
103  AmlFVarPkg{after: AmlCur}
104  # the bottom: the definition block, or the method evaluated
105  AmlFTop{}
106
107type AmlMode is Data:
108  # the next term of a term list, or the list's end
109  AmlMExec{}
110  # one operand, of this kind
111  AmlMEval{k: AmlArgK}
112  # a value for the frame on top
113  AmlMGive{v: V.AmlValue}
114  AmlMDone{v: V.AmlValue}
115  AmlMFail{e: E.AcpiError}
116
117# a Notify: the object's path and the value
118type AmlNote is Data:
119  AmlNote{path: String, value: W.W64}
120
121type AmlEnv is Data:
122  # wide: 64-bit integers; notes and debug: last first; clock: Timer, in
123  # 100 ns units (Sleep and Stall advance it)
124  AmlEnv{wide: Bool, opts: AmlOptions, notes: List<&2, AmlNote>, debug: List<&2, V.AmlValue>, clock: W.W64}
125
126type AmlWorld<-H: Data> is Data:
127  AmlWorld{ctx: AmlCtx, ns: S.AmlNs, host: H, env: AmlEnv}
128
129type AmlMachine<-H: Data> is Data:
130  AmlMachine{mode: AmlMode, cur: AmlCur, frames: List<&2, AmlFrame>, w: AmlWorld<H>}
131
132# a value read, and the world after reading it
133type AmlRead<-H: Data> is Data:
134  AmlRead{w: AmlWorld<H>, v: V.AmlValue}
135
136def AmlMachine.mode(-H: Data, m: AmlMachine<H>) -> AmlMode:
137  match m:
138    case AmlMachine{md, c, fs, w}:
139      md
140
141def AmlMachine.world(-H: Data, m: AmlMachine<H>) -> AmlWorld<H>:
142  match m:
143    case AmlMachine{md, c, fs, w}:
144      w
145
146# the machine has stopped: Done or Fail
147def AmlMachine.halted(-H: Data, m: AmlMachine<H>) -> Bool:
148  match m:
149    case AmlMachine{AmlMDone{v}, c, fs, w}:
150      True{}
151    case AmlMachine{AmlMFail{e}, c, fs, w}:
152      True{}
153    case AmlMachine{md, c, fs, w}:
154      False{}
155
156def in.fail(-H: Data, +e: E.AcpiError, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
157  AmlMachine{AmlMFail{e}, c, fs, w}
158
159# World parts
160
161def AmlWorld.ctx(-H: Data, w: AmlWorld<H>) -> AmlCtx:
162  match w:
163    case AmlWorld{c, n, h, e}:
164      c
165
166def AmlWorld.ns(-H: Data, w: AmlWorld<H>) -> S.AmlNs:
167  match w:
168    case AmlWorld{c, n, h, e}:
169      n
170
171def AmlWorld.env(-H: Data, w: AmlWorld<H>) -> AmlEnv:
172  match w:
173    case AmlWorld{c, n, h, e}:
174      e
175
176def AmlWorld.host(-H: Data, w: AmlWorld<H>) -> H:
177  match w:
178    case AmlWorld{c, n, h, e}:
179      h
180
181def in.scope(-H: Data, w: AmlWorld<H>) -> String:
182  match w:
183    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
184      s
185
186def in.wide(-H: Data, w: AmlWorld<H>) -> Bool:
187  match w:
188    case AmlWorld{c, n, h, AmlEnv{wd, o, nt, d, cl}}:
189      wd
190
191def in.with_ns(-H: Data, w: AmlWorld<H>, n: S.AmlNs) -> AmlWorld<H>:
192  match w:
193    case AmlWorld{c, n0, h, e}:
194      AmlWorld{c, n, h, e}
195
196def in.with_host(-H: Data, w: AmlWorld<H>, h: H) -> AmlWorld<H>:
197  match w:
198    case AmlWorld{c, n, h0, e}:
199      AmlWorld{c, n, h, e}
200
201def in.with_ctx(-H: Data, w: AmlWorld<H>, c: AmlCtx) -> AmlWorld<H>:
202  match w:
203    case AmlWorld{c0, n, h, e}:
204      AmlWorld{c, n, h, e}
205
206def in.with_env(-H: Data, w: AmlWorld<H>, e: AmlEnv) -> AmlWorld<H>:
207  match w:
208    case AmlWorld{c, n, h, e0}:
209      AmlWorld{c, n, h, e}
210
211def in.with_scope(-H: Data, w: AmlWorld<H>, s: String) -> AmlWorld<H>:
212  match w:
213    case AmlWorld{AmlCtx{s0, a, l, t}, n, h, e}:
214      AmlWorld{AmlCtx{s, a, l, t}, n, h, e}
215
216# a name created: in the namespace, and among the method call's names
217def in.define(-H: Data, w: AmlWorld<H>, +p: String, o: S.AmlObject) -> AmlWorld<H>:
218  match w:
219    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
220      AmlWorld{AmlCtx{s, a, l, Con{p, t}}, S.AmlNs.set(n, p, o), h, e}
221
222def in.note(-H: Data, w: AmlWorld<H>, nt: AmlNote) -> AmlWorld<H>:
223  match w:
224    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
225      AmlWorld{c, n, h, AmlEnv{wd, o, Con{nt, nts}, d, cl}}
226
227def in.debug(-H: Data, w: AmlWorld<H>, v: V.AmlValue) -> AmlWorld<H>:
228  match w:
229    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
230      AmlWorld{c, n, h, AmlEnv{wd, o, nts, Con{v, d}, cl}}
231
232def in.tick(-H: Data, w: AmlWorld<H>, +dt: W.W64) -> AmlWorld<H>:
233  match w:
234    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
235      AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, W.W64.add(cl, dt)}}
236
237def in.clock(-H: Data, w: AmlWorld<H>) -> W.W64:
238  match w:
239    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
240      cl
241
242def in.opts(-H: Data, w: AmlWorld<H>) -> AmlOptions:
243  match w:
244    case AmlWorld{c, n, h, AmlEnv{wd, o, nts, d, cl}}:
245      o
246
247# Decoding: reading from the cursor
248
249type AmlB is Data:
250  AmlB{b: U32, cur: AmlCur}
251
252type AmlPkgC is Data:
253  # the package's contents, and what follows the package
254  AmlPkgC{body: AmlCur, after: AmlCur}
255
256type AmlNameC is Data:
257  AmlNameC{name: N.AmlName, cur: AmlCur}
258
259def cur.byte(c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlB>:
260  match c:
261    case AmlCur{code, lim}:
262      match code lim:
263        case Con{h, t} 1n+p:
264          Done{AmlB{h, AmlCur{t, p}}}
265        case _ _:
266          Fail{E.AcpiAmlTruncated{}}
267
268def cur.at_end(c: AmlCur) -> Bool:
269  match c:
270    case AmlCur{code, lim}:
271      Nat.is_eq(lim, 0n)
272
273# the next byte, if the list has one
274def cur.peek(c: AmlCur) -> Maybe<&2, U32>:
275  match c:
276    case AmlCur{code, lim}:
277      match lim:
278        case 0n:
279          None{}
280        case 1n+p:
281          List.head(&2, U32, code)
282
283def cur.skip(+n: Nat, c: AmlCur) -> AmlCur:
284  match c:
285    case AmlCur{code, lim}:
286      AmlCur{B.drop(n, code), Nat.sub(lim, n)}
287
288def cur.take(+n: Nat, c: AmlCur) -> B.Octets:
289  match c:
290    case AmlCur{code, lim}:
291      B.Octets.of_list(B.take.fast(n, code))
292
293def cur.len(c: AmlCur) -> Nat:
294  match c:
295    case AmlCur{code, lim}:
296      lim
297
298def cur.pkg.k(ok: Bool, +inner: Nat, rest: List<&2, U32>, +outer: Nat) -> Result<&2, &2, E.AcpiError, AmlPkgC>:
299  match ok:
300    case False{}:
301      Fail{E.AcpiAmlBadPkgLength{}}
302    case True{}:
303      +r = rest
304      Done{AmlPkgC{AmlCur{r, inner}, AmlCur{B.drop(inner, r), outer}}}
305
306def cur.pkg.go(r: Result<&2, &2, E.AcpiError, K.AmlPkgL>, +lim: Nat) -> Result<&2, &2, E.AcpiError, AmlPkgC>:
307  match r:
308    case Fail{e}:
309      Fail{e}
310    case Done{K.AmlPkgL{v, +size, rest}}:
311      +total = U32.to_nat(v)
312      cur.pkg.k(Bool.and(Nat.is_le(size, total), Nat.is_le(total, lim)), Nat.sub(total, size), rest, Nat.sub(lim, total))
313
314# a PkgLength and the package it covers (the value counts the PkgLength's
315# own bytes); AcpiAmlBadPkgLength if it runs past the enclosing list
316def cur.pkg(c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlPkgC>:
317  match c:
318    case AmlCur{+code, +lim}:
319      cur.pkg.go(K.pk.dec(code), lim)
320
321def cur.name.fit(ok: Bool, n: N.AmlName, rest: List<&2, U32>, left: Nat) -> Result<&2, &2, E.AcpiError, AmlNameC>:
322  match ok:
323    case False{}:
324      Fail{E.AcpiAmlTruncated{}}
325    case True{}:
326      Done{AmlNameC{n, AmlCur{rest, left}}}
327
328def cur.name.k(ok: Bool, +n: N.AmlName, +size: Nat, rest: List<&2, U32>, +lim: Nat) -> Result<&2, &2, E.AcpiError, AmlNameC>:
329  match ok:
330    case False{}:
331      Fail{E.AcpiAmlUnsupported{"a NameString not in its shortest form"}}
332    case True{}:
333      cur.name.fit(Nat.is_le(size, lim), n, rest, Nat.sub(lim, size))
334
335def cur.name.go(r: Result<&2, &2, E.AcpiError, N.AmlNameL>, +code: List<&2, U32>, +lim: Nat) -> Result<&2, &2, E.AcpiError, AmlNameC>:
336  match r:
337    case Fail{e}:
338      Fail{e}
339    case Done{N.AmlNameL{+n, rest}}:
340      +size = N.AmlName.size(n)
341      cur.name.k(B.list_eq.fast(B.take.fast(size, code), N.nm.enc(n)), n, size, rest, lim)
342
343# a NameString (in the shortest form, as compilers write it)
344def cur.name(c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlNameC>:
345  match c:
346    case AmlCur{+code, +lim}:
347      cur.name.go(N.nm.dec(code), code, lim)
348
349def cur.fold(xs: List<&2, U32>, +sh: Nat, acc: W.W64) -> W.W64:
350  match xs:
351    case Nil{}:
352      acc
353    case Con{h, t}:
354      cur.fold(t, Nat.add(sh, 8n), W.W64.or(acc, W.W64.shl(W.W64.from_u32(U32.and(h, 255)), sh)))
355
356type AmlImm is Data:
357  AmlImm{v: W.W64, cur: AmlCur}
358
359def cur.imm.k(ok: Bool, +n: Nat, c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlImm>:
360  match ok:
361    case False{}:
362      Fail{E.AcpiAmlTruncated{}}
363    case True{}:
364      match c:
365        case AmlCur{+code, lim}:
366          Done{AmlImm{cur.fold(B.take.fast(n, code), 0n, W.W64.zero()), AmlCur{B.drop(n, code), Nat.sub(lim, n)}}}
367
368# n bytes of immediate data, little-endian
369def cur.imm(+n: Nat, +c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlImm>:
370  cur.imm.k(Nat.is_le(n, cur.len(c)), n, c)
371
372# Named objects
373
374def in.alias.go(n: Nat, +ns: S.AmlNs, +p: String, o: Maybe<&2, S.AmlObject>) -> String:
375  match n:
376    case 0n:
377      p
378    case 1n+k:
379      match o:
380        case Some{S.AmlOAlias{+t}}:
381          in.alias.go(k, ns, t, S.AmlNs.get(ns, t))
382        case _:
383          p
384
385# an alias followed to what it names (up to 8 aliases deep)
386def in.unalias(+ns: S.AmlNs, +p: String) -> String:
387  in.alias.go(8n, ns, p, S.AmlNs.get(ns, p))
388
389def in.int.of(o: Maybe<&2, S.AmlObject>) -> W.W64:
390  match o:
391    case Some{S.AmlOData{V.AmlInt{x}}}:
392      x
393    case _:
394      W.W64.zero()
395
396# the Integer a Name holds (0 if there is none)
397def in.name_int(+ns: S.AmlNs, +p: String) -> W.W64:
398  in.int.of(S.AmlNs.get(ns, p))
399
400def in.up.go(n: Nat, hit: Bool, +ns: S.AmlNs, +p: String, +seg: String) -> W.W64:
401  match n:
402    case 0n:
403      W.W64.zero()
404    case 1n+k:
405      match hit:
406        case True{}:
407          in.name_int(ns, S.AmlPath.child(p, seg))
408        case False{}:
409          +up = S.AmlPath.parent(p)
410          in.up.go(k, S.AmlNs.has(ns, S.AmlPath.child(up, seg)), ns, up, seg)
411
412# the Integer seg names in p or the nearest scope enclosing it (0 if none)
413def in.up_int(+ns: S.AmlNs, +p: String, +seg: String) -> W.W64:
414  in.up.go(String.length(p), S.AmlNs.has(ns, S.AmlPath.child(p, seg)), ns, p, seg)
415
416def in.base.pick(pci: Bool, +ns: S.AmlNs, +parent: String, +off: W.W64) -> W.W64:
417  match pci:
418    case False{}:
419      off
420    case True{}:
421      +adr = W.W64.lo(in.name_int(ns, S.AmlPath.child(parent, "_ADR")))
422      +bus = W.W64.lo(in.up_int(ns, parent, "_BBN"))
423      +seg = W.W64.lo(in.up_int(ns, parent, "_SEG"))
424      W.W64.add(Hs.AmlPci.address(seg, bus, U32.shrn(adr, 16n), U32.and(adr, 65535), 0), off)
425
426def in.desc.go(o: Maybe<&2, S.AmlObject>, +ns: S.AmlNs, +off: Nat, +bits: Nat, +flags: U32) -> Result<&2, &2, E.AcpiError, F.AmlFieldDesc>:
427  match o:
428    case Some{S.AmlORegion{+sp, +roff, len, +parent}}:
429      Done{F.AmlFieldDesc{sp, in.base.pick(U32.is_eq(sp, 2), ns, parent, roff), len, off, bits, flags}}
430    case _:
431      Fail{E.AcpiAmlBadType{"the region of a field is not an OperationRegion"}}
432
433# a field unit of a region, its region resolved
434def in.desc(+ns: S.AmlNs, +region: String, +off: Nat, +bits: Nat, +flags: U32) -> Result<&2, &2, E.AcpiError, F.AmlFieldDesc>:
435  in.desc.go(S.AmlNs.get(ns, in.unalias(ns, region)), ns, off, bits, flags)
436
437def in.fdesc(o: Maybe<&2, S.AmlObject>, +ns: S.AmlNs) -> Result<&2, &2, E.AcpiError, F.AmlFieldDesc>:
438  match o:
439    case Some{S.AmlOField{r, off, bits, flags}}:
440      in.desc(ns, r, off, bits, flags)
441    case _:
442      Fail{E.AcpiAmlBadType{"a register of an IndexField is not a field"}}
443
444# Reading
445
446def in.nth(xs: List<&2, V.AmlValue>, i: Nat) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
447  match xs i:
448    case Nil{} _:
449      Fail{E.AcpiAmlRange{}}
450    case Con{h, t} 0n:
451      Done{h}
452    case Con{h, t} 1n+k:
453      in.nth(t, k)
454
455def in.byte.at(m: Maybe<&2, U32>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
456  match m:
457    case None{}:
458      Fail{E.AcpiAmlRange{}}
459    case Some{b}:
460      Done{V.AmlInt{W.W64.from_u32(b)}}
461
462# element i of a package, buffer or string
463def AmlValue.element(v: V.AmlValue, +i: Nat) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
464  match v:
465    case V.AmlPkg{xs}:
466      in.nth(xs, i)
467    case V.AmlBuf{b}:
468      in.byte.at(B.Octets.at(b, i))
469    case V.AmlStr{s}:
470      in.byte.at(B.Octets.at(s, i))
471    case _:
472      Fail{E.AcpiAmlBadType{"Index of a value that is not a package, buffer or string"}}
473
474def in.ctx.arg(-H: Data, w: AmlWorld<H>, i: Nat) -> V.AmlValue:
475  match w:
476    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
477      Maybe.default(&2, V.AmlValue, List.get(&2, V.AmlValue, a, i), V.AmlUninit{})
478
479def in.ctx.local(-H: Data, w: AmlWorld<H>, i: Nat) -> V.AmlValue:
480  match w:
481    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
482      Maybe.default(&2, V.AmlValue, List.get(&2, V.AmlValue, l, i), V.AmlUninit{})
483
484# xs with element i replaced (padded with Uninitialized up to i)
485def in.list.set(i: Nat, xs: List<&2, V.AmlValue>, v: V.AmlValue) -> List<&2, V.AmlValue>:
486  match i xs:
487    case 0n Nil{}:
488      [v]
489    case 0n Con{h, t}:
490      Con{v, t}
491    case 1n+k Nil{}:
492      Con{V.AmlUninit{}, in.list.set(k, Nil{}, v)}
493    case 1n+k Con{h, t}:
494      Con{h, in.list.set(k, t, v)}
495
496def in.set.arg(-H: Data, w: AmlWorld<H>, i: Nat, v: V.AmlValue) -> AmlWorld<H>:
497  match w:
498    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
499      AmlWorld{AmlCtx{s, in.list.set(i, a, v), l, t}, n, h, e}
500
501def in.set.local(-H: Data, w: AmlWorld<H>, i: Nat, v: V.AmlValue) -> AmlWorld<H>:
502  match w:
503    case AmlWorld{AmlCtx{s, a, l, t}, n, h, e}:
504      AmlWorld{AmlCtx{s, a, in.list.set(i, l, v), t}, n, h, e}
505
506def in.wrap(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, V.AmlValue>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
507  match r:
508    case Fail{e}:
509      Fail{e}
510    case Done{v}:
511      Done{AmlRead{w, v}}
512
513def in.got.int(-H: Data, +wide: Bool, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
514  match r:
515    case Fail{e}:
516      Fail{e}
517    case Done{Hs.AmlHostAns{h, x}}:
518      Done{AmlRead{in.with_host(H, w, h), V.AmlInt{V.AmlInt.fit(wide, x)}}}
519
520def in.got.buf(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, F.AmlFieldBuf<H>>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
521  match r:
522    case Fail{e}:
523      Fail{e}
524    case Done{F.AmlFieldBuf{h, o}}:
525      Done{AmlRead{in.with_host(H, w, h), V.AmlBuf{o}}}
526
527def in.field.rd(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, small: Bool, +w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
528  match small:
529    case True{}:
530      match r:
531        case Fail{e}:
532          Fail{e}
533        case Done{+d}:
534          in.got.int(H, in.wide(H, w), w, F.AmlField.read_int(~H, ~io, d, AmlWorld.host(H, w)))
535    case False{}:
536      match r:
537        case Fail{e}:
538          Fail{e}
539        case Done{+d}:
540          in.got.buf(H, w, F.AmlField.read_buf(~H, ~io, d, AmlWorld.host(H, w)))
541
542def in.ixfield.rd(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ri: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, rd: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, +f: F.AmlFieldDesc, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
543  match ri rd:
544    case Done{+i} Done{+d}:
545      in.got.int(H, in.wide(H, w), w, F.AmlField.read_indexed(~H, ~io, i, d, f, AmlWorld.host(H, w)))
546    case Fail{e} _:
547      Fail{e}
548    case Done{i} Fail{e}:
549      Fail{e}
550
551def in.data.of(o: Maybe<&2, S.AmlObject>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
552  match o:
553    case Some{S.AmlOData{v}}:
554      Done{v}
555    case _:
556      Fail{E.AcpiAmlBadType{"the source of a buffer field is not data"}}
557
558# the data a location holds, without reading hardware: a Name value, a
559# Local, an Arg (the buffer behind a buffer field)
560def in.read_data(-H: Data, +w: AmlWorld<H>, l: V.AmlLoc) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
561  match l:
562    case V.AmlLName{+p}:
563      in.data.of(S.AmlNs.get(AmlWorld.ns(H, w), in.unalias(AmlWorld.ns(H, w), p)))
564    case V.AmlLLocal{i}:
565      Done{in.ctx.local(H, w, i)}
566    case V.AmlLArg{i}:
567      Done{in.ctx.arg(H, w, i)}
568    case _:
569      Fail{E.AcpiAmlUnsupported{"a buffer field of an element"}}
570
571def in.bf.rd.pick(-H: Data, small: Bool, +wide: Bool, +w: AmlWorld<H>, +b: B.Octets, +off: Nat, +bits: Nat) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
572  match small:
573    case True{}:
574      in.wrap(H, w, Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{V.AmlInt.fit(wide, x)}, F.AmlBits.get(b, off, bits)))
575    case False{}:
576      Done{AmlRead{w, V.AmlBuf{F.AmlBits.get_buf(b, off, bits)}}}
577
578def in.bf.rd(-H: Data, +wide: Bool, +w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, V.AmlValue>, +off: Nat, +bits: Nat) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
579  match r:
580    case Fail{e}:
581      Fail{e}
582    case Done{V.AmlBuf{+b}}:
583      in.bf.rd.pick(H, Nat.is_le(bits, 64n), wide, w, b, off, bits)
584    case Done{v}:
585      Fail{E.AcpiAmlBadType{"the source of a buffer field is not a buffer"}}
586
587def in.ix.desc(+ns: S.AmlNs, +off: Nat, +bits: Nat, +flags: U32) -> F.AmlFieldDesc:
588  F.AmlFieldDesc{0, W.W64.zero(), W.W64.max(), off, bits, flags}
589
590# the value of a named object (alias followed): a field unit is read
591# through the host
592def in.read_obj(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +p: String, o: Maybe<&2, S.AmlObject>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
593  match o:
594    case None{}:
595      Fail{E.AcpiAmlUndefined{p}}
596    case Some{S.AmlOData{v}}:
597      Done{AmlRead{w, v}}
598    case Some{S.AmlOField{r, +off, +bits, +flags}}:
599      in.field.rd(~H, ~io, Nat.is_le(bits, 64n), w, in.desc(AmlWorld.ns(H, w), r, off, bits, flags))
600    case Some{S.AmlOIndexField{i, d, +off, +bits, +flags}}:
601      in.ixfield.rd(~H, ~io, in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), i), AmlWorld.ns(H, w)), in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), d), AmlWorld.ns(H, w)), in.ix.desc(AmlWorld.ns(H, w), off, bits, flags), w)
602    case Some{S.AmlOBufField{l, +off, +bits}}:
603      in.bf.rd(H, in.wide(H, w), w, in.read_data(H, w, l), off, bits)
604    case Some{+obj}:
605      Done{AmlRead{w, V.AmlObj{p, S.AmlObject.type(obj)}}}
606
607def in.elem.rd(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, +i: Nat) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
608  match r:
609    case Fail{e}:
610      Fail{e}
611    case Done{AmlRead{w, v}}:
612      in.wrap(H, w, AmlValue.element(v, i))
613
614# the value at a location
615def in.read_loc(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, l: V.AmlLoc, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
616  match l:
617    case V.AmlLName{+p}:
618      +q = in.unalias(AmlWorld.ns(H, w), p)
619      in.read_obj(~H, ~io, w, q, S.AmlNs.get(AmlWorld.ns(H, w), q))
620    case V.AmlLLocal{i}:
621      Done{AmlRead{w, in.ctx.local(H, w, i)}}
622    case V.AmlLArg{i}:
623      Done{AmlRead{w, in.ctx.arg(H, w, i)}}
624    case V.AmlLIndex{base, +i}:
625      in.elem.rd(H, in.read_loc(~H, ~io, base, w), i)
626    case V.AmlLElem{v, +i}:
627      in.wrap(H, w, AmlValue.element(v, i))
628    case V.AmlLDebug{}:
629      Done{AmlRead{w, V.AmlUninit{}}}
630    case V.AmlLNone{}:
631      Done{AmlRead{w, V.AmlUninit{}}}
632
633# Writing
634
635def in.host.w(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
636  match r:
637    case Fail{e}:
638      Fail{e}
639    case Done{Hs.AmlHostAns{h, x}}:
640      Done{in.with_host(H, w, h)}
641
642def in.field.wr.int(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +d: F.AmlFieldDesc, r: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
643  match r:
644    case Fail{e}:
645      Fail{e}
646    case Done{x}:
647      in.host.w(H, w, F.AmlField.write_int(~H, ~io, d, AmlWorld.host(H, w), x))
648
649def in.field.wr.buf(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +d: F.AmlFieldDesc, r: Result<&2, &2, E.AcpiError, B.Octets>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
650  match r:
651    case Fail{e}:
652      Fail{e}
653    case Done{o}:
654      in.host.w(H, w, F.AmlField.write_buf(~H, ~io, d, AmlWorld.host(H, w), o))
655
656def in.field.wr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, small: Bool, +w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
657  match small:
658    case True{}:
659      match r:
660        case Fail{e}:
661          Fail{e}
662        case Done{+d}:
663          in.field.wr.int(~H, ~io, w, d, V.AmlValue.to_int(in.wide(H, w), v))
664    case False{}:
665      match r:
666        case Fail{e}:
667          Fail{e}
668        case Done{+d}:
669          in.field.wr.buf(~H, ~io, w, d, V.AmlValue.to_buf(in.wide(H, w), v))
670
671def in.ixfield.wr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ri: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, rd: Result<&2, &2, E.AcpiError, F.AmlFieldDesc>, rx: Result<&2, &2, E.AcpiError, W.W64>, +f: F.AmlFieldDesc, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
672  match ri rd rx:
673    case Done{+i} Done{+d} Done{+x}:
674      in.host.w(H, w, F.AmlField.write_indexed(~H, ~io, i, d, f, AmlWorld.host(H, w), x))
675    case Fail{e} _ _:
676      Fail{e}
677    case Done{i} Fail{e} _:
678      Fail{e}
679    case Done{i} Done{d} Fail{e}:
680      Fail{e}
681
682def in.fit.buf(+n: Nat, +o: B.Octets) -> B.Octets:
683  +h = B.Octets.take(n, o)
684  B.Octets.append(h, B.Octets.zeros(Nat.sub(n, B.Octets.len(h))))
685
686# the value v stored where a Name holds old: converted to old type when
687# old is an Integer, a String or a Buffer (a Buffer keeps its length)
688def in.convert(+wide: Bool, old: V.AmlValue, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
689  match old:
690    case V.AmlInt{x}:
691      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, y => V.AmlInt{y}, V.AmlValue.to_int(wide, v))
692    case V.AmlStr{s}:
693      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlStr{t}, V.AmlValue.to_str(wide, v))
694    case V.AmlBuf{+b}:
695      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlBuf{in.fit.buf(B.Octets.len(b), t)}, V.AmlValue.to_buf(wide, v))
696    case _:
697      Done{v}
698
699def in.set.data(-H: Data, +w: AmlWorld<H>, +p: String, r: Result<&2, &2, E.AcpiError, V.AmlValue>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
700  match r:
701    case Fail{e}:
702      Fail{e}
703    case Done{v}:
704      Done{in.with_ns(H, w, S.AmlNs.set(AmlWorld.ns(H, w), p, S.AmlOData{v}))}
705
706# a buffer put back where a buffer field found it
707def in.put.data(-H: Data, +w: AmlWorld<H>, l: V.AmlLoc, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
708  match l:
709    case V.AmlLName{+p}:
710      Done{in.with_ns(H, w, S.AmlNs.set(AmlWorld.ns(H, w), in.unalias(AmlWorld.ns(H, w), p), S.AmlOData{v}))}
711    case V.AmlLLocal{i}:
712      Done{in.set.local(H, w, i, v)}
713    case V.AmlLArg{i}:
714      Done{in.set.arg(H, w, i, v)}
715    case _:
716      Fail{E.AcpiAmlUnsupported{"a buffer field of an element"}}
717
718def in.bf.wr.go(-H: Data, +w: AmlWorld<H>, l: V.AmlLoc, r: Result<&2, &2, E.AcpiError, B.Octets>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
719  match r:
720    case Fail{e}:
721      Fail{e}
722    case Done{b}:
723      in.put.data(H, w, l, V.AmlBuf{b})
724
725def in.bf.wr(-H: Data, +w: AmlWorld<H>, +l: V.AmlLoc, src: Result<&2, &2, E.AcpiError, V.AmlValue>, +off: Nat, +bits: Nat, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
726  match src:
727    case Fail{e}:
728      Fail{e}
729    case Done{V.AmlBuf{+b}}:
730      in.bf.wr.go(H, w, l, Result.bind(&2, &2, E.AcpiError, W.W64, B.Octets, V.AmlValue.to_int(in.wide(H, w), v), x => F.AmlBits.set(b, off, Nat.min(bits, 64n), x)))
731    case Done{o}:
732      Fail{E.AcpiAmlBadType{"the source of a buffer field is not a buffer"}}
733
734# Store to a named object (chapter 19, Store): a Name converted to its type, a field
735# unit written through the host, a buffer field into its buffer
736def in.store.obj(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +w: AmlWorld<H>, +p: String, o: Maybe<&2, S.AmlObject>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
737  match o:
738    case None{}:
739      Fail{E.AcpiAmlUndefined{p}}
740    case Some{S.AmlOData{old}}:
741      in.set.data(H, w, p, in.convert(in.wide(H, w), old, v))
742    case Some{S.AmlOField{r, +off, +bits, +flags}}:
743      in.field.wr(~H, ~io, Nat.is_le(bits, 64n), w, in.desc(AmlWorld.ns(H, w), r, off, bits, flags), v)
744    case Some{S.AmlOIndexField{i, d, +off, +bits, +flags}}:
745      in.ixfield.wr(~H, ~io, in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), i), AmlWorld.ns(H, w)), in.fdesc(S.AmlNs.get(AmlWorld.ns(H, w), d), AmlWorld.ns(H, w)), V.AmlValue.to_int(in.wide(H, w), v), in.ix.desc(AmlWorld.ns(H, w), off, bits, flags), w)
746    case Some{S.AmlOBufField{+l, +off, +bits}}:
747      in.bf.wr(H, w, l, in.read_data(H, w, l), off, bits, v)
748    case Some{obj}:
749      Fail{E.AcpiAmlBadType{"Store to an object that holds no data"}}
750
751def in.elem.pkg(ok: Bool, xs: List<&2, V.AmlValue>, i: Nat, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
752  match ok:
753    case True{}:
754      Done{V.AmlPkg{in.list.set(i, xs, v)}}
755    case False{}:
756      Fail{E.AcpiAmlRange{}}
757
758def in.elem.wrap(str: Bool, b: B.Octets) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
759  match str:
760    case True{}:
761      Done{V.AmlStr{b}}
762    case False{}:
763      Done{V.AmlBuf{b}}
764
765def in.elem.bytes(ok: Bool, str: Bool, +b: B.Octets, +i: Nat, r: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
766  match ok r:
767    case False{} _:
768      Fail{E.AcpiAmlRange{}}
769    case True{} Fail{e}:
770      Fail{e}
771    case True{} Done{x}:
772      +nb = B.Octets.concat([B.Octets.take(i, b), B.Octets.of_list([W.W64.lo(x)]), B.Octets.drop(1n+i, b)])
773      in.elem.wrap(str, nb)
774
775def in.elem.set(base: V.AmlValue, +i: Nat, +wide: Bool, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
776  match base:
777    case V.AmlPkg{+xs}:
778      in.elem.pkg(Nat.is_lt(i, List.length(&2, V.AmlValue, xs)), xs, i, v)
779    case V.AmlBuf{+b}:
780      in.elem.bytes(Nat.is_lt(i, B.Octets.len(b)), False{}, b, i, V.AmlValue.to_int(wide, v))
781    case V.AmlStr{+b}:
782      in.elem.bytes(Nat.is_lt(i, B.Octets.len(b)), True{}, b, i, V.AmlValue.to_int(wide, v))
783    case _:
784      Fail{E.AcpiAmlBadType{"Index of a value that is not a package, buffer or string"}}
785
786type AmlPut<-H: Data> is Data:
787  AmlPut{w: AmlWorld<H>, v: V.AmlValue}
788
789def in.put.res(-H: Data, w: AmlWorld<H>, r: Result<&2, &2, E.AcpiError, V.AmlValue>) -> Result<&2, &2, E.AcpiError, AmlPut<H>>:
790  match r:
791    case Fail{e}:
792      Fail{e}
793    case Done{v}:
794      Done{AmlPut{w, v}}
795
796def in.put.idx.go(-H: Data, r: Result<&2, &2, E.AcpiError, V.AmlValue>, +w: AmlWorld<H>, base: V.AmlLoc) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
797  match r:
798    case Fail{e}:
799      Fail{e}
800    case Done{nv}:
801      in.put.data(H, w, base, nv)
802
803def in.put.idx(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, base: V.AmlLoc, +i: Nat, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
804  match r:
805    case Fail{e}:
806      Fail{e}
807    case Done{AmlRead{+w, old}}:
808      in.put.idx.go(H, in.elem.set(old, i, in.wide(H, w), v), w, base)
809
810# an element of a package, buffer or string at a location replaced
811# (Store to Index(...)); the location must be a Name, a Local or an Arg
812def in.put.index(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +base: V.AmlLoc, +i: Nat, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
813  in.put.idx(H, in.read_loc(~H, ~io, base, w), base, i, v)
814
815def in.is_writable(o: Maybe<&2, S.AmlObject>) -> Bool:
816  match o:
817    case Some{S.AmlOField{r, off, n, f}}:
818      True{}
819    case Some{S.AmlOIndexField{i, d, off, n, f}}:
820      True{}
821    case Some{S.AmlOBufField{l, off, n}}:
822      True{}
823    case _:
824      False{}
825
826def in.put.name(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, fieldy: Bool, +w: AmlWorld<H>, +p: String, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
827  match fieldy:
828    case True{}:
829      in.store.obj(~H, ~io, w, p, S.AmlNs.get(AmlWorld.ns(H, w), p), v)
830    case False{}:
831      Done{in.with_ns(H, w, S.AmlNs.set(AmlWorld.ns(H, w), p, S.AmlOData{v}))}
832
833# CopyObject (chapter 19), and how Index writes back: the value replaces what
834# the location holds, without conversion (a field unit is written)
835def in.put(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, l: V.AmlLoc, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
836  match l:
837    case V.AmlLName{+p}:
838      +q = in.unalias(AmlWorld.ns(H, w), p)
839      in.put.name(~H, ~io, in.is_writable(S.AmlNs.get(AmlWorld.ns(H, w), q)), w, q, v)
840    case V.AmlLLocal{i}:
841      Done{in.set.local(H, w, i, v)}
842    case V.AmlLArg{i}:
843      Done{in.set.arg(H, w, i, v)}
844    case V.AmlLIndex{base, i}:
845      in.put.index(~H, ~io, base, i, w, v)
846    case V.AmlLElem{x, i}:
847      Done{w}
848    case V.AmlLDebug{}:
849      Done{in.debug(H, w, v)}
850    case V.AmlLNone{}:
851      Done{w}
852
853# Store (chapter 19) to a location, an Arg holding a reference excepted
854def in.store.base(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, l: V.AmlLoc, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
855  match l:
856    case V.AmlLName{+p}:
857      +q = in.unalias(AmlWorld.ns(H, w), p)
858      in.store.obj(~H, ~io, w, q, S.AmlNs.get(AmlWorld.ns(H, w), q), v)
859    case V.AmlLLocal{i}:
860      Done{in.set.local(H, w, i, v)}
861    case V.AmlLArg{i}:
862      Done{in.set.arg(H, w, i, v)}
863    case V.AmlLIndex{base, i}:
864      in.put.index(~H, ~io, base, i, w, v)
865    case V.AmlLElem{x, i}:
866      Done{w}
867    case V.AmlLDebug{}:
868      Done{in.debug(H, w, v)}
869    case V.AmlLNone{}:
870      Done{w}
871
872def in.store.arg(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, cur: V.AmlValue, +i: Nat, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
873  match cur:
874    case V.AmlRef{l2}:
875      in.store.base(~H, ~io, l2, w, v)
876    case _:
877      Done{in.set.arg(H, w, i, v)}
878
879# Store to a location; an Arg that holds a reference is stored through
880def in.store(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +l: V.AmlLoc, +w: AmlWorld<H>, +v: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
881  match l:
882    case V.AmlLArg{+i}:
883      in.store.arg(~H, ~io, in.ctx.arg(H, w, i), i, w, v)
884    case _:
885      in.store.base(~H, ~io, l, w, v)
886
887# Machine transitions
888
889def in.mk(-H: Data, md: AmlMode, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
890  AmlMachine{md, c, fs, w}
891
892def in.give(-H: Data, v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
893  AmlMachine{AmlMGive{v}, c, fs, w}
894
895def in.no.cur() -> AmlCur:
896  AmlCur{Nil{}, 0n}
897
898# a world after a change, or the failure; then v is given
899def in.then.give(-H: Data, r: Result<&2, &2, E.AcpiError, AmlWorld<H>>, v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
900  match r:
901    case Fail{e}:
902      AmlMachine{AmlMFail{e}, c, fs, w}
903    case Done{w2}:
904      AmlMachine{AmlMGive{v}, c, fs, w2}
905
906def in.read.give(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
907  match r:
908    case Fail{e}:
909      AmlMachine{AmlMFail{e}, c, fs, w}
910    case Done{AmlRead{w2, v}}:
911      AmlMachine{AmlMGive{v}, c, fs, w2}
912
913def in.val.give(-H: Data, r: Result<&2, &2, E.AcpiError, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
914  match r:
915    case Fail{e}:
916      AmlMachine{AmlMFail{e}, c, fs, w}
917    case Done{v}:
918      AmlMachine{AmlMGive{v}, c, fs, w}
919
920def in.loc(v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlLoc>:
921  match v:
922    case V.AmlRef{l}:
923      Done{l}
924    case V.AmlUninit{}:
925      Done{V.AmlLNone{}}
926    case _:
927      Fail{E.AcpiAmlBadOperand{112}}
928
929def in.store.give2(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, +v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
930  match r:
931    case Fail{e}:
932      AmlMachine{AmlMFail{e}, c, fs, w}
933    case Done{l}:
934      in.then.give(H, in.store(~H, ~io, l, w, v), v, c, fs, w)
935
936# the result of an operator stored in its Target, then given
937def in.store.give(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlValue>, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
938  match r:
939    case Fail{e}:
940      AmlMachine{AmlMFail{e}, c, fs, w}
941    case Done{+v}:
942      in.store.give2(~H, ~io, in.loc(t), v, c, fs, w)
943
944# Integer operators (19.6: Add, Subtract, Multiply, ShiftLeft, ShiftRight,
945# And, NAnd, Or, NOr, XOr, Mod). Mod by zero is AcpiAmlDivZero.
946
947def in.mod(z: Bool, +x: W.W64, +y: W.W64) -> Result<&2, &2, E.AcpiError, W.W64>:
948  match z:
949    case True{}:
950      Fail{E.AcpiAmlDivZero{}}
951    case False{}:
952      Done{W.W64.mod(x, y)}
953
954def in.shift.pick(big: Bool, left: Bool, +wide: Bool, +x: W.W64, +n: Nat) -> W.W64:
955  match big:
956    case True{}:
957      W.W64.zero()
958    case False{}:
959      match left:
960        case True{}:
961          V.AmlInt.fit(wide, W.W64.shl(x, n))
962        case False{}:
963          W.W64.shr(x, n)
964
965# shifts by 64 or more give 0
966def in.shift(left: Bool, +wide: Bool, +x: W.W64, +y: W.W64) -> W.W64:
967  in.shift.pick(Bool.or(Bool.not(U32.is_eq(W.W64.hi(y), 0)), U32.is_le(64, W.W64.lo(y))), left, wide, x, U32.to_nat(W.W64.lo(y)))
968
969def in.int2(+op: Nat, +wide: Bool, +x: W.W64, +y: W.W64) -> Result<&2, &2, E.AcpiError, W.W64>:
970  match op:
971    case 114n:
972      Done{V.AmlInt.fit(wide, W.W64.add(x, y))}
973    case 116n:
974      Done{V.AmlInt.fit(wide, W.W64.sub(x, y))}
975    case 119n:
976      Done{V.AmlInt.fit(wide, W.W64.mul(x, y))}
977    case 121n:
978      Done{in.shift(True{}, wide, x, y)}
979    case 122n:
980      Done{in.shift(False{}, wide, x, y)}
981    case 123n:
982      Done{W.W64.and(x, y)}
983    case 124n:
984      Done{V.AmlInt.fit(wide, W.W64.not(W.W64.and(x, y)))}
985    case 125n:
986      Done{W.W64.or(x, y)}
987    case 126n:
988      Done{V.AmlInt.fit(wide, W.W64.not(W.W64.or(x, y)))}
989    case 127n:
990      Done{W.W64.xor(x, y)}
991    case 133n:
992      in.mod(W.W64.is_zero(y), x, y)
993    case _:
994      Fail{E.AcpiAmlBadOpcode{U32.from_nat(op)}}
995
996type AmlInts is Data:
997  AmlInts{x: W.W64, y: W.W64}
998
999def in.ints.go(ra: Result<&2, &2, E.AcpiError, W.W64>, rb: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, AmlInts>:
1000  match ra rb:
1001    case Done{x} Done{y}:
1002      Done{AmlInts{x, y}}
1003    case Fail{e} _:
1004      Fail{e}
1005    case Done{x} Fail{e}:
1006      Fail{e}
1007
1008def in.ints(+wide: Bool, a: V.AmlValue, b: V.AmlValue) -> Result<&2, &2, E.AcpiError, AmlInts>:
1009  in.ints.go(V.AmlValue.to_int(wide, a), V.AmlValue.to_int(wide, b))
1010
1011def in.bad(-H: Data, +code: U32, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
1012  AmlMachine{AmlMFail{E.AcpiAmlBadOperand{code}}, c, fs, w}
1013
1014def in.int2.v(+op: Nat, +wide: Bool, r: Result<&2, &2, E.AcpiError, AmlInts>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1015  match r:
1016    case Fail{e}:
1017      Fail{e}
1018    case Done{AmlInts{x, y}}:
1019      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, z => V.AmlInt{z}, in.int2(op, wide, x, y))
1020
1021def in.ap.int2(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1022  match args:
1023    case Con{a, Con{b, Con{t, Nil{}}}}:
1024      in.store.give(~H, ~io, in.int2.v(op, in.wide(H, w), in.ints(in.wide(H, w), a, b)), t, c, fs, w)
1025    case _:
1026      in.bad(H, U32.from_nat(op), c, fs, w)
1027
1028def in.div.pick(z: Bool, +x: W.W64, +y: W.W64) -> Result<&2, &2, E.AcpiError, AmlInts>:
1029  match z:
1030    case True{}:
1031      Fail{E.AcpiAmlDivZero{}}
1032    case False{}:
1033      Done{AmlInts{W.W64.div(x, y), W.W64.mod(x, y)}}
1034
1035# Divide: the remainder to its Target, the quotient to its own
1036def in.div.v(r: Result<&2, &2, E.AcpiError, AmlInts>) -> Result<&2, &2, E.AcpiError, AmlInts>:
1037  match r:
1038    case Fail{e}:
1039      Fail{e}
1040    case Done{AmlInts{+x, +y}}:
1041      in.div.pick(W.W64.is_zero(y), x, y)
1042
1043def in.div.q(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlWorld<H>>, +q: W.W64, qt: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1044  match r:
1045    case Fail{e}:
1046      AmlMachine{AmlMFail{e}, c, fs, w}
1047    case Done{+w2}:
1048      in.store.give(~H, ~io, Done{V.AmlInt{q}}, qt, c, fs, w2)
1049
1050def in.div.st(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlInts>, rt: V.AmlValue, qt: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1051  match r:
1052    case Fail{e}:
1053      AmlMachine{AmlMFail{e}, c, fs, w}
1054    case Done{AmlInts{+q, rm}}:
1055      in.div.q(~H, ~io, Result.bind(&2, &2, E.AcpiError, V.AmlLoc, AmlWorld<H>, in.loc(rt), l => in.store(~H, ~io, l, w, V.AmlInt{rm})), q, qt, c, fs, w)
1056
1057def in.ap.div(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1058  match args:
1059    case Con{a, Con{b, Con{rt, Con{qt, Nil{}}}}}:
1060      in.div.st(~H, ~io, in.div.v(in.ints(in.wide(H, w), a, b)), rt, qt, c, fs, w)
1061    case _:
1062      in.bad(H, 120, c, fs, w)
1063
1064# Not, FindSetLeftBit, FindSetRightBit: one operand and a Target
1065
1066def in.fsb.first(none: Bool, +i: Nat, acc: Nat) -> Nat:
1067  match none:
1068    case True{}:
1069      Nat.add(i, 1n)
1070    case False{}:
1071      acc
1072
1073def in.fsb.pick(set: Bool, left: Bool, +i: Nat, +acc: Nat) -> Nat:
1074  match set:
1075    case False{}:
1076      acc
1077    case True{}:
1078      match left:
1079        case True{}:
1080          Nat.add(i, 1n)
1081        case False{}:
1082          in.fsb.first(Nat.is_eq(acc, 0n), i, acc)
1083
1084def in.fsb.go(n: Nat, +x: W.W64, +i: Nat, +left: Bool, acc: Nat) -> Nat:
1085  match n:
1086    case 0n:
1087      acc
1088    case 1n+p:
1089      in.fsb.go(p, x, Nat.add(i, 1n), left, in.fsb.pick(W.W64.is_eq(W.W64.and(W.W64.shr(x, i), W.W64.one()), W.W64.one()), left, i, acc))
1090
1091def in.int1(+op: Nat, +wide: Bool, +x: W.W64) -> W.W64:
1092  match op:
1093    case 128n:
1094      V.AmlInt.fit(wide, W.W64.not(x))
1095    case 129n:
1096      W.W64.from_nat(in.fsb.go(64n, x, 0n, True{}, 0n))
1097    case _:
1098      W.W64.from_nat(in.fsb.go(64n, x, 0n, False{}, 0n))
1099
1100def in.ap.int1(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1101  match args:
1102    case Con{a, Con{t, Nil{}}}:
1103      in.store.give(~H, ~io, Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{in.int1(op, in.wide(H, w), x)}, V.AmlValue.to_int(in.wide(H, w), a)), t, c, fs, w)
1104    case _:
1105      in.bad(H, U32.from_nat(op), c, fs, w)
1106
1107# Increment, Decrement: read, change, store back
1108
1109def in.incdec.op(inc: Bool, +x: W.W64) -> W.W64:
1110  match inc:
1111    case True{}:
1112      W.W64.add(x, W.W64.one())
1113    case False{}:
1114      W.W64.sub(x, W.W64.one())
1115
1116def in.incdec.v(-H: Data, +inc: Bool, +wide: Bool, r: Result<&2, &2, E.AcpiError, AmlRead<H>>) -> Result<&2, &2, E.AcpiError, AmlPut<H>>:
1117  match r:
1118    case Fail{e}:
1119      Fail{e}
1120    case Done{AmlRead{w2, v}}:
1121      in.put.res(H, w2, Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{V.AmlInt.fit(wide, in.incdec.op(inc, x))}, V.AmlValue.to_int(wide, v)))
1122
1123def in.incdec.st(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlPut<H>>, +l: V.AmlLoc, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1124  match r:
1125    case Fail{e}:
1126      AmlMachine{AmlMFail{e}, c, fs, w}
1127    case Done{AmlPut{+w2, +v}}:
1128      in.then.give(H, in.store(~H, ~io, l, w2, v), v, c, fs, w2)
1129
1130def in.incdec.loc(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +inc: Bool, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1131  match r:
1132    case Fail{e}:
1133      AmlMachine{AmlMFail{e}, c, fs, w}
1134    case Done{+l}:
1135      in.incdec.st(~H, ~io, in.incdec.v(H, inc, in.wide(H, w), in.read_loc(~H, ~io, l, w)), l, c, fs, w)
1136
1137def in.ap.incdec(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +inc: Bool, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1138  match args:
1139    case Con{t, Nil{}}:
1140      in.incdec.loc(~H, ~io, inc, in.loc(t), c, fs, w)
1141    case _:
1142      in.bad(H, 117, c, fs, w)
1143
1144# Logical operators (LAnd, LOr, LNot, LEqual, LGreater, LLess): Ones or 0
1145
1146def in.truth(+wide: Bool, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, Bool>:
1147  Result.map(&2, &2, E.AcpiError, W.W64, Bool, x => Bool.not(W.W64.is_zero(x)), V.AmlValue.to_int(wide, v))
1148
1149def in.bool.v(+wide: Bool, r: Result<&2, &2, E.AcpiError, Bool>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1150  Result.map(&2, &2, E.AcpiError, Bool, V.AmlValue, b => V.AmlInt{V.AmlInt.of_bool(wide, b)}, r)
1151
1152def in.logic2(ra: Result<&2, &2, E.AcpiError, Bool>, rb: Result<&2, &2, E.AcpiError, Bool>, op: Nat) -> Result<&2, &2, E.AcpiError, Bool>:
1153  match ra rb:
1154    case Done{x} Done{y}:
1155      match op:
1156        case 144n:
1157          Done{Bool.and(x, y)}
1158        case _:
1159          Done{Bool.or(x, y)}
1160    case Fail{e} _:
1161      Fail{e}
1162    case Done{x} Fail{e}:
1163      Fail{e}
1164
1165def in.cmp.op(+op: Nat, c: Cmp) -> Bool:
1166  match op:
1167    case 147n:
1168      Cmp.is_eq(c)
1169    case 148n:
1170      Cmp.is_gt(c)
1171    case _:
1172      Cmp.is_lt(c)
1173
1174def in.logic.pick(cmp: Bool, +op: Nat, +wide: Bool, a: V.AmlValue, +b: V.AmlValue) -> Result<&2, &2, E.AcpiError, Bool>:
1175  match cmp:
1176    case True{}:
1177      Result.map(&2, &2, E.AcpiError, Cmp, Bool, x => in.cmp.op(op, x), V.AmlValue.compare(wide, a, b))
1178    case False{}:
1179      in.logic2(in.truth(wide, a), in.truth(wide, b), op)
1180
1181def in.logic.two(+op: Nat, +wide: Bool, a: V.AmlValue, +b: V.AmlValue) -> Result<&2, &2, E.AcpiError, Bool>:
1182  in.logic.pick(Nat.is_le(147n, op), op, wide, a, b)
1183
1184def in.ap.logic(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1185  match args:
1186    case Con{a, Nil{}}:
1187      +wide = in.wide(H, w)
1188      in.val.give(H, in.bool.v(wide, Result.map(&2, &2, E.AcpiError, Bool, Bool, b => Bool.not(b), in.truth(wide, a))), c, fs, w)
1189    case Con{a, Con{b, Nil{}}}:
1190      +wide = in.wide(H, w)
1191      in.val.give(H, in.bool.v(wide, in.logic.two(op, wide, a, b)), c, fs, w)
1192    case _:
1193      in.bad(H, U32.from_nat(op), c, fs, w)
1194
1195# Store, CopyObject, RefOf, DerefOf
1196
1197def in.ap.store(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1198  match args:
1199    case Con{v, Con{t, Nil{}}}:
1200      in.store.give(~H, ~io, Done{v}, t, c, fs, w)
1201    case _:
1202      in.bad(H, 112, c, fs, w)
1203
1204def in.put.give(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, +v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1205  match r:
1206    case Fail{e}:
1207      AmlMachine{AmlMFail{e}, c, fs, w}
1208    case Done{l}:
1209      in.then.give(H, in.put(~H, ~io, l, w, v), v, c, fs, w)
1210
1211def in.ap.copy(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1212  match args:
1213    case Con{+v, Con{t, Nil{}}}:
1214      in.put.give(~H, ~io, in.loc(t), v, c, fs, w)
1215    case _:
1216      in.bad(H, 157, c, fs, w)
1217
1218def in.deref.name(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, m: Maybe<&2, String>, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
1219  match m:
1220    case None{}:
1221      Fail{E.AcpiAmlUndefined{"DerefOf of a name"}}
1222    case Some{p}:
1223      in.read_loc(~H, ~io, V.AmlLName{p}, w)
1224
1225def in.deref(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, v: V.AmlValue, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
1226  match v:
1227    case V.AmlRef{l}:
1228      in.read_loc(~H, ~io, l, w)
1229    case V.AmlStr{s}:
1230      in.deref.name(~H, ~io, S.AmlNs.resolve(AmlWorld.ns(H, w), in.scope(H, w), N.AmlName.of_text(B.Octets.to_string(s))), w)
1231    case _:
1232      Fail{E.AcpiAmlBadOperand{131}}
1233
1234def in.ap.deref(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1235  match args:
1236    case Con{v, Nil{}}:
1237      in.read.give(H, in.deref(~H, ~io, v, w), c, fs, w)
1238    case _:
1239      in.bad(H, 131, c, fs, w)
1240
1241# Index (chapter 19): a reference to an element; it is also put in the Target
1242
1243def in.index.ref(base: V.AmlValue, +i: Nat) -> V.AmlValue:
1244  match base:
1245    case V.AmlRef{l}:
1246      V.AmlRef{V.AmlLIndex{l, i}}
1247    case _:
1248      V.AmlRef{V.AmlLElem{base, i}}
1249
1250def in.size.of(v: V.AmlValue) -> Result<&2, &2, E.AcpiError, Nat>:
1251  match v:
1252    case V.AmlStr{s}:
1253      Done{B.Octets.len(s)}
1254    case V.AmlBuf{b}:
1255      Done{B.Octets.len(b)}
1256    case V.AmlPkg{xs}:
1257      Done{List.length(&2, V.AmlValue, xs)}
1258    case _:
1259      Fail{E.AcpiAmlBadType{"SizeOf or Index of a value that is not a string, buffer or package"}}
1260
1261# the value a source operand stands for (read when it is a location)
1262def in.source(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, v: V.AmlValue, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlRead<H>>:
1263  match v:
1264    case V.AmlRef{l}:
1265      in.read_loc(~H, ~io, l, w)
1266    case _:
1267      Done{AmlRead{w, v}}
1268
1269def in.index.put(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ok: Bool, +ref: V.AmlValue, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1270  match ok:
1271    case False{}:
1272      AmlMachine{AmlMFail{E.AcpiAmlRange{}}, c, fs, w}
1273    case True{}:
1274      in.put.give(~H, ~io, in.loc(t), ref, c, fs, w)
1275
1276def in.index.fits(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, Nat>, +base: V.AmlValue, +i: Nat, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1277  match r:
1278    case Fail{e}:
1279      AmlMachine{AmlMFail{e}, c, fs, w}
1280    case Done{n}:
1281      in.index.put(~H, ~io, Nat.is_lt(i, n), in.index.ref(base, i), t, c, fs, w)
1282
1283def in.index.chk(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, +base: V.AmlValue, +i: Nat, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1284  match r:
1285    case Fail{e}:
1286      AmlMachine{AmlMFail{e}, c, fs, w}
1287    case Done{AmlRead{+w2, v}}:
1288      in.index.fits(~H, ~io, in.size.of(v), base, i, t, c, fs, w2)
1289
1290def in.index.go(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ri: Result<&2, &2, E.AcpiError, W.W64>, +base: V.AmlValue, t: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1291  match ri:
1292    case Fail{e}:
1293      AmlMachine{AmlMFail{e}, c, fs, w}
1294    case Done{x}:
1295      in.index.chk(~H, ~io, in.source(~H, ~io, base, w), base, W.W64.to_nat(x), t, c, fs, w)
1296
1297def in.small.pick(ok: Bool, x: W.W64) -> Result<&2, &2, E.AcpiError, W.W64>:
1298  match ok:
1299    case True{}:
1300      Done{x}
1301    case False{}:
1302      Fail{E.AcpiAmlRange{}}
1303
1304def in.small.chk(r: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, W.W64>:
1305  match r:
1306    case Fail{e}:
1307      Fail{e}
1308    case Done{+x}:
1309      in.small.pick(U32.is_eq(W.W64.hi(x), 0), x)
1310
1311# an Integer operand that must be small (an index or a count: below 2^32)
1312def in.small.int(+wide: Bool, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, W.W64>:
1313  in.small.chk(V.AmlValue.to_int(wide, v))
1314
1315def in.ap.index(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1316  match args:
1317    case Con{+base, Con{i, Con{t, Nil{}}}}:
1318      in.index.go(~H, ~io, in.small.int(in.wide(H, w), i), base, t, c, fs, w)
1319    case _:
1320      in.bad(H, 136, c, fs, w)
1321
1322# SizeOf, ObjectType
1323
1324def in.size.give(-H: Data, r: Result<&2, &2, E.AcpiError, AmlRead<H>>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1325  match r:
1326    case Fail{e}:
1327      AmlMachine{AmlMFail{e}, c, fs, w}
1328    case Done{AmlRead{w2, v}}:
1329      in.val.give(H, Result.map(&2, &2, E.AcpiError, Nat, V.AmlValue, n => V.AmlInt{W.W64.from_nat(n)}, in.size.of(v)), c, fs, w2)
1330
1331def in.ap.size(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1332  match args:
1333    case Con{v, Nil{}}:
1334      in.size.give(H, in.source(~H, ~io, v, w), c, fs, w)
1335    case _:
1336      in.bad(H, 135, c, fs, w)
1337
1338def in.otype.obj(o: Maybe<&2, S.AmlObject>) -> U32:
1339  match o:
1340    case Some{x}:
1341      S.AmlObject.type(x)
1342    case None{}:
1343      0
1344
1345def in.otype(-H: Data, v: V.AmlValue, +w: AmlWorld<H>) -> U32:
1346  match v:
1347    case V.AmlRef{V.AmlLName{+p}}:
1348      in.otype.obj(S.AmlNs.get(AmlWorld.ns(H, w), in.unalias(AmlWorld.ns(H, w), p)))
1349    case V.AmlRef{V.AmlLLocal{i}}:
1350      V.AmlValue.type(in.ctx.local(H, w, i))
1351    case V.AmlRef{V.AmlLArg{i}}:
1352      V.AmlValue.type(in.ctx.arg(H, w, i))
1353    case V.AmlRef{V.AmlLDebug{}}:
1354      16
1355    case _:
1356      V.AmlValue.type(v)
1357
1358def in.ap.otype(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1359  match args:
1360    case Con{v, Nil{}}:
1361      in.give(H, V.AmlInt{W.W64.from_u32(in.otype(H, v, w))}, c, fs, w)
1362    case _:
1363      in.bad(H, 142, c, fs, w)
1364
1365def in.condref.put(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, V.AmlLoc>, +v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1366  match r:
1367    case Fail{e}:
1368      AmlMachine{AmlMFail{e}, c, fs, w}
1369    case Done{l}:
1370      in.then.give(H, in.put(~H, ~io, l, w, v), V.AmlInt{V.AmlInt.ones(in.wide(H, w))}, c, fs, w)
1371
1372# CondRefOf (chapter 19): Ones and the reference in the Target if the object
1373# exists, Zero otherwise
1374def in.ap.condref(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1375  match args:
1376    case Con{V.AmlRef{l}, Con{t, Nil{}}}:
1377      in.condref.put(~H, ~io, in.loc(t), V.AmlRef{l}, c, fs, w)
1378    case Con{x, Con{t, Nil{}}}:
1379      in.give(H, V.AmlInt{W.W64.zero()}, c, fs, w)
1380    case _:
1381      in.bad(H, 274, c, fs, w)
1382
1383# Concatenate (chapter 19): by the first operand type
1384
1385def in.concat(+wide: Bool, a: V.AmlValue, +b: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1386  match a:
1387    case V.AmlInt{x}:
1388      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, y => V.AmlBuf{B.Octets.append(V.val.int.bytes(wide, x), V.val.int.bytes(wide, y))}, V.AmlValue.to_int(wide, b))
1389    case V.AmlStr{s}:
1390      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlStr{B.Octets.append(s, t)}, V.AmlValue.to_str(wide, b))
1391    case V.AmlBuf{s}:
1392      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, t => V.AmlBuf{B.Octets.append(s, t)}, V.AmlValue.to_buf(wide, b))
1393    case _:
1394      Fail{E.AcpiAmlBadType{"Concatenate of a value that is not an integer, string or buffer"}}
1395
1396def in.ap.concat(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1397  match args:
1398    case Con{a, Con{b, Con{t, Nil{}}}}:
1399      in.store.give(~H, ~io, in.concat(in.wide(H, w), a, b), t, c, fs, w)
1400    case _:
1401      in.bad(H, 115, c, fs, w)
1402
1403# ToInteger, ToBuffer (chapter 19)
1404
1405def in.to_int(+wide: Bool, v: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1406  match v:
1407    case V.AmlStr{s}:
1408      Done{V.AmlInt{V.AmlValue.parse_int(wide, B.Octets.to_list(s))}}
1409    case _:
1410      Result.map(&2, &2, E.AcpiError, W.W64, V.AmlValue, x => V.AmlInt{x}, V.AmlValue.to_int(wide, v))
1411
1412def in.conv.v(+op: Nat, +wide: Bool, a: V.AmlValue) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1413  match op:
1414    case 153n:
1415      in.to_int(wide, a)
1416    case _:
1417      Result.map(&2, &2, E.AcpiError, B.Octets, V.AmlValue, b => V.AmlBuf{b}, V.AmlValue.to_buf(wide, a))
1418
1419def in.ap.conv(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1420  match args:
1421    case Con{a, Con{t, Nil{}}}:
1422      in.store.give(~H, ~io, in.conv.v(op, in.wide(H, w), a), t, c, fs, w)
1423    case _:
1424      in.bad(H, U32.from_nat(op), c, fs, w)
1425
1426# Notify (chapter 19; 5.6.6, device object notifications): recorded, for the caller
1427
1428def in.notify(-H: Data, t: V.AmlValue, r: Result<&2, &2, E.AcpiError, W.W64>, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
1429  match t r:
1430    case V.AmlRef{V.AmlLName{p}} Done{x}:
1431      Done{in.note(H, w, AmlNote{p, x})}
1432    case _ Fail{e}:
1433      Fail{e}
1434    case _ Done{x}:
1435      Fail{E.AcpiAmlBadOperand{134}}
1436
1437def in.ap.notify(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1438  match args:
1439    case Con{t, Con{v, Nil{}}}:
1440      in.then.give(H, in.notify(H, t, V.AmlValue.to_int(in.wide(H, w), v), w), V.AmlUninit{}, c, fs, w)
1441    case _:
1442      in.bad(H, 134, c, fs, w)
1443
1444# Sleep and Stall advance the clock Timer reads (by 10000 and 10 units of
1445# 100 ns per millisecond and microsecond); nothing waits
1446
1447def in.sleep.go(-H: Data, r: Result<&2, &2, E.AcpiError, W.W64>, +per: U32, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1448  match r:
1449    case Fail{e}:
1450      AmlMachine{AmlMFail{e}, c, fs, w}
1451    case Done{x}:
1452      in.give(H, V.AmlUninit{}, c, fs, in.tick(H, w, W.W64.mul(x, W.W64.from_u32(per))))
1453
1454def in.ap.sleep(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +per: U32, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1455  match args:
1456    case Con{v, Nil{}}:
1457      in.sleep.go(H, V.AmlValue.to_int(in.wide(H, w), v), per, c, fs, w)
1458    case _:
1459      in.bad(H, 290, c, fs, w)
1460
1461# Fatal (chapter 19)
1462def in.ap.fatal(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1463  match args:
1464    case Con{V.AmlInt{t}, Con{V.AmlInt{k}, Con{v, Nil{}}}}:
1465      AmlMachine{AmlMFail{E.AcpiAmlFatal{W.W64.lo(t), W.W64.lo(k), Result.default(&2, &2, E.AcpiError, W.W64, V.AmlValue.to_int(in.wide(H, w), v), W.W64.zero())}}, c, fs, w}
1466    case _:
1467      in.bad(H, 306, c, fs, w)
1468
1469# Definitions: Name, OperationRegion, Alias, External, Mutex, Event and the
1470# CreateField family. A name already defined is AcpiAmlDuplicate.
1471
1472def in.path(v: V.AmlValue) -> String:
1473  match v:
1474    case V.AmlRef{V.AmlLName{p}}:
1475      p
1476    case _:
1477      ""
1478
1479def in.def.chk(-H: Data, dup: Bool, +p: String, o: S.AmlObject, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1480  match dup:
1481    case True{}:
1482      AmlMachine{AmlMFail{E.AcpiAmlDuplicate{p}}, c, fs, w}
1483    case False{}:
1484      in.give(H, V.AmlUninit{}, c, fs, in.define(H, w, p, o))
1485
1486def in.def.obj(-H: Data, +p: String, o: S.AmlObject, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1487  in.def.chk(H, S.AmlNs.has(AmlWorld.ns(H, w), p), p, o, c, fs, w)
1488
1489def in.ap.name(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1490  match args:
1491    case Con{n, Con{v, Nil{}}}:
1492      in.def.obj(H, in.path(n), S.AmlOData{v}, c, fs, w)
1493    case _:
1494      in.bad(H, 8, c, fs, w)
1495
1496def in.region.v(ro: Result<&2, &2, E.AcpiError, W.W64>, rl: Result<&2, &2, E.AcpiError, W.W64>, +sp: U32, +scope: String) -> Result<&2, &2, E.AcpiError, S.AmlObject>:
1497  match ro rl:
1498    case Done{o} Done{l}:
1499      Done{S.AmlORegion{sp, o, l, scope}}
1500    case Fail{e} _:
1501      Fail{e}
1502    case Done{o} Fail{e}:
1503      Fail{e}
1504
1505def in.def.res(-H: Data, +p: String, r: Result<&2, &2, E.AcpiError, S.AmlObject>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1506  match r:
1507    case Fail{e}:
1508      AmlMachine{AmlMFail{e}, c, fs, w}
1509    case Done{o}:
1510      in.def.obj(H, p, o, c, fs, w)
1511
1512def in.ap.region(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1513  match args:
1514    case Con{n, Con{V.AmlInt{sp}, Con{o, Con{l, Nil{}}}}}:
1515      +wide = in.wide(H, w)
1516      in.def.res(H, in.path(n), in.region.v(V.AmlValue.to_int(wide, o), V.AmlValue.to_int(wide, l), W.W64.lo(sp), in.scope(H, w)), c, fs, w)
1517    case _:
1518      in.bad(H, 384, c, fs, w)
1519
1520def in.ap.alias(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1521  match args:
1522    case Con{src, Con{dst, Nil{}}}:
1523      in.def.obj(H, in.path(dst), S.AmlOAlias{in.path(src)}, c, fs, w)
1524    case _:
1525      in.bad(H, 6, c, fs, w)
1526
1527def in.ext.pick(-H: Data, has: Bool, +p: String, +k: U32, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1528  match has:
1529    case True{}:
1530      in.give(H, V.AmlUninit{}, c, fs, w)
1531    case False{}:
1532      in.give(H, V.AmlUninit{}, c, fs, in.define(H, w, p, S.AmlOExternal{k}))
1533
1534# External declares an object defined elsewhere; it defines nothing if the
1535# object exists
1536def in.ap.external(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1537  match args:
1538    case Con{n, Con{V.AmlInt{k}, Con{a, Nil{}}}}:
1539      +p = in.path(n)
1540      in.ext.pick(H, S.AmlNs.has(AmlWorld.ns(H, w), p), p, W.W64.lo(k), c, fs, w)
1541    case _:
1542      in.bad(H, 21, c, fs, w)
1543
1544def in.ap.mutex(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1545  match args:
1546    case Con{n, Con{V.AmlInt{s}, Nil{}}}:
1547      in.def.obj(H, in.path(n), S.AmlOMutex{W.W64.lo(s)}, c, fs, w)
1548    case Con{n, Nil{}}:
1549      in.def.obj(H, in.path(n), S.AmlOEvent{}, c, fs, w)
1550    case _:
1551      in.bad(H, 257, c, fs, w)
1552
1553# CreateBitField, CreateByteField, CreateWordField, CreateDWordField,
1554# CreateQWordField, CreateField: a buffer field of a buffer Name, Local or Arg
1555
1556def in.cf.size(+op: Nat) -> Nat:
1557  match op:
1558    case 141n:
1559      1n
1560    case 140n:
1561      8n
1562    case 139n:
1563      16n
1564    case 138n:
1565      32n
1566    case _:
1567      64n
1568
1569def in.cf.off(+op: Nat, +i: Nat) -> Nat:
1570  match op:
1571    case 141n:
1572      i
1573    case 275n:
1574      i
1575    case _:
1576      Nat.mul(i, 8n)
1577
1578def in.cf.bits(+op: Nat, +n: Nat) -> Nat:
1579  match op:
1580    case 275n:
1581      n
1582    case _:
1583      in.cf.size(op)
1584
1585def in.cf.mk(+op: Nat, src: V.AmlValue, ri: Result<&2, &2, E.AcpiError, W.W64>, rn: Result<&2, &2, E.AcpiError, W.W64>) -> Result<&2, &2, E.AcpiError, S.AmlObject>:
1586  match src ri rn:
1587    case V.AmlRef{l} Done{+i} Done{n}:
1588      Done{S.AmlOBufField{l, in.cf.off(op, W.W64.to_nat(i)), in.cf.bits(op, W.W64.to_nat(n))}}
1589    case _ Fail{e} _:
1590      Fail{e}
1591    case _ Done{i} Fail{e}:
1592      Fail{e}
1593    case _ Done{i} Done{n}:
1594      Fail{E.AcpiAmlUnsupported{"a buffer field of a buffer that has no name"}}
1595
1596def in.ap.create(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +op: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1597  match args:
1598    case Con{src, Con{i, Con{n, Nil{}}}}:
1599      +wide = in.wide(H, w)
1600      in.def.res(H, in.path(n), in.cf.mk(op, src, in.small.int(wide, i), Done{W.W64.zero()}), c, fs, w)
1601    case Con{src, Con{i, Con{k, Con{n, Nil{}}}}}:
1602      +wide = in.wide(H, w)
1603      in.def.res(H, in.path(n), in.cf.mk(op, src, in.small.int(wide, i), in.small.int(wide, k)), c, fs, w)
1604    case _:
1605      in.bad(H, U32.from_nat(op), c, fs, w)
1606
1607# \_OSI (5.7.2): Ones if the operating system supports the feature named
1608
1609def in.osi.has(xs: List<&2, String>, +s: String) -> Bool:
1610  match xs:
1611    case Nil{}:
1612      False{}
1613    case Con{h, t}:
1614      Bool.or(String.eq(h, s), in.osi.has(t, s))
1615
1616def in.opts.osi(o: AmlOptions) -> List<&2, String>:
1617  match o:
1618    case AmlOptions{osi, os, rev}:
1619      osi
1620
1621def in.osi.v(+wide: Bool, +osi: List<&2, String>, r: Result<&2, &2, E.AcpiError, B.Octets>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1622  match r:
1623    case Fail{e}:
1624      Fail{e}
1625    case Done{s}:
1626      Done{V.AmlInt{V.AmlInt.of_bool(wide, in.osi.has(osi, B.Octets.to_string(s)))}}
1627
1628def in.ap.osi(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1629  match args:
1630    case Con{v, Nil{}}:
1631      +wide = in.wide(H, w)
1632      in.val.give(H, in.osi.v(wide, in.opts.osi(in.opts(H, w)), V.AmlValue.to_str(wide, v)), c, fs, w)
1633    case _:
1634      in.bad(H, 0, c, fs, w)
1635
1636# Method calls and returns
1637
1638def in.mbody(o: Maybe<&2, S.AmlObject>) -> B.Octets:
1639  match o:
1640    case Some{S.AmlOMethod{n, f, b}}:
1641      b
1642    case _:
1643      B.Octets.empty()
1644
1645def in.locals() -> List<&2, V.AmlValue>:
1646  [V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}, V.AmlUninit{}]
1647
1648# the method at p called with args: its body runs in its own scope, with
1649# fresh Locals; FCall remembers where to come back
1650def in.call(-H: Data, +p: String, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1651  +body = B.Octets.to_list(in.mbody(S.AmlNs.get(AmlWorld.ns(H, w), p)))
1652  AmlMachine{AmlMExec{}, AmlCur{body, B.len.fast(body)}, Con{AmlFCall{AmlWorld.ctx(H, w), c}, fs}, in.with_ctx(H, w, AmlCtx{p, args, in.locals(), Nil{}})}
1653
1654def in.drop.temps(ts: List<&2, String>, ns: S.AmlNs) -> S.AmlNs:
1655  match ts:
1656    case Nil{}:
1657      ns
1658    case Con{t, rest}:
1659      in.drop.temps(rest, S.AmlNs.remove(ns, t))
1660
1661def in.temps(c: AmlCtx) -> List<&2, String>:
1662  match c:
1663    case AmlCtx{s, a, l, t}:
1664      t
1665
1666# back from a method: its names removed, the caller context restored
1667def in.back(-H: Data, w: AmlWorld<H>, saved: AmlCtx) -> AmlWorld<H>:
1668  match w:
1669    case AmlWorld{c, n, h, e}:
1670      AmlWorld{saved, in.drop.temps(in.temps(c), n), h, e}
1671
1672# Return: frames dropped to the method call (or the bottom)
1673def in.unwind.ret(-H: Data, fs: List<&2, AmlFrame>, v: V.AmlValue, w: AmlWorld<H>) -> AmlMachine<H>:
1674  match fs:
1675    case Nil{}:
1676      AmlMachine{AmlMDone{v}, in.no.cur(), Nil{}, w}
1677    case Con{AmlFCall{saved, back}, rest}:
1678      AmlMachine{AmlMGive{v}, back, rest, in.back(H, w, saved)}
1679    case Con{AmlFTop{}, rest}:
1680      AmlMachine{AmlMDone{v}, in.no.cur(), [AmlFTop{}], w}
1681    case Con{f, rest}:
1682      in.unwind.ret(H, rest, v, w)
1683
1684# Break: frames dropped to the While, then on after it
1685def in.unwind.brk(-H: Data, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
1686  match fs:
1687    case Nil{}:
1688      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), Nil{}, w}
1689    case Con{AmlFWhile{s, after, b}, rest}:
1690      AmlMachine{AmlMExec{}, after, rest, w}
1691    case Con{AmlFCall{saved, back}, rest}:
1692      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, back, rest, w}
1693    case Con{AmlFTop{}, rest}:
1694      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), rest, w}
1695    case Con{f, rest}:
1696      in.unwind.brk(H, rest, w)
1697
1698# Continue: frames dropped to the While, whose predicate is read again
1699def in.unwind.cont(-H: Data, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
1700  match fs:
1701    case Nil{}:
1702      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), Nil{}, w}
1703    case Con{AmlFWhile{+s, after, b}, rest}:
1704      AmlMachine{AmlMEval{AmlKTerm{}}, s, Con{AmlFWhile{s, after, False{}}, rest}, w}
1705    case Con{AmlFCall{saved, back}, rest}:
1706      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, back, rest, w}
1707    case Con{AmlFTop{}, rest}:
1708      AmlMachine{AmlMFail{E.AcpiAmlBadControl{}}, in.no.cur(), rest, w}
1709    case Con{f, rest}:
1710      in.unwind.cont(H, rest, w)
1711
1712def in.ap.ret(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1713  match args:
1714    case Con{v, Nil{}}:
1715      in.unwind.ret(H, fs, v, w)
1716    case _:
1717      in.bad(H, 164, c, fs, w)
1718
1719# Operators: what each opcode takes (an extended opcode 0x5B xx is 256 + xx)
1720
1721def in.kT() -> AmlArgK:
1722  AmlKTerm{}
1723
1724def in.kG() -> AmlArgK:
1725  AmlKTarget{}
1726
1727def in.kS() -> AmlArgK:
1728  AmlKBase{}
1729
1730def in.kN() -> AmlArgK:
1731  AmlKName{}
1732
1733def in.kY() -> AmlArgK:
1734  AmlKByte{}
1735
1736def in.tt.g() -> List<&2, AmlArgK>:
1737  [in.kT(), in.kT(), in.kG()]
1738
1739def in.t.g() -> List<&2, AmlArgK>:
1740  [in.kT(), in.kG()]
1741
1742def in.kinds(+op: Nat) -> Maybe<&2, List<&2, AmlArgK>>:
1743  match op:
1744    case 6n:
1745      Some{[in.kG(), in.kN()]}
1746    case 8n:
1747      Some{[in.kN(), in.kT()]}
1748    case 21n:
1749      Some{[in.kN(), in.kY(), in.kY()]}
1750    case 112n:
1751      Some{in.t.g()}
1752    case 113n:
1753      Some{[in.kG()]}
1754    case 114n:
1755      Some{in.tt.g()}
1756    case 115n:
1757      Some{in.tt.g()}
1758    case 116n:
1759      Some{in.tt.g()}
1760    case 117n:
1761      Some{[in.kG()]}
1762    case 118n:
1763      Some{[in.kG()]}
1764    case 119n:
1765      Some{in.tt.g()}
1766    case 120n:
1767      Some{[in.kT(), in.kT(), in.kG(), in.kG()]}
1768    case 121n:
1769      Some{in.tt.g()}
1770    case 122n:
1771      Some{in.tt.g()}
1772    case 123n:
1773      Some{in.tt.g()}
1774    case 124n:
1775      Some{in.tt.g()}
1776    case 125n:
1777      Some{in.tt.g()}
1778    case 126n:
1779      Some{in.tt.g()}
1780    case 127n:
1781      Some{in.tt.g()}
1782    case 128n:
1783      Some{in.t.g()}
1784    case 129n:
1785      Some{in.t.g()}
1786    case 130n:
1787      Some{in.t.g()}
1788    case 131n:
1789      Some{[in.kT()]}
1790    case 133n:
1791      Some{in.tt.g()}
1792    case 134n:
1793      Some{[in.kG(), in.kT()]}
1794    case 135n:
1795      Some{[in.kS()]}
1796    case 136n:
1797      Some{[in.kS(), in.kT(), in.kG()]}
1798    case 138n:
1799      Some{[in.kS(), in.kT(), in.kN()]}
1800    case 139n:
1801      Some{[in.kS(), in.kT(), in.kN()]}
1802    case 140n:
1803      Some{[in.kS(), in.kT(), in.kN()]}
1804    case 141n:
1805      Some{[in.kS(), in.kT(), in.kN()]}
1806    case 142n:
1807      Some{[in.kS()]}
1808    case 143n:
1809      Some{[in.kS(), in.kT(), in.kN()]}
1810    case 144n:
1811      Some{[in.kT(), in.kT()]}
1812    case 145n:
1813      Some{[in.kT(), in.kT()]}
1814    case 146n:
1815      Some{[in.kT()]}
1816    case 147n:
1817      Some{[in.kT(), in.kT()]}
1818    case 148n:
1819      Some{[in.kT(), in.kT()]}
1820    case 149n:
1821      Some{[in.kT(), in.kT()]}
1822    case 150n:
1823      Some{in.t.g()}
1824    case 153n:
1825      Some{in.t.g()}
1826    case 157n:
1827      Some{in.t.g()}
1828    case 164n:
1829      Some{[in.kT()]}
1830    case 257n:
1831      Some{[in.kN(), in.kY()]}
1832    case 258n:
1833      Some{[in.kN()]}
1834    case 274n:
1835      Some{[AmlKCond{}, in.kG()]}
1836    case 275n:
1837      Some{[in.kS(), in.kT(), in.kT(), in.kN()]}
1838    case 289n:
1839      Some{[in.kT()]}
1840    case 290n:
1841      Some{[in.kT()]}
1842    case 291n:
1843      Some{[in.kG(), AmlKWord{}]}
1844    case 292n:
1845      Some{[in.kG()]}
1846    case 293n:
1847      Some{[in.kG(), in.kT()]}
1848    case 294n:
1849      Some{[in.kG()]}
1850    case 295n:
1851      Some{[in.kG()]}
1852    case 304n:
1853      Some{Nil{}}
1854    case 306n:
1855      Some{[in.kY(), AmlKDWord{}, in.kT()]}
1856    case 307n:
1857      Some{Nil{}}
1858    case 384n:
1859      Some{[in.kN(), in.kY(), in.kT(), in.kT()]}
1860    case _:
1861      None{}
1862
1863# the operators that are statements: refused where a value is wanted
1864def in.is_stmt(+op: Nat) -> Bool:
1865  match op:
1866    case 6n:
1867      True{}
1868    case 8n:
1869      True{}
1870    case 21n:
1871      True{}
1872    case 134n:
1873      True{}
1874    case 138n:
1875      True{}
1876    case 139n:
1877      True{}
1878    case 140n:
1879      True{}
1880    case 141n:
1881      True{}
1882    case 143n:
1883      True{}
1884    case 164n:
1885      True{}
1886    case 257n:
1887      True{}
1888    case 258n:
1889      True{}
1890    case 275n:
1891      True{}
1892    case 289n:
1893      True{}
1894    case 290n:
1895      True{}
1896    case 292n:
1897      True{}
1898    case 294n:
1899      True{}
1900    case 295n:
1901      True{}
1902    case 306n:
1903      True{}
1904    case 384n:
1905      True{}
1906    case _:
1907      False{}
1908
1909def in.refof(args: List<&2, V.AmlValue>) -> Result<&2, &2, E.AcpiError, V.AmlValue>:
1910  match args:
1911    case Con{t, Nil{}}:
1912      Done{t}
1913    case _:
1914      Fail{E.AcpiAmlBadOperand{113}}
1915
1916def in.apply.code(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +code: Nat, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
1917  match code:
1918    case 6n:
1919      in.ap.alias(~H, ~io, args, c, fs, w)
1920    case 8n:
1921      in.ap.name(~H, ~io, args, c, fs, w)
1922    case 21n:
1923      in.ap.external(~H, ~io, args, c, fs, w)
1924    case 112n:
1925      in.ap.store(~H, ~io, args, c, fs, w)
1926    case 113n:
1927      in.val.give(H, in.refof(args), c, fs, w)
1928    case 114n:
1929      in.ap.int2(~H, ~io, 114n, args, c, fs, w)
1930    case 115n:
1931      in.ap.concat(~H, ~io, args, c, fs, w)
1932    case 116n:
1933      in.ap.int2(~H, ~io, 116n, args, c, fs, w)
1934    case 117n:
1935      in.ap.incdec(~H, ~io, True{}, args, c, fs, w)
1936    case 118n:
1937      in.ap.incdec(~H, ~io, False{}, args, c, fs, w)
1938    case 119n:
1939      in.ap.int2(~H, ~io, 119n, args, c, fs, w)
1940    case 120n:
1941      in.ap.div(~H, ~io, args, c, fs, w)
1942    case 121n:
1943      in.ap.int2(~H, ~io, 121n, args, c, fs, w)
1944    case 122n:
1945      in.ap.int2(~H, ~io, 122n, args, c, fs, w)
1946    case 123n:
1947      in.ap.int2(~H, ~io, 123n, args, c, fs, w)
1948    case 124n:
1949      in.ap.int2(~H, ~io, 124n, args, c, fs, w)
1950    case 125n:
1951      in.ap.int2(~H, ~io, 125n, args, c, fs, w)
1952    case 126n:
1953      in.ap.int2(~H, ~io, 126n, args, c, fs, w)
1954    case 127n:
1955      in.ap.int2(~H, ~io, 127n, args, c, fs, w)
1956    case 128n:
1957      in.ap.int1(~H, ~io, 128n, args, c, fs, w)
1958    case 129n:
1959      in.ap.int1(~H, ~io, 129n, args, c, fs, w)
1960    case 130n:
1961      in.ap.int1(~H, ~io, 130n, args, c, fs, w)
1962    case 131n:
1963      in.ap.deref(~H, ~io, args, c, fs, w)
1964    case 133n:
1965      in.ap.int2(~H, ~io, 133n, args, c, fs, w)
1966    case 134n:
1967      in.ap.notify(~H, ~io, args, c, fs, w)
1968    case 135n:
1969      in.ap.size(~H, ~io, args, c, fs, w)
1970    case 136n:
1971      in.ap.index(~H, ~io, args, c, fs, w)
1972    case 138n:
1973      in.ap.create(~H, ~io, 138n, args, c, fs, w)
1974    case 139n:
1975      in.ap.create(~H, ~io, 139n, args, c, fs, w)
1976    case 140n:
1977      in.ap.create(~H, ~io, 140n, args, c, fs, w)
1978    case 141n:
1979      in.ap.create(~H, ~io, 141n, args, c, fs, w)
1980    case 142n:
1981      in.ap.otype(~H, ~io, args, c, fs, w)
1982    case 143n:
1983      in.ap.create(~H, ~io, 143n, args, c, fs, w)
1984    case 144n:
1985      in.ap.logic(~H, ~io, 144n, args, c, fs, w)
1986    case 145n:
1987      in.ap.logic(~H, ~io, 145n, args, c, fs, w)
1988    case 146n:
1989      in.ap.logic(~H, ~io, 146n, args, c, fs, w)
1990    case 147n:
1991      in.ap.logic(~H, ~io, 147n, args, c, fs, w)
1992    case 148n:
1993      in.ap.logic(~H, ~io, 148n, args, c, fs, w)
1994    case 149n:
1995      in.ap.logic(~H, ~io, 149n, args, c, fs, w)
1996    case 150n:
1997      in.ap.conv(~H, ~io, 150n, args, c, fs, w)
1998    case 153n:
1999      in.ap.conv(~H, ~io, 153n, args, c, fs, w)
2000    case 157n:
2001      in.ap.copy(~H, ~io, args, c, fs, w)
2002    case 164n:
2003      in.ap.ret(~H, ~io, args, c, fs, w)
2004    case 257n:
2005      in.ap.mutex(~H, ~io, args, c, fs, w)
2006    case 258n:
2007      in.ap.mutex(~H, ~io, args, c, fs, w)
2008    case 274n:
2009      in.ap.condref(~H, ~io, args, c, fs, w)
2010    case 275n:
2011      in.ap.create(~H, ~io, 275n, args, c, fs, w)
2012    case 289n:
2013      in.ap.sleep(~H, ~io, 10, args, c, fs, w)
2014    case 290n:
2015      in.ap.sleep(~H, ~io, 10000, args, c, fs, w)
2016    case 291n:
2017      in.give(H, V.AmlInt{W.W64.zero()}, c, fs, w)
2018    case 293n:
2019      in.give(H, V.AmlInt{W.W64.zero()}, c, fs, w)
2020    case 304n:
2021      in.give(H, V.AmlInt{W.W64.from_u32(2)}, c, fs, w)
2022    case 306n:
2023      in.ap.fatal(~H, ~io, args, c, fs, w)
2024    case 307n:
2025      in.give(H, V.AmlInt{in.clock(H, w)}, c, fs, w)
2026    case 384n:
2027      in.ap.region(~H, ~io, args, c, fs, w)
2028    case _:
2029      AmlMachine{AmlMFail{E.AcpiAmlBadOpcode{U32.from_nat(code)}}, c, fs, w}
2030
2031def in.apply(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, op: AmlOp, args: List<&2, V.AmlValue>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2032  match op:
2033    case AmlOpCode{code}:
2034      in.apply.code(~H, ~io, U32.to_nat(code), args, c, fs, w)
2035    case AmlOpCall{p, n}:
2036      in.call(H, p, args, c, fs, w)
2037    case AmlOpOsi{}:
2038      in.ap.osi(~H, ~io, args, c, fs, w)
2039
2040# an operator reached: its operands are read next (if it has any)
2041def in.start(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, op: AmlOp, ks: List<&2, AmlArgK>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2042  match ks:
2043    case Nil{}:
2044      in.apply(~H, ~io, op, Nil{}, c, fs, w)
2045    case Con{+k, rest}:
2046      AmlMachine{AmlMEval{k}, c, Con{AmlFArgs{op, Nil{}, Con{k, rest}}, fs}, w}
2047
2048def in.times(n: Nat, +k: AmlArgK) -> List<&2, AmlArgK>:
2049  match n:
2050    case 0n:
2051      Nil{}
2052    case 1n+p:
2053      Con{k, in.times(p, k)}
2054
2055def in.invoke(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +p: String, +nargs: Nat, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2056  in.start(~H, ~io, AmlOpCall{p, nargs}, in.times(nargs, AmlKTerm{}), c, fs, w)
2057
2058# Names as operands
2059
2060def in.name.val(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, o: Maybe<&2, S.AmlObject>, +p: String, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2061  match o:
2062    case Some{S.AmlOMethod{n, f, b}}:
2063      in.invoke(~H, ~io, p, n, c, fs, w)
2064    case Some{S.AmlOBuiltin{i}}:
2065      in.start(~H, ~io, AmlOpOsi{}, [AmlKTerm{}], c, fs, w)
2066    case _:
2067      in.read.give(H, in.read_obj(~H, ~io, w, p, o), c, fs, w)
2068
2069def in.name.base(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, o: Maybe<&2, S.AmlObject>, +p: String, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2070  match o:
2071    case Some{S.AmlOMethod{n, f, b}}:
2072      in.invoke(~H, ~io, p, n, c, fs, w)
2073    case _:
2074      in.give(H, V.AmlRef{V.AmlLName{p}}, c, fs, w)
2075
2076def in.name.res(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, k: AmlArgK, m: Maybe<&2, String>, +n: N.AmlName, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2077  match k m:
2078    case AmlKTarget{} Some{p}:
2079      in.give(H, V.AmlRef{V.AmlLName{p}}, c, fs, w)
2080    case AmlKCond{} Some{p}:
2081      in.give(H, V.AmlRef{V.AmlLName{p}}, c, fs, w)
2082    case AmlKCond{} None{}:
2083      in.give(H, V.AmlUninit{}, c, fs, w)
2084    case AmlKElem{} Some{p}:
2085      in.give(H, V.AmlRef{V.AmlLName{p}}, c, fs, w)
2086    case AmlKElem{} None{}:
2087      in.give(H, V.AmlRef{V.AmlLName{S.AmlPath.of_name(in.scope(H, w), n)}}, c, fs, w)
2088    case AmlKBase{} Some{+p}:
2089      +q = in.unalias(AmlWorld.ns(H, w), p)
2090      in.name.base(~H, ~io, S.AmlNs.get(AmlWorld.ns(H, w), q), q, c, fs, w)
2091    case _ Some{+p}:
2092      +q = in.unalias(AmlWorld.ns(H, w), p)
2093      in.name.val(~H, ~io, S.AmlNs.get(AmlWorld.ns(H, w), q), q, c, fs, w)
2094    case _ None{}:
2095      AmlMachine{AmlMFail{E.AcpiAmlUndefined{N.AmlName.show(n)}}, c, fs, w}
2096
2097def in.name.go(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, r: Result<&2, &2, E.AcpiError, AmlNameC>, k: AmlArgK, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2098  match r:
2099    case Fail{e}:
2100      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2101    case Done{AmlNameC{+n, c}}:
2102      match k:
2103        case AmlKName{}:
2104          in.give(H, V.AmlRef{V.AmlLName{S.AmlPath.of_name(in.scope(H, w), n)}}, c, fs, w)
2105        case _:
2106          in.name.res(~H, ~io, k, S.AmlNs.resolve(AmlWorld.ns(H, w), in.scope(H, w), n), n, c, fs, w)
2107
2108# Data objects
2109
2110def in.imm.give(-H: Data, +wide: Bool, r: Result<&2, &2, E.AcpiError, AmlImm>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2111  match r:
2112    case Fail{e}:
2113      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2114    case Done{AmlImm{v, c}}:
2115      AmlMachine{AmlMGive{V.AmlInt{V.AmlInt.fit(wide, v)}}, c, fs, w}
2116
2117type AmlStrL is Data:
2118  AmlStrL{bytes: List<&2, U32>, size: Nat}
2119
2120def in.str.z(xs: List<&2, U32>) -> Bool:
2121  match xs:
2122    case Con{+h, t}:
2123      U32.is_eq(h, 0)
2124    case Nil{}:
2125      False{}
2126
2127def in.str.go(n: Nat, xs: List<&2, U32>, z: Bool, acc: List<&2, U32>, +k: Nat) -> Maybe<&2, AmlStrL>:
2128  match n:
2129    case 0n:
2130      None{}
2131    case 1n+p:
2132      match xs:
2133        case Nil{}:
2134          None{}
2135        case Con{h, +t}:
2136          match z:
2137            case True{}:
2138              Some{AmlStrL{List.reverse(&2, U32, acc), Nat.add(k, 1n)}}
2139            case False{}:
2140              in.str.go(p, t, in.str.z(t), Con{h, acc}, Nat.add(k, 1n))
2141
2142def in.str.give(-H: Data, m: Maybe<&2, AmlStrL>, +c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2143  match m:
2144    case None{}:
2145      AmlMachine{AmlMFail{E.AcpiAmlTruncated{}}, c, fs, w}
2146    case Some{AmlStrL{bs, +n}}:
2147      AmlMachine{AmlMGive{V.AmlStr{B.Octets.of_list(bs)}}, cur.skip(n, c), fs, w}
2148
2149# a String: its bytes up to the NUL
2150def in.string(-H: Data, +c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2151  match c:
2152    case AmlCur{+code, +lim}:
2153      in.str.give(H, in.str.go(lim, code, in.str.z(code), Nil{}, 0n), AmlCur{code, lim}, fs, w)
2154
2155def in.buffer(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2156  match r:
2157    case Fail{e}:
2158      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2159    case Done{AmlPkgC{body, after}}:
2160      AmlMachine{AmlMEval{AmlKTerm{}}, body, Con{AmlFBuffer{after}, fs}, w}
2161
2162def in.pad(n: Nat, xs: List<&2, V.AmlValue>) -> List<&2, V.AmlValue>:
2163  match n xs:
2164    case 0n _:
2165      xs
2166    case 1n+p Nil{}:
2167      Con{V.AmlUninit{}, in.pad(p, Nil{})}
2168    case 1n+p Con{h, t}:
2169      Con{h, in.pad(p, t)}
2170
2171def in.pkg.first(-H: Data, empty: Bool, +n: Nat, body: AmlCur, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2172  match empty:
2173    case True{}:
2174      AmlMachine{AmlMGive{V.AmlPkg{in.pad(n, Nil{})}}, after, fs, w}
2175    case False{}:
2176      AmlMachine{AmlMEval{AmlKElem{}}, body, Con{AmlFPkg{n, Nil{}, after}, fs}, w}
2177
2178def in.pkg.start(-H: Data, r: Result<&2, &2, E.AcpiError, AmlImm>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2179  match r:
2180    case Fail{e}:
2181      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2182    case Done{AmlImm{n, +body}}:
2183      in.pkg.first(H, cur.at_end(body), W.W64.to_nat(n), body, after, fs, w)
2184
2185def in.package(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2186  match r:
2187    case Fail{e}:
2188      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2189    case Done{AmlPkgC{body, after}}:
2190      in.pkg.start(H, cur.imm(1n, body), after, fs, w)
2191
2192def in.varpackage(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2193  match r:
2194    case Fail{e}:
2195      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2196    case Done{AmlPkgC{body, after}}:
2197      AmlMachine{AmlMEval{AmlKTerm{}}, body, Con{AmlFVarPkg{after}, fs}, w}
2198
2199def in.zero(-H: Data, k: AmlArgK, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2200  match k:
2201    case AmlKTarget{}:
2202      in.give(H, V.AmlRef{V.AmlLNone{}}, c, fs, w)
2203    case AmlKCond{}:
2204      in.give(H, V.AmlRef{V.AmlLNone{}}, c, fs, w)
2205    case _:
2206      in.give(H, V.AmlInt{W.W64.zero()}, c, fs, w)
2207
2208def in.lvar(-H: Data, k: AmlArgK, l: V.AmlLoc, v: V.AmlValue, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2209  match k:
2210    case AmlKTarget{}:
2211      in.give(H, V.AmlRef{l}, c, fs, w)
2212    case AmlKBase{}:
2213      in.give(H, V.AmlRef{l}, c, fs, w)
2214    case AmlKCond{}:
2215      in.give(H, V.AmlRef{l}, c, fs, w)
2216    case _:
2217      in.give(H, v, c, fs, w)
2218
2219# Statements that hold term lists
2220
2221def in.enter(-H: Data, +path: String, body: AmlCur, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2222  AmlMachine{AmlMExec{}, body, Con{AmlFSeq{after, in.scope(H, w)}, fs}, in.with_scope(H, w, path)}
2223
2224def in.scope.target(m: Maybe<&2, String>, +scope: String, n: N.AmlName) -> String:
2225  match m:
2226    case Some{p}:
2227      p
2228    case None{}:
2229      S.AmlPath.of_name(scope, n)
2230
2231def in.scope.k(-H: Data, r: Result<&2, &2, E.AcpiError, AmlNameC>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2232  match r:
2233    case Fail{e}:
2234      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2235    case Done{AmlNameC{+n, body}}:
2236      +p = in.scope.target(S.AmlNs.resolve(AmlWorld.ns(H, w), in.scope(H, w), n), in.scope(H, w), n)
2237      in.enter(H, p, body, after, fs, w)
2238
2239# Scope (chapter 19): the term list runs in the named scope
2240def in.scope.op(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2241  match r:
2242    case Fail{e}:
2243      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2244    case Done{AmlPkgC{body, after}}:
2245      in.scope.k(H, cur.name(body), after, fs, w)
2246
2247def in.method.flags(-H: Data, +p: String, r: Result<&2, &2, E.AcpiError, AmlB>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2248  match r:
2249    case Fail{e}:
2250      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2251    case Done{AmlB{+f, +c}}:
2252      in.def.chk(H, S.AmlNs.has(AmlWorld.ns(H, w), p), p, S.AmlOMethod{U32.to_nat(U32.and(f, 7)), f, cur.take(cur.len(c), c)}, after, fs, w)
2253
2254def in.method.k(-H: Data, rn: Result<&2, &2, E.AcpiError, AmlNameC>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2255  match rn:
2256    case Fail{e}:
2257      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2258    case Done{AmlNameC{n, c}}:
2259      in.method.flags(H, S.AmlPath.of_name(in.scope(H, w), n), cur.byte(c), after, fs, w)
2260
2261# Method (chapter 19): defined, its body kept for when it is called
2262def in.method.op(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2263  match r:
2264    case Fail{e}:
2265      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2266    case Done{AmlPkgC{body, after}}:
2267      in.method.k(H, cur.name(body), after, fs, w)
2268
2269def in.dev.go(-H: Data, dup: Bool, +p: String, +kind: U32, body: AmlCur, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2270  match dup:
2271    case True{}:
2272      AmlMachine{AmlMFail{E.AcpiAmlDuplicate{p}}, body, fs, w}
2273    case False{}:
2274      in.enter(H, p, body, after, fs, in.define(H, w, p, S.AmlOScope{kind}))
2275
2276def in.dev.fits(-H: Data, ok: Bool, +p: String, +kind: U32, body: AmlCur, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2277  match ok:
2278    case False{}:
2279      AmlMachine{AmlMFail{E.AcpiAmlTruncated{}}, body, fs, w}
2280    case True{}:
2281      in.dev.go(H, S.AmlNs.has(AmlWorld.ns(H, w), p), p, kind, body, after, fs, w)
2282
2283def in.dev.k(-H: Data, +kind: U32, +extra: Nat, rn: Result<&2, &2, E.AcpiError, AmlNameC>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2284  match rn:
2285    case Fail{e}:
2286      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2287    case Done{AmlNameC{n, +c}}:
2288      +p = S.AmlPath.of_name(in.scope(H, w), n)
2289      in.dev.fits(H, Nat.is_le(extra, cur.len(c)), p, kind, cur.skip(extra, c), after, fs, w)
2290
2291# Device, Processor, PowerResource, ThermalZone (chapter 19): an object whose term list runs in its own scope;
2292# Processor's ID and block and PowerResource's level and order are skipped
2293def in.dev.op(-H: Data, +kind: U32, +extra: Nat, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2294  match r:
2295    case Fail{e}:
2296      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2297    case Done{AmlPkgC{body, after}}:
2298      in.dev.k(H, kind, extra, cur.name(body), after, fs, w)
2299
2300def in.if.op(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2301  match r:
2302    case Fail{e}:
2303      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2304    case Done{AmlPkgC{body, after}}:
2305      AmlMachine{AmlMEval{AmlKTerm{}}, body, Con{AmlFIf{after}, fs}, w}
2306
2307def in.while.op(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2308  match r:
2309    case Fail{e}:
2310      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2311    case Done{AmlPkgC{+body, after}}:
2312      AmlMachine{AmlMEval{AmlKTerm{}}, body, Con{AmlFWhile{body, after, False{}}, fs}, w}
2313
2314def in.skip.op(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2315  match r:
2316    case Fail{e}:
2317      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2318    case Done{AmlPkgC{body, after}}:
2319      AmlMachine{AmlMExec{}, after, fs, w}
2320
2321# Field and IndexField (chapter 19): the field list is read in one
2322# step, a field unit defined for each NamedField
2323
2324# what the field units are of
2325type AmlFk is Data:
2326  AmlFkRegion{region: String}
2327  AmlFkIndex{index: String, data: String}
2328
2329type AmlFlSt<-H: Data> is Data:
2330  AmlFlSt{c: AmlCur, off: Nat, flags: U32, w: AmlWorld<H>}
2331
2332type AmlFlNext<-H: Data> is Data:
2333  AmlFlMore{st: AmlFlSt<H>}
2334  AmlFlEnd{w: AmlWorld<H>}
2335
2336def fl.unit(k: AmlFk, +off: Nat, +bits: Nat, +flags: U32) -> S.AmlObject:
2337  match k:
2338    case AmlFkRegion{r}:
2339      S.AmlOField{r, off, bits, flags}
2340    case AmlFkIndex{i, d}:
2341      S.AmlOIndexField{i, d, off, bits, flags}
2342
2343def fl.bits.fit(ok: Bool, v: U32, c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlImm>:
2344  match ok:
2345    case True{}:
2346      Done{AmlImm{W.W64.from_u32(v), c}}
2347    case False{}:
2348      Fail{E.AcpiAmlTruncated{}}
2349
2350def fl.bits.go(r: Result<&2, &2, E.AcpiError, K.AmlPkgL>, +lim: Nat) -> Result<&2, &2, E.AcpiError, AmlImm>:
2351  match r:
2352    case Fail{e}:
2353      Fail{e}
2354    case Done{K.AmlPkgL{v, +size, rest}}:
2355      fl.bits.fit(Nat.is_le(size, lim), v, AmlCur{rest, Nat.sub(lim, size)})
2356
2357# a PkgLength used as a number of bits
2358def fl.bits(c: AmlCur) -> Result<&2, &2, E.AcpiError, AmlImm>:
2359  match c:
2360    case AmlCur{+code, +lim}:
2361      fl.bits.go(K.pk.dec(code), lim)
2362
2363def fl.reserved(-H: Data, r: Result<&2, &2, E.AcpiError, AmlImm>, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2364  match r:
2365    case Fail{e}:
2366      Fail{e}
2367    case Done{AmlImm{n, c}}:
2368      Done{AmlFlMore{AmlFlSt{c, Nat.add(off, W.W64.to_nat(n)), flags, w}}}
2369
2370def fl.access.fit(-H: Data, ok: Bool, c: AmlCur, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2371  match ok:
2372    case True{}:
2373      Done{AmlFlMore{AmlFlSt{c, off, flags, w}}}
2374    case False{}:
2375      Fail{E.AcpiAmlTruncated{}}
2376
2377def fl.access(-H: Data, +skip: Nat, r: Result<&2, &2, E.AcpiError, AmlB>, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2378  match r:
2379    case Fail{e}:
2380      Fail{e}
2381    case Done{AmlB{t, +c}}:
2382      fl.access.fit(H, Nat.is_le(skip, cur.len(c)), cur.skip(skip, c), off, U32.or(U32.and(flags, 4294967280), U32.and(t, 15)), w)
2383
2384def fl.named.def(-H: Data, dup: Bool, +p: String, o: S.AmlObject, c: AmlCur, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2385  match dup:
2386    case True{}:
2387      Fail{E.AcpiAmlDuplicate{p}}
2388    case False{}:
2389      Done{AmlFlMore{AmlFlSt{c, off, flags, in.define(H, w, p, o)}}}
2390
2391def fl.named.k(-H: Data, k: AmlFk, +seg: String, r: Result<&2, &2, E.AcpiError, AmlImm>, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2392  match r:
2393    case Fail{e}:
2394      Fail{e}
2395    case Done{AmlImm{n, c}}:
2396      +bits = W.W64.to_nat(n)
2397      +p = S.AmlPath.child(in.scope(H, w), seg)
2398      fl.named.def(H, S.AmlNs.has(AmlWorld.ns(H, w), p), p, fl.unit(k, off, bits, flags), c, Nat.add(off, bits), flags, w)
2399
2400def fl.named.chk(-H: Data, k: AmlFk, ok: Bool, +seg: String, +c: AmlCur, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2401  match ok:
2402    case False{}:
2403      Fail{E.AcpiAmlBadName{}}
2404    case True{}:
2405      fl.named.k(H, k, seg, fl.bits(c), off, flags, w)
2406
2407def fl.named.seg(-H: Data, k: AmlFk, ok: Bool, +b: U32, +c: AmlCur, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2408  match ok:
2409    case False{}:
2410      Fail{E.AcpiAmlTruncated{}}
2411    case True{}:
2412      +seg = B.Octets.append(B.Octets.of_list([b]), cur.take(3n, c))
2413      fl.named.chk(H, k, N.AmlName.seg_ok(seg), B.Octets.to_string(seg), cur.skip(3n, c), off, flags, w)
2414
2415def fl.named(-H: Data, k: AmlFk, +b: U32, +c: AmlCur, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2416  fl.named.seg(H, k, Nat.is_le(3n, cur.len(c)), b, c, off, flags, w)
2417
2418def fl.elem(-H: Data, k: AmlFk, +n: Nat, +b: U32, +c: AmlCur, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2419  match n:
2420    case 0n:
2421      fl.reserved(H, fl.bits(c), off, flags, w)
2422    case 1n:
2423      fl.access(H, 1n, cur.byte(c), off, flags, w)
2424    case 2n:
2425      Fail{E.AcpiAmlUnsupported{"ConnectField"}}
2426    case 3n:
2427      fl.access(H, 2n, cur.byte(c), off, flags, w)
2428    case _:
2429      fl.named(H, k, b, c, off, flags, w)
2430
2431def fl.byte(-H: Data, k: AmlFk, r: Result<&2, &2, E.AcpiError, AmlB>, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2432  match r:
2433    case Fail{e}:
2434      Fail{e}
2435    case Done{AmlB{+b, c}}:
2436      fl.elem(H, k, U32.to_nat(b), b, c, off, flags, w)
2437
2438def fl.step.go(-H: Data, k: AmlFk, end: Bool, +c: AmlCur, +off: Nat, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2439  match end:
2440    case True{}:
2441      Done{AmlFlEnd{w}}
2442    case False{}:
2443      fl.byte(H, k, cur.byte(c), off, flags, w)
2444
2445def fl.step(-H: Data, k: AmlFk, st: AmlFlSt<H>) -> Result<&2, &2, E.AcpiError, AmlFlNext<H>>:
2446  match st:
2447    case AmlFlSt{+c, off, flags, w}:
2448      fl.step.go(H, k, cur.at_end(c), c, off, flags, w)
2449
2450# every element takes at least two bytes, so the list length is enough fuel
2451def fl.loop(-H: Data, fuel: Nat, +k: AmlFk, r: Result<&2, &2, E.AcpiError, AmlFlNext<H>>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
2452  match fuel:
2453    case 0n:
2454      match r:
2455        case Fail{e}:
2456          Fail{e}
2457        case Done{AmlFlEnd{w}}:
2458          Done{w}
2459        case Done{AmlFlMore{st}}:
2460          Fail{E.AcpiAmlTruncated{}}
2461    case 1n+p:
2462      match r:
2463        case Fail{e}:
2464          Fail{e}
2465        case Done{AmlFlEnd{w}}:
2466          Done{w}
2467        case Done{AmlFlMore{st}}:
2468          fl.loop(H, p, k, fl.step(H, k, st))
2469
2470def fl.run(-H: Data, +k: AmlFk, +c: AmlCur, +flags: U32, +w: AmlWorld<H>) -> Result<&2, &2, E.AcpiError, AmlWorld<H>>:
2471  fl.loop(H, cur.len(c), k, Done{AmlFlMore{AmlFlSt{c, 0n, flags, w}}})
2472
2473def fl.done(-H: Data, r: Result<&2, &2, E.AcpiError, AmlWorld<H>>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2474  match r:
2475    case Fail{e}:
2476      AmlMachine{AmlMFail{e}, after, fs, w}
2477    case Done{w2}:
2478      AmlMachine{AmlMExec{}, after, fs, w2}
2479
2480def fl.flags(-H: Data, +k: AmlFk, r: Result<&2, &2, E.AcpiError, AmlB>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2481  match r:
2482    case Fail{e}:
2483      AmlMachine{AmlMFail{e}, after, fs, w}
2484    case Done{AmlB{f, c}}:
2485      fl.done(H, fl.run(H, k, c, f, w), after, fs, w)
2486
2487def fl.path(-H: Data, +n: N.AmlName, +w: AmlWorld<H>) -> String:
2488  in.scope.target(S.AmlNs.resolve(AmlWorld.ns(H, w), in.scope(H, w), n), in.scope(H, w), n)
2489
2490def fl.region.k(-H: Data, rn: Result<&2, &2, E.AcpiError, AmlNameC>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2491  match rn:
2492    case Fail{e}:
2493      AmlMachine{AmlMFail{e}, after, fs, w}
2494    case Done{AmlNameC{n, c}}:
2495      fl.flags(H, AmlFkRegion{fl.path(H, n, w)}, cur.byte(c), after, fs, w)
2496
2497def fl.field.op(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2498  match r:
2499    case Fail{e}:
2500      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2501    case Done{AmlPkgC{body, after}}:
2502      fl.region.k(H, cur.name(body), after, fs, w)
2503
2504def fl.index.d(-H: Data, +i: String, rn: Result<&2, &2, E.AcpiError, AmlNameC>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2505  match rn:
2506    case Fail{e}:
2507      AmlMachine{AmlMFail{e}, after, fs, w}
2508    case Done{AmlNameC{n, c}}:
2509      fl.flags(H, AmlFkIndex{i, fl.path(H, n, w)}, cur.byte(c), after, fs, w)
2510
2511def fl.index.k(-H: Data, rn: Result<&2, &2, E.AcpiError, AmlNameC>, after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2512  match rn:
2513    case Fail{e}:
2514      AmlMachine{AmlMFail{e}, after, fs, w}
2515    case Done{AmlNameC{n, c}}:
2516      fl.index.d(H, fl.path(H, n, w), cur.name(c), after, fs, w)
2517
2518def fl.indexfield.op(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2519  match r:
2520    case Fail{e}:
2521      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2522    case Done{AmlPkgC{body, after}}:
2523      fl.index.k(H, cur.name(body), after, fs, w)
2524
2525# Terms: the dispatch on the first byte
2526
2527def in.unsupported(-H: Data, +what: String, c: AmlCur, fs: List<&2, AmlFrame>, w: AmlWorld<H>) -> AmlMachine<H>:
2528  AmlMachine{AmlMFail{E.AcpiAmlUnsupported{what}}, c, fs, w}
2529
2530def in.expr.ok(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, ok: Bool, +op: Nat, +code: U32, ks: List<&2, AmlArgK>, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2531  match ok:
2532    case True{}:
2533      in.start(~H, ~io, AmlOpCode{U32.from_nat(op)}, ks, c, fs, w)
2534    case False{}:
2535      AmlMachine{AmlMFail{E.AcpiAmlBadOperand{code}}, c, fs, w}
2536
2537def in.unknown.name(+n: Nat) -> String:
2538  match n:
2539    case 132n:
2540      "ConcatenateResTemplate"
2541    case 137n:
2542      "Match"
2543    case 151n:
2544      "ToDecimalString"
2545    case 152n:
2546      "ToHexString"
2547    case 156n:
2548      "ToString"
2549    case 158n:
2550      "Mid"
2551    case _:
2552      ""
2553
2554def in.unknown.go(-H: Data, bad: Bool, what: String, code: U32, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2555  match bad:
2556    case True{}:
2557      AmlMachine{AmlMFail{E.AcpiAmlBadOpcode{code}}, c, fs, w}
2558    case False{}:
2559      AmlMachine{AmlMFail{E.AcpiAmlUnsupported{what}}, c, fs, w}
2560
2561def in.unknown.pick(-H: Data, +what: String, +code: U32, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2562  in.unknown.go(H, String.is_empty(what), what, code, c, fs, w)
2563
2564# an opcode with no operator here: AcpiAmlUnsupported if ACPI defines it
2565# (named in README.md), AcpiAmlBadOpcode otherwise
2566def in.unknown(-H: Data, +n: Nat, +code: U32, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2567  in.unknown.pick(H, in.unknown.name(n), code, c, fs, w)
2568
2569def in.expr(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +n: Nat, +code: U32, m: Maybe<&2, List<&2, AmlArgK>>, exec: Bool, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2570  match m:
2571    case None{}:
2572      in.unknown(H, n, code, c, fs, w)
2573    case Some{ks}:
2574      in.expr.ok(~H, ~io, Bool.or(exec, Bool.not(in.is_stmt(n))), n, code, ks, c, fs, w)
2575
2576def in.stmt.ext(-H: Data, +x: Nat, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2577  match x:
2578    case 129n:
2579      fl.field.op(H, cur.pkg(c), fs, w)
2580    case 130n:
2581      in.dev.op(H, 6, 0n, cur.pkg(c), fs, w)
2582    case 131n:
2583      in.dev.op(H, 12, 6n, cur.pkg(c), fs, w)
2584    case 132n:
2585      in.dev.op(H, 11, 3n, cur.pkg(c), fs, w)
2586    case 133n:
2587      in.dev.op(H, 13, 0n, cur.pkg(c), fs, w)
2588    case _:
2589      fl.indexfield.op(H, cur.pkg(c), fs, w)
2590
2591def in.stmt.ext.chk(-H: Data, exec: Bool, +x: Nat, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2592  match exec:
2593    case True{}:
2594      in.stmt.ext(H, x, c, fs, w)
2595    case False{}:
2596      AmlMachine{AmlMFail{E.AcpiAmlBadOperand{U32.add(23296, U32.from_nat(x))}}, c, fs, w}
2597
2598# an extended opcode (0x5B, then this byte)
2599def in.term.ext(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, k: AmlArgK, +x: Nat, +e: U32, +exec: Bool, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2600  match x:
2601    case 49n:
2602      in.lvar(H, k, V.AmlLDebug{}, V.AmlUninit{}, c, fs, w)
2603    case 129n:
2604      in.stmt.ext.chk(H, exec, 129n, c, fs, w)
2605    case 130n:
2606      in.stmt.ext.chk(H, exec, 130n, c, fs, w)
2607    case 131n:
2608      in.stmt.ext.chk(H, exec, 131n, c, fs, w)
2609    case 132n:
2610      in.stmt.ext.chk(H, exec, 132n, c, fs, w)
2611    case 133n:
2612      in.stmt.ext.chk(H, exec, 133n, c, fs, w)
2613    case 134n:
2614      in.stmt.ext.chk(H, exec, 134n, c, fs, w)
2615    case 135n:
2616      in.unsupported(H, "BankField", c, fs, w)
2617    case 136n:
2618      in.unsupported(H, "DataTableRegion", c, fs, w)
2619    case 31n:
2620      in.unsupported(H, "LoadTable", c, fs, w)
2621    case 32n:
2622      in.unsupported(H, "Load", c, fs, w)
2623    case 42n:
2624      in.unsupported(H, "Unload", c, fs, w)
2625    case 40n:
2626      in.unsupported(H, "FromBCD", c, fs, w)
2627    case 41n:
2628      in.unsupported(H, "ToBCD", c, fs, w)
2629    case _:
2630      in.expr(~H, ~io, Nat.add(256n, x), U32.add(23296, e), in.kinds(Nat.add(256n, x)), exec, c, fs, w)
2631
2632def in.term.extb(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, k: AmlArgK, r: Result<&2, &2, E.AcpiError, AmlB>, +exec: Bool, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2633  match r:
2634    case Fail{e}:
2635      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2636    case Done{AmlB{+e, c}}:
2637      in.term.ext(~H, ~io, k, U32.to_nat(e), e, exec, c, fs, w)
2638
2639def in.name.lead.go(k: N.AmlLeadKind) -> Bool:
2640  match k:
2641    case N.AmlLNull{}:
2642      False{}
2643    case N.AmlLOther{}:
2644      False{}
2645    case _:
2646      True{}
2647
2648def in.name.lead(+b: U32) -> Bool:
2649  in.name.lead.go(N.AmlLead.classify(b))
2650
2651# the cursor with b in front again (a NameString is read from its start)
2652def in.unread(+b: U32, c: AmlCur) -> AmlCur:
2653  match c:
2654    case AmlCur{code, lim}:
2655      AmlCur{Con{b, code}, 1n+lim}
2656
2657def in.term.rest.pick(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, local: Bool, arg: Bool, name: Bool, k: AmlArgK, +n: Nat, +b: U32, +exec: Bool, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2658  match local:
2659    case True{}:
2660      +i = Nat.sub(n, 96n)
2661      in.lvar(H, k, V.AmlLLocal{i}, in.ctx.local(H, w, i), c, fs, w)
2662    case False{}:
2663      match arg:
2664        case True{}:
2665          +i = Nat.sub(n, 104n)
2666          in.lvar(H, k, V.AmlLArg{i}, in.ctx.arg(H, w, i), c, fs, w)
2667        case False{}:
2668          match name:
2669            case True{}:
2670              in.name.go(~H, ~io, cur.name(in.unread(b, c)), k, fs, w)
2671            case False{}:
2672              in.expr(~H, ~io, n, b, in.kinds(n), exec, c, fs, w)
2673
2674def in.term.rest(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, k: AmlArgK, +n: Nat, +b: U32, +exec: Bool, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2675  in.term.rest.pick(~H, ~io, Bool.and(Nat.is_le(96n, n), Nat.is_le(n, 103n)), Bool.and(Nat.is_le(104n, n), Nat.is_le(n, 110n)), in.name.lead(b), k, n, b, exec, c, fs, w)
2676
2677def in.stmt.go(-H: Data, +n: Nat, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2678  match n:
2679    case 16n:
2680      in.scope.op(H, cur.pkg(c), fs, w)
2681    case 20n:
2682      in.method.op(H, cur.pkg(c), fs, w)
2683    case 160n:
2684      in.if.op(H, cur.pkg(c), fs, w)
2685    case 161n:
2686      in.skip.op(H, cur.pkg(c), fs, w)
2687    case 162n:
2688      in.while.op(H, cur.pkg(c), fs, w)
2689    case 165n:
2690      in.unwind.brk(H, fs, w)
2691    case 159n:
2692      in.unwind.cont(H, fs, w)
2693    case _:
2694      AmlMachine{AmlMExec{}, c, fs, w}
2695
2696# a statement: refused (AcpiAmlBadOperand) where a value is wanted
2697def in.stmt(-H: Data, exec: Bool, +n: Nat, c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2698  match exec:
2699    case True{}:
2700      in.stmt.go(H, n, c, fs, w)
2701    case False{}:
2702      AmlMachine{AmlMFail{E.AcpiAmlBadOperand{U32.from_nat(n)}}, c, fs, w}
2703
2704# the term whose first byte b has been read; exec: at statement level
2705def in.term(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, +n: Nat, k: AmlArgK, +b: U32, +exec: Bool, +c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2706  match n:
2707    case 0n:
2708      in.zero(H, k, c, fs, w)
2709    case 1n:
2710      in.give(H, V.AmlInt{W.W64.one()}, c, fs, w)
2711    case 255n:
2712      in.give(H, V.AmlInt{V.AmlInt.ones(in.wide(H, w))}, c, fs, w)
2713    case 10n:
2714      in.imm.give(H, in.wide(H, w), cur.imm(1n, c), fs, w)
2715    case 11n:
2716      in.imm.give(H, in.wide(H, w), cur.imm(2n, c), fs, w)
2717    case 12n:
2718      in.imm.give(H, in.wide(H, w), cur.imm(4n, c), fs, w)
2719    case 14n:
2720      in.imm.give(H, in.wide(H, w), cur.imm(8n, c), fs, w)
2721    case 13n:
2722      in.string(H, c, fs, w)
2723    case 17n:
2724      in.buffer(H, cur.pkg(c), fs, w)
2725    case 18n:
2726      in.package(H, cur.pkg(c), fs, w)
2727    case 19n:
2728      in.varpackage(H, cur.pkg(c), fs, w)
2729    case 91n:
2730      in.term.extb(~H, ~io, k, cur.byte(c), exec, fs, w)
2731    case 16n:
2732      in.stmt(H, exec, 16n, c, fs, w)
2733    case 20n:
2734      in.stmt(H, exec, 20n, c, fs, w)
2735    case 160n:
2736      in.stmt(H, exec, 160n, c, fs, w)
2737    case 161n:
2738      in.stmt(H, exec, 161n, c, fs, w)
2739    case 162n:
2740      in.stmt(H, exec, 162n, c, fs, w)
2741    case 163n:
2742      in.stmt(H, exec, 163n, c, fs, w)
2743    case 204n:
2744      in.stmt(H, exec, 204n, c, fs, w)
2745    case 165n:
2746      in.stmt(H, exec, 165n, c, fs, w)
2747    case 159n:
2748      in.stmt(H, exec, 159n, c, fs, w)
2749    case _:
2750      in.term.rest(~H, ~io, k, n, b, exec, c, fs, w)
2751
2752def in.read.term(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, k: AmlArgK, r: Result<&2, &2, E.AcpiError, AmlB>, +exec: Bool, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2753  match r:
2754    case Fail{e}:
2755      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2756    case Done{AmlB{+b, c}}:
2757      in.term(~H, ~io, U32.to_nat(b), k, b, exec, c, fs, w)
2758
2759# Eval: one operand
2760def in.eval(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, k: AmlArgK, +c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2761  match k:
2762    case AmlKByte{}:
2763      in.imm.give(H, True{}, cur.imm(1n, c), fs, w)
2764    case AmlKWord{}:
2765      in.imm.give(H, True{}, cur.imm(2n, c), fs, w)
2766    case AmlKDWord{}:
2767      in.imm.give(H, True{}, cur.imm(4n, c), fs, w)
2768    case AmlKName{}:
2769      in.name.go(~H, ~io, cur.name(c), AmlKName{}, fs, w)
2770    case _:
2771      in.read.term(~H, ~io, k, cur.byte(c), False{}, fs, w)
2772
2773def in.skip.else.pick(-H: Data, is_else: Bool, +after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2774  match is_else:
2775    case True{}:
2776      in.skip.op(H, cur.pkg(cur.skip(1n, after)), fs, w)
2777    case False{}:
2778      AmlMachine{AmlMExec{}, after, fs, w}
2779
2780# after an If body: an Else that follows is skipped
2781def in.skip.else(-H: Data, m: Maybe<&2, U32>, +after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2782  match m:
2783    case Some{+b}:
2784      in.skip.else.pick(H, U32.is_eq(b, 161), after, fs, w)
2785    case None{}:
2786      AmlMachine{AmlMExec{}, after, fs, w}
2787
2788# the end of a term list: what the frame on top does next
2789def in.end(-H: Data, fs: List<&2, AmlFrame>, c: AmlCur, +w: AmlWorld<H>) -> AmlMachine<H>:
2790  match fs:
2791    case Con{AmlFSeq{after, scope}, rest}:
2792      AmlMachine{AmlMExec{}, after, rest, in.with_scope(H, w, scope)}
2793    case Con{AmlFIfBody{+after}, rest}:
2794      in.skip.else(H, cur.peek(after), after, rest, w)
2795    case Con{AmlFWhile{+s, after, b}, rest}:
2796      AmlMachine{AmlMEval{AmlKTerm{}}, s, Con{AmlFWhile{s, after, False{}}, rest}, w}
2797    case Con{AmlFCall{saved, back}, rest}:
2798      AmlMachine{AmlMGive{V.AmlUninit{}}, back, rest, in.back(H, w, saved)}
2799    case Con{AmlFTop{}, rest}:
2800      AmlMachine{AmlMDone{V.AmlUninit{}}, c, Con{AmlFTop{}, rest}, w}
2801    case _:
2802      AmlMachine{AmlMFail{E.AcpiAmlTruncated{}}, c, fs, w}
2803
2804def in.else.body(-H: Data, r: Result<&2, &2, E.AcpiError, AmlPkgC>, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2805  match r:
2806    case Fail{e}:
2807      AmlMachine{AmlMFail{e}, in.no.cur(), fs, w}
2808    case Done{AmlPkgC{body, after}}:
2809      AmlMachine{AmlMExec{}, body, Con{AmlFSeq{after, in.scope(H, w)}, fs}, w}
2810
2811def in.else.pick(-H: Data, is_else: Bool, +after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2812  match is_else:
2813    case True{}:
2814      in.else.body(H, cur.pkg(cur.skip(1n, after)), fs, w)
2815    case False{}:
2816      AmlMachine{AmlMExec{}, after, fs, w}
2817
2818# a false If: its Else, if one follows, runs
2819def in.else.run(-H: Data, m: Maybe<&2, U32>, +after: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2820  match m:
2821    case Some{+b}:
2822      in.else.pick(H, U32.is_eq(b, 161), after, fs, w)
2823    case None{}:
2824      AmlMachine{AmlMExec{}, after, fs, w}
2825
2826def in.if.k(-H: Data, r: Result<&2, &2, E.AcpiError, Bool>, c: AmlCur, +after: AmlCur, rest: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2827  match r:
2828    case Fail{e}:
2829      AmlMachine{AmlMFail{e}, c, rest, w}
2830    case Done{True{}}:
2831      AmlMachine{AmlMExec{}, c, Con{AmlFIfBody{after}, rest}, w}
2832    case Done{False{}}:
2833      in.else.run(H, cur.peek(after), after, rest, w)
2834
2835def in.while.k(-H: Data, r: Result<&2, &2, E.AcpiError, Bool>, c: AmlCur, start: AmlCur, after: AmlCur, rest: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2836  match r:
2837    case Fail{e}:
2838      AmlMachine{AmlMFail{e}, c, rest, w}
2839    case Done{True{}}:
2840      AmlMachine{AmlMExec{}, c, Con{AmlFWhile{start, after, True{}}, rest}, w}
2841    case Done{False{}}:
2842      AmlMachine{AmlMExec{}, after, rest, w}
2843
2844def in.buf.k(-H: Data, r: Result<&2, &2, E.AcpiError, W.W64>, +c: AmlCur, after: AmlCur, rest: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2845  match r:
2846    case Fail{e}:
2847      AmlMachine{AmlMFail{e}, c, rest, w}
2848    case Done{n}:
2849      +init = cur.take(cur.len(c), c)
2850      AmlMachine{AmlMGive{V.AmlBuf{in.fit.buf(Nat.max(W.W64.to_nat(n), B.Octets.len(init)), init)}}, after, rest, w}
2851
2852def in.pkg.k(-H: Data, end: Bool, +n: Nat, +got: List<&2, V.AmlValue>, c: AmlCur, after: AmlCur, rest: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2853  match end:
2854    case True{}:
2855      AmlMachine{AmlMGive{V.AmlPkg{in.pad(n, List.reverse(&2, V.AmlValue, got))}}, after, rest, w}
2856    case False{}:
2857      AmlMachine{AmlMEval{AmlKElem{}}, c, Con{AmlFPkg{n, got, after}, rest}, w}
2858
2859def in.varpkg.k(-H: Data, r: Result<&2, &2, E.AcpiError, W.W64>, +c: AmlCur, after: AmlCur, rest: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2860  match r:
2861    case Fail{e}:
2862      AmlMachine{AmlMFail{e}, c, rest, w}
2863    case Done{n}:
2864      in.pkg.k(H, cur.at_end(c), W.W64.to_nat(n), Nil{}, c, after, rest, w)
2865
2866def in.give.args(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, op: AmlOp, got: List<&2, V.AmlValue>, todo: List<&2, AmlArgK>, v: V.AmlValue, c: AmlCur, rest: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2867  match todo:
2868    case Con{k, Con{+k2, m2}}:
2869      AmlMachine{AmlMEval{k2}, c, Con{AmlFArgs{op, Con{v, got}, Con{k2, m2}}, rest}, w}
2870    case _:
2871      in.apply(~H, ~io, op, List.reverse(&2, V.AmlValue, Con{v, got}), c, rest, w)
2872
2873# Give: a value for the frame on top
2874def in.give.to(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, fs: List<&2, AmlFrame>, v: V.AmlValue, +c: AmlCur, +w: AmlWorld<H>) -> AmlMachine<H>:
2875  match fs:
2876    case Con{AmlFArgs{op, got, todo}, rest}:
2877      in.give.args(~H, ~io, op, got, todo, v, c, rest, w)
2878    case Con{AmlFIf{+after}, rest}:
2879      in.if.k(H, in.truth(in.wide(H, w), v), c, after, rest, w)
2880    case Con{AmlFWhile{start, after, False{}}, rest}:
2881      in.while.k(H, in.truth(in.wide(H, w), v), c, start, after, rest, w)
2882    case Con{AmlFBuffer{after}, rest}:
2883      in.buf.k(H, in.small.int(in.wide(H, w), v), c, after, rest, w)
2884    case Con{AmlFPkg{+n, got, after}, rest}:
2885      in.pkg.k(H, cur.at_end(c), n, Con{v, got}, c, after, rest, w)
2886    case Con{AmlFVarPkg{after}, rest}:
2887      in.varpkg.k(H, in.small.int(in.wide(H, w), v), c, after, rest, w)
2888    case _:
2889      AmlMachine{AmlMExec{}, c, fs, w}
2890
2891# Exec: the next term of the list, or its end
2892def in.exec(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, end: Bool, +c: AmlCur, fs: List<&2, AmlFrame>, +w: AmlWorld<H>) -> AmlMachine<H>:
2893  match end:
2894    case True{}:
2895      in.end(H, fs, c, w)
2896    case False{}:
2897      in.read.term(~H, ~io, AmlKTerm{}, cur.byte(c), True{}, fs, w)
2898
2899# One step of the machine
2900def AmlM.step(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, m: AmlMachine<H>) -> AmlMachine<H>:
2901  match m:
2902    case AmlMachine{md, +c, fs, +w}:
2903      match md:
2904        case AmlMExec{}:
2905          in.exec(~H, ~io, cur.at_end(c), c, fs, w)
2906        case AmlMEval{k}:
2907          in.eval(~H, ~io, k, c, fs, w)
2908        case AmlMGive{v}:
2909          in.give.to(~H, ~io, fs, v, c, w)
2910        case AmlMDone{v}:
2911          AmlMachine{AmlMDone{v}, c, fs, w}
2912        case AmlMFail{e}:
2913          AmlMachine{AmlMFail{e}, c, fs, w}
2914
2915# Running: at most n steps
2916
2917type AmlRun<-H: Data> is Data:
2918  AmlRun{m: AmlMachine<H>, steps: Nat}
2919
2920def AmlRun.steps(-H: Data, r: AmlRun<H>) -> Nat:
2921  match r:
2922    case AmlRun{m, s}:
2923      s
2924
2925def AmlRun.machine(-H: Data, r: AmlRun<H>) -> AmlMachine<H>:
2926  match r:
2927    case AmlRun{m, s}:
2928      m
2929
2930# h: m has halted; used: the steps taken so far
2931def AmlM.run.go(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, h: Bool, m: AmlMachine<H>, used: Nat) -> AmlRun<H>:
2932  match n:
2933    case 0n:
2934      AmlRun{m, used}
2935    case 1n+p:
2936      match h:
2937        case True{}:
2938          AmlRun{m, used}
2939        case False{}:
2940          +m2 = AmlM.step(~H, ~io, m)
2941          AmlM.run.go(~H, ~io, p, AmlMachine.halted(H, m2), m2, 1n+used)
2942
2943# the machine run until it halts, or for n steps
2944def AmlM.run(~H: Data, ~io: H -> Hs.AmlHostOp -> Result<&2, &2, E.AcpiError, Hs.AmlHostAns<H>>, n: Nat, +m: AmlMachine<H>) -> AmlRun<H>:
2945  AmlM.run.go(~H, ~io, n, AmlMachine.halted(H, m), m, 0n)