aml_interp.bend
bend-osdev-acpi@0.1.2.0 · 2,945 lines · 0 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.1/word64.bend as W
24import bend-osdev-bytes@0.1.1.1/bytes.bend as B
25import bend-osdev-acpi@0.1.2.0/error.bend as E
26import bend-osdev-acpi@0.1.2.0/aml_pkglength.bend as K
27import bend-osdev-acpi@0.1.2.0/aml_name.bend as N
28import bend-osdev-acpi@0.1.2.0/aml_value.bend as V
29import bend-osdev-acpi@0.1.2.0/aml_ns.bend as S
30import bend-osdev-acpi@0.1.2.0/aml_host.bend as Hs
31import bend-osdev-acpi@0.1.2.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)