Setup traverses every declared frame once per occurrence, without executing
choices or repeat counts. The callback is for setup, not runtime advancement:
an unselected branch has no completed transfer to rearm. Reinitializing an
already live frame through this traversal is forbidden by the frame contract.
365def nativeProtocolFrames =
366 (lambda erased operation : Type 0 .
367 (lambda erased payload : Type 0 .
368 (lambda erased decision : Type 0 .
369 (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
370 (lambda unrestricted program : (family ParticipantProtocol operation payload decision) .
371 (eliminate
372 ParticipantProtocol
373 (lambda unrestricted current : (family ParticipantProtocol operation payload decision) .
374 (pi unrestricted tail : (family NativePhysicalCommands) .
375 (family NativePhysicalCommands)))
376 program
377 (branch
378 ParticipantProtocolEnd
379 .
380 (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
381 (branch ParticipantProtocolLocal value rest induction . induction)
382 (branch
383 ParticipantProtocolTransfer
384 direction
385 identity
386 value
387 rest
388 induction
389 .
390 (lambda unrestricted tail : (family NativePhysicalCommands) .
391 (transfer direction identity value (induction tail))))
392 (branch
393 ParticipantProtocolRepeat
394 count
395 body
396 rest
397 bodyFrames
398 restFrames
399 .
400 (lambda unrestricted tail : (family NativePhysicalCommands) .
401 (bodyFrames (restFrames tail))))
402 (branch
403 ParticipantProtocolChoice
404 role
405 identity
406 selector
407 announcements
408 zeroBody
409 oneBody
410 rest
411 zeroFrames
412 oneFrames
413 restFrames
414 .
415 (lambda unrestricted tail : (family NativePhysicalCommands) .
416 (app
417 (eliminate
418 ProtocolAnnouncements
419 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
420 (pi unrestricted tail : (family NativePhysicalCommands) .
421 (family NativePhysicalCommands)))
422 announcements
423 (branch
424 ProtocolAnnouncementsEnd
425 .
426 (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
427 (branch
428 ProtocolAnnouncementsNext
429 identity
430 value
431 rest
432 induction
433 .
434 (lambda unrestricted tail : (family NativePhysicalCommands) .
435 (transfer
436 (nat-eliminate
437 (lambda unrestricted flag : Nat . (family ProtocolDirection))
438 (constructor ProtocolDirection ProtocolReceive)
439 (lambda unrestricted prior : Nat .
440 (lambda unrestricted ignored : (family ProtocolDirection) .
441 (constructor ProtocolDirection ProtocolSend)))
442 (naturalEqual role (regionTransferSender identity)))
443 identity
444 value
445 (induction tail)))))
446 (zeroFrames (oneFrames (restFrames 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.