Struct trivial_kernel::context::Context

pub struct Context<S: Store> { /* fields omitted */ }

Implementations

impl<S: Store> Context<S>

pub fn get_proof_stack(&self) -> &Stack

pub fn get_proof_heap(&self) -> &Heap

pub fn get_unify_stack(&self) -> &Stack

pub fn get_unify_heap(&self) -> &Heap

pub fn get_store(&self) -> &S

pub fn get_hyp_stack(&self) -> &Stack

pub fn clear_except_store(&mut self)

pub fn binder_check<T: Table>(
    table: &T,
    ty: &T::Var,
    current_sort: u8,
    bv: &mut u64
) -> KResult

pub fn allocate_binders<T: Table<Var = S::Var>>(
    &mut self,
    table: &T,
    current_sort: u8,
    binders: &[T::Var]
) -> KResult

Trait Implementations

impl<S: Debug + Store> Debug for Context<S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<S: Default + Store> Default for Context<S>

fn default() -> Context<S>

Returns the “default value” for a type.

impl<S: Store> Display for Context<S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T, S: Store> Proof<T> for Context<S> where
    T: Table<Var = S::Var>, 

fn end(&mut self) -> KResult

fn reference(&mut self, idx: u32) -> KResult

fn dummy(&mut self, table: &T, sort: u32, current_sort: u32) -> KResult

fn term(
    &mut self,
    table: &T,
    idx: u32,
    current_term: u32,
    save: bool,
    def: bool
) -> KResult

fn theorem(&mut self, table: &T, idx: u32, save: bool) -> KResult

fn theorem_start(
    &mut self,
    table: &T,
    idx: u32,
    current_theorem: u32,
    save: bool
) -> KResult<(Stepper, Ptr, bool)>

fn theorem_end(&mut self, target: Ptr, save: bool) -> KResult

fn hyp(&mut self, table: &T) -> KResult

fn conv(&mut self) -> KResult

fn refl(&mut self) -> KResult

fn symm(&mut self) -> KResult

fn cong(&mut self) -> KResult

fn unfold_start(&mut self, table: &T) -> KResult<(Stepper, Ptr, Ptr)>

fn unfold_end(&mut self, t_ptr: Ptr, e: Ptr) -> KResult

fn unfold(&mut self, table: &T) -> KResult

fn conv_cut(&mut self) -> KResult

fn conv_ref(&mut self, idx: u32) -> KResult

fn conv_save(&mut self) -> KResult

fn save(&mut self) -> KResult

fn execute(
    &mut self,
    table: &T,
    state: &State,
    command: Command<Proof>,
    is_definition: bool
) -> KResult<bool>

fn step(
    &mut self,
    table: &T,
    state: &State,
    command: Command<Proof>,
    is_definition: bool
) -> KResult<Option<FinalizeState>>

impl<S: Store> Run<S> for Context<S>

fn run<T>(
    &mut self,
    stream: Range<usize>,
    table: &T,
    mode: Mode,
    target: Ptr
) -> KResult where
    T: Table<Var = S::Var>, 

impl<SS: Store> Run<SS> for Context<SS>

fn run<T: Table, S>(
    &mut self,
    state: &State,
    table: &T,
    is_definition: bool,
    stream: S
) -> KResult where
    T: Table<Var = SS::Var>,
    S: IntoIterator,
    S::Item: TryInto<Command<Proof>>, 

impl<S: Store> Unify for Context<S>

fn end(&mut self, mode: Mode) -> KResult

fn term(&mut self, idx: u32, save: bool) -> KResult

fn reference(&mut self, idx: u32) -> KResult

fn dummy(&mut self, sort: u32) -> KResult

fn hyp_thm(&mut self) -> KResult

fn hyp_thm_end(&mut self) -> KResult

fn execute(&mut self, command: Command<Unify>, mode: Mode) -> KResult<bool>