Struct chalk_engine::ExClause
source · pub struct ExClause<I: Interner> {
pub subst: Substitution<I>,
pub ambiguous: bool,
pub constraints: Vec<InEnvironment<Constraint<I>>>,
pub subgoals: Vec<Literal<I>>,
pub delayed_subgoals: Vec<InEnvironment<Goal<I>>>,
pub answer_time: TimeStamp,
pub floundered_subgoals: Vec<FlounderedSubgoal<I>>,
}
Expand description
The paper describes these as A :- D | G
.
Fields§
§subst: Substitution<I>
The substitution which, applied to the goal of our table, would yield A.
ambiguous: bool
True if any subgoals were depended upon negatively and
were not fully evaluated, or if we encountered a CannotProve
goal. (In the full SLG algorithm, we would use delayed literals here,
but we don’t bother, as we don’t need that support.)
constraints: Vec<InEnvironment<Constraint<I>>>
Region constraints we have accumulated.
subgoals: Vec<Literal<I>>
Subgoals: literals that must be proven
delayed_subgoals: Vec<InEnvironment<Goal<I>>>
We assume that negative literals cannot have coinductive cycles.
answer_time: TimeStamp
Time stamp that is incremented each time we find an answer to
some subgoal. This is used to figure out whether any of the
floundered subgoals may no longer be floundered: we record the
current time when we add something to the list of floundered
subgoals, and then we can compare whether its value has
changed since then. This is not the same TimeStamp
of
Forest
’s clock.
floundered_subgoals: Vec<FlounderedSubgoal<I>>
List of subgoals that have floundered. See FlounderedSubgoal
for more information.
Trait Implementations§
source§impl<I: PartialEq + Interner> PartialEq for ExClause<I>
impl<I: PartialEq + Interner> PartialEq for ExClause<I>
source§impl<I: Interner> TypeFoldable<I> for ExClause<I>
impl<I: Interner> TypeFoldable<I> for ExClause<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 ExClause<I>
impl<I: Interner> TypeVisitable<I> for ExClause<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 ExClause<I>
impl<I: Interner> StructuralPartialEq for ExClause<I>
Auto Trait Implementations§
impl<I> Freeze for ExClause<I>where
<I as Interner>::InternedSubstitution: Freeze,
impl<I> RefUnwindSafe for ExClause<I>where
<I as Interner>::InternedSubstitution: RefUnwindSafe,
<I as Interner>::InternedGoal: RefUnwindSafe,
<I as Interner>::InternedProgramClauses: RefUnwindSafe,
<I as Interner>::InternedLifetime: RefUnwindSafe,
<I as Interner>::InternedType: RefUnwindSafe,
impl<I> Send for ExClause<I>
impl<I> Sync for ExClause<I>
impl<I> Unpin for ExClause<I>
impl<I> UnwindSafe for ExClause<I>where
<I as Interner>::InternedSubstitution: UnwindSafe,
<I as Interner>::InternedGoal: UnwindSafe,
<I as Interner>::InternedProgramClauses: UnwindSafe,
<I as Interner>::InternedLifetime: UnwindSafe,
<I as Interner>::InternedType: 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.