Offsets are accumulated from the very pieces copied into the output. No
caller has a second field-offset table. Admitted field shapes/constant
extents make formatting total for all captured machine words. References
were validated before this stage and cannot change during the drain.
113def recordPatchCommands =
114 (lambda unrestricted parts : (family TelemetryRecordParts) .
115 (lambda unrestricted source : (family NativePhysicalOperand) .
116 (lambda unrestricted identities : (family NativePhysicalOperand) .
117 (lambda unrestricted identity : Bytes .
118 (eliminate
119 TelemetryRecordParts
120 (lambda unrestricted current : (family TelemetryRecordParts) .
121 (pi unrestricted at : Nat .
122 (pi unrestricted commands : (family NativePhysicalCommands) .
123 (family NativePhysicalCommands))))
124 parts
125 (branch
126 TelemetryRecordEnd
127 .
128 (lambda unrestricted at : Nat .
129 (lambda unrestricted commands : (family NativePhysicalCommands) . commands)))
130 (branch
131 TelemetryRecordLiteral
132 bytes
133 tail
134 induction
135 .
136 (lambda unrestricted at : Nat .
137 (lambda unrestricted commands : (family NativePhysicalCommands) .
138 (induction (naturalAdd at (bytes-length bytes)) commands))))
139 (branch
140 TelemetryRecordDecimal
141 signed
142 offset
143 tail
144 induction
145 .
146 (lambda unrestricted at : Nat .
147 (lambda unrestricted commands : (family NativePhysicalCommands) .
148 (recordCellCommand
149 (nativeTelemetryDecimalWordCellRoutine signed offset)
150 source
151 at
152 captureRecordBytes
153 telemetryDecimalCellBytes
154 identity
155 (induction (naturalAdd at telemetryDecimalCellBytes) commands)))))
156 (branch
157 TelemetryRecordHex
158 sourceKind
159 offset
160 width
161 reverse
162 nonzero
163 tail
164 induction
165 .
166 (lambda unrestricted at : Nat .
167 (lambda unrestricted commands : (family NativePhysicalCommands) .
168 (recordCellCommand
169 (nativeTelemetryHexSliceCellRoutine width reverse offset)
170 (aosChoose (family NativePhysicalOperand) sourceKind identities source)
171 at
172 (aosChoose Nat sourceKind telemetryIdentitySetBytes captureRecordBytes)
173 (telemetryHexCellBytes width)
174 identity
175 (induction (naturalAdd at (telemetryHexCellBytes width)) commands))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.