Struct Checker 

pub struct Checker<Split: SplitStrategy> {
    pub(crate) backend: AnyBackend,
    pub(crate) rules: RuleSet<Split>,
    pub(crate) modules: DashSet<Module, FxBuildHasher>,
    pub(crate) documents: DashSet<Document, FxBuildHasher>,
    pub(crate) facts: GlobalFacts,
    pub(crate) hoas: Option<HOASSymbols>,
    pub(crate) implicits: AtomicUsize,
    pub(crate) current: Vec<LeafUri>,
    pub(crate) context: Vec<ModuleUri>,
    pub(crate) __phantom: PhantomData<Split>,
}

Fields

backend: AnyBackend

rules: RuleSet<Split>

modules: DashSet<Module, FxBuildHasher>

documents: DashSet<Document, FxBuildHasher>

facts: GlobalFacts

hoas: Option<HOASSymbols>

implicits: AtomicUsize

current: Vec<LeafUri>

context: Vec<ModuleUri>

__phantom: PhantomData<Split>

Implementations

impl<Split: SplitStrategy> Checker<Split>

pub(crate) fn get_module_like(&self, uri: &ModuleUri) -> Result<ModuleLike, ()>

pub(crate) fn get_module(&self, uri: &ModuleUri) -> Result<Module, ()>

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

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

impl<Split: SplitStrategy> Checker<Split>

pub(crate) fn new_solvable(&self) -> Id

impl<Split: SplitStrategy> Checker<Split>

pub(crate) fn wrap_task<'t, R: Debug + Clone + 'static, F>( &'t self, task: CheckingTask<'t>, unknowns: Option<Solutions>, then: F, ) -> (Option<R>, Solutions, PreCheckLog)

where F: FnOnce(CheckRef<'t, '_, Split>) -> Option<R>,

pub(crate) fn wrap_none<'t, R: Debug + Clone + 'static, F>( &'t self, unknowns: Option<Solutions>, then: F, ) -> (Solutions, R)

where F: FnOnce(CheckRef<'t, '_, Split>) -> R,

impl<Split: SplitStrategy> Checker<Split>

pub fn check_assertion( &mut self, p: &LogicalParagraph, ) -> Option<Vec<CheckResult>>

pub fn check_definition(&mut self, p: &LogicalParagraph) -> Vec<CheckResult>

pub fn check_proof(&mut self, p: &LogicalParagraph) -> Option<CheckResult>

fn proof_step( &mut self, s: &ParagraphStep, context: &mut ProofCheckState<'_>, block: Option<&SymbolUri>, ) -> Option<ProofStepResult>

fn step_data_i( &self, context: &mut ProofCheckState<'_>, hoas: &HOASSymbols, var_name: Option<&DocumentElementUri>, method: Option<&Term>, justification: Option<&Term>, arguments: &[Option<(Term, SourceRange)>], yields: Option<&Term>, needs_def: bool, block: Option<&SymbolUri>, ) -> (Option<ProofStepCheckResult>, Option<Term>, Option<Term>)

fn step_data( &mut self, context: &mut ProofCheckState<'_>, var_name: Option<&DocumentElementUri>, method: Option<&Term>, justification: Option<&Term>, arguments: &[Option<(Term, SourceRange)>], yields: Option<&Term>, is_assumption: bool, block: Option<&SymbolUri>, ) -> Option<ProofStepCheckResult>

fn conclusion_step( &self, context: &mut ProofCheckState<'_>, var_name: Option<&DocumentElementUri>, method: Option<&Term>, justification: Option<&Term>, arguments: &[Option<(Term, SourceRange)>], yields: Option<&Term>, block: Option<&SymbolUri>, ) -> Option<ProofStepCheckResult>

impl<Split: SplitStrategy> Checker<Split>

pub(crate) fn bind_implicits(&self, nt: &Term) -> Option<Term>

fn collect_implicits(&self, nt: &Term) -> Option<(Vec<ComponentVar>, Term)>

impl<Split: SplitStrategy> Checker<Split>

pub(crate) fn add_fact(&mut self, s: &Symbol)

impl<Split: SplitStrategy> Checker<Split>

pub(crate) fn reset(&self)

pub fn into_cache(self) -> CheckerCache

pub fn set_cache(&mut self, cache: CheckerCache)

pub fn new(backend: AnyBackend) -> Self

pub(crate) fn set_hoas(&mut self)

pub fn hoas(&self) -> Option<&HOASSymbols>

pub fn check_document( &mut self, d: &Document, ) -> Result<(DocumentCheckResult, Vec<Module>), ModuleUri>

pub fn check_module( &mut self, m: &Module, ) -> Result<Vec<ContentCheckResult>, ModuleUri>

pub fn check_subterm_term( &mut self, term: Term, sub: Term, ) -> Option<SubtermCheckResult>

pub fn check_subterm_path( &mut self, term: Term, path: TermPath, ) -> Option<SubtermCheckResult>

pub(crate) fn check_subterm_i( &self, unks: Solutions, sub: &Term, ctx: Vec<&ComponentVar>, ) -> SubtermCheckResult

pub(crate) fn check_components( &self, tpc: &TermContainer, dfc: &TermContainer, bind: bool, ) -> Option<SymbolCheckResult>

pub(crate) fn df_only( &self, df: &Term, dfc: &TermContainer, tpc: &TermContainer, bind: bool, set_presentation: bool, ) -> SymbolCheckResult

pub(crate) fn infer_df( &self, dfc: &TermContainer, tp: &Term, tpc: &TermContainer, bind: bool, ) -> SymbolCheckResult

pub(crate) fn df_and_tp( &self, df: &Term, dfc: &TermContainer, tp: &Term, tpc: &TermContainer, bind: bool, set_df_presentation: bool, ) -> SymbolCheckResult

pub fn check_symbol(&mut self, s: &Symbol) -> Option<SymbolCheckResult>

pub fn check_variable( &mut self, s: &VariableDeclaration, ) -> Option<SymbolCheckResult>

pub(crate) fn check_type( &self, unknowns: Option<Solutions>, tm: &Term, tp: &Term, ) -> (Option<bool>, Solutions, PreCheckLog)

pub(crate) fn prove( &self, unknowns: Option<Solutions>, goal: &Term, ) -> (Option<Term>, Solutions, PreCheckLog)

pub(crate) fn check_subtype( &self, unknowns: Option<Solutions>, sub: &Term, sup: &Term, ) -> (Option<bool>, Solutions, PreCheckLog)

pub(crate) fn infer_type( &self, unknowns: Option<Solutions>, t: &Term, ) -> (Option<Term>, Solutions, PreCheckLog)

pub(crate) fn check_inhabitable( &self, unknowns: Option<Solutions>, t: &Term, ) -> (Option<bool>, Solutions, PreCheckLog)

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

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

pub(crate) fn check_morphism( &mut self, m: &Morphism, ) -> Option<Vec<CheckResult>>

pub fn add_modules(&mut self, modules: Vec<Module>) -> Result<(), ModuleUri>

Errors

pub fn set_context(&mut self, m: Vec<ModuleUri>) -> Result<(), ModuleUri>

Errors

pub(crate) fn load_context(&mut self, m: &Module)

pub(crate) fn sort(&mut self, modules: Vec<ModuleUri>) -> usize