Struct Context

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

Implementations

impl<S: Store> Context<S>

pub fn proof_stack(&self) -> &Stack

pub fn proof_heap(&self) -> &Heap

pub fn unify_stack(&self) -> &Stack

pub fn unify_heap(&self) -> &Heap

pub fn store(&self) -> &S

pub fn 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: Clone + Store> Clone for Context<S>

fn clone(&self) -> Context<S>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

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<S: Hash + Store> Hash for Context<S>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

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

fn cmp(&self, other: &Context<S>) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

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

fn eq(&self, other: &Context<S>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

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

fn partial_cmp(&self, other: &Context<S>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

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, S>( &mut self, state: &State, table: &T, is_definition: bool, stream: S, ) -> KResult

where T: Table<Var = SS::Var> + Table, 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>

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

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