Accelerator.SM86.QMD

1module Accelerator.SM86.QMD
2
3family SM86QMDWord32 : Type 0
4constructor SM86QMDWord32Value
5field unrestricted sm86QMDWord32Byte0 : Byte
6field unrestricted sm86QMDWord32Byte1 : Byte
7field unrestricted sm86QMDWord32Byte2 : Byte
8field unrestricted sm86QMDWord32Byte3 : Byte
9end-family
10
11family SM86QMDPhysicalConfig : Type 0
12constructor SM86QMDPhysicalConfigValue
13field unrestricted sm86QMDPrefetchBaseShifted : (family SM86QMDWord32)
14field unrestricted sm86QMDGridX : (family SM86QMDWord32)
15field unrestricted sm86QMDGridYField : (family SM86QMDWord32)
16field unrestricted sm86QMDGridZField : (family SM86QMDWord32)
17field unrestricted sm86QMDSharedMemoryField : (family SM86QMDWord32)
18field unrestricted sm86QMDBlockXField : (family SM86QMDWord32)
19field unrestricted sm86QMDBlockYZField : (family SM86QMDWord32)
20field unrestricted sm86QMDRegisterField : (family SM86QMDWord32)
21field unrestricted sm86QMDConstantBufferLow : (family SM86QMDWord32)
22field unrestricted sm86QMDConstantBufferHighField : (family SM86QMDWord32)
23field unrestricted sm86QMDProgramAddressLow : (family SM86QMDWord32)
24field unrestricted sm86QMDProgramAddressHighField : (family SM86QMDWord32)
25field unrestricted sm86QMDPrefetchControlField : (family SM86QMDWord32)
26end-family
27
28def sm86QMDWord32 =
29  (lambda unrestricted byte0 : Byte .
30    (lambda unrestricted byte1 : Byte .
31      (lambda unrestricted byte2 : Byte .
32        (lambda unrestricted byte3 : Byte .
33          (constructor SM86QMDWord32 SM86QMDWord32Value
34            byte0 byte1 byte2 byte3)))))
35
36def sm86EncodeQMDWord32 =
37  (lambda unrestricted value : (family SM86QMDWord32) .
38    (eliminate SM86QMDWord32
39      (lambda unrestricted current : (family SM86QMDWord32) . Bytes)
40      value
41      (branch SM86QMDWord32Value byte0 byte1 byte2 byte3 .
42        (bytes-cons byte0
43          (bytes-cons byte1
44            (bytes-cons byte2
45              (bytes-cons byte3 b"")))))))
46
47def sm86QMDZeroWord32 : Bytes =
48  (bytes 0 0 0 0)
49
50def sm86QMDRepeatBytes =
51  (lambda unrestricted count : Nat .
52    (lambda unrestricted payload : Bytes .
53      (nat-eliminate
54        (lambda unrestricted current : Nat . Bytes)
55        b""
56        (lambda unrestricted predecessor : Nat .
57          (lambda unrestricted induction : Bytes .
58            (bytes-append payload induction)))
59        count)))
60
61def sm86QMDZeroDwords =
62  (lambda unrestricted count : Nat .
63    (app sm86QMDRepeatBytes count sm86QMDZeroWord32))
64
65def sm86QMDProgramModeDword : Bytes =
66  (bytes 64 0 0 0)
67
68def sm86QMDReleaseDword : Bytes =
69  (bytes 0 0 0 252)
70
71def sm86QMDGridControlDword : Bytes =
72  (bytes 0 0 1 68)
73
74def sm86QMDCompletionControlDword : Bytes =
75  (bytes 0 0 0 8)
76
77def sm86EncodeQMD =
78  (lambda unrestricted config : (family SM86QMDPhysicalConfig) .
79    (eliminate SM86QMDPhysicalConfig
80      (lambda unrestricted current : (family SM86QMDPhysicalConfig) . Bytes)
81      config
82      (branch SM86QMDPhysicalConfigValue
83        prefetchBase gridX gridY gridZ sharedMemory blockX blockYZ
84        registerField constantBufferLow constantBufferHigh
85        programAddressLow programAddressHigh prefetchControl .
86        (bytes-append
87          (app sm86QMDZeroDwords (byte-to-nat (byte 4)))
88          (bytes-append
89            sm86QMDProgramModeDword
90            (bytes-append
91              sm86QMDReleaseDword
92              (bytes-append
93                (app sm86QMDZeroDwords (byte-to-nat (byte 2)))
94                (bytes-append
95                  (app sm86EncodeQMDWord32 prefetchBase)
96                  (bytes-append
97                    (app sm86QMDZeroDwords (byte-to-nat (byte 2)))
98                    (bytes-append
99                      sm86QMDGridControlDword
100                      (bytes-append
101                        (app sm86EncodeQMDWord32 gridX)
102                        (bytes-append
103                          (app sm86EncodeQMDWord32 gridY)
104                          (bytes-append
105                            (app sm86EncodeQMDWord32 gridZ)
106                            (bytes-append
107                              (app sm86QMDZeroDwords (byte-to-nat (byte 2)))
108                              (bytes-append
109                                (app sm86EncodeQMDWord32 sharedMemory)
110                                (bytes-append
111                                  (app sm86EncodeQMDWord32 blockX)
112                                  (bytes-append
113                                    (app sm86EncodeQMDWord32 blockYZ)
114                                    (bytes-append
115                                      (app sm86EncodeQMDWord32 registerField)
116                                      (bytes-append
117                                        (app sm86QMDZeroDwords
118                                          (byte-to-nat (byte 2)))
119                                        (bytes-append
120                                          sm86QMDCompletionControlDword
121                                          (bytes-append
122                                            (app sm86QMDZeroDwords
123                                              (byte-to-nat (byte 8)))
124                                            (bytes-append
125                                              (app sm86EncodeQMDWord32
126                                                constantBufferLow)
127                                              (bytes-append
128                                                (app sm86EncodeQMDWord32
129                                                  constantBufferHigh)
130                                                (bytes-append
131                                                  (app sm86QMDZeroDwords
132                                                    (byte-to-nat (byte 14)))
133                                                  (bytes-append
134                                                    (app sm86EncodeQMDWord32
135                                                      programAddressLow)
136                                                    (bytes-append
137                                                      (app sm86EncodeQMDWord32
138                                                        programAddressHigh)
139                                                      (bytes-append
140                                                        sm86QMDZeroWord32
141                                                        (bytes-append
142                                                          (app sm86EncodeQMDWord32
143                                                            prefetchControl)
144                                                          (app sm86QMDZeroDwords
145                                                            (byte-to-nat
146                                                              (byte 12)))))))))))))))))))))))))))))))