Struct InterpreterAndEmbedderState 

pub struct InterpreterAndEmbedderState<'a> {
    pub interpreter_state: InterpreterState<'a>,
    pub embedder_state: EmbedderState<'a>,
    pub newly_evaluated_terms: NewlyEvaluatedTerms,
}

A more convenient, stateful wrapper around an InterpreterState and EmbedderState which automatically tracks any NewlyEvaluatedTerms originating from evaluations, and an interface which allows for using these to update the wrapped EmbedderState at a caller-chosen time.

Fields

interpreter_state: InterpreterState<'a>

embedder_state: EmbedderState<'a>

newly_evaluated_terms: NewlyEvaluatedTerms

Implementations

impl<'a> InterpreterAndEmbedderState<'a>

pub fn get_context(&self) -> &Context

Gets the Context that this InterpreterAndEmbedderState exists in.

pub fn evaluate(&mut self, term_app: &TermApplication) -> TermReference

Given a TermApplication, uses the wrapped InterpreterState to evaluate the application, returning a TermReference for the result of the evaluation. Any newly-evaluated terms which result from evaluation will be added to this InterpreterAndEmbedderState’s newly_evaluated_terms member variable.

pub fn ensure_every_type_has_a_term_on_init(&mut self)

Convenience method to force the wrapped InterpreterState to have at least one term inhabiting every type, assuming that it doesn’t really matter what these are. Calling this method will result in every newly-added term being added to the wrapped NewlyEvaluatedTerms

pub fn bayesian_update_step(&mut self)

Uses the wrapped NewlyEvaluatedTerms and InterpreterState to update the embeddings within the wrapped EmbedderState. Calling this method will not modfiy the wrapped NewlyEvaluatedTerms, in case they are still of use after an embedding update in your particular use-case.

pub fn clear_newly_received(&mut self)

Clears out the wrapped NewlyEvaluatedTerms, which typically will indicate that a new cycle of evaluations of terms against the InterpreterState is about to begin.

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

Constructs a new InterpreterAndEmbedderState with the given PriorSpecifications for crate::term_model::TermModels and crate::elaborator::Elaborators within the given Context.