Struct FormulaRef

pub struct FormulaRef<'a> { /* private fields */ }

A Formula reference in the context of a Database. This allows the values in the Formula to be resolved,

Implementations

impl<'a> FormulaRef<'a>

pub fn as_sexpr(&self) -> String

Convert this formula into an s-expression string.

pub fn write_sexpr(&self, w: &mut impl Write) -> Result

Write this formula as an s-expression to the given writer.

pub fn complete_substitutions<E>( &self, substitutions: &mut Substitutions, wvp: &mut impl WorkVariableProvider<E>, ) -> Result<(), E>

Handles the variables present in the formula but not in the substitution list The function f provided can modify on the fly the substitution list, adding any missing one.

pub fn append_to_stack_buffer(self, stack_buffer: &mut Vec<u8>) -> Range<usize>

Appends this formula to the provided stack buffer.

The ProofBuilder structure uses a dense representation of formulas as byte strings, using the high bit to mark the end of each token. This function creates such a byte string, stores it in the provided buffer, and returns the range the newly added string occupies on the buffer.

See crate::verify for more about this format.

pub fn build_syntax_proof<I: Copy, A: Default + FromIterator<I>>( self, stack_buffer: &mut Vec<u8>, arr: &mut dyn ProofBuilder<Item = I, Accum = A>, ) -> I

Builds the syntax proof for this formula.

In Metamath, it is possible to write proofs that a given formula is a well-formed formula. This method builds such a syntax proof for the formula into a crate::proof::ProofTree, stores that proof tree in the provided ProofBuilder arr, and returns the index of that ProofTree within arr.

Methods from Deref<Target = Formula>

pub fn labels_iter(&self) -> LabelIter<'_>

Iterates through the labels of a formula, depth-first, pre-order. Items are the label, and a boolean indicating whether the current label is a variable or not.

pub fn as_ref<'a>(&'a self, db: &'a Database) -> FormulaRef<'a>

Augment a formula with a database reference, to produce a FormulaRef. The resulting object implements Display, Debug, and IntoIterator.

pub fn dump(&self, nset: &Nameset)

Debug only, dumps the internal structure of the formula.

pub fn get_typecode(&self) -> TypeCode

Returns the typecode of this formula

pub fn is_singleton(&self) -> bool

Returns whether this formula consists in a single token.

pub fn get_by_path(&self, path: &[usize]) -> Option<Label>

Returns the label obtained when following the given path. Each element of the path gives the index of the child to retrieve. For example, the empty

pub fn unify( &self, other: &Formula, substitutions: &mut Substitutions, ) -> Result<(), UnificationError>

Unify this formula with the given formula model If successful, the provided substitutions are completed with the substitutions which needs to be made in other in order to match this formula.

pub fn substitute(&self, substitutions: &Substitutions) -> Formula

Perform substitutions This returns a new Formula object, built from this formula, where all instances of the variables specified in the substitutions are replaced by the corresponding formulas.

pub fn replace(&self, old_sub_fmla: &Formula, new_sub_fmla: &Formula) -> Formula

Replace all instances of old_sub_fmla in this formula by new_sub_fmla. Where substitute works on variables only, this

Trait Implementations

impl<'a> Clone for FormulaRef<'a>

fn clone(&self) -> FormulaRef<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for FormulaRef<'a>

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

Formats the value using the given formatter.

impl<'a> Deref for FormulaRef<'a>

type Target = Formula

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

impl<'a> Display for FormulaRef<'a>

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

Formats the value using the given formatter.

impl<'a> IntoIterator for FormulaRef<'a>

type Item = Atom

The type of the elements being iterated over.

type IntoIter = Flatten<'a>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Flatten<'a>

Creates an iterator from a value.

impl<'a> Copy for FormulaRef<'a>