Struct chalk_engine::FlounderedSubgoal
source · pub struct FlounderedSubgoal<I: Interner> {
pub floundered_literal: Literal<I>,
pub floundered_time: TimeStamp,
}Expand description
A “floundered” subgoal is one that contains unbound existential variables for which it cannot produce a value. The classic example of floundering is a negative subgoal:
not { Implemented(?T: Foo) }
The way the prolog solver works, it basically enumerates all the
ways that a given goal can be true. But we can’t use this
technique to find all the ways that ?T: Foo can be false – so
we call it floundered. In other words, we can evaluate a negative
goal, but only if we know what ?T is – we can’t use the
negative goal to help us figuring out ?T.
In addition to negative goals, we use floundering to prevent the
trait solver from trying to enumerate very large goals with tons
of answers. For example, we consider a goal like ?T: Sized to
“flounder”, since we can’t hope to enumerate all types that are
Sized. The same is true for other special traits like Clone.
Floundering can also occur indirectly. For example:
trait Foo { }
impl<T> Foo for T { }
trying to solve ?T: Foo would immediately require solving ?T: Sized, and hence would flounder.
Fields§
§floundered_literal: Literal<I>Literal that floundered.
floundered_time: TimeStampCurrent value of the strand’s clock at the time of floundering.
Trait Implementations§
source§impl<I: Clone + Interner> Clone for FlounderedSubgoal<I>
impl<I: Clone + Interner> Clone for FlounderedSubgoal<I>
source§fn clone(&self) -> FlounderedSubgoal<I>
fn clone(&self) -> FlounderedSubgoal<I>
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read moresource§impl<I: Debug + Interner> Debug for FlounderedSubgoal<I>
impl<I: Debug + Interner> Debug for FlounderedSubgoal<I>
source§impl<I: Hash + Interner> Hash for FlounderedSubgoal<I>
impl<I: Hash + Interner> Hash for FlounderedSubgoal<I>
source§impl<I: PartialEq + Interner> PartialEq for FlounderedSubgoal<I>
impl<I: PartialEq + Interner> PartialEq for FlounderedSubgoal<I>
source§fn eq(&self, other: &FlounderedSubgoal<I>) -> bool
fn eq(&self, other: &FlounderedSubgoal<I>) -> bool
self and other values to be equal, and is used
by ==.source§impl<I: Interner> TypeFoldable<I> for FlounderedSubgoal<I>
impl<I: Interner> TypeFoldable<I> for FlounderedSubgoal<I>
source§fn try_fold_with<E>(
self,
folder: &mut dyn FallibleTypeFolder<I, Error = E>,
outer_binder: DebruijnIndex,
) -> Result<Self, E>
fn try_fold_with<E>( self, folder: &mut dyn FallibleTypeFolder<I, Error = E>, outer_binder: DebruijnIndex, ) -> Result<Self, E>
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
fn fold_with( self, folder: &mut dyn TypeFolder<I, Error = Infallible>, outer_binder: DebruijnIndex, ) -> Self
try_fold_with for use with infallible
folders. Do not override this method, to ensure coherence with
try_fold_with.source§impl<I: Interner> TypeVisitable<I> for FlounderedSubgoal<I>
impl<I: Interner> TypeVisitable<I> for FlounderedSubgoal<I>
source§fn visit_with<B>(
&self,
visitor: &mut dyn TypeVisitor<I, BreakTy = B>,
outer_binder: DebruijnIndex,
) -> ControlFlow<B>
fn visit_with<B>( &self, visitor: &mut dyn TypeVisitor<I, BreakTy = B>, outer_binder: DebruijnIndex, ) -> ControlFlow<B>
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: Eq + Interner> Eq for FlounderedSubgoal<I>
impl<I: Interner> StructuralPartialEq for FlounderedSubgoal<I>
Auto Trait Implementations§
impl<I> Freeze for FlounderedSubgoal<I>
impl<I> RefUnwindSafe for FlounderedSubgoal<I>where
<I as Interner>::InternedGoal: RefUnwindSafe,
<I as Interner>::InternedProgramClauses: RefUnwindSafe,
impl<I> Send for FlounderedSubgoal<I>
impl<I> Sync for FlounderedSubgoal<I>
impl<I> Unpin for FlounderedSubgoal<I>
impl<I> UnwindSafe for FlounderedSubgoal<I>where
<I as Interner>::InternedGoal: UnwindSafe,
<I as Interner>::InternedProgramClauses: UnwindSafe,
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
§impl<T> Cast for T
impl<T> Cast for T
source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
source§default unsafe fn clone_to_uninit(&self, dst: *mut T)
default unsafe fn clone_to_uninit(&self, dst: *mut T)
clone_to_uninit)§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
key and return true if they are equal.§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
§impl<T, I> Shift<I> for Twhere
T: TypeFoldable<I>,
I: Interner,
impl<T, I> Shift<I> for Twhere
T: TypeFoldable<I>,
I: Interner,
§fn shifted_in(self, interner: I) -> T
fn shifted_in(self, interner: I) -> T
§fn shifted_in_from(self, interner: I, source_binder: DebruijnIndex) -> T
fn shifted_in_from(self, interner: I, source_binder: DebruijnIndex) -> T
outer_binder so that it is
valid at the innermost binder. See [DebruijnIndex::shifted_in_from]
for a detailed explanation.§fn shifted_out_to(
self,
interner: I,
target_binder: DebruijnIndex,
) -> Result<T, NoSolution>
fn shifted_out_to( self, interner: I, target_binder: DebruijnIndex, ) -> Result<T, NoSolution>
outer_binder. See [DebruijnIndex::shifted_out_to]
for a detailed explanation.