Type Alias Goal

pub type Goal = Goal<Interner>;

Aliased Type

struct Goal { /* private fields */ }

Implementations

impl<I> Goal<I>

where I: Interner,

pub fn all<II>(interner: I, iter: II) -> Goal<I>

where II: IntoIterator<Item = Goal<I>>,

Creates a single goal that only holds if a list of goals holds.

impl<I> Goal<I>

where I: Interner,

pub fn new(interner: I, interned: GoalData<I>) -> Goal<I>

Create a new goal using GoalData.

pub fn interned(&self) -> &<I as Interner>::InternedGoal

Gets the interned goal.

pub fn data(&self, interner: I) -> &GoalData<I>

Gets the interned goal data.

pub fn quantify( self, interner: I, kind: QuantifierKind, binders: VariableKinds<I>, ) -> Goal<I>

Create a goal using a forall or exists quantifier.

pub fn negate(self, interner: I) -> Goal<I>

Takes a goal G and turns it into not { G }.

pub fn compatible(self, interner: I) -> Goal<I>

Takes a goal G and turns it into compatible { G }.

pub fn implied_by(self, interner: I, predicates: ProgramClauses<I>) -> Goal<I>

Create an implication goal that holds if the predicates are true.

pub fn is_trivially_true(&self, interner: I) -> bool

True if this goal is “trivially true” – i.e., no work is required to prove it.

Trait Implementations

impl<I> CastTo<Goal<I>> for Goal<I>

where I: Interner,

fn cast_to(self, _interner: <Goal<I> as HasInterner>::Interner) -> Goal<I>

Cast a value to type T.

impl<T, I> CastTo<Goal<I>> for T

where I: Interner, T: CastTo<DomainGoal<I>>,

fn cast_to(self, interner: I) -> Goal<I>

Cast a value to type T.

impl<I> Clone for Goal<I>

where I: Clone + Interner, <I as Interner>::InternedGoal: Clone,

fn clone(&self) -> Goal<I>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<I> Debug for Goal<I>

where I: Interner,

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

Formats the value using the given formatter.

impl<I> GoalExt<I> for Goal<I>

where I: Interner,

fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>

Returns a canonical goal in which the outermost exists<> and forall<> quantifiers (as well as implications) have been “peeled” and are converted into free universal or existential variables. Assumes that this goal is a “closed goal” which does not – at present – contain any variables. Useful for REPLs and tests but not much else.

fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>

Given a goal with no free variables (a “closed” goal), creates a canonical form suitable for solving. This is a suitable choice if you don’t actually care about the values of any of the variables within; otherwise, you might want into_peeled_goal.

Panics

Will panic if this goal does in fact contain free variables.

impl<I> HasInterner for Goal<I>

where I: Interner,

type Interner = I

The interner associated with the type.

impl<I> Hash for Goal<I>

where I: Hash + Interner, <I as Interner>::InternedGoal: Hash,

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

where __H: Hasher,

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<I> IsCoinductive<I> for Goal<I>

where I: Interner,

fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool

A goal G has coinductive semantics if proving G is allowed to assume G is true (very roughly speaking). In the case of chalk-ir, this is true for goals of the form T: AutoTrait, or if it is of the form WellFormed(T: Trait) where Trait is any trait. The latter is needed for dealing with WF requirements and cyclic traits, which generates cycles in the proof tree which must not be rejected but instead must be treated as a success.

impl<I> Ord for Goal<I>

where I: Ord + Interner, <I as Interner>::InternedGoal: Ord,

fn cmp(&self, other: &Goal<I>) -> 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<I> PartialEq for Goal<I>

where I: PartialEq + Interner, <I as Interner>::InternedGoal: PartialEq,

fn eq(&self, other: &Goal<I>) -> 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<I> PartialOrd for Goal<I>

where I: PartialOrd + Interner, <I as Interner>::InternedGoal: PartialOrd,

fn partial_cmp(&self, other: &Goal<I>) -> 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<I> TypeFoldable<I> for Goal<I>

where I: Interner,

Folding a goal invokes the fold_goal callback (which will, by default, invoke super-fold).

fn try_fold_with<E>( self, folder: &mut dyn FallibleTypeFolder<I, Error = E>, outer_binder: DebruijnIndex, ) -> Result<Goal<I>, E>

Apply the given folder folder to self; binders is the number of binders that are in scope when beginning the folder. Typically binders starts as 0, but is adjusted when we encounter Binders<T> in the IR or other similar constructs.

fn fold_with( self, folder: &mut dyn TypeFolder<I, Error = Infallible>, outer_binder: DebruijnIndex, ) -> Self

A convenient alternative to try_fold_with for use with infallible folders. Do not override this method, to ensure coherence with try_fold_with.

impl<I> TypeSuperFoldable<I> for Goal<I>

where I: Interner,

Superfold folds recursively.

fn try_super_fold_with<E>( self, folder: &mut dyn FallibleTypeFolder<I, Error = E>, outer_binder: DebruijnIndex, ) -> Result<Goal<I>, E>

Recursively folds the value.

fn super_fold_with( self, folder: &mut dyn TypeFolder<I, Error = Infallible>, outer_binder: DebruijnIndex, ) -> Self

A convenient alternative to try_super_fold_with for use with infallible folders. Do not override this method, to ensure coherence with try_super_fold_with.

impl<I> TypeSuperVisitable<I> for Goal<I>

where I: Interner,

fn super_visit_with<B>( &self, visitor: &mut dyn TypeVisitor<I, BreakTy = B>, outer_binder: DebruijnIndex, ) -> ControlFlow<B>

Recursively visits the type contents.

impl<I> TypeVisitable<I> for Goal<I>

where I: Interner,

fn visit_with<B>( &self, visitor: &mut dyn TypeVisitor<I, BreakTy = B>, outer_binder: DebruijnIndex, ) -> ControlFlow<B>

Apply the given visitor visitor to self; binders is the number of binders that are in scope when beginning the visitor. Typically binders starts as 0, but is adjusted when we encounter Binders<T> in the IR or other similar constructs.

impl<I> Zip<I> for Goal<I>

where I: Interner,

fn zip_with<Z>( zipper: &mut Z, variance: Variance, a: &Goal<I>, b: &Goal<I>, ) -> Result<(), NoSolution>

where Z: Zipper<I>,

Uses the zipper to walk through two values, ensuring that they match.

impl<I> Copy for Goal<I>

where I: Copy + Interner, <I as Interner>::InternedGoal: Copy,

impl<I> Eq for Goal<I>

where I: Eq + Interner, <I as Interner>::InternedGoal: Eq,

impl<I> StructuralPartialEq for Goal<I>

where I: Interner,