diff options
| -rw-r--r-- | src/librustc/traits/mod.rs | 12 | ||||
| -rw-r--r-- | src/librustc_traits/lowering.rs | 12 |
2 files changed, 24 insertions, 0 deletions
diff --git a/src/librustc/traits/mod.rs b/src/librustc/traits/mod.rs index dce1a89d142..8c5c36c3699 100644 --- a/src/librustc/traits/mod.rs +++ b/src/librustc/traits/mod.rs @@ -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>>>), diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs index b69d97b67e8..296ad18c480 100644 --- a/src/librustc_traits/lowering.rs +++ b/src/librustc_traits/lowering.rs @@ -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![]), } } |