Struct TypeInfo

pub struct TypeInfo { /* private fields */ }

Stores resolved typechecking information.

Implementations

impl TypeInfo

pub fn add_presort<S: Presort>(&mut self, span: Span) -> Result<(), TypeError>

Adds a sort constructor to the typechecker’s known set of types.

pub fn get_sorts_by<S: Sort>( &self, pred: impl Fn(&Arc<S>) -> bool, ) -> Vec<Arc<S>>

Returns all sorts that satisfy the type and predicate.

pub fn get_sorts<S: Sort>(&self) -> Vec<Arc<S>>

Returns all sorts based on the type.

pub fn get_sort_by<S: Sort>(&self, pred: impl Fn(&Arc<S>) -> bool) -> Arc<S>

Returns a sort that satisfies the type and predicate.

pub fn get_sort<S: Sort>(&self) -> Arc<S>

Returns a sort based on the type.

pub fn get_arcsorts_by(&self, f: impl Fn(&ArcSort) -> bool) -> Vec<ArcSort>

Returns all sorts that satisfy the predicate.

pub fn get_arcsort_by(&self, f: impl Fn(&ArcSort) -> bool) -> ArcSort

Returns a sort based on the predicate.

pub fn typecheck_facts( &self, symbol_gen: &mut SymbolGen, facts: &[Fact], ) -> Result<Vec<ResolvedFact>, TypeError>

pub fn get_sort_by_name(&self, sym: &str) -> Option<&ArcSort>

pub fn get_prims(&self, sym: &str) -> Option<&[PrimitiveWithId]>

pub fn is_primitive(&self, sym: &str) -> bool

pub fn get_func_type(&self, sym: &str) -> Option<&FuncType>

pub fn is_constructor(&self, sym: &str) -> bool

pub fn get_global_sort(&self, sym: &str) -> Option<&ArcSort>

pub fn is_global(&self, sym: &str) -> bool

Trait Implementations

impl Clone for TypeInfo

fn clone(&self) -> TypeInfo

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Default for TypeInfo

fn default() -> TypeInfo

Returns the “default value” for a type.