Accelerator.SM86.Immediate

1module Accelerator.SM86.Immediate
2
3family SM86Unsigned32 : Type 0
4constructor SM86Unsigned32Value
5field unrestricted sm86Unsigned32Byte0 : Byte
6field unrestricted sm86Unsigned32Byte1 : Byte
7field unrestricted sm86Unsigned32Byte2 : Byte
8field unrestricted sm86Unsigned32Byte3 : Byte
9
10end-family
11
12def sm86Unsigned32 =
13  (lambda unrestricted b0 : Byte .
14    (lambda unrestricted b1 : Byte .
15      (lambda unrestricted b2 : Byte .
16        (lambda unrestricted b3 : Byte .
17          (constructor SM86Unsigned32 SM86Unsigned32Value b0 b1 b2 b3)))))
18
19def sm86Unsigned32Zero : (family SM86Unsigned32) =
20  (constructor SM86Unsigned32 SM86Unsigned32Value (byte 0) (byte 0) (byte 0) (byte 0))
21
22def sm86Unsigned32One : (family SM86Unsigned32) =
23  (constructor SM86Unsigned32 SM86Unsigned32Value (byte 1) (byte 0) (byte 0) (byte 0))
24
25-- Encoding modulo 2^32 is explicit. Callers accepting unbounded values
26-- must admit their extents before using this transport conversion.
27def sm86Unsigned32FromNaturalTruncated =
28  (lambda unrestricted value : Nat .
29    (sm86Unsigned32 (nat-to-byte value) (nat-to-byte (nat-divide value 256))
30      (nat-to-byte (nat-divide value 65536)) (nat-to-byte (nat-divide value 16777216))))
31
32def encodeSM86Unsigned32LE =
33  (lambda unrestricted value : (family SM86Unsigned32) .
34    (eliminate
35      SM86Unsigned32
36      (lambda unrestricted current : (family SM86Unsigned32) . Bytes)
37      value
38      (branch SM86Unsigned32Value b0 b1 b2 b3 . (bytes b0 b1 b2 b3))))