Struct EmbedderState 

pub struct EmbedderState<'a> {
    pub model_spaces: HashMap<TypeId, EmbeddingSpace<'a>>,
    pub ctxt: &'a Context,
}

An EmbedderState keeps track of the embeddings of function terms (TermModels) which come from some InterpreterState, and also the learned Elaborators for every function type.

Fields

model_spaces: HashMap<TypeId, EmbeddingSpace<'a>>

ctxt: &'a Context

Implementations

impl<'a> EmbedderState<'a>

pub fn sample(&self, rng: &mut ThreadRng) -> SampledEmbedderState<'a>

Draws a sample from the distribution over TermModels represented in this EmbedderState, yielding a SampledEmbedderState.

pub fn new( model_prior_specification: &'a dyn PriorSpecification, elaborator_prior_specification: &'a dyn PriorSpecification, ctxt: &'a Context, ) -> EmbedderState<'a>

Creates a new EmbedderState, initially populated with default embeddings for primitive terms in the passed Context.

pub fn init_embeddings_for_new_terms( &mut self, newly_evaluated_terms: &NewlyEvaluatedTerms, )

Initializes default embeddings for the passed collection of terms in a NewlyEvaluatedTerms.

pub fn bayesian_update_step( &mut self, interpreter_state: &InterpreterState<'_>, newly_evaluated_terms: &NewlyEvaluatedTerms, )

Given an InterpreterState and a collection of NewlyEvaluatedTerms, performs a bottom-up (data) update followed by a top-down (prior) update recursively on all modified terms. This method may be used to keep the TermModels in this EmbedderState up-to-date with new information.

pub fn has_embedding(&self, term_ptr: TermPointer) -> bool

Determines whether/not there is a stored TermModel for the given TermPointer.

pub fn get_embedding(&self, term_ptr: TermPointer) -> &TermModel<'_>

Given a TermPointer pointing to a TermModel tracked by this EmbedderState, yields a reference to the TermModel. Panics if there is no such entry stored.

pub fn get_mut_embedding(&mut self, term_ptr: TermPointer) -> &mut TermModel<'a>

Like EmbedderState, but yields a mutable reference to the TermModel given a TermPointer pointing to it.