1
Fork 0

Add documentation

This commit is contained in:
scalexm 2018-03-14 15:19:17 +01:00
parent 2bbd16de13
commit e8f3ed5db2
2 changed files with 24 additions and 0 deletions

View file

@ -245,6 +245,14 @@ pub type Obligations<'tcx, O> = Vec<Obligation<'tcx, O>>;
pub type PredicateObligations<'tcx> = Vec<PredicateObligation<'tcx>>;
pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
/// The following types:
/// * `WhereClauseAtom`
/// * `DomainGoal`
/// * `Goal`
/// * `Clause`
/// are used for representing the trait system in the form of
/// logic programming clauses. They are part of the interface
/// for the chalk SLG solver.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum WhereClauseAtom<'tcx> {
Implemented(ty::TraitPredicate<'tcx>),
@ -270,6 +278,7 @@ pub enum QuantifierKind {
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub enum Goal<'tcx> {
// FIXME: use interned refs instead of `Box`
Implies(Vec<Clause<'tcx>>, Box<Goal<'tcx>>),
And(Box<Goal<'tcx>>, Box<Goal<'tcx>>),
Not(Box<Goal<'tcx>>),
@ -289,8 +298,11 @@ impl<'tcx> From<DomainGoal<'tcx>> for Clause<'tcx> {
}
}
/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
/// Harrop Formulas".
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub enum Clause<'tcx> {
// FIXME: again, use interned refs instead of `Box`
Implies(Vec<Goal<'tcx>>, DomainGoal<'tcx>),
DomainGoal(DomainGoal<'tcx>),
ForAll(Box<ty::Binder<Clause<'tcx>>>),

View file

@ -17,6 +17,7 @@ use syntax::ast;
use rustc_data_structures::sync::Lrc;
trait Lower<T> {
/// Lower a rustc construction (e.g. `ty::TraitPredicate`) to a chalk-like type.
fn lower(&self) -> T;
}
@ -56,6 +57,15 @@ impl<'tcx> Lower<DomainGoal<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
}
}
/// `ty::Binder` is used for wrapping a rustc construction possibly containing generic
/// lifetimes, e.g. `for<'a> T: Fn(&'a i32)`. Instead of representing higher-ranked things
/// in that leaf-form (i.e. `Holds(Implemented(Binder<TraitPredicate>))` in the previous
/// example), we model them with quantified goals, e.g. as for the previous example:
/// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like
/// `Binder<Holds(Implemented(TraitPredicate))>`.
///
/// Also, if `self` does not contain generic lifetimes, we can safely drop the binder and we
/// can directly lower to a leaf goal instead of a quantified goal.
impl<'tcx, T> Lower<Goal<'tcx>> for ty::Binder<T>
where T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx> + Copy
{
@ -95,6 +105,8 @@ crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
let item = tcx.hir.expect_item(node_id);
match item.node {
hir::ItemImpl(..) => program_clauses_for_impl(tcx, def_id),
// FIXME: other constructions e.g. traits, associated types...
_ => Lrc::new(vec![]),
}
}