Struct smt2::typing::TypeChecker

pub struct TypeChecker<S: Sort> { /* fields omitted */ }

Implementations

impl<S: Sort> TypeChecker<S>

pub fn new() -> TypeChecker<S>

pub fn new_type_variable(&mut self, span: Span) -> TypeRef<S>

pub fn new_attached_type_variable(
    &mut self,
    span: Span,
    pointer: *mut Option<GroundSort<S>>
) -> TypeRef<S>

pub fn assert_equal<A: Into<TypeRef<S>>, B: Into<TypeRef<S>>>(
    &mut self,
    expected: A,
    given: B
)

Add a new constraint to the type checker.

Even of the system is not satisfiable, this function never fail. Type errors are detected with the TypeChecker::resolve method.

pub fn var(&self, index: usize) -> &TypeRef<S>

pub fn push<T: Into<TypeRef<S>>>(&mut self, ty: T)

pub fn pop(&mut self, len: usize)

pub fn enter(&mut self, span: Span)

pub fn leave(&mut self)

pub fn location(&self) -> Span

pub fn representant(&self, id: usize) -> (usize, TypeRef<S>)

pub fn redirected(&self, ty: &TypeRef<S>) -> TypeRef<S>

pub fn unify(
    &self,
    expected: TypeRef<S>,
    given: TypeRef<S>,
    root: bool,
    span: Span
) -> Result<(TypeRef<S>, Vec<Constraint<S>>), SortMissmatch<S>>

pub fn resolve(&mut self) -> Result<(), S>

Resolve all the constraints.

pub unsafe fn apply(&self) -> Result<(), S>

Apply the resolved types.