[−][src]Trait chalk_solve::clauses::program_clauses::ToProgramClauses

pub trait ToProgramClauses<I: Interner> {
    fn to_program_clauses(
        &self, 
        builder: &mut ClauseBuilder<'_, I>, 
        environment: &Environment<I>
    );
}

Trait for lowering a given piece of rust-ir source (e.g., an impl or struct definition) into its associated "program clauses" -- that is, into the lowered, logical rules that it defines.

Required methods

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    environment: &Environment<I>
)

Loading content...

Implementors

impl<I: Interner> ToProgramClauses<I> for AdtDatum<I>[src]

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    _environment: &Environment<I>
)[src]

Given the following type definition: struct Foo<T: Eq> { }, generate:

-- Rule WellFormed-Type
forall<T> {
    WF(Foo<T>) :- WF(T: Eq).
}

-- Rule Implied-Bound-From-Type
forall<T> {
    FromEnv(T: Eq) :- FromEnv(Foo<T>).
}

forall<T> {
    IsFullyVisible(Foo<T>) :- IsFullyVisible(T).
}

If the type Foo is marked #[upstream], we also generate:

forall<T> { IsUpstream(Foo<T>). }

Otherwise, if the type Foo is not marked #[upstream], we generate:

forall<T> { IsLocal(Foo<T>). }

Given an #[upstream] type that is also fundamental:

#[upstream]
#[fundamental]
struct Box<T, U> {}

We generate the following clauses:

forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(T). }
forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(U). }

forall<T, U> { IsUpstream(Box<T, U>) :- IsUpstream(T), IsUpstream(U). }

// Generated for both upstream and local fundamental types
forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(T). }
forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(U). }

impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I>[src]

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    _environment: &Environment<I>
)[src]

For each associated type, we define the "projection equality" rules. There are always two; one for a successful normalization, and one for the "fallback" notion of equality.

Given: (here, 'a and T represent zero or more parameters)

trait Foo {
    type Assoc<'a, T>: Bounds where WC;
}

we generate the 'fallback' rule:

-- Rule AliasEq-Placeholder
forall<Self, 'a, T> {
    AliasEq(<Self as Foo>::Assoc<'a, T> = (Foo::Assoc<'a, T>)<Self>).
}

and

-- Rule AliasEq-Normalize
forall<Self, 'a, T, U> {
    AliasEq(<T as Foo>::Assoc<'a, T> = U) :-
        Normalize(<T as Foo>::Assoc -> U).
}

We used to generate an "elaboration" rule like this:

forall<T> {
    T: Foo :- exists<U> { AliasEq(<T as Foo>::Assoc = U) }.
}

but this caused problems with the recursive solver. In particular, whenever normalization is possible, we cannot solve that projection uniquely, since we can now elaborate AliasEq to fallback or normalize it. So instead we handle this kind of reasoning through the FromEnv predicate.

We also generate rules specific to WF requirements and implied bounds:

-- Rule WellFormed-AssocTy
forall<Self, 'a, T> {
    WellFormed((Foo::Assoc)<Self, 'a, T>) :- WellFormed(Self: Foo), WellFormed(WC).
}

-- Rule Implied-WC-From-AssocTy
forall<Self, 'a, T> {
    FromEnv(WC) :- FromEnv((Foo::Assoc)<Self, 'a, T>).
}

-- Rule Implied-Bound-From-AssocTy
forall<Self, 'a, T> {
    FromEnv(<Self as Foo>::Assoc<'a,T>: Bounds) :- FromEnv(Self: Foo), WC.
}

-- Rule Implied-Trait-From-AssocTy
forall<Self,'a, T> {
    FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>).
}

impl<I: Interner> ToProgramClauses<I> for AssociatedTyValue<I>[src]

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    _environment: &Environment<I>
)[src]

Given the following trait:

trait Iterable {
    type IntoIter<'a>: 'a;
}

Then for the following impl:

impl<T> Iterable for Vec<T> where T: Clone {
    type IntoIter<'a> = Iter<'a, T>;
}

we generate:

-- Rule Normalize-From-Impl
forall<'a, T> {
    Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :-
        Implemented(T: Clone),  // (1)
        Implemented(Iter<'a, T>: 'a).   // (2)
}

impl<I: Interner> ToProgramClauses<I> for FnDefDatum<I>[src]

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    _environment: &Environment<I>
)[src]

Given the following function definition: fn bar<T>() where T: Eq, generate:

-- Rule WellFormed-Type
forall<T> {
    WF(bar<T>) :- WF(T: Eq)
}

-- Rule Implied-Bound-From-Type
forall<T> {
    FromEnv(T: Eq) :- FromEnv(bar<T>).
}

