Structural-tree frontend for dynamic processes

This file turns the structural concurrent syntax into a frontend for the dynamic Concurrent.Process core.

The present frontend keeps one important design choice from the original structural execution story: one process step corresponds to exactly one scheduled structural frontier event. The dynamic process step therefore uses a single move type Front S, but its node semantics record:

• the full controller path Control.controllers control event associated to each chosen frontier event event; and
• the current local view Current.view me control profile of that same frontier event for each party me.

So the structural tree language remains an important source language, but the dynamic process core is now the semantic center.

structure Interaction.Concurrent.Tree.State (Party : Type u) : Type (u + 1)

State Party is one structural concurrent residual state packaged together with its control tree and observation profile.

This is the exact structural data needed to view the current tree as one state of a dynamic Concurrent.Process.

• spec : Spec
• control : Control Party self.spec
• profile : Profile Party self.spec

def Interaction.Concurrent.Tree.State.currentStep {Party : Type u} [DecidableEq Party] (st : State Party) : Step Party (State Party)

currentStep st is the one-step process view of the structural residual state st.

Its move type is the current structural frontier Front st.spec. The controller-path contribution of each move is exactly Control.controllers st.control, and the local view of that move is exactly Current.view me st.control st.profile.

def Interaction.Concurrent.Tree.State.eventOfTranscript {Party : Type u} [DecidableEq Party] (st : State Party) : st.currentStep.spec.Transcript → Front st.spec

eventOfTranscript st tr forgets the trivial done tail of the process step transcript and recovers the scheduled structural frontier event.

def Interaction.Concurrent.Tree.State.transcriptOfEvent {Party : Type u} [DecidableEq Party] (st : State Party) : Front st.spec → st.currentStep.spec.Transcript

transcriptOfEvent st event re-expresses a structural frontier event as the corresponding one-step process transcript.

def Interaction.Concurrent.Tree.toProcess {Party : Type u} [DecidableEq Party] : Process Party

toProcess compiles the structural concurrent-tree frontend into the dynamic Concurrent.Process core.

Each process state is one packaged structural residual state, and each process step is the current frontier interaction produced by State.currentStep.

def Interaction.Concurrent.Tree.init {Party : Type u} {spec : Spec} (control : Control Party spec) (profile : Profile Party spec) : State Party

Package one structural residual state as the initial state of the tree frontend process.

def Interaction.Concurrent.Tree.ofLinearization {Party : Type u} [DecidableEq Party] {spec : Spec} (control : Control Party spec) (profile : Profile Party spec) : Trace spec → toProcess.Trace (init control profile)

ofLinearization control profile trace converts a structural frontier trace into the corresponding dynamic process execution trace of Tree.toProcess.