Each effect lowers through the maintained policy owners. End supplies a
terminal acknowledgement only when no explicit Finish has already done so.
Inserted nested loops preserve the application's active loop coordinates.
349def nativeObservedLowerSteps =
350 (lambda unrestricted applicationBytes : Nat .
351 (lambda unrestricted applicationSlots : Nat .
352 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
353 (lambda unrestricted sink : (family NativePhysicalOperand) .
354 (lambda unrestricted directory : (family NativePhysicalOperand) .
355 (lambda unrestricted identity : Bytes .
356 (lambda unrestricted steps : (family NativeObservedSteps) .
357 (app
358 (eliminate
359 NativeObservedSteps
360 (lambda unrestricted current : (family NativeObservedSteps) .
361 (pi unrestricted closed : Nat . (family NativePhysicalCommands)))
362 steps
363 (branch
364 NativeObservedStepsEnd
365 .
366 (lambda unrestricted closed : Nat .
367 (aosChoose
368 (family NativePhysicalCommands)
369 closed
370 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
371 (nativeTelemetryRoutedPolicyBoundaryCommands
372 applicationBytes
373 plan
374 1
375 sink
376 directory
377 (nativeObservedCaptureSlot applicationSlots)
378 (nativeObservedPublicationSlot applicationSlots)
379 (nativeObservedWorkSlot applicationSlots)
380 identity
381 (nativeLaunchRecipeAssertEqual
382 (nativeLaunchRecipeSlotValue
383 (nativeObservedPublicationSlot applicationSlots))
384 (nativeLaunchRecipeImmediate 0)
385 (nativeTelemetryFailureIdentity
386 b"telemetry:terminal-publication-refused")
387 (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))))
388 (branch
389 NativeObservedOperation
390 operation
391 following
392 induction
393 .
394 (lambda unrestricted closed : Nat .
395 (nativeLaunchRecipeCommand operation identity (induction closed))))
396 (branch
397 NativeObservedCommand
398 command
399 following
400 induction
401 .
402 (lambda unrestricted closed : Nat .
403 (constructor
404 NativePhysicalCommands
405 NativePhysicalCommandsNext
406 command
407 (induction closed))))
408 (branch
409 NativeObservedOpenJournal
410 pathAt
411 fileSlot
412 directorySlot
413 following
414 induction
415 .
416 (lambda unrestricted closed : Nat .
417 (nativeObservedJournalCommands
418 applicationBytes
419 plan
420 pathAt
421 fileSlot
422 directorySlot
423 (nativeObservedWorkSlot applicationSlots)
424 identity
425 (induction closed))))
426 (branch
427 NativeObservedCaptureBoundary
428 tag
429 values
430 coordinate
431 following
432 induction
433 .
434 (lambda unrestricted closed : Nat .
435 (nativeTelemetryRoutedCaptureAndContinueCommands
436 applicationBytes
437 plan
438 tag
439 values
440 coordinate
441 sink
442 directory
443 (nativeObservedCaptureSlot applicationSlots)
444 (nativeObservedPublicationSlot applicationSlots)
445 (nativeObservedWorkSlot applicationSlots)
446 (nativeObservedRetrySlot applicationSlots)
447 identity
448 (induction closed))))
449 (branch
450 NativeObservedFinish
451 following
452 induction
453 .
454 (lambda unrestricted closed : Nat .
455 (nativeTelemetryRoutedPolicyBoundaryCommands
456 applicationBytes
457 plan
458 1
459 sink
460 directory
461 (nativeObservedCaptureSlot applicationSlots)
462 (nativeObservedPublicationSlot applicationSlots)
463 (nativeObservedWorkSlot applicationSlots)
464 identity
465 (nativeLaunchRecipeAssertEqual
466 (nativeLaunchRecipeSlotValue
467 (nativeObservedPublicationSlot applicationSlots))
468 (nativeLaunchRecipeImmediate 0)
469 (nativeTelemetryFailureIdentity
470 b"telemetry:terminal-publication-refused")
471 (induction 1))))))
472 0))))))))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.