Trait ContainerSort

Source

pub trait ContainerSort:
    Any
    + Send
    + Sync
    + Debug {
    type Container: ContainerValue;

    // Required methods
    fn name(&self) -> &str;
    fn is_eq_container_sort(&self) -> bool;
    fn inner_sorts(&self) -> Vec<ArcSort> ⓘ;
    fn inner_values(
        &self,
        _: &ContainerValues,
        _: Value,
    ) -> Vec<(ArcSort, Value)>;
    fn reconstruct_termdag(
        &self,
        _: &ContainerValues,
        _: Value,
        _: &mut TermDag,
        _: Vec<TermId>,
    ) -> TermId;
    fn serialized_name(
        &self,
        container_values: &ContainerValues,
        value: Value,
    ) -> String;

    // Provided methods
    fn register_primitives(&self, _eg: &mut EGraph) { ... }
    fn rebuild_container_normalizer(
        &self,
    ) -> Option<(String, PrimitiveValidator)> { ... }
    fn to_arcsort(self) -> ArcSort
       where Self: Sized { ... }
}

Expand description

A “default” implementation of Sort for types which just want to store a pure data structure in the e-graph. If you implement this trait, do not implement Sort or BaseSort. Use add_container_sort to register container sorts with the EGraph. See Sort for documentation of the methods. Do not override to_arcsort.

Required Associated Types§

Source

type Container: ContainerValue

Required Methods§

Source

fn reconstruct_termdag( &self, _: &ContainerValues, _: Value, _: &mut TermDag, _: Vec<TermId>, ) -> TermId

Source

fn serialized_name( &self, container_values: &ContainerValues, value: Value, ) -> String

Provided Methods§

Source

fn register_primitives(&self, _eg: &mut EGraph)

Source

fn rebuild_container_normalizer(&self) -> Option<(String, PrimitiveValidator)>

Optional: a container that supports proofs returns its canonical constructor head and the validator that canonicalizes its term form (e.g. set-of sorts and dedups). None (the default) means proofs are unsupported for this container. See Sort::rebuild_container_normalizer.

Source