forall<T> {
    IsFullyVisible(bar<T>) :- IsFullyVisible(T).
}

impl<I: Interner> ToProgramClauses<I> for ImplDatum<I>[src]

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    _environment: &Environment<I>
)[src]

Given impl<T: Clone> Clone for Vec<T> { ... }, generate:

-- Rule Implemented-From-Impl
forall<T> {
    Implemented(Vec<T>: Clone) :- Implemented(T: Clone).
}

For a negative impl like impl... !Clone for ..., however, we generate nothing -- this is just a way to opt out from the default auto trait impls, it doesn't have any positive effect on its own.

impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I>[src]

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    _environment: &Environment<I>
)[src]

Given opaque type T<U>: A + B = HiddenTy where U: C;, we generate:

AliasEq(T<U> = HiddenTy) :- Reveal.
AliasEq(T<U> = !T<U>).
WF(T<U>) :- WF(U: C).
Implemented(!T<U>: A).
Implemented(!T<U>: B).

where !T<..> is the placeholder for the unnormalized type T<..>.

impl<I: Interner> ToProgramClauses<I> for TraitDatum<I>[src]

fn to_program_clauses(
    &self,
    builder: &mut ClauseBuilder<'_, I>,
    environment: &Environment<I>
)[src]

Given the following trait declaration: trait Ord<T> where Self: Eq<T> { ... }, generate:

-- Rule WellFormed-TraitRef
forall<Self, T> {
   WF(Self: Ord<T>) :- Implemented(Self: Ord<T>), WF(Self: Eq<T>).
}

and the reverse rules:

-- Rule Implemented-From-Env
forall<Self, T> {
   (Self: Ord<T>) :- FromEnv(Self: Ord<T>).
}

-- Rule Implied-Bound-From-Trait
forall<Self, T> {
    FromEnv(Self: Eq<T>) :- FromEnv(Self: Ord<T>).
}

As specified in the orphan rules, if a trait is not marked #[upstream], the current crate can implement it for any type. To represent that, we generate:

// `Ord<T>` would not be `#[upstream]` when compiling `std`
forall<Self, T> { LocalImplAllowed(Self: Ord<T>). }

For traits that are #[upstream] (i.e. not in the current crate), the orphan rules dictate that impls are allowed as long as at least one type parameter is local and each type prior to that is fully visible. That means that each type prior to the first local type cannot contain any of the type parameters of the impl.

This rule is fairly complex, so we expand it and generate a program clause for each possible case. This is represented as follows:

// for `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }`
forall<Self, T, U, V> {
    LocalImplAllowed(Self: Foo<T, U, V>) :- IsLocal(Self).
}

forall<Self, T, U, V> {
    LocalImplAllowed(Self: Foo<T, U, V>) :-
        IsFullyVisible(Self),
        IsLocal(T).
}

forall<Self, T, U, V> {
    LocalImplAllowed(Self: Foo<T, U, V>) :-
        IsFullyVisible(Self),
        IsFullyVisible(T),
        IsLocal(U).
}

forall<Self, T, U, V> {
    LocalImplAllowed(Self: Foo<T, U, V>) :-
        IsFullyVisible(Self),
        IsFullyVisible(T),
        IsFullyVisible(U),
        IsLocal(V).
}

The overlap check uses compatible { ... } mode to ensure that it accounts for impls that may exist in some other compatible world. For every upstream trait, we add a rule to account for the fact that upstream crates are able to compatibly add impls of upstream traits for upstream types.

// For `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }`
forall<Self, T, U, V> {
    Implemented(Self: Foo<T, U, V>) :-
        Implemented(Self: Eq<T>), // where clauses
        Compatible,               // compatible modality
        IsUpstream(Self),
        IsUpstream(T),
        IsUpstream(U),
        IsUpstream(V),
        CannotProve.              // returns ambiguous
}

In certain situations, this is too restrictive. Consider the following code:

/* In crate std */
trait Sized { }
struct str { }

/* In crate bar (depends on std) */
trait Bar { }
impl Bar for str { }
impl<T> Bar for T where T: Sized { }

Here, because of the rules we've defined, these two impls overlap. The std crate is upstream to bar, and thus it is allowed to compatibly implement Sized for str. If str can implement Sized in a compatible future, these two impls definitely overlap since the second impl covers all types that implement Sized.

The solution we've got right now is to mark Sized as "fundamental" when it is defined. This signals to the Rust compiler that it can rely on the fact that str does not implement Sized in all contexts. A consequence of this is that we can no longer add an implementation of Sized compatibly for str. This is the trade off you make when defining a fundamental trait.

To implement fundamental traits, we simply just do not add the rule above that allows upstream types to implement upstream traits. Fundamental traits are not allowed to compatibly do that.

Loading content...