Struct formality_core::binder::CoreBinder

pub struct CoreBinder<L: Language, T> { /* private fields */ }

Implementations

impl<L: Language, T: CoreFold<L>> CoreBinder<L, T>

pub fn open(&self) -> (Vec<CoreBoundVar<L>>, T)

Accesses the contents of the binder.

The variables inside will be renamed to fresh var indices that do not alias any other indices seen during this computation.

The expectation is that you will create a term and use Binder::new.

pub fn dummy(term: T) -> Self

pub fn new(variables: impl Upcast<Vec<CoreVariable<L>>>, term: T) -> Self

Given a set of variables (X, Y, Z) and a term referecing some subset of them, create a binder where exactly those variables are bound (even the ones not used).

pub fn mentioned(variables: impl Upcast<Vec<CoreVariable<L>>>, term: T) -> Self

Given a set of variables (X, Y, Z) and a term referecing some subset of them, create a binder for just those variables that are mentioned.

pub fn into<U>(self) -> CoreBinder<L, U>

where T: Into<U>,

pub fn len(&self) -> usize

Number of variables bound by this binder

pub fn is_empty(&self) -> bool

pub fn instantiate_with( &self, parameters: &[impl Upcast<CoreParameter<L>>] ) -> Fallible<T>

Instantiate the binder with the given parameters, returning an err if the parameters are the wrong number or ill-kinded.

pub fn instantiate( &self, op: impl FnMut(CoreKind<L>, VarIndex) -> CoreParameter<L> ) -> T

Instantiate the term, replacing each bound variable with op(i).

pub fn peek(&self) -> &T

Accesses the data inside the binder. Use this for simple tests that extract data that is independent of the bound variables. If that’s not the case, use open.

pub fn kinds(&self) -> &[CoreKind<L>]

Returns the kinds of each variable bound by this binder

pub fn map<U: CoreFold<L>>(&self, op: impl FnOnce(T) -> U) -> CoreBinder<L, U>

Trait Implementations

impl<L: Clone + Language, T: Clone> Clone for CoreBinder<L, T>

fn clone(&self) -> CoreBinder<L, T>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<L: Language, T: CoreFold<L>> CoreFold<L> for CoreBinder<L, T>

fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self

Replace uses of variables with values from the substitution.

fn shift_in(&self) -> Self

Produce a version of this term where any debruijn indices which appear free are incremented by one.

fn replace_free_var( &self, v: impl Upcast<CoreVariable<L>>, p: impl Upcast<CoreParameter<L>> ) -> Self

Replace all appearances of free variable v with p.

impl<L, T> CoreParse<L> for CoreBinder<L, T>

where L: Language, T: CoreTerm<L>,

Parse a binder: find the names in scope, parse the contents, and then replace names with debruijn indices.

fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>

Parse a single instance of this type, returning an error if no such instance is present.

fn parse_many<'t>( scope: &Scope<L>, text: &'t str, close_char: char ) -> ParseResult<'t, Vec<Self>>

Parse many instances of self, expecting close_char to appear after the last instance (close_char is not consumed).

fn parse_comma<'t>( scope: &Scope<L>, text: &'t str, close_char: char ) -> ParseResult<'t, Vec<Self>>

Comma separated list with optional trailing comma.

impl<L: Language, T: CoreVisit<L>> CoreVisit<L> for CoreBinder<L, T>

fn free_variables(&self) -> Vec<CoreVariable<L>>

Extract the list of free variables (for the purposes of this function, defined by Variable::is_free). The list may contain duplicates and must be in a determinstic order (though the order itself isn’t important).

fn size(&self) -> usize

Measures the overall size of the term by counting constructors etc. Used to determine overflow.

fn assert_valid(&self)

Asserts various validity constraints and panics if they are not held. These validition constraints should never fail unless there is a bug in our logic. This is to aid with fuzzing and bug detection.

fn references_only_universal_variables(&self) -> bool

True if this term references only universal variables. This means that it contains no existential variables. If this is a goal, then when we prove it true, we don’t expect any substitution. This is similar, but not identical, to the commonly used term “ground term”, which in Prolog refers to a term that contains no variables. The difference here is that the term may contain variables, but only those instantiated universally (∀).

impl<L: Language, T> Debug for CoreBinder<L, T>

where T: Debug,

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

Formats the value using the given formatter.

impl<L: Default + Language, T: Default> Default for CoreBinder<L, T>

fn default() -> CoreBinder<L, T>

Returns the “default value” for a type.

impl<L: Language, T, U> DowncastTo<CoreBinder<L, T>> for CoreBinder<L, U>

where T: DowncastFrom<U>,

fn downcast_to(&self) -> Option<CoreBinder<L, T>>

impl<L: Hash + Language, T: Hash> Hash for CoreBinder<L, T>

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<L: Ord + Language, T: Ord> Ord for CoreBinder<L, T>

fn cmp(&self, other: &CoreBinder<L, T>) -> 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 + PartialOrd,

Restrict a value to a certain interval.

impl<L: PartialEq + Language, T: PartialEq> PartialEq for CoreBinder<L, T>

fn eq(&self, other: &CoreBinder<L, T>) -> bool

This method tests for self and other values to be equal, and is used by ==.

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

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

impl<L: PartialOrd + Language, T: PartialOrd> PartialOrd for CoreBinder<L, T>

fn partial_cmp(&self, other: &CoreBinder<L, T>) -> Option<Ordering>

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

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

This method tests less than (for self and other) and is used by the < operator.

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

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

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

This method tests greater than (for self and other) and is used by the > operator.

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

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

impl<L: Language, T, U> UpcastFrom<CoreBinder<L, T>> for CoreBinder<L, U>

where T: Clone + Upcast<U>, U: Clone,

fn upcast_from(term: CoreBinder<L, T>) -> Self

impl<L: Language, T: CoreTerm<L>> CoreTerm<L> for CoreBinder<L, T>

impl<L: Eq + Language, T: Eq> Eq for CoreBinder<L, T>

impl<L: Language, T> StructuralEq for CoreBinder<L, T>

impl<L: Language, T> StructuralPartialEq for CoreBinder<L, T>