pub struct SessionStore { /* private fields */ }Expand description
Store of all sessions managed by the VM.
Provides type lookup/update methods that match the Lean
SessionStore.lookupType / SessionStore.updateType pattern.
Implementations§
Source§impl SessionStore
impl SessionStore
Sourcepub fn open_with_sid(
&mut self,
sid: SessionId,
roles: Vec<String>,
buffer_config: &BufferConfig,
initial_types: &BTreeMap<String, LocalTypeR>,
) -> SessionId
pub fn open_with_sid( &mut self, sid: SessionId, roles: Vec<String>, buffer_config: &BufferConfig, initial_types: &BTreeMap<String, LocalTypeR>, ) -> SessionId
Open a new session with an externally supplied session id.
Callers should source ids from SessionStore::next_session_id().
Sourcepub fn open(
&mut self,
roles: Vec<String>,
buffer_config: &BufferConfig,
initial_types: &BTreeMap<String, LocalTypeR>,
) -> SessionId
pub fn open( &mut self, roles: Vec<String>, buffer_config: &BufferConfig, initial_types: &BTreeMap<String, LocalTypeR>, ) -> SessionId
Open a new session with the given roles, buffer config, and initial local types.
Returns the session ID. Endpoints are constructed as Endpoint { sid, role }.
Sourcepub fn next_session_id(&self) -> SessionId
pub fn next_session_id(&self) -> SessionId
Next session identifier that will be allocated by open.
Sourcepub fn lookup_type(&self, ep: &Endpoint) -> Option<&LocalTypeR>
pub fn lookup_type(&self, ep: &Endpoint) -> Option<&LocalTypeR>
Lookup the current local type for an endpoint.
Matches Lean SessionStore.lookupType.
Sourcepub fn update_type(&mut self, ep: &Endpoint, new_type: LocalTypeR)
pub fn update_type(&mut self, ep: &Endpoint, new_type: LocalTypeR)
Update the local type for an endpoint (type advancement on commit).
Matches Lean SessionStore.updateType.
Sourcepub fn update_original(&mut self, ep: &Endpoint, new_original: LocalTypeR)
pub fn update_original(&mut self, ep: &Endpoint, new_original: LocalTypeR)
Update the original type (when entering a new Mu scope).
Sourcepub fn original_type(&self, ep: &Endpoint) -> Option<&LocalTypeR>
pub fn original_type(&self, ep: &Endpoint) -> Option<&LocalTypeR>
Get the original type for recursive unfolding.
Sourcepub fn remove_type(&mut self, ep: &Endpoint)
pub fn remove_type(&mut self, ep: &Endpoint)
Remove type entry (on Halt/End — session endpoint completed).
Sourcepub fn get(&self, sid: SessionId) -> Option<&SessionState>
pub fn get(&self, sid: SessionId) -> Option<&SessionState>
Get a reference to a session.
Sourcepub fn get_mut(&mut self, sid: SessionId) -> Option<&mut SessionState>
pub fn get_mut(&mut self, sid: SessionId) -> Option<&mut SessionState>
Get a mutable reference to a session.
Sourcepub fn iter(&self) -> impl Iterator<Item = &SessionState>
pub fn iter(&self) -> impl Iterator<Item = &SessionState>
Iterate over all sessions.
Sourcepub fn active_count(&self) -> usize
pub fn active_count(&self) -> usize
Number of active sessions.
Sourcepub fn session_ids(&self) -> Vec<SessionId> ⓘ
pub fn session_ids(&self) -> Vec<SessionId> ⓘ
All session IDs.
Sourcepub fn lookup_handler(&self, edge: &Edge) -> Option<&HandlerId>
pub fn lookup_handler(&self, edge: &Edge) -> Option<&HandlerId>
Lookup edge-bound handler id.
Sourcepub fn default_handler_for_session(&self, sid: SessionId) -> Option<&HandlerId>
pub fn default_handler_for_session(&self, sid: SessionId) -> Option<&HandlerId>
Lookup a default handler id for a session.
Sourcepub fn set_default_handler_for_session(
&mut self,
sid: SessionId,
handler: HandlerId,
)
pub fn set_default_handler_for_session( &mut self, sid: SessionId, handler: HandlerId, )
Set the default handler id for a session.
Sourcepub fn update_handler(&mut self, edge: &Edge, handler: HandlerId)
pub fn update_handler(&mut self, edge: &Edge, handler: HandlerId)
Update edge-bound handler id.
Sourcepub fn lookup_trace(&self, edge: &Edge) -> Option<&[ValType]>
pub fn lookup_trace(&self, edge: &Edge) -> Option<&[ValType]>
Lookup coherence trace for an edge.
Sourcepub fn update_trace(&mut self, edge: &Edge, trace: Vec<ValType>)
pub fn update_trace(&mut self, edge: &Edge, trace: Vec<ValType>)
Update coherence trace for an edge.