142def drainRecordCommands =
143 (lambda unrestricted applicationBytes : Nat .
144 (lambda unrestricted ordinaryCapacity : Nat .
145 (lambda unrestricted reservedCapacity : Nat .
146 (lambda unrestricted bound : Nat .
147 (lambda unrestricted scratchBytes : Nat .
148 (lambda unrestricted recipe : (family TelemetryRecordPlan) .
149 (lambda unrestricted resultSlot : Nat .
150 (lambda unrestricted identity : Bytes .
151 (lambda unrestricted tail : (family NativePhysicalCommands) .
152 (nativeTelemetryRecordCommands
153 recipe
154 (publicationStateLoad
155 applicationBytes
156 ordinaryCapacity
157 reservedCapacity
158 publicationSavedR13At)
159 (drainState
160 (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity))
161 (telemetryDrainScratchAt
162 applicationBytes
163 ordinaryCapacity
164 reservedCapacity
165 bound)
166 resultSlot
167 identity
168 (nativeLaunchRecipeCommand
169 (constructor
170 NativePhysicalOperation
171 NativePhysicalMachineRoutine
172 (drainAppendRoutine bound)
173 (constructor
174 NativePhysicalArguments
175 NativePhysicalArgumentsValue
176 (publicationStateAddress
177 applicationBytes
178 ordinaryCapacity
179 reservedCapacity
180 0)
181 (drainState
182 (telemetryDrainScratchAt
183 applicationBytes
184 ordinaryCapacity
185 reservedCapacity
186 bound))
187 (nativeLaunchRecipeImmediate (telemetryDrainRecordBytes recipe))
188 (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bound))
189 (nativeLaunchRecipeImmediate scratchBytes)
190 (nativeLaunchRecipeImmediate 0))
191 (nativeLaunchRecipeStore resultSlot))
192 identity
193 (nativeLaunchRecipeCommand
194 (constructor
195 NativePhysicalOperation
196 NativePhysicalRepeatBeginCounted
197 (nativeLaunchRecipeSlotValue resultSlot))
198 identity
199 (nativeLaunchRecipeCommand
200 (constructor
201 NativePhysicalOperation
202 NativePhysicalMachineRoutine
203 drainMemoryCopyRoutine
204 (constructor
205 NativePhysicalArguments
206 NativePhysicalArgumentsValue
207 (publicationStateLoad
208 applicationBytes
209 ordinaryCapacity
210 reservedCapacity
211 publicationSavedR12At)
212 (drainState
213 (naturalAdd
214 (telemetryDrainScratchAt
215 applicationBytes
216 ordinaryCapacity
217 reservedCapacity
218 bound)
219 telemetryRecordAt))
220 (nativeLaunchRecipeImmediate (telemetryDrainRecordBytes recipe))
221 (nativeLaunchRecipeImmediate 0)
222 (nativeLaunchRecipeImmediate 0)
223 (nativeLaunchRecipeImmediate 0))
224 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult))
225 identity
226 (nativeLaunchRecipeCommand
227 (constructor
228 NativePhysicalOperation
229 NativePhysicalAddWord64
230 (publicationStateAddress
231 applicationBytes
232 ordinaryCapacity
233 reservedCapacity
234 publicationSavedR13At)
235 (publicationStateLoad
236 applicationBytes
237 ordinaryCapacity
238 reservedCapacity
239 publicationSavedR13At)
240 (nativeLaunchRecipeImmediate captureRecordBytes))
241 identity
242 (nativeLaunchRecipeCommand
243 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
244 identity
245 tail)))))))))))))))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.