Struct CheckRef 

pub struct CheckRef<'c, 'i, Split: SplitStrategy> {
    pub(crate) top: &'c Checker<Split>,
    pub(crate) context: ContextWrap<'c, 'i>,
    pub(crate) proof_state: &'i ProverState,
    pub(crate) solutions: MutableRefList<'i, Solutions>,
    pub(crate) messages: &'i mut SmallVec<CheckLogCow<'c>, 2>,
    pub(crate) cancel: &'i CancelToken<'i, Split::CancelToken>,
    pub(crate) added: u8,
    pub(crate) traced: bool,
}

Fields

top: &'c Checker<Split>

context: ContextWrap<'c, 'i>

proof_state: &'i ProverState

solutions: MutableRefList<'i, Solutions>

messages: &'i mut SmallVec<CheckLogCow<'c>, 2>

cancel: &'i CancelToken<'i, Split::CancelToken>

added: u8

traced: bool

Implementations

impl<Split: SplitStrategy> CheckRef<'_, '_, Split>

pub(crate) fn get_declaration<T: IsDeclaration>( &self, uri: &SymbolUri, ) -> Result<SharedDeclaration<T>, ()>

Errors

pub(crate) fn get_symbol( &self, uri: &SymbolUri, ) -> Result<SharedDeclaration<Symbol>, ()>

Errors

pub(crate) fn get_symbol_type(&mut self, uri: &SymbolUri) -> Option<Term>

pub(crate) fn get_symbol_definiens(&mut self, uri: &SymbolUri) -> Option<Term>

pub fn get_variable( &self, uri: &DocumentElementUri, ) -> Result<SharedDocumentElement<VariableDeclaration>, ()>

Errors

pub(crate) fn get_var_definiens(&mut self, var: &Variable) -> Option<Term>

impl<'t, Split: SplitStrategy> CheckRef<'t, '_, Split>

pub fn check_equality(&mut self, lhs: &'t Term, rhs: &'t Term) -> Option<bool>

pub(crate) fn check_equality_i( &mut self, lhs: &'t Term, rhs: &'t Term, ) -> Option<bool>

fn congruence(&mut self, lhs: &'t Term, rhs: &'t Term) -> Option<bool>

fn congruence_i(&mut self, lhs: &'t Term, rhs: &'t Term) -> Option<bool>

fn congruence_cont(&mut self, lhs: &'t Term, rhs: &'t Term) -> Option<bool>

fn congruence_app( &mut self, lhs: &'t ApplicationTerm, rhs: &'t ApplicationTerm, ) -> Option<bool>

fn congruence_bind( &mut self, lhs: &'t BindingTerm, rhs: &'t BindingTerm, ) -> Option<bool>

impl<'t, Split: SplitStrategy> CheckRef<'t, '_, Split>

pub fn infer_type(&mut self, t: &'t Term) -> Option<Term>

pub(crate) fn infer_type_i(&mut self, t: &'t Term) -> Option<Term>

pub fn infer_var_type(&mut self, var: &'t Variable) -> Option<Term>

pub(crate) fn infer_var_type_i(&mut self, var: &Variable) -> Option<Term>

impl<Split: SplitStrategy> CheckRef<'_, '_, Split>

pub const fn rules(&self) -> &RuleSet<Split>

pub(crate) fn prepare( &self, t: Term, path: Option<&mut TermPath>, ) -> (Solutions, Term)

pub(crate) fn revert_prepare(&self, t: Term) -> Term

pub fn get_head( &self, t: &Term, ) -> Option<Either<SharedDeclaration<Symbol>, SharedDocumentElement<VariableDeclaration>>>

fn push_down_implicits(term: Term) -> Term

fn prepare_i( &mut self, t: Term, path: Option<(&mut SmallVec<u8, 16>, usize)>, ) -> Term

fn revert_i(&mut self, t: Term) -> Term

fn prepare_recurse( &mut self, term: Term, then: fn(&mut CheckRef<'_, '_, Split>, Term, Option<(&mut SmallVec<u8, 16>, usize)>) -> Term, path: Option<(&mut SmallVec<u8, 16>, usize)>, ) -> Term

fn prepare_cv( &mut self, cv: &ComponentVar, then: fn(&mut Self, Term, Option<(&mut SmallVec<u8, 16>, usize)>) -> Term, path: Option<(&mut SmallVec<u8, 16>, usize)>, ) -> ComponentVar

impl<'t, Split: SplitStrategy> CheckRef<'t, '_, Split>

pub fn prove(&mut self, goal: &'t Term) -> Option<Term>

pub(crate) fn prove_i(&mut self, goal: &'t Term) -> Option<Term>

fn backchain(&mut self, goal: &'t Term) -> Option<Term>

impl<'t, Split: SplitStrategy> CheckRef<'t, '_, Split>

pub fn simplify_full(&mut self, expand: bool, term: &'t Term) -> Option<Term>

fn simplify_full_first( &mut self, expand: bool, term: &'t Term, recursion_limit: &mut usize, total_limit: &mut usize, ) -> Option<Cow<'t, Term>>

fn simplify_full_i( &mut self, expand: bool, term: &'t Term, recursion_limit: &mut usize, total_limit: &mut usize, ) -> Option<Term>

pub fn simplify_until( &mut self, term: &'t Term, until: impl FnMut(&Self, &Term) -> bool, ) -> Option<Cow<'t, Term>>

fn simplify_until_i( &mut self, term: &'t Term, until: impl FnMut(&Self, &Term) -> bool, recursion_limit: &mut usize, total_limit: &mut usize, ) -> Option<Cow<'t, Term>>

pub(crate) fn simplify_rules<Rl: CheckerRule + ?Sized, R>( &mut self, rules: &'t [Box<Rl>], term: &'t Term, applicable: impl Fn(&Rl, &Term) -> bool, apply: impl for<'s> Fn(CheckRef<'s, '_, Split>, &Rl, &'s Term) -> Option<R> + Send + Sync, ) -> Option<R>

where R: Send + Sync + Debug + Clone + 'static,

pub(crate) fn simplify_until_two( &mut self, term1: &'t Term, term2: &'t Term, until: impl FnMut(&Self, &Term, &Term) -> bool, ) -> Option<(Cow<'t, Term>, Cow<'t, Term>)>

pub(crate) fn simplify_rules_two<Rl: CheckerRule + ?Sized + 'static, R>( &mut self, rules: &'t [Box<Rl>], term1: &'t Term, term2: &'t Term, applicable: impl Fn(&CheckRef<'_, '_, Split>, &Rl, &Term, &Term) -> bool, apply: impl for<'s> Fn(CheckRef<'s, '_, Split>, &Rl, &'s Term, &'s Term) -> Option<R> + Sync, abort: impl Fn(&Term, &Term) -> bool + Send + Sync, ) -> Either<Option<R>, (Term, Term)>

where R: Send + Sync + Debug + Clone + 'static,

fn simplify_one(&mut self, expand: bool, term: &'t Term) -> Option<Term>

fn simplify_one_i(&mut self, expand: bool, term: &'t Term) -> Option<Term>

pub(crate) fn simplify_implicit(&mut self, term: &'t Term) -> Option<Term>

fn simplify_one_default(&mut self, expand: bool, term: &'t Term) -> Option<Term>

fn arg_full( &mut self, expand: bool, arg: &'t Argument, recursion_limit: &mut usize, total_limit: &mut usize, ) -> Option<Argument>

fn bound_arg_full( &mut self, expand: bool, arg: &'t BoundArgument, recusion_limit: &mut usize, total_limit: &mut usize, ) -> Option<BoundArgument>

fn cv_full( &mut self, expand: bool, arg: &'t ComponentVar, recursion_limit: &mut usize, total_limit: &mut usize, ) -> Option<ComponentVar>

impl<Split: SplitStrategy> CheckRef<'_, '_, Split>

pub fn new_solvable(&mut self) -> Term

pub(crate) fn solve_equality( &mut self, unk: &Id, solution: &Term, ) -> Option<bool>

pub(crate) fn solve_upper_bound( &mut self, unk: &Id, bound: &Term, ) -> Option<bool>

pub(crate) fn solve_lower_bound( &mut self, unk: &Id, bound: &Term, ) -> Option<bool>

pub(crate) fn merge_solutions(&mut self, solutions: Solutions)

fn add_solvable(&mut self, name: Id)

pub fn get_solution(&self, name: &Id) -> Option<Term>

fn get_solvable<'s>(&'s self, name: &Id) -> Option<&'s Solvable>

pub(crate) fn get_solvable_type(&mut self, name: &Id) -> Term

fn solve(&mut self, name: Id, solution: Term) -> Option<()>

fn solve_type(&mut self, name: Id, tp: Term)

pub(crate) fn subst(&self, term: Term) -> Term

impl<'t, Split: SplitStrategy> CheckRef<'t, '_, Split>

pub fn check_type(&mut self, tm: &'t Term, tp: &'t Term) -> Option<bool>

pub fn check_subtype(&mut self, sub: &'t Term, sup: &'t Term) -> Option<bool>

pub fn check_inhabitable(&mut self, t: &'t Term) -> Option<bool>

pub fn check_universe(&mut self, t: &'t Term) -> Option<bool>

pub(crate) fn check_type_i( &mut self, tm: &'t Term, tp: &'t Term, ) -> Option<bool>

pub(crate) fn check_subtype_i( &mut self, sub: &'t Term, sup: &'t Term, ) -> Option<bool>

pub(crate) fn check_inhabitable_i(&mut self, tm: &'t Term) -> Option<bool>

fn check_universe_i(&mut self, tm: &'t Term) -> Option<bool>

impl<'c, 'i, Split: SplitStrategy> CheckRef<'c, 'i, Split>

pub fn extend_context<C: CowLike<'c>>(&mut self, var: C)

pub fn add_msg(&mut self, line: CheckLogCow<'c>)

pub fn comment(&mut self, msg: impl Into<Cow<'static, str>>)

pub fn counter(&mut self, msg: &'static str, num: usize)

pub fn failure(&mut self, msg: impl Into<Cow<'static, str>>)

pub(crate) fn split(&mut self) -> (&[Cow<'c, ComponentVar>], Trace<'c, '_>)

pub fn iter_context(&self) -> impl ExactSizeIterator<Item = &ComponentVar>

pub(crate) fn traced<R: Clone>( &mut self, tsk: CheckingTask<'c>, f: impl FnOnce(&mut Self) -> Option<R>, ) -> Result<R, RefCheckLog<'c>>

pub(crate) fn untraced<R: Clone>( &mut self, task: CheckingTask<'c>, f: impl FnOnce(&mut Self) -> Option<R>, ) -> Option<R>

pub(crate) fn traced_inner<R: Clone>( &mut self, task: CheckingTask<'c>, f: impl FnOnce(&mut Self) -> Option<R>, ) -> (Option<R>, RefCheckLog<'c>)

pub const fn depth(&self) -> usize

pub(crate) fn branch_traced<R: Clone>( &mut self, task: CheckingTask<'c>, f: impl FnOnce(CheckRef<'c, '_, Split>) -> Option<R>, ) -> Result<R, RefCheckLog<'c>>

pub fn scoped<'nt, R: Send + Sync + 'static>( &'nt mut self, f: impl FnOnce(&mut CheckRef<'nt, '_, Split>) -> R, ) -> R

pub(crate) fn copied(&self) -> CheckRefBranch<'c, 'i, Split>

pub(crate) fn cancellable<R: Send>( &mut self, f: impl FnOnce(&mut Self) -> R, ) -> R

pub(crate) fn wrap_check<R: Clone>( &mut self, task: CheckingTask<'c>, f: impl FnOnce(&mut Self) -> Option<R>, ) -> Option<R>

impl<Split: SplitStrategy> CheckRef<'_, '_, Split>

pub fn facts_for( &self, goal: &Term, ) -> impl Iterator<Item = (GlobalOrLocal, Vec<GoalPremise>)>

Trait Implementations

impl<Split: SplitStrategy> Drop for CheckRef<'_, '_, Split>

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